Research article:
Samuel R. Buss.
"On model theory for intuitionstic bounded arithmetic with
applications to independence."
In Feasible Mathematics: A Mathematical Sciences Institute Workshop
held in Ithaca, New York, June 1989. S. Buss and P. Scott (eds).
Birkhauser, 1990, pp. 27-47.
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.