Reflection ranks via infinitary derivations

TL;DR

This work shows that the reflection strength of $Π^1_1$-sound extensions of $\mathsf{ACA}_0^+$, as captured by the $Π^1_1$-reflection ranks, aligns precisely with their proof-theoretic ordinals. The authors provide an alternative proof of this alignment by developing and formalizing cut-elimination for infinitary derivations within $\mathsf{ACA}_0$, and then establishing a two-way equivalence between $\mathsf{RFN}^{1+\alpha}_{Π^1_1}(ACA_0)$ and $WO(\varepsilon_\alpha)$. Central to the argument are ordinal notation systems, Schmerl’s reflexive induction, and Buchholz-style proof transformations, all carried out in a weak arithmetical framework. The result deepens the link between iterated reflection and ordinal analysis, offering a broadly accessible, technically robust route to the same identification of reflection ranks with proof-theoretic ordinals.

Abstract

There is no infinite sequence of $Π^1_1$-sound extensions of $\mathsf{ACA}_0$ each of which proves $Π^1_1$-reflection of the next. This engenders a well-founded ``reflection ranking'' of $Π^1_1$-sound extensions of $\mathsf{ACA}_0$. For any $Π^1_1$-sound theory $T$ extending $\mathsf{ACA}^+_0$, the reflection rank of $T$ equals the proof-theoretic ordinal of $T$. This provides an alternative characterization of the notion of ``proof-theoretic ordinal,'' which is one of the central concepts of proof theory. In this note we provide an alternative proof of this theorem using cut-elimination for infinitary derivations.

Theorems & Definitions (40)

• Theorem 1.1
• Theorem 1.2
• Remark 2.1
• Remark 2.2
• Lemma 2.3
• Theorem 2.4
• Theorem 2.5
• Proposition 2.6: $\mathsf{ACA}_0$
• Theorem 2.7: Schmerl
• proof