Local induction and provably total computable functions (Q2453069)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Local induction and provably total computable functions |
scientific article |
Statements
Local induction and provably total computable functions (English)
0 references
6 June 2014
0 references
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.
0 references
first-order arithmetic
0 references
conservation results
0 references
parameter-free induction
0 references
primitive recursive functions
0 references