Proof Society 2025

Invited

Proof theory of stable ordinals

Toshiyasu Arai
University of Tokyo

on  Thu, 15:50in  Class A (Zaal 1.05)for  50min

An ordinal S\mathbb{S} is said to be stable (in a universe LL) iff LSΣ1LL_\mathbb{S} \prec_{\Sigma_1} L. An existence of stable ordinals is closely related to Π12\Pi_1^2-Comprehension Axiom in second order arithmetic in one side, and Σ1\Sigma_1-Separation axiom in set theory on the other.

In this talk let us report proof theory (ordinal analysis) of set theories for stable ordinals. Stable ordinals are eliminated from derivations of Σ\Sigma-sentences on ω1CK\omega_1^{CK} to obtain an upper bound of the proof-theoretic ordinal of the theory. Derivations are controlled by operators as in [3, 5]. A computable notation system of ordinals is extracted from the elimination procedure. ψ\psi-functions in [2] and Mostowski collapsing functions on ordinals are main constructors in the system. Well-foundedness of the system is proved through maximal distinguished classes in [1, 4], which are Σ12\Sigma_1^2-definable.

[1] W. Buchholz, Normalfunktionen und konstruktive Systeme von Ordinalzahlen, Proof Theory Symposion Keil 1974 (J. Diller and G. H. Müller, editors), Lecture Notes in Mathematics vol. 500, Springer, 1975, pp. 4-25.
[2] W. Buchholz, A new system of proof-theoretic ordinal functions, Annals of Pure and Applied Logic vol. 32 (1986), pp. 195-208.
[3] W. Buchholz, A simplified version of local predicativity, Proof Theory (P. H. G. Aczel, H. Simmons and S. S. Wainer, editors), Cambridge UP, 1992, pp. 115-147.
[4] G. Jäger, A well-ordering proof for Feferman’s theory T0T_0 , Archiv für mathematische Logik und Grundlagenforschung vol. 23 (1983), pp. 65-77.
[5] M. Rathjen, Proof theory of reflection, Annals of Pure and Applied Logic vol. 68 (1994), pp. 181-224.

Download the abstract.

 Overview  Program