Reflection ranks and ordinal analysis

TL;DR

This paper introduces the reflection rank as a new way to measure the strength of certain logical theories, showing it aligns with proof-theoretic ordinals and providing simpler proofs of well-foundedness for ordinal systems.

Contribution

It defines reflection rank for $ ext{ACA}_0$ extensions, proves its equivalence to proof-theoretic ordinals, and simplifies well-foundedness proofs of ordinal notation systems.

Findings

Reflection rank matches proof-theoretic ordinal for theories extending $ ext{ACA}_0^+$.

No descending sequences of $ ext{Pi}^1_1$ sound extensions of $ ext{ACA}_0$ in the reflection strength order.

Proof-theoretic ordinal of iterated $ ext{Pi}^1_1$ reflection is $ ext{epsilon}_ ext{alpha}$.

Abstract

It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderness phenomenon by studying a coarsening of the consistency strength order, namely, the $\Pi^1_1$ reflection strength order. We prove that there are no descending sequences of $\Pi^1_1$ sound extensions of $\mathsf{ACA}_0$ in this order. Accordingly, we can attach a rank in this order, which we call reflection rank, to any $\Pi^1_1$ sound extension of $\mathsf{ACA}_0$. We prove that for any $\Pi^1_1$ sound theory $T$ extending $\mathsf{ACA}_0^+$, the reflection rank of $T$ equals the proof-theoretic ordinal of $T$. We also prove that the proof-theoretic ordinal of $\alpha$ iterated $\Pi^1_1$ reflection is $\varepsilon_\alpha$. Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles.