A uniform characterization of _1-reflection over the fragments of Peano arithmetic

DOI10.1142/9789811236488_0005MaRDI QIDQ5081870zbMATH OpenOpenAlexFDO

Authors Anton Freund

Publication date 17 June 2022

Published in Proof and Computation II (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1512.05122

zbMATH Keywords

fragments of Peano arithmeticreflection principle

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30)

Abstract: We show that the theory $ISigm{a}_1$ of $Sigm{a}_1$-induction proves the following statement: For all $ngeq2$, the uniform $Sigm{a}_1$-reflection principle over the theory $ISigm{a}_n$ is equivalent to the totality of the function $F_{omeg{a}_n}$ at stage $omeg{a}_n$ of the fast-growing hierarchy. The method applied is a formalization of infinite proof theory. The literature contains several proofs which place the quantification over $n$ in the meta-theory (and also prove the separate cases $n=0,1$). In contrast, the author knows of no explicit argument that would allow us to internalize the quantification while keeping the meta-theory as low as $ISigm{a}_1$. It is well possible that this has been considered before. Our aim is merely to provide a detailed exposition of this important result.

Recommendations

• Reflection Principles in Fragments of Peano Arithmetic
• Slow reflection
• A note on fragments of uniform reflection in second order arithmetic
• Majorizing provably recursive functions in fragments of PA
• Reflection principles and provability algebras in formal arithmetic

Cited in

(7)

• Short proofs for slow consistency
• Slow reflection
• Strict \({\varPi^1_1}\)-reflection in bounded arithmetic
• Arithmetical reflection and the provability of soundness
• Reflection principles and provability algebras in formal arithmetic
• Reflection Principles in Fragments of Peano Arithmetic
• A note on fragments of uniform reflection in second order arithmetic

This page was built for publication: A uniform characterization of \(\Sigma_1\)-reflection over the fragments of Peano arithmetic

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