Research article:

    Samuel R. Buss.
    "A note on bootstrapping intuitionistic bounded arithmetic."
    In Proof Theory: a selection of papers from the Leeds Theory Programme 1990.
    P. Aczel, H. Simmons, S. Wainer (eds).
    Cambridge University Press, 1992, pp. 142-169.

Download article: postscript or PDF

    Abstract: This paper, firstly, discusses the relationship between Buss's definition and Cook and Urquhart's definition of BASIC axioms and of~$IS^1_2$. The two definitions of BASIC axioms are not equivalent; however, each intuitionistically implies the law of the excluded middle for quantifier-free formulas. There is an elementary proof that the definitions of~$IS^1_2$ are equivalent which is not based on realizability or functional interpretations.
    Secondly, it is shown that any negated positive consequence of $S^1_2$ is also a theorem of~$IS^1_2$. Some possible additional axioms for~$IS^1_2$ are investigated.

Back to Sam Buss's publications page.