Reflection ranks via infinitary derivations
Walsh, James · arXiv (Cornell University) · 2021
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.