Local induction and provably total computable functions

DOI10.1016/J.APAL.2014.04.012MaRDI QIDQ2453069zbMATH OpenOpenAlexFDO

Authors F. Félix Lara Martin, Andrés Cordón-Franco

Publication date 6 June 2014

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2014.04.012

zbMATH Keywords

conservation resultsfirst-order arithmeticparameter-free inductionprimitive recursive functions

Mathematics Subject Classification ID

Models of arithmetic and set theory (03C62) Recursive functions and relations, subrecursive hierarchies (03D20) First-order arithmetic and fragments (03F30)

Review text

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.

Recommendations

• Local induction and provably total computable functions: a case study
• Parameter free induction and provably total computable functions
• Induction rules, reflection principles, and provably recursive functions
• Computer Science Logic
• Functions provably total in $I^{-}Σ_{n}$

Cites work

• A proof-theoretic analysis of collection
• Conservation results for parameter-free _n-induction
• Functions provably total in $I^{-}Σ_{n}$
• Herbrand analyses
• scientific article; zbMATH DE number 3857078 (Why is no real title available?)
• scientific article; zbMATH DE number 733384 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• Induction rules, reflection principles, and provably recursive functions
• Induction, minimization and collection for \(\Delta_{n+1}(T)\)-formulas
• Notes on polynomially bounded arithmetic
• On parameter free induction schemas
• Parameter free induction and provably total computable functions
• Saturated models of universal theories

Cited in

(14)

• Parameter free induction and provably total computable functions
• Induction rules in bounded arithmetic
• On axiom schemes for \(T\)-provably \(\Delta_1\) formulas
• Local induction and provably total computable functions: a case study
• ON THE LOCAL-INDICABILITY COHEN–LYNDON THEOREM
• On Σ₁‐definable Functions Provably Total in I ∏
• On the induction schema for decidable predicates
• Provably total functions of Basic Arithmetic
• Computer Science Logic
• On the optimality of conservation results for local reflection in arithmetic
• A simple proof of Parsons' theorem
• Functions provably total in $I^{-}Σ_{n}$
• MODEL THEORY AND PROOF THEORY OF THE GLOBAL REFLECTION PRINCIPLE
• An interpretation of Shenoy and Shafer's axioms for local computation

This page was built for publication: Local induction and provably total computable functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2453069)