§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory came into existence in (...) 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2is still something to be sought. However, for reasons that cannot be explained here,-comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2in the foreseeable future.Roughly speaking,ordinally informativeproof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory (...) came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2 is still something to be sought. However, for reasons that cannot be explained here, -comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2 in the foreseeable future.Roughly speaking, ordinally informative proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory came into existence in (...) 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2is still something to be sought. However, for reasons that cannot be explained here,-comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2in the foreseeable future.Roughly speaking,ordinally informativeproof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

In this paper we give a new and comparatively simple proof of the following theorem by Girard [1]:“If ∀x∈ ${\cal O}$ ∃y∈ ${\cal O}$ ψ(x,y) (where the relationψ is arithmetic and positive in Kleene's ${\cal O}$ ), then there exists a recursive DilatorD such that ∀α≧ω∀x∈ ${\cal O}$ <α∃y∈ ${\cal O}$ (...) modification of Girard's system in [1]) we construct in a uniform way for each ordinalα a derivation Tα of the formula ∀x ∈ ${\cal O}$ <α∃y∈ ${\cal O}$ ψ(x, y), and then defineD immediately from the family (Tα)α∈On. Especially we set D(α):=Kleene-Brouwer length of (Tα). (shrink)