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 .
By and large, ordinal analyses for set theories are more uniform and
transparent than for subsystems of . The axiom systems for
set theories considered in this paper are formulated in the usual
language of set theory (called hereafter) containing
as the only non-logical symbol besides . Formulae are
built from prime formulae and by use of
propositional connectives and quantifiers .
Quantifiers of the forms , are
called bounded. Bounded or
-formulae are the formulae wherein all
quantifiers are bounded; -formulae are those of the form
where is a
-formula. For , -formulae
(-formulae) are the formulae with a prefix of n
alternating unbounded quantifiers starting with a universal
(existential) one followed by a -formula. The class of
-formulae is the smallest class of formulae containing the
-formulae which is closed under , ,
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
for all bounded formulae , Bounded Collection
for all bounded formulae , and Set Induction
for all formulae .
A transitive set A such that 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
. The constructible hierarchy is obtained by iterating the
definable powerset operation through the ordinals
So any element of of level is definable from
elements of with levels and the parameter
. An ordinal is admissible if the
structure is a model of
KP.
Formulae of can be easily translated into the language of
set theory. Some of the subtheories of considered above have
set-theoretic counterparts, characterized by extensions of
KP. KPi is an extension of
KP via the axiom
KPI denotes the system KPi without
Bounded Collection. It turns out that
proves the same -formulae as KPi, while
proves the same -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
, while KPi is the
set-theoretic counterpart to . 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
(where can be taken
to be ) each equipped with their own
“collapsing” function
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 -Reflection on the basis of
the other axioms of KP (see Barwise 1975).
Furthermore, admissible sets of the form also satisfy
-reflection, i.e., if with bounded and
, then there exists such
that and .
In essence, admissible proof theory is a gathering of cut-elimination
and collapsing techniques that can handle infinitary calculi of set
theory with and/or 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
is said to be recursively Mahlo if it satisfies
-reflection in the above sense but with the extra condition
that the reflecting set 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 are
intrinsically singular, i.e., they can be approached from below by a
definable sequence of ordinals
with . In the
representation system for KPM this is no longer the
case. One needs a collapsing function whose values
are regular ordinals themselves, meaning that
they are furnished with their own collapsing function . 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.,
. The purpose of this section is to report on the next major
step in analyzing fragments of . This is obviously the
ordinal analysis of the system
.[55]
The strength of dwarfs that of
. The treatment of
-comprehension posed formidable technical challenges (see
Rathjen 1995, 2005a,b). Other approaches to ordinal analysis of
systems above 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., -reflection.
Definition D.2 is said to be
-reflecting if -reflection. By -reflection we mean the scheme
where C is , expresses that z is
a transitive set and is the formula resulting from C by
restricting all unbounded quantifiers in C to z.
An ordinal representation, , for dealing with
-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 -reflecting ordinal. The levels of collapsing
functions in now become transfinite. They mirror a
transfinite hierarchy of Mahloness. Moreover, the proof-theoretic
treatment of features a new
technique for collapsing families of proofs, called “stationary
collapsing”.
Climbing up in the hierarchy of -reflection, stronger
cardinal notions are required to develop the pertaining representation
systems. Another description of a weakly compact cardinal is that it
is -indescribable. As a rule of thumb, one can develop a
representation system sufficient for analyzing
-reflection by making use of a -indescribable
cardinals (see Rathjen 2005a). Already at that level things become
very involved. At this point the reader might ask whether the theories
with -reflection carry us anywhere near the level of
-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,
-comprehension corresponds to -separation,
i.e., the scheme of axioms
for all -formulas . The precise relationship is as
follows:
Theorem D.3 -separation and
prove the same sentences of second
order arithmetic.
The ordinals such that -Separation are familiar from ordinal recursion
theory.
Definition D.4 An admissible ordinal
is said to be nonprojectible if there is no total
-recursive function mapping one-one into some
, where a function is called -recursive if it is
definable in .
The key to the “largeness” properties of nonprojectible
ordinals is that for any nonprojectible ordinal ,
is a limit of -elementary substructures,
i.e., for every there exists a such that is a -elementary
substructure of , written .
Such ordinals satisfying have
strong reflecting properties. For instance, if for some set-theoretic sentence C (containing parameters
from ), then there exists a such
that . This is because implies , hence using .
The last result makes it clear that an ordinal analysis of
-comprehension would necessarily involve a
proof-theoretic treatment of reflections beyond those surfacing in
admissible proof theory. The notion of stability will be
instrumental.
Definition D.5 is
-stable if
.
For our purposes we need refinements of this notion, the simplest
being provided by -reflection for all n which suffices
to express one step in the relation; cf. Richter &
Aczel 1973: 1.18.
Lemma D.6
iff is
-reflecting for all n.
In the following, we will gradually slice -comprehension
into degrees of reflection to achieve a sense of scale. A further
refinement of the notion of -stability will be addressed
next.
Definition D.7 is said to be
--reflecting if whenever is a
set-theoretic formula,
and , then
there exists such that
and
.
The notion of being
--reflecting is defined in the same vein.
Putting the previous definition to work, one gets:
Corollary D.8 If is
--reflecting, then, for all n,
is --reflecting.
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 is a limit of smaller ordinals
such that . In the
ordinal representation system for , there
will be symbols and for and
, 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
where is a formula, are set
terms of levels , and
. These rules suffice to bring about the
embedding -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
--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.