\documentclass[12pt]{article}
\usepackage{amsmath,amssymb,amsfonts}
\begin{document}
In this paper we apply some new and some old methods in order to
construct classical and intuitionistic models for theories of
bounded arithmetic. We use these models to obtain proof theoretic
consequences. In particular, we construct an $\omega$-chain of
models of $\rm BASIC$ such that the union of its worlds satisfies
$\rm S_2^1$ but none of its worlds satisfies the sentence $\forall
x\exists y (x=0\vee
x=y+1)$. Interpreting this chain as a Kripke model shows
that double negation of the above mentioned sentence is not provable
in the intuitionistic theory of $\rm BASIC$ plus polynomial
induction on $\rm coNP$ formulas.
\end{document}