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

    Identifiers