Induction rules, reflection principles, and provably recursive functions Original Research Article

A well-known result (Leivant, 1983) states that, over basic Kalmar elementary arithmetic EA, the induction schema for ∑n formulas is equivalent to the uniform reflection principle for ∑n + 1 formulas (n ⩾ 1). We show that fragments of arithmetic axiomatized by various forms of induction rules admit a precise axiomatization in terms of reflection principles as well. Thus, the closure of EA under the induction rule for ∑n (or Πn + 1) formulas is equivalent to ω times iterated ∑n reflection principle. Moreover, for k < ω, k times iterated ∑n reflection principle over EA precisely corresponds to the extension of EA by ⩽k nested applications of ∑n induction rule. The above relationship holds in greater generality than just stated. In fact, we give general formulas characterizing in terms of iterated reflection principles the extension of any given theory (containing EA) by ⩽k nested applications of ∑n or Πn induction rules. In particular, the closure of a theory T under just one application of ∑1 induction rule is equivalent to T together with ∑1 reflection principle for each finite Π2 axiomatized subtheory of T. These results have closely parallel ones in the theory of subrecursive function classes. The rules under study correspond, in a canonical way, to natural closure operators on the classes of provably recursive functions. Thus, ∑1 induction rule precisely corresponds to the primitive recursive closure operator, and ∑1 collection rule, introduced below, corresponds to the elementary closure operator.