D. Proof Theory of Set Theories

Clever coding allows one to express an enormous amount of ordinary mathematics in the language of second order arithmetic. Still, many statements of mathematics can only be captured in a circumscribed way in this language. More natural languages for developing mathematics are provided type theory and in its most general form by set theory. With the work of Jäger and Pohlers (1982) the forum of ordinal analysis switched from the realm of second-order arithmetic to set theory, shaping what is now called admissible proof theory, after the models of Kripke-Platek set theory, KP. Their work culminated in the analysis of the system $({\mathrm{\Delta }}_2^1\text{-}\mathbf{\text{CA}})+\mathbf{\text{BI}}$.

By and large, ordinal analyses for set theories are more uniform and transparent than for subsystems of ${\mathbf{Z}}_2$. The axiom systems for set theories considered in this paper are formulated in the usual language of set theory (called ${\mathcal{L}}_{\in }$ hereafter) containing $\in$ as the only non-logical symbol besides $=$. Formulae are built from prime formulae $a\in b$ and $a=b$ by use of propositional connectives and quantifiers $\mathrm{\forall }x,\mathrm{\exists }x$. Quantifiers of the forms $\mathrm{\forall }x\in a$, $\mathrm{\exists }x\in a$ are called bounded. Bounded or ${\mathrm{\Delta }}_0$-formulae are the formulae wherein all quantifiers are bounded; ${\mathrm{\Sigma }}_1$-formulae are those of the form $\mathrm{\exists }x\phi (x)$ where $\phi (a)$ is a ${\mathrm{\Delta }}_0$-formula. For $n>0$, ${\mathrm{\Pi }}_n$-formulae (${\mathrm{\Sigma }}_n$-formulae) are the formulae with a prefix of n alternating unbounded quantifiers starting with a universal (existential) one followed by a ${\mathrm{\Delta }}_0$-formula. The class of $\mathrm{\Sigma }$-formulae is the smallest class of formulae containing the ${\mathrm{\Delta }}_0$-formulae which is closed under $\wedge$, $\vee$, bounded quantification and unbounded existential quantification.

One of the set theories which is amenable to ordinal analysis is Kripke-Platek set theory, KP. Its standard models are called admissible sets. One of the reasons that this is an important theory is that a great deal of set theory requires only the axioms of KP. An even more important reason is that admissible sets have been a major source of interaction between model theory, recursion theory and set theory (cf. Barwise 1975). KP arises from ZF by completely omitting the power set axiom and restricting Separation and Collection to bounded formulae. These alterations are suggested by the informal notion of “predicative”. To be more precise, the axioms of KP consist of Extensionality, Pair, Union, Infinity, Bounded Separation

$$\mathrm{\exists }x\mathrm{\forall }u[u\in x\leftrightarrow (u\in a\wedge F(u))]$$

for all bounded formulae $F(u)$, Bounded Collection

$$\mathrm{\forall }x\in a\mathrm{\exists }yG(x,y)\to \mathrm{\exists }z\mathrm{\forall }x\in a\mathrm{\exists }y\in zG(x,y)$$

for all bounded formulae $G(x,y)$, and Set Induction

$$\mathrm{\forall }x[(\mathrm{\forall }y\in xH(y))\to H(x)],\to \mathrm{\forall }xH(x)$$

for all formulae $H(x)$.

A transitive set A such that $(A,\in )$ is a model of KP is called an admissible set. Of particular interest are the models of KP formed by segments of Gödel’s constructible hierarchy $\mathbf{L}$. The constructible hierarchy is obtained by iterating the definable powerset operation through the ordinals

$$\begin{array}{rl}{\mathbf{L}}_0& =\mathrm{\varnothing },\\ {\mathbf{L}}_{\lambda }& =\bigcup \{{\mathbf{L}}_{\beta }:\beta <\lambda \}\lambda \text{ limit}\\ {\mathbf{L}}_{\beta +1}& =\{X:X\subseteq {\mathbf{L}}_{\beta };X\text{ definable over }⟨{\mathbf{L}}_{\beta },\in ⟩\}.\end{array}$$

So any element of $\mathbf{L}$ of level $\alpha$ is definable from elements of $\mathbf{L}$ with levels $<\alpha$ and the parameter ${\mathbf{L}}_{\alpha }$. An ordinal $\alpha$ is admissible if the structure $({\mathbf{L}}_{\alpha },\in )$ is a model of KP.

