Local induction and provably total computable functions (Q2453069): Difference between revisions

The paper gives an answer to Kaye's question about the class of provably total computable functions of \(I \Pi ^{-}_{2}\) (i.e., the fragment of Peano arithmetic obtained by restricting the induction scheme to parameter free \(\Pi _{2}\) formulas). This has been answered already by \textit{L. D. Beklemishev} [Theor. Comput. Sci. 224, No. 1--2, 13--33 (1999; Zbl 0930.03082)] who showed that this is precisely the class of primitive recursive functions. His proof needed the metamathematical machinery (reflection principle, provability logic etc.). The proof given in the paper under review is more direct -- an analysis of certain local variants of induction principle closely related to \(I \Pi ^{-}_{2}\) is used. The methods are in fact model-theoretic and allow for a general study of \(I \Pi ^{-}_{n+1}\) for all \(n \geq 0\). In particular, a new conservation result for these theories, namely that \(I \Pi ^{-}_{n+1}\) is \(\Pi_{n+2}\)-conservative over \(I \Sigma_{n}\) for each \(n \geq 1\) is derived.