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.