Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2107.03521 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- 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.