  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.

Logic