A note on bootstrapping intuitionistic bounded arithmetic
Samuel R. Buss · Cambridge University Press eBooks · 1993
This paper, firstly, discusses the relationship between Buss’s definition and Cook and Urquhart’s definition of BASIC axioms and of IS1 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 IS1 2 are equivalent which is not based on realizability or functional interpretations. Secondly, it is shown that any negated positive consequence of S1 2 is also a theorem of IS1 2. Some possible additional axioms for IS1 2 are investigated.