Formulae of ${\mathcal{L}}_2$ can be easily translated into the language of set theory. Some of the subtheories of ${\mathbf{Z}}_2$ considered above have set-theoretic counterparts, characterized by extensions of KP. KPi is an extension of KP via the axiom

$$\begin{array}{}\text{(}\mathit{\text{Lim}}\text{)}& \mathrm{\forall }x\mathrm{\exists }y[x\in y\wedge y\text{ is an admissible set}].\end{array}$$

KPI denotes the system KPi without Bounded Collection. It turns out that $({\mathrm{\Delta }}_2^1\text{-}\mathbf{\text{CA}})+\mathbf{\text{BI}}$ proves the same ${\mathcal{L}}_2$-formulae as KPi, while $({\mathbf{\Pi }}_1^1\text{-}\mathbf{\text{CA}})$ proves the same ${\mathcal{L}}_2$-formulae as KPl (see Jäger 1986).

D.1 Admissible proof theory.

KP is the weakest in a line of theories that were analyzed by proof theorists of the Munich school in the late 1970s and 1980s. It can be viewed as a set-theoretic version of other well known theories.

In many respects, KP is a very special case. Several fascinating aspects of ordinal analysis do not yet exhibit themselves at the level of KP.

Recall that KPI is the set-theoretic version of $({\mathbf{\Pi }}_1^1\text{-}\mathbf{\text{CA}})+\mathbf{\text{BI}}$, while KPi is the set-theoretic counterpart to $({\mathrm{\Delta }}_2^1\text{-}\mathbf{\text{CA}})+\mathbf{\text{BI}}$. The main axiom of KPI says that every set is contained in an admissible set (one also says that the admissible sets are cofinal in the universe) without requiring the universe to be admissible, too. To get a sense of scale for comparing KP, KPI, and KPi it is perhaps best to relate the large cardinal assumptions that give rise to the pertinent ordinal representation systems. In the case of KPI the assumption is that there are infinitely many large ordinals ${\mathrm{\Omega }}_1,{\mathrm{\Omega }}_2,{\mathrm{\Omega }}_3,\dots$ (where ${\mathrm{\Omega }}_n$ can be taken to be ${\mathrm{\aleph }}_n$) each equipped with their own “collapsing” function $\alpha \mapsto {\psi }_{{\mathrm{\Omega }}_n}(\alpha )$ as we saw in section 5.3.1. The ordinal system sufficient for KPi is built using the much bolder assumption that there is an inaccessible cardinal I.

As the above set theories are based on the notion of admissible set it is suitable to call the proof theory concerned with them “admissible proof theory”. The salient feature of admissible sets is that they are models of Bounded Collection and that that principle is equivalent to $\mathrm{\Sigma }$-Reflection on the basis of the other axioms of KP (see Barwise 1975). Furthermore, admissible sets of the form ${\mathbf{L}}_{\kappa }$ also satisfy ${\mathrm{\Pi }}_2$-reflection, i.e., if ${\mathbf{L}}_{\kappa }\models \mathrm{\forall }x\mathrm{\exists }yC(x,y,\overrightarrow{a})$ with $C(x,y)$ bounded and $\overrightarrow{a}\in {\mathbf{L}}_{\kappa }$, then there exists $\rho <\kappa$ such that $\overrightarrow{a}\in {\mathbf{L}}_{\rho }$ and ${\mathbf{L}}_{\rho }\models \mathrm{\forall }x\mathrm{\exists }yC(x,y,\overrightarrow{a})$.

In essence, admissible proof theory is a gathering of cut-elimination and collapsing techniques that can handle infinitary calculi of set theory with $\mathrm{\Sigma }$ and/or ${\mathrm{\Pi }}_2$ reflection rules, and thus lends itself to ordinal analyses of theories of the form KP+ “there are x many admissibles” or KP+ “there are many admissibles”.

