The behavior of higher proof theory I: Case $Σ^1_2$

TL;DR

This work extends Walsh's $\,\Pi^1_1$-proof-theoretic framework to the $\Sigma^1_2$ level by introducing and analyzing predilators, dilators, and the novel notion of pseudodilators. It defines the $\ ext{$\Sigma^1_2$-proof-theoretic ordinal}$ $s^1_2(T)$ via climaxes of recursive predilators, and proves two Walsh-style equivalences relating $s^1_2$ to $\Sigma^1_2$-consequences and to $\mathsf{RFN}$-statements, with precise basing requirements (notably $\Sigma^1_2-\mathsf{AC}_0$). A key result is that $s^1_2$ governs $\Sigma^1_2$-reflection strength in a manner analogous to the $\Pi^1_1$-case, and a later connection to $\prec^{\Pi^1_2}_{\Sigma^1_2}$-ranks demonstrates a well-founded hierarchy for $\Sigma^1_2$-sound theories. The work also provides concrete evaluative examples (e.g., $s^1_2(\mathsf{ACA}_0)=s^1_2(\mathsf{KP})=\omega_1^{\mathsf{CK}}$) and discusses the limitations and potential of $s^1_2$-based analysis for future exploration at higher projective levels.

Abstract

The current ordinal analysis provides the proof-theoretic ordinal of a theory, which calibrates the robustness of the $Π^1_1$-consequences of the theory. We can ask whether there is an ordinal characteristic capturing more complex consequences, and it turns out that we can define the $Σ^1_2$-proof-theoretic ordinal capturing the robustness of the $Σ^1_2$-consequences of a theory. In this paper, we study the behavior of $Σ^1_2$-proof-theoretic ordinal, and it turns out that $Σ^1_2$-proof-theoretic ordinal also follows an analogue of Walsh's characterization of proof-theoretic ordinal.

Theorems & Definitions (141)

• Theorem 1.1
• Definition 1
• Definition 2
• Theorem 1.2: Walsh Walsh2023characterizations
• Theorem 1.3
• Theorem 1.4: Kleene normal form theorem
• Theorem
• Theorem
• Theorem
• Proposition 1