English

Reflection ranks via infinitary derivations

Logic 2025-03-27 v3

Abstract

There is no infinite sequence of Π11\Pi^1_1-sound extensions of ACA0\mathsf{ACA}_0 each of which proves Π11\Pi^1_1-reflection of the next. This engenders a well-founded ``reflection ranking'' of Π11\Pi^1_1-sound extensions of ACA0\mathsf{ACA}_0. For any Π11\Pi^1_1-sound theory TT extending ACA0+\mathsf{ACA}^+_0, the reflection rank of TT equals the proof-theoretic ordinal of TT. 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.

Keywords

Cite

@article{arxiv.2107.03521,
  title  = {Reflection ranks via infinitary derivations},
  author = {James Walsh},
  journal= {arXiv preprint arXiv:2107.03521},
  year   = {2025}
}

Comments

This replaces an earlier paper containing joint work with Fedor Pakhomov. In this version the sections have been rearranged slightly and various typos and ambiguities have been corrected

R2 v1 2026-06-24T03:58:58.360Z