\documentclass[12pt]{article}
\usepackage{amsmath,amssymb,amsfonts}
\begin{document}
In the first section of this paper we show that $i\Pi_1\equiv W\neg\neg l\Pi_1$ and that a Kripke model which decides bounded formulas forces $i\Pi_1$ if and only if the union of the worlds in any path in it satisfies $I\Pi_1$. In particular, the union of the worlds in any path of a Kripke model
of $HA$ models $I\Pi_1$. In the second section of the paper, we show that for equivalence of forcing and satisfaction of
$\Pi_m$-formulas in a linear Kripke model deciding ${\Delta_0}$-formulas, it is necessary and sufficient that the model be $\Sigma_m$-elementary. This implies that if a linear Kripke model forces $PEM_{\mbox{prenex}}$, then it forces $PEM$. We also show that, for each $n\geqslant 1$, $i\Phi_{n}$ does not prove ${\cal H}(I\Pi_n)$. Here, $\Phi_n$'s are Burr's fragments
of $HA$.
\end{document}