§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.
A block theoretic proof of Thompson’s $$A\times B$$-lemma
