Reflection ranks via infinitary derivations
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913757996777472 |
|---|---|
| author | Walsh, James |
| author_facet | Walsh, James |
| 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2107_03521 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Reflection ranks via infinitary derivations Walsh, James Logic 03F35, 03F05, 03F15, 03F25 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. |
| title | Reflection ranks via infinitary derivations |
| topic | Logic 03F35, 03F05, 03F15, 03F25 |
| url | https://arxiv.org/abs/2107.03521 |