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.

Back to Sam Buss's publications page.