Consistency statements and iterations of computable functions in I₁ and PRA

DOI10.1007/S00153-010-0199-2MaRDI QIDQ711565zbMATH OpenOpenAlexWikidataFDO

Authors Joost J. Joosten

Publication date 27 October 2010

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-010-0199-2

zbMATH Keywords

arithmetical theoriescomputable functionsconservativityconsistency statementsdefinable cuts

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 is devoted to the interrelations between two weak systems of arithmetic: PRA (= primitive recursive arithmetic) and I\(\Sigma_{1}\) (= Robinson's arithmetic Q plus the \(\Sigma_{1}\)-induction rule). A characterization of I\(\Sigma_{1}\) in terms of PRA and iterations of a class of functions is given. In particular, it is shown that PRA is closed under iterations of these functions whereas I\(\Sigma_{1}\) is provably closed under iteration. A sufficient condition for a model of PRA to be a model of I\(\Sigma_{1}\) is given. This enables the author to give a model-theoretic proof of Parson's theorem stating that I\(\Sigma_{1}\) is \(\Pi_{2}\) conservative over PRA. A purely syntactical proof of Parson's theorem is also given. It is also shown that I\(\Sigma_{1}\) proves the consistency of PRA on a definable I\(\Sigma_{1}\)-cut. A consequence of this is the fact that proofs in I\(\Sigma_{1}\) can have non-elementary speed up over proofs in PRA.

Recommendations

• A simple proof of Parsons' theorem
• Fragments of HA based on \(\Sigma_ 1\)-induction
• Fragments of arithmetic
• On some generalizations of the primitive recursive arithmetic
• Things that can and things that cannot be done in PRA

Cites work

• Existence and feasibility in arithmetic
• Grundlagen der Mathematik I
• Herbrand analyses
• scientific article; zbMATH DE number 4004177 (Why is no real title available?)
• scientific article; zbMATH DE number 51556 (Why is no real title available?)
• scientific article; zbMATH DE number 1215494 (Why is no real title available?)
• scientific article; zbMATH DE number 1226875 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• scientific article; zbMATH DE number 3320380 (Why is no real title available?)
• Induction rules, reflection principles, and provably recursive functions
• Notes on polynomially bounded arithmetic
• On n-quantifier induction
• On the scheme of induction for bounded arithmetic formulas
• Proof theory
• Proof-theoretic analysis by iterated reflection
• Quantifier-free and one-quantifier systems
• Saturated models of universal theories
• The closed fragment of the interpretability logic of PRA with a constant for I\(\Sigma^1\)

Cited in

(3)

• Things that can and things that cannot be done in PRA
• A simple proof of Parsons' theorem
• An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics

This page was built for publication: Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA

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