A theory on the verge of admissible proof theory is KPM, designed to axiomatize essential features of a recursively Mahlo universe of sets. An admissible ordinal $\kappa$ is said to be recursively Mahlo if it satisfies ${\mathrm{\Pi }}_2$-reflection in the above sense but with the extra condition that the reflecting set ${\mathbf{L}}_{\rho }$ be admissible as well. The ordinal representation (Rathjen 1990) for KPM is built on the assumption that there exists a (weakly) Mahlo cardinal. The novel feature over previous work is that there are two layers of collapsing functions. In all of the ordinal representation systems for admissible proof theory, collapsed ordinals ${\psi }_{\pi }(\alpha )$ are intrinsically singular, i.e., they can be approached from below by a definable sequence $({\beta }_{\xi }{)}_{\xi <\lambda }$ of ordinals ${\beta }_{\xi }$ with $\xi <\lambda <{\psi }_{\pi }(\alpha )$. In the representation system for KPM this is no longer the case. One needs a collapsing function ${\psi }_M$ whose values ${\psi }_M(\delta )$ are regular ordinals themselves, meaning that they are furnished with their own collapsing function $\xi \mapsto {\psi }_{{\psi }_M(\delta )}(\xi )$. The ordinal analysis for KPM was carried out in Rathjen 1991. A different approach to KPM using ordinal diagrams is due to Arai (2003).

D.2 Beyond admissible proof theory

Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., ${\mathbf{Z}}_2$. The purpose of this section is to report on the next major step in analyzing fragments of ${\mathbf{Z}}_2$. This is obviously the ordinal analysis of the system $({\mathbf{\Pi }}_2^1\text{-}\mathbf{\text{CA}})$.^[55] The strength of $({\mathbf{\Pi }}_2^1\text{-}\mathbf{\text{CA}})$ dwarfs that of $({\mathrm{\Delta }}_2^1\text{-}\mathbf{\text{CA}})+\mathbf{\text{BI}}$. The treatment of ${\mathrm{\Pi }}_2^1$-comprehension posed formidable technical challenges (see Rathjen 1995, 2005a,b). Other approaches to ordinal analysis of systems above $({\mathrm{\Delta }}_2^1\text{-}\mathbf{\text{CA}})$ are due to Arai (2003, 2004) who uses ordinal diagrams and finite deductions.

The means of admissible proof theory are certainly too weak to deal with the next level of reflection having three alternations of quantifiers, i.e., ${\mathrm{\Pi }}_3$-reflection.

An ordinal representation, $\mathcal{T}(\mathcal{K})$, for dealing with ${\mathrm{\Pi }}_3$-reflection was developed in Rathjen 1994b, utilizing the notion of a weakly compact cardinal. That such a cardinal notion played a role is not a mere accident. Indeed, in Richter & Aczel 1973 the recursively large analogue of a weakly compact cardinal was equated with a ${\mathrm{\Pi }}_3$-reflecting ordinal. The levels of collapsing functions in $\mathcal{T}(\mathcal{K})$ now become transfinite. They mirror a transfinite hierarchy of Mahloness. Moreover, the proof-theoretic treatment of $\mathbf{KP}+{\mathrm{\Pi }}_3\text{-Reflection}$ features a new technique for collapsing families of proofs, called “stationary collapsing”.

Climbing up in the hierarchy of ${\mathrm{\Pi }}_n$-reflection, stronger cardinal notions are required to develop the pertaining representation systems. Another description of a weakly compact cardinal is that it is ${\mathrm{\Pi }}_1^1$-indescribable. As a rule of thumb, one can develop a representation system sufficient for analyzing ${\mathrm{\Pi }}_{n+3}$-reflection by making use of a ${\mathrm{\Pi }}_n^1$-indescribable cardinals (see Rathjen 2005a). Already at that level things become very involved. At this point the reader might ask whether the theories with ${\mathrm{\Pi }}_n$-reflection carry us anywhere near the level of ${\mathrm{\Pi }}_2^1$-comprehension. The answer is, unfortunately, “no” by a wide margin. To make this more visible, we need a few more preparations. On the set-theoretic side, ${\mathrm{\Pi }}_2^1$-comprehension corresponds to ${\mathrm{\Sigma }}_1$-separation, i.e., the scheme of axioms

$$\mathrm{\exists }z(z=\{x\in a:\varphi (x)\})$$

for all ${\mathrm{\Sigma }}_1$-formulas $\varphi$. The precise relationship is as follows:

The ordinals $\kappa$ such that ${\mathbf{L}}_{\kappa }\models \mathbf{KP}+{\mathrm{\Sigma }}_1$-Separation are familiar from ordinal recursion theory.

The key to the “largeness” properties of nonprojectible ordinals is that for any nonprojectible ordinal $\kappa$, ${\mathbf{L}}_{\kappa }$ is a limit of ${\mathrm{\Sigma }}_1$-elementary substructures, i.e., for every $\beta <\kappa$ there exists a $\beta <\rho <\kappa$ such that ${\mathbf{L}}_{\rho }$ is a ${\mathrm{\Sigma }}_1$-elementary substructure of ${\mathbf{L}}_{\kappa }$, written ${\mathbf{L}}_{\rho }{\prec }_1{\mathbf{L}}_{\kappa }$.

Such ordinals satisfying ${\mathbf{L}}_{\rho }{\prec }_1{\mathbf{L}}_{\kappa }$ have strong reflecting properties. For instance, if ${\mathbf{L}}_{\rho }\models C$ for some set-theoretic sentence C (containing parameters from ${\mathbf{L}}_{\rho }$), then there exists a $\gamma <\rho$ such that ${\mathbf{L}}_{\gamma }\models C$. This is because ${\mathbf{L}}_{\rho }\models C$ implies ${\mathbf{L}}_{\kappa }\models \mathrm{\exists }\gamma C^{{\mathbf{L}}_{\gamma }}$, hence ${\mathbf{L}}_{\rho }\models \mathrm{\exists }\gamma C^{{\mathbf{L}}_{\gamma }}$ using ${\mathbf{L}}_{\rho }{\prec }_1{\mathbf{L}}_{\kappa }$.

The last result makes it clear that an ordinal analysis of ${\mathrm{\Pi }}_2^1$-comprehension would necessarily involve a proof-theoretic treatment of reflections beyond those surfacing in admissible proof theory. The notion of stability will be instrumental.

For our purposes we need refinements of this notion, the simplest being provided by ${\mathrm{\Pi }}_n$-reflection for all n which suffices to express one step in the ${\prec }_1$ relation; cf. Richter & Aczel 1973: 1.18.

In the following, we will gradually slice ${\mathrm{\Pi }}_2^1$-comprehension into degrees of reflection to achieve a sense of scale. A further refinement of the notion of $\delta$-stability will be addressed next.

Putting the previous definition to work, one gets:

At this point let us return to proof theory to explain the need for even further refinements of the preceding notions. Recall that the first nonprojectible ordinal $\rho$ is a limit of smaller ordinals ${\rho }_n$ such that ${\mathbf{L}}_{{\rho }_n}{\prec }_1{\mathbf{L}}_{\rho }$. In the ordinal representation system for $({\mathrm{\Pi }}_2^1\text{-}\mathbf{\text{CA}})$, there will be symbols ${\mathfrak{E}}_n$ and ${\mathfrak{E}}_{\omega }$ for ${\rho }_n$ and $\rho$, respectively. They are proof-theoretic analogues of cardinals with very high degrees of indescribability. They were called “reducible cardinals” in Rathjen 2005b.

The associated infinitary proof system will have rules

$$\begin{array}{}\text{(}{\mathit{\text{Ref}}}_{\mathrm{\Sigma }({\mathbf{L}}_{{\mathfrak{E}}_n+\delta })}\text{)}& \frac{\mathrm{\Gamma }\Rightarrow \mathrm{\Delta },C(\overrightarrow{s}{)}^{{\mathbf{L}}_{{\mathfrak{E}}_n+\delta }}}{\mathrm{\Gamma }\Rightarrow \mathrm{\Delta },(\mathrm{\exists }z\in {\mathbf{L}}_{{\mathfrak{E}}_n})(\mathrm{\exists }\overrightarrow{x}\in {\mathbf{L}}_{{\mathfrak{E}}_n})[\mathit{\text{Tran}}(z)\wedge C(\overrightarrow{x}{)}^z]},\end{array}$$

where $C(\overrightarrow{x})$ is a $\mathrm{\Sigma }$ formula, $\overrightarrow{s}$ are set terms of levels $<{\mathfrak{E}}_n+\delta$, and $\delta <{\mathfrak{E}}_{\omega }$. These rules suffice to bring about the embedding $\mathbf{KP}+{\mathrm{\Sigma }}_1$-Separation into the infinitary proof system, but other reflection rules galore will be needed to carry out cut-elimination. For example, there will be “many” ordinals in the pertaining representation system that play the role of $\delta$-${\mathrm{\Pi }}_{n+1}$-reflecting ordinals by virtue of corresponding reflection rules in the infinitary calculus. The corresponding collapsing functions also have new features. Instead of collapsing a single ordinal they will have to collapse intervals. In that way they are reminiscent of inverses of elementary embeddings, with the latter being associated with very large cardinals in classical set theory.