Reflection ranks via infinitary derivations

Abstract

There is no infinite sequence of ${\hat{I}}_1^1$-sound extensions of ${\mathsf{ACA}}_0$ each of which proves ${\hat{I}}_1^1$-reflection of the next. This engenders a well-founded ``reflection ranking'' of ${\hat{I}}_1^1$-sound extensions of ${\mathsf{ACA}}_0$. For any ${\hat{I}}_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.

This replaces an earlier paper containing joint work with Fedor Pakhomov. In this version the sections have been rearranged slightly and various typos and ambiguities have been corrected