A Uniform Characterization of $\Sigma_1$-Reflection over the Fragments of Peano Arithmetic

TL;DR

This paper provides a detailed proof-theoretic analysis showing that the uniform $ ext{Sigma}_1$-reflection over fragments of Peano Arithmetic is equivalent to the totality of certain fast-growing functions, all within a low-level theory.

Contribution

It offers an explicit internal proof of the equivalence between reflection principles and fast-growing functions in a weak base theory, filling a gap in the literature.

Findings

Uniform $ ext{Sigma}_1$-reflection over $I ext{Sigma}_n$ corresponds to the totality of $F_{ ext{omega}_n}$.

The proof formalizes the connection within $I ext{Sigma}_1$, avoiding stronger meta-theoretic assumptions.

Provides a detailed exposition of an important result in proof theory.

Abstract

We show that the theory $I\Sigma_1$ of $\Sigma_1$-induction proves the following statement: For all $n\geq 2$, the uniform $\Sigma_1$-reflection principle over the theory $I\Sigma_n$ is equivalent to the totality of the function $F_{\omega_n}$ at stage $\omega_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 $I\Sigma_1$. It is well possible that this has been considered before. Our aim is merely to provide a detailed exposition of this important result.