Proof theory of stable ordinals
Toshiyasu Arai
University of Tokyo
An ordinal is said to be stable (in a universe ) iff . An existence of stable ordinals is closely related to -Comprehension Axiom in second order arithmetic in one side, and -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 -sentences on 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. -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 -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 , 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.