There is no infinite sequence of \(\Pi ^1_1\) -sound extensions of \(\textsf{ACA}_0\) each of which proves \(\Pi ^1_1\) -reflection of the next. This engenders a well-founded “reflection ranking” of \(\Pi ^1_1\) -sound extensions of \(\textsf{ACA}_0\) . For any \(\Pi ^1_1\) -sound theory T extending \(\textsf{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. We provide an alternative proof of this theorem using cut-elimination for infinitary derivations.
