In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible (...) sets also renders a new and perspicuous approach to well-ordering proofs possible. MSC: 03F15, 03F35. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical (...) point of view. (shrink)

In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.

It is shown how the strong ordinal notation systems that figure in proof theory and have been previously defined by employing large cardinals, can be developed directly on the basis of their recursively large counterparts. Thereby we provide a completely new approach to well-ordering proofs as will be exemplified by determining the proof-theoretic ordinal of the systemKPM of [R91].

The foundations of mathematics are divided into proof theory and set theory. Proof theory tries to justify the world of infinite mind from the standpoint of finite mind. Set theory tries to know more and more of the world of the infinite mind. The development of two subjects are discussed including a new proof of the accessibility of ordinal diagrams. Finally the world of large cardinals appears when we go slightly beyond girard's categorical approach to proof theory.