Proof theory and ordinal analysis (Q2276954)

This paper is some kind of report on the results of a several years' proof theoretic research program, in a certain sense continuing the contribution of the same author in the appendix of the second edition of \textit{G. Takeuti}'s monograph on Proof Theory (1987; Zbl 0609.03019). The topic is ordinal analysis of certain axiom systems, especially by using the method of local predicativity. Ordinal analysis means to calculate the proof theoretic ordinal of the axiom system. To do this, to each formula \(\phi\) of the underlying language of the system, an ordinal \(| \phi |\), the norm of \(\phi\), is associated. The supremum of the norms of all \((\Pi^ 1_ 1)\) sentences which are consequences of the axioms of the system is the proof theoretic ordinal. The following axiom systems are considered: number theory, generalized inductive definitions, Kripke-Platek set theory. The languages are described, the ordinal notations used and ordinal assignments are defined in such a detail that the principle of the method of local predicativity becomes clear. The author points out how and why besides the generalized inductive definitions subsystems of set theory are used for ordinal analysis. The author mentions applications of the results treated so far, to set theory and recursive number theory. So it is possible to gain a good survey of the provably total \(\Sigma_ 1\)-functions of a system of set theory and a classification of the \(\Pi^ 0_ 2\)-Skolem functions and the provably recursive functions in number theory. In the concluding remarks the transition from predicativity to impredicativity is revisited and the connection between ``abstract'' concepts like large cardinals, admissible large ordinals on the one hand and the ``concrete'' counterparts, their collapsings, on the other hand is emphasized. In this setting the author recognizes the ideal and the real elements of Hilbert's program. The reflection of the properties of large cardinals in their applications in proof theory justifies the concern of set theory in these hypothetical objects. Finally the following goals of further research on the topic are listed: the application to functionals of higher types and the ordinal analysis of subsystems of analysis with \(\Pi^ 1_ 2\)-comprehension.