Local induction and provably total computable functions (Q2453069)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 6301454
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Local induction and provably total computable functions |
scientific article; zbMATH DE number 6301454 |
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
0.9385699033737184
0 references
0.8865372538566589
0 references
0.8865372538566589
0 references
0.8274780511856079
0 references
0.7906363606452942
0 references