The optimality of induction as an axiomatization of arithmetic
Daniel M. Leivant · Journal of Symbolic Logic · 1983
By induction for a formula φ we mean the schema (where the terms in brackets are implicitly substituted for some fixed variable, with the usual restrictions). Let be the schema IAφ for φ in Πn (i.e. ); similarly for . Each instance of is Δn+2, and each instance of is Σn+1 Thus the universal closure of an instance α is Πn+2 in either case. Charles Parsons [72] proved that and are equivalent over Z0, where Z0 is essentially Primitive Recursive Arithmetic augmented by classical First Order Logic [Parsons 70]. Theorem. For each n > 0 there is a Πn formula π for which is not derivable in Z0from (i) true Πn+1sentences; nor even (ii) Πn+1sentences consistent withZ0.