Induction rules, reflection principles, and provably recursive functions (Q1361250)

The author characterizes \(\Pi_n\)- and \(\Sigma_n\)-induction rules, \(\Pi_n\)-IR and \(\Sigma_n\)-IR, respectively. With a rule, in contrast to an axiom, one can take into account how many times it is applied nestedly. Thus, for instance, \([T,\Sigma_n\text{-IR}]_k\) is the theory obtained from the given \(T\) by using \(\Sigma_n\)-IR at most \(k\) times. \(\Pi\)- and \(\Sigma\)-IR are related. He shows, for example, that \([T,\Pi_{n+2}\text{-IR}]_k\) is included in \([T,\Sigma_{n+1}\text{-IR}]_{k+1}\), where \(T\) is any \(\Pi_{n+2}\)-theory extending Kalmar elementary arithmetic, EA. The main result is the relation with the reflection principle, \(\text{RFN}_\Gamma(T)\), for formulas in \(\Gamma\). For \(T\) extending EA, \([T,\Sigma_{n+1}\text{-IR}]_1\) is equivalent to \(T+\{\text{RFN}_{\Sigma_{n+1}}(T_0)/T_0\) is finite \(\Pi_{n+2}\)-axiomatized subtheory of \(T\}\). Similar characterization of \(\Pi_n\)-IR is given with respect to \(\Pi_n\)-RFN. Results of different nature pertain to characterizations of various classes of functions. For example, for a theory \(T\) axiomatized by one \(\Pi_2\) sentence, a function is shown to be total in \([T,\Sigma_1\text{-IR}]_1\) exactly when it is obtained from the standard witness function of \(T\) by composition and one application of primitive recursion. Since the results are of a positive nature, namely a formula proved in a theory is also obtained in another way, etc., what the author does is a careful analysis of the situation at hand, using familiar tools like Herbrand theorem. This paper is self-contained, as the author provides abundant information and explanations. Indeed, he ``did not try to be overly laconic''.