__Research article:__

** Samuel R. Buss.
"On model theory for intuitionstic bounded arithmetic with
applications to independence."
In **

**Download article: postscript or PDF.
**

**Abstract: **$\IPVplus$ is IPV (which is essentially
$IS^1_2$) with polynomial-induction on $\Sigma^{b+}_1$-formulas disjoined with arbitrary
formulas in which the induction variable does not occur. This paper proves that $\IPVplus$
is sound and complete with respect to Kripke structures in which every world is a model of
CPV (essentially $S^1_2$). Thus IPV is sound with respect to such structures. In this
setting, this is a strengthening of the usual completeness and soundness theorems for
first-order intuitionistic theories. Using Kripke structures a conservation result is
proved for $\PV_1$ over IPV.

Cook-Urquhart and Krajicek-Pudlak have proved independence results
stating that it is consistent with IPV and PV that extended Frege systems are super. As an
application of Kripke models for IPV, we give a proof of a strengthening of Cook and
Urquhart's theorem using the model-theoretic construction of Krajicek and Pudlak.