## 1. Proof Theory: A New Subject

 

Hilbert viewed the *axiomatic method* as the crucial tool for
mathematics (and rational discourse in general). In a talk to the
Swiss Mathematical Society in 1917, published the following year as
*Axiomatisches Denken* (1918), he articulates his broad
perspective on that method and presents it "at work" by
considering, in detail, examples from various parts of mathematics and
also from physics. Proceeding axiomatically is not just developing a
subject in a rigorous way from first principles, but rather requires,
for advanced subjects, their deeper conceptual organization and
serves, for newer investigations, as a tool for discovery. In his talk
Hilbert reflects on his investigations of the arithmetic of real
numbers and of Euclidean geometry from before 1900. We emphasize the
particular form of his axiomatic formulations; they are not logical
formulations, but rather mathematical ones: he defines Euclidean space
in a similar way as other abstract notions like group or field;
that's why we call it *structural
 axiomatics*.[1]
 However, Hilbert turns from the past and looks to the future,
pointing out a programmatic direction for research in the
*foundations* of mathematics; he writes:



> 
> 
> To conquer this field [concerning the foundations of mathematics] we
> must turn the concept of a specifically mathematical proof itself into
> an object of investigation, just as the astronomer considers the
> movement of his position, the physicist studies the theory of his
> apparatus, and the philosopher criticizes reason itself.
> 
> 
> 



He then asserts, "The execution of this program is at present
still an unsolved task". During the following winter term
1917-18, Hilbert--with the assistance of Paul
Bernays--gave a lecture course entitled *Prinzipien der
Mathematik*. Here modern mathematical logic is invented in one
fell swoop and completes the shift from structural to formal
axiomatics. This dramatic shift allows the constructive, elementary
definition of the syntax of theories and, in particular, of the
concept of *proof in a formal theory*. This fundamental insight
underpins the articulation of the consistency problem and seems to
open a way of proving, meta-mathematically, that no proof in a formal
theory establishes a contradiction.



That perspective is formulated first in a talk Bernays presented in
the fall of 1921, published as "Uber Hilberts Gedanken zur
Grundlegung der Mathematik" (1922). Starting with a discussion
of *structural axiomatics* and pointing out its assumption of a
system of objects that satisfies the axioms, he asserts this
assumption contains "something so-to-speak transcendent for
mathematics". He raises the question, "which principled
position should be taken with respect to it?" Bernays believes
that it might be perfectly coherent to appeal to an *intuitive*
grasp of the natural number sequence or even of the manifold of real
numbers. However, that could not be an intuition in any primitive
sense and would conflict with the tendency of the exact sciences to
use only restricted means to acquire knowledge.



> 
> 
> Under this perspective we are going to try, whether it is not possible
> to give a foundation to these transcendent assumptions in such a way
> that only primitive intuitive knowledge is used. (Bernays 1922:
> 11)
> 
> 
> 



Meaningful mathematics is to be based, Bernays demands, on primitive
intuitive knowledge that includes, however, induction concerning
natural numbers--both as a proof and definition principle. In the
outline for the lectures *Grundlagen der Mathematik* to be
given in the winter term 1921-22, Bernays discusses a few weeks
after his talk "constructive arithmetic" and then the
"broader formulation of constructive thought":



> 
> 
> Construction of the proofs, by means of which the formalization of the
> higher inferences is made possible and the consistency problem is
> becoming accessible in a general way. 
> 
> 
> 



Bernays concludes the outline by suggesting, "This would be
followed by the development of proof theory". The outline was
sent to Hilbert on 17 October 1921 and it was followed strictly in the
lectures of the following term--with only one terminological
change: "constructive" in the above formulations is turned
into
 "finitist".[2]




Bernays's notes of the 1921/22 lectures reflect the consequence
of that change in attitude. They contain a substantial development of
"finitist arithmetic" and "finitist logic" in
a quantifier-free formalism. Finitist arithmetic involves induction
and primitive
 recursion[3]
 from the outset, and the central metamathematical arguments all
proceed straightforwardly by induction on proof figures. The third
part of these lectures is entitled *The grounding of the
consistency of arithmetic by Hilbert's new proof theory*.
Here we find the first significant consistency proof--from a
finitist
 perspective.[4]
 The proof is sketched in Hilbert's Leipzig talk (Hilbert 1923:
184) and was presented in a modified form during the winter term of
1922/23; in that form the proof is given in Ackermann 1925: 4-7.
Ackermann's article was submitted for publication in early 1924,
and by then the proof had taken on a certain canonical form that is
still found in the presentation of Hilbert and Bernays 1934:
220-230. Let us see what was achieved by following
Ackermann's concise discussion.


### 1.1 Hilbert's *Ansatz* and Results

 

The proof is given in section II of Ackermann's paper entitled,
tellingly, *The consistency proof before the addition of the
transfinite axioms*. Ackermann uses a logical calculus in
axiomatic form that is taken over from Hilbert's lectures and is
discussed below in
 section 2.
 Here we just note that it involves two logical rules, namely, modus
ponens and substitution (for individual, function and statement
variables) in axioms. The non-logical axioms concern identity, zero
and successor, and recursion equations that define primitive recursive
functions. The first step in the argument turns the linear proof into
a tree, so that any formula occurrence is used at most once as a
premise of an inference (*Auflosung in Beweisfaden*);
this is done in preparation for the second step, namely, the
elimination of all necessarily free variables (*Ausschaltung der
Variablen*); in the third step, the numerical value of the closed
terms is computed (*Reduktion der Funktionale*). The resulting
syntactic configurations, a *Beweisfigur*, contains now only
*numerical formulae* that are built up from equations or
inequations between numerals and Boolean connectives; these formulae
can be effectively determined to be true or false. By induction on the
"*Beweisfigur*" one shows that all its component
formulae are true; thus, a formula like \(0\ne 0\) is not provable.
The induction principle can be directly incorporated into these
considerations when it is formulated as a rule for quantifier-free
statements. That was not done in Ackermann's discussion of the
proof, but had been achieved already by Hilbert and Bernays in their
1922/23 lectures.



These proof theoretic considerations are striking and important as
they involve for the first time genuine transformations of formal
derivations. Nevertheless, they are preliminary as they concern a
quantifier-free theory that is a *part* of finitist mathematics
and *need* not be secured by a consistency proof. What has to
be secured is "transfinite logic" with its "ideal
elements", as Hilbert put it later. The strategy was direct and
started to emerge already in 1921. First, introduce functional terms
by the *transfinite
 axiom*[5]


 

\[A(a) \to A(\varepsilon x\ldot A(x))\]


and define quantifiers by 

 

 \[
 \exists x A(x) \leftrightarrow A(\varepsilon x\ldot A(x))
 \]


and

 

\[
\forall x A(x) \leftrightarrow A(\varepsilon x\ldot \neg A(x)).
\]


Using the epsilon terms, quantifiers can now be eliminated from proofs
in quantificational logic, thus transforming them into quantifier-free
ones. Finally, the given derivation allows one, so it was conjectured,
to determine numerical values for the epsilon terms. In his Leipzig
talk of September 1922, published in 1923, Hilbert discussed this
*Ansatz* for eliminating quantifiers and reducing the
transfinite case to that of the quantifier-free theory. He presented
the actual execution of this strategic plan only "for the
simplest case" (in Hilbert 1923: 1143-1144). However, the
talk was crucial in the development of proof theory and the finitist
program: "With the structure of proof theory, presented to us in
the Leipzig talk, the principled form of its conception had been
reached". That is how Bernays characterizes its achievement in
his essay on *Hilbert's investigations of the foundations of
arithmetic* (1935: 204)



Ackermann continued in section III of his 1925 at the very spot where
Hilbert and Bernays had left off. His paper, submitted to
*Mathematische Annalen* in March of 1924, and the corrective
work he did in 1925 led to the conviction that the consistency of
elementary arithmetic had been established. The corrective work had
been done to address difficulties von Neumann had pointed out, but was
not published by Ackermann; it was only presented in the second volume
of Hilbert and Bernays 1939 (pp.
 93-130).[6]
 Von Neumann's own proof theoretic investigations, submitted to
*Mathematische Zeitschrift* in July 1925, were published under
the title *Zur Hilbertschen Beweistheorie* in 1927.
Hilbert's 1928 Bologna Lecture prominently took
Ackermann's and von Neumann's work as having established
the consistency of elementary arithmetic, the proof making use only of
finitist principles. Let **F** be a theory containing exclusively
such principles, like *primitive recursive arithmetic*
**PRA**; the principles of **PRA** consist
of the Peano axioms for zero and successor, the defining equations for
all primitive recursive functions (defined in
 note 3),
 and quantifier-free induction. Now the significance of a consistency
proof in **F** can be articulated as follows:




Theorem 1.1 Let **T** be a theory that
contains a modicum of arithmetic and let *A* be a
\(\Pi^0\_1\)-statement, i.e., one of the form \(\forall
x\_1\ldots\forall x\_n\,P(x\_1,\ldots,x\_n)\) with quantifiers ranging
over naturals and *P* a primitive recursive predicate, i.e., a
predicate with a primitive recursive characteristic function. If
**F** proves the consistency of **T** and **T** proves
*A*, then **F** proves *A*.




This theorem can be expressed and proved in **PRA** and
ensures that a **T**-proof of a "real", finitistically
meaningful statement *A* leads to a finitistically valid statement.
This point is made clear in Hilbert's 1927-Hamburg lecture
(Hilbert 1927). There he takes *A* to be the Fermat proposition
and argues that if we had a proof of *A* in a theory containing
"ideal" elements, a finistist consistency proof for that
theory would allow us to transform that proof into a finitist one.



The belief that Ackermann and von Neumann had established the
consistency of elementary arithmetic was expressed as late as December
1930 by Hilbert in his third Hamburg talk (Hilbert 1931a) and by Bernays in April 1931
in a letter to Godel (see Godel 2003: 98-103). Bernays
asserts there that he has "repeatedly considered
[Ackermann's modified proof] and viewed it as correct". He
continues, referring to Godel's incompleteness results,



> 
> 
> On the basis of your results one must now conclude, however, that that
> proof cannot be formalized within the system *Z* [of elementary
> number theory]; this must in fact hold true even if the system is
> restricted so that, of the recursive definitions, only those for
> addition and multiplication are retained. On the other hand, I
> don't see at which place in Ackermann's proof the
> formalization within *Z* should become impossible, ...
> 
> 
> 



At the end of his letter, Bernays mentions that Herbrand misunderstood
him in a recent conversation on which Herbrand had reported in a
letter to Godel with a copy to Bernays. Not only had Herbrand
misunderstood Bernays, but Bernays had also misunderstood Herbrand as
to the extent of the latter's consistency result that was to be
published a few months later as Herbrand 1931. Bernays understood
Herbrand as having claimed that he had established the consistency of
full first-order arithmetic: Herbrand's system is indeed a
first-order theory with a rich collection of finitist functions, but
it uses the induction principle only for quantifier-free
 formulae.[7]
 Godel asserted in December 1933 that this theorem of
Herbrand's was even then the strongest result that had been
obtained in the pursuit of Hilbert's finitist program, and he
formulated the result in a beautiful informal way as follows:



> 
> 
> If we take a theory, which is constructive in the sense that each
> existence assertion made in the axioms is covered by a construction,
> and if we add to this theory the non-constructive notion of existence
> and all the logical rules concerning it, e.g., the law of the excluded
> middle, we shall never get into any contradiction. (Godel 1933:
> 52)
> 
> 
> 



Godel himself had been much more ambitious in early 1930; his
goal was then to prove the consistency of analysis! According to Wang
(1981: 654), his idea was "to prove the consistency of analysis
by number theory, where one can assume the truth of number theory, not
only the consistency". The plan for establishing the consistency
of analysis relative to number theory did not work out, instead
Godel found that sufficiently strong formal theories like
*Principia Mathematica* and Zermelo-Fraenkel set theory are
(syntactically) incomplete.


### 1.2 Incompleteness and a Reduction

 

In 1931 Godel published a paper (1931a) that showed that there
are true arithmetic statements that cannot be proved in the formal
system of *Principia Mathematica*, assuming *PM* to be
consistent. His methods not only applied to *PM* but to any
formal system that contains a modicum of arithmetic. A couple of
months after Godel had announced this result at a conference in
Konigsberg in September 1930, von Neumann and Godel
independently realized that a striking corollary could be drawn from
the incompleteness theorem. Every consistent and effectively
axiomatized theory that allows for the development of basic parts of
arithmetic cannot prove its own consistency. This came to be known as
the *second incompleteness theorem*. (For details on these
theorems and their history see
 appendix A.4)
 The second incompleteness theorem refutes the general ambitions of
Hilbert's program under the sole and very plausible assumption
that finitist mathematics is contained in one of the formal theories
of arithmetic, analysis or set theory. As a matter of fact,
contemporary characterizations of finitist mathematics have elementary
arithmetic as an upper
 bound.[8]
 In response to Godel's result, Hilbert attempted in his
last published paper (1931b) to formulate a strategy for consistency
proofs that is reminiscent of his considerations in the early 1920s
(when thinking about the object theories as constructive) and clearly
extends the finitist standpoint. He introduced a broad constructive
framework that includes full intuitionist arithmetic and suggested
extendibility of the new "method" to "the case of
function variables and even higher sorts of variables". He also
formulated a new kind of rule that allowed the introduction of a new
axiom \(\forall x A(x)\) as soon as all the numerical instances
\(A(n)\) had been established by finitist proofs; in 1931 that is done
for quantifier-free \(A(x)\), whereas in 1931b that is extended to
formulae of arbitrary complexity. The semi-formal calculi, which
articulate the broader framework, are based on rules that reflect
mathematical practice, but also define the meaning of logical
connectives. Indeed, Hilbert's reasons for taking them to be
evidently consistent are expressed in a single sentence: "All
transfinite rules and inference schemata are consistent; for they
amount to definitions". Adding the *tertium non datur* in
the form 

 

\[{\forall x A(x)} \lor {\exists x \neg A(x)}\]


yields now the classical version of the theory and it is that addition
that has to be
 justified.[9]
 Hilbert's problematic considerations for this new
metamathematical step inspired Gentzen's
"Urdissertation" when he began working in late 1931 on a
consistency proof for elementary
 arithmetic.[10]




As part of his "Urdissertation", Gentzen had established
by the end of 1932 the reduction of classical to intuitionist
arithmetic, a result that had also been obtained by Godel.
Gentzen's investigations led, finally in 1935, to his first
consistency proof for arithmetic. In the background was a normal form
theorem for intuitionist logic that will be discussed in the next
section together with Gentzen's actual dissertation and the
special calculi he introduced there. Now we just formulate the
Gentzen-Godel result "connecting" classical
first-order number theory **PA** with its intuitionist
version **HA**. The non-logical principles of these
theories aim at describing \(\fN\), the arguably most important
structure in mathematics, namely, Dedekind's simply infinite
system \(\bbN\) together with zero, successor, multiplication,
exponentiation and the less-than relation: 

 

\[{\fN}=(\bbN; 0^{\bbN}, S^{\bbN},+^{\bbN},\times^{\bbN},E^{\bbN},<^{\bbN}).\]


They are formulated in the first-order language that has the relation
symbols =, <, the function symbols *S*, +, \(\times\),
*E* and the constant symbol 0. The axioms comprise the usual
equations for zero, successor, addition, multiplication,
exponentiation, and the less-than relation. In addition, the
*induction principle* is given by the schema 

\[\tag{IND}
{F(0)} \land {\forall x[F(x)\to F(Sx)]\to \forall x F(x)}
\]

 for
all formulae \(F(x)\) of the language. These principles together with
classical logic constitute the theory of *first order
arithmetic* or *first order number theory*, also known as
*Dedekind-Peano arithmetic*, **PA**; together with
intuitionist logic they constitute *intuitionistic first order
arithmetic* commonly known as *Heyting-arithmetic*,
**HA**.



Now we are considering the syntactic translation \(\tau\) from the
common language of **PA** and **HA** into
its "negative" fragment that replaces disjunctions
\(A\lor B\) by their de Morgan equivalent \(\neg (\neg A\land \neg
B)\) and existential statements \(\exists x A(x)\) by \(\neg \forall
x \neg A(x)\). The reductive result obtained by Gentzen and Godel
in 1933 is now stated quite easily:




Theorem 1.2


1. **PA** proves the equivalence of *A* and \(\tau(A)\)
for any formula *A*.
2. If **PA** proves *A*, then **HA**
proves \(\tau(A)\).




For atomic sentences like \(1\ne 1\) the translation \(\tau\) is
clearly the identity, and the provability of \(1\ne 1\) in
**PA** would imply its provability in
**HA**. Thus, **PA** is consistent relative
to **HA**. This result is technically of great interest
and had a profound effect on the perspective concerning the
relationship between finitism and intuitionism: finitist and
intuitionist mathematics were considered as co-extensional; this
theorem showed that intuitionist mathematics is actually stronger than
finitist mathematics. Thus, if the intuitionist standpoint is taken to
guarantee the soundness of **HA**, then it guarantees the
consistency of **PA**. The corresponding connection
between classical and intuitionist logic had been established already
by Kolmogorov (1925) who not only formalized intuitionist logic but
also observed the translatability of classical into intuitionist
logic. His work, though, seems not to have been noticed at the time or
even in 1932, when Gentzen and Godel established their result for
classical and intuitionist arithmetic.



The foundational discussion concerning extended
"constructive" viewpoints is taken up in
 section 4.
 There, and throughout our paper the concepts of
"proof-theoretic reducibility" and "proof-theoretic
equivalence" will play a central role. The connection between
**PA** and **HA** is paradigmatic and leads
to the notion of *proof-theoretic reduction*. Before we can
furnish a precise definition, we should perhaps stress that many
concepts can be expressed in the language of **PRA** (as
well as **PA**) via coding, also known as *Godel
numbering*. Any finite object such as a string of symbols or an
array of symbols can be coded via a single natural number in such a
way that the string or array can be retrieved from the number when we
know how the coding is done. Typical finite objects include formulae
in a given language and also proofs in a theory. Talk about formulae
or proofs can then be replaced by talking about predicates of numbers
that single out the codes of formulae and proofs, respectively. We
then say that the concepts of formula and proof have been arithmetized
and thereby rendered expressible in the language of
**PRA**.




Definition 1.3 Let \(\bT\_1\), \(\bT\_2\) be a
pair of theories with languages \(\cL\_1\) and \(\cL\_2\), respectively,
and let \(\Phi\) be a (primitive recursive) collection of formulae
common to both languages. Furthermore, \(\Phi\) should contain the
closed equations of the language of **PRA**.



We then say that \(\bT\_1\) is *proof-theoretically
\(\Phi\)-reducible to \(\bT\_2\)*, written
\(\bT\_1\leq\_{\Phi}\bT\_2\), if there exists a primitive recursive
function *f* such that 

 

\[\tag{1}
 \PRA\vdash \forall x \forall y\,[ {\rform\_{\Phi}(x)} \land {\proof\_{\bT\_1}(
y,x)} \rightarrow {\proof\_{\bT\_2}(f(y),x)}].\]


Here \(\rform\_{\Phi}\) and \(\proof\_{\bT\_i}\) are arithmetized
formalizations of \(\Phi\) and the proof relation in \(\bT\_i\),
respectively, i.e., \(\rform\_{\Phi}(x)\) expresses that *x* is
the Godel number of a formula in \(\Phi\) while
\(\proof\_{\bT\_i}(y,x)\) expresses that *y* codes a proof in
\(\bT\_i\) of a formula with Godel number *x*.



\(\bT\_1\) and \(\bT\_2\) are said to be *proof-theoretically
\(\Phi\)-equivalent*, written \(\bT\_1\equiv\_{\Phi}\bT\_2\), if
\(\bT\_1\leq\_{\Phi}\bT\_2\) and \(\bT\_2\leq\_{\Phi}\bT\_1\).



The appropriate class \(\Phi\) is revealed in the process of reduction
itself, so that in the statement of theorems we simply say that
\(\bT\_1\) is *proof-theoretically reducible* to \(\bT\_2\)
(written \(\bT\_1\leq \bT\_2\)) and \(\bT\_1\) and \(\bT\_2\) are
*proof-theoretically equivalent* (written \(\bT\_1 \equiv
\bT\_2\)), respectively. Alternatively, we shall say that \(\bT\_1\) and
\(\bT\_2\) have the *same proof-theoretic strength* when
\(\bT\_1\equiv \bT\_2\). In practice, if \(\bT\_1\equiv \bT\_2\) is shown
via proof-theoretic
 means[11]
 this always entails that the two theories prove at least the same
\(\Pi^0\_2\) sentences (those of the complexity of the twin prime
conjecture). The complexity of formulae of **PRA** is
stratified as follows. The \(\Sigma^0\_0\) and \(\Pi^0\_0\) formulae are
of the form \(R(t\_1,\ldots,t\_n)\) where *R* is a predicate symbol
for an *n*-ary primitive recursive predicate. A formula is
\(\Sigma^0\_{k+1}\) (\(\Pi^0\_{k+1}\)) if it is of the form 



\[
\exists y\_1\ldots \exists y\_m\,F(y\_1,\ldots,y\_m) 
(\forall y\_1\ldots \forall y\_m\,F(y\_1,\ldots,y\_m))
\]


with \(F(y\_1,\ldots,y\_m)\) being of complexity \(\Pi^0\_k\)
(\(\Sigma^0\_k\)). Thus the complexity of a formula is measured in
terms of quantifier alternations. For instance \(\Pi^0\_2\)-formulae
have two alternations starting with a block of universal quantifiers
or more explicitly they are of the shape 

 

\[\forall x\_1\ldots\forall x\_n \exists y\_1\ldots \exists y\_m\,R(x\_1,\ldots,x\_n,y\_1,\ldots,y\_m)\] 


with *R* primitive recursive.



## 2. New Logical Calculi

 

For the reduction of classical elementary number theory to its
intuitionist version, Godel and Gentzen used different logical
calculi. Godel used the system Herbrand had investigated in his
1931, whereas Gentzen employed the formalization of intuitionist
arithmetic from Heyting 1930. For his further finitist investigations
Gentzen introduced new calculi that were to become of utmost
importance for proof theory: natural deduction and sequent
calculi.


### 2.1 From Axioms to Rules: Natural Reasoning

 

As we noted above, Gentzen had already begun in 1931 to be concerned
with the consistency of full elementary number theory. As the logical
framework he used, what we now call, natural deduction calculi. They
evolved from an axiomatic calculus that had been used by Hilbert and
Bernays since 1922 and introduced an important modification of the
calculus for sentential logic. The connectives \(\land \) and \(\lor\)
are incorporated, and the axioms for these connectives are as follows:


 

\[\begin{align}
A\land B & \to A \\
 A\land B & \to B \\
A & \to (B \to A\land B) \\
A & \to A\lor B \\
 B & \to A\lor B \\
(A \to C) & \to ((B \to C) \to (A\lor B \to C))
\end{align}\]


Hilbert and Bernays introduced this new logical formalism for two
reasons, (i) to be able to better and more easily formalize
mathematics, and (ii) to bring out the understanding of logical
connectives in methodological parallel to the treatment of geometric
concepts in *Foundations of geometry*. The methodological
advantages of this calculus are discussed in Bernays 1927: 10:



> 
> 
> The starting formulae can be chosen in quite different ways. A great
> deal of effort has been spent, in particular, to get by with a minimal
> number of axioms, and the limit of what is possible has indeed been
> reached. However, for the purposes of logical investigations it is
> better to separate out, in line with the axiomatic procedure for
> geometry, different axiom groups in such a way that each of them
> expresses the role of a single logical operation.
> 
> 
> 



Then Bernays lists four groups, namely, axioms for the conditional
\(\to\), for \(\land \) and \(\lor\) as above, and for negation
\(\neg\). The axioms for the conditional are not only reflecting
logical properties, but also structural features as in the later
sequent calculus (and in Frege's *Begriffsschrift*,
1879). 

 

\[\begin{align}
A & \to (B \to A)\\
(A \to (A \to B)) & \to (A \to B)\\
(A \to (B \to C)) & \to (B \to (A \to C))\\
(B \to C) & \to ((A \to B) \to (A \to C))
\end{align}\]


As axioms for negation one can choose: 

 

\[\begin{align}
A & \to (\neg A \to B)\\
(A \to B) & \to ((\neg A \to B) \to B)
\end{align}\]


Hilbert formulates this logical system in *Uber das
Unendliche* and in his second Hamburg talk of 1927, but gives a
slightly different formulation of the axioms for negation, calling
them the *principle of contradiction* and the *principle of
double negation*: 

 

\[\begin{align}
(A \to (B \land \neg B)) &\to \neg A\\
\neg\neg A & \to A
\end{align}\]


Clearly, the axioms correspond directly to the natural deduction rules
for these connectives, and one finds here the origin of
Gentzen's natural deduction calculi. Bernays had investigated in
his *Habilitationsschrift* (1918) rule based calculi. However,
in the given context, the simplicity of the metamathematical
description of calculi seemed paramount, and in Bernays 1927 (p. 17)
one finds the programmatic remark: "We want to have as few rules
as possible, rather put much into axioms".



Gentzen was led to a rule-based calculus with *introduction*
and *elimination rules* for every logical connective. The truly
distinctive feature of this new type of calculus was for Gentzen,
however, making and discharging assumptions. This feature, he
remarked, most directly reflects a crucial aspect of mathematical
 argumentation.[12]
 Here we formulate the distinctive rules that involve contradictions
and go beyond minimal logic that has I- and E-rules for all logical
connectives. Intuitionist logic is obtained from minimal logic by
adding the rule: from \(\perp\) infer any formula *A*, i.e.,
*ex falso quodlibet*. In the case of classical logic, if a
proof of \(\perp\) is obtained from the assumption \(\neg A\), then
infer *A* (and cancel the assumption \(\neg A\)). Gentzen
discovered a remarkable fact for the intuitionist calculus, having
observed that proofs can have peculiar *detours* of the
following form: a formula is obtained by an I-rule and is then the
major premise of the corresponding E-rule. For conjunction such a
detour is depicted as follows: 

 

\[
\cfrac{\begin{array}{c}\vdots \\ A\end{array} \quad \begin{array}{c}\vdots \\ B\end{array}}
{\cfrac{A\land B}{B}}
\]


Clearly, a proof of *B* is already contained in the given
derivation. Proofs without detours are called *normal*, and
Gentzen showed that any proof can be effectively transformed via
"reduction steps" into a normal one.




Theorem 2.1 (Normalization for intuitionist
logic) A proof of *A* from a set of assumptions \(\Gamma\)
can be transformed into a normal proof of *A* from the same set
of assumptions.




Focusing on normal proofs, Gentzen proved then that the complexity of
formulae in such proofs can be bounded by that of assumptions and
conclusion.




Corollary 2.2 (Subformula property) If
\(\cD\) is a normal proof of *A* from \(\Gamma\), then every
formula in \(\cD\) is either a subformula of an element \(\Gamma\) or
of *A*.




As Gentzen recounts matters at the very beginning of his dissertation
(1934/35), he was led by the
investigation of the natural calculus to his
 *Hauptsatz*[13]
 when he could not extend the considerations to classical logic.



> 
> 
> To be able to formulate it [the *Hauptsatz*] in a direct way, I
> had to base it on a particularly suitable logical calculus. The
> calculus of natural deduction turned out not to be appropriate for
> that purpose.
> 
> 
> 



So, Gentzen focused his attention on sequent calculi that had been
introduced by Paul Hertz and which had been the subject of
Gentzen's first scientific paper (1932).


### 2.2 Sequent Calculi

 

In his thesis Gentzen introduced a form of the sequent calculus and
his technique of *cut elimination*. As this is a tool of utmost
importance in proof theory, an outline of the underlying ideas will be
discussed next. The sequent calculus can be generalized to so-called
infinitary logics and is central for ordinal analysis. The
*Hauptsatz* is also called the *cut elimination
theorem*.



We use upper case Greek letters
\(\Gamma,\Delta,\Lambda,\Theta,\Xi\ldots\) to range over finite lists
of formulae. \(\Gamma\subseteq \Delta\) means that every formula of
\(\Gamma\) is also a formula of \(\Delta\). A *sequent* is an
expression \(\Gamma\Rightarrow \Delta\) where \(\Gamma\) and
\(\Delta\) are finite sequences of formulae \(A\_1,\ldots,A\_n\) and
\(B\_1,\ldots, B\_m\), respectively. We also allow for the possibility
that \(\Gamma\) or \(\Delta\) (or both) are empty. The empty sequence
will be denoted by \(\emptyset\). \(\Sigma \Rightarrow \Delta\) is
read, informally, as \(\Gamma\) yields \(\Delta\) or, rather, the
*conjunction* of the \(A\_i\) yields the *disjunction* of
the \(B\_j\).



The *logical axioms* of the calculus are of the form 



\[A \Rightarrow A \]


where *A* is any formula. In point of fact, one could limit this
axiom to the case of atomic formulae *A*. We have *structural
rules* of the form 

 

\[
\frac{\Gamma \Rightarrow \Delta}{\Gamma' \Rightarrow \Delta'}
\qquad \textrm{if } \Gamma \subseteq \Gamma', \Delta \subseteq \Delta'. 
\]


A special case of the structural rule, known as *contraction*,
occurs when the lower sequent has fewer occurrences of a formula than
the upper sequent. For instance, \(A, \Gamma\Rightarrow\Delta, B\)
follows structurally from \(A,A,\Gamma \Rightarrow \Delta,B,B\).



Now we list the rules for the logical connectives. 

 

 \[\begin{array}{cc}
 \textrm{Left} & \textrm{Right} \\
\displaystyle \frac{\Gamma \Rightarrow {\Delta,A}}{{\neg A, \Gamma} \Rightarrow \Delta}
 & 
\displaystyle \frac{{B, \Gamma} \Rightarrow {\Delta}}{{\Gamma} \Rightarrow {\Delta, \neg B}}
\\[2ex]
\displaystyle \frac{{\Gamma} \Rightarrow {\Delta, A} \qquad 
{B,\Lambda} \Rightarrow {\Theta}}
{{{A\rightarrow B},\Gamma, \Lambda} \Rightarrow {\Delta, \Theta}}
& 
\displaystyle \frac{{A, \Gamma} \Rightarrow {\Delta, B}}{{\Gamma} \Rightarrow {\Delta, {A \rightarrow B}}}
\\[2ex]
\displaystyle \frac{{A, \Gamma} \Rightarrow {\Delta}}{{A\land B,\Gamma} \Rightarrow {\Delta}}
\quad \frac{{B, \Gamma} \Rightarrow {\Delta}}{{A\land B,\Gamma} \Rightarrow {\Delta}}
 &
\displaystyle \frac{{\Gamma} \Rightarrow {\Delta, A} \qquad 
{\Gamma} \Rightarrow {\Delta, B}}
 {{\Gamma} \Rightarrow {\Delta, {A\land B}}}
 \\[2ex]
\displaystyle \frac{{A,\Gamma} \Rightarrow {\Delta} \qquad 
{B,\Gamma} \Rightarrow {\Delta}}
{{{A\lor B},\Gamma} \Rightarrow {\Delta}}
 &
 \displaystyle \frac{{\Gamma} \Rightarrow {\Delta, A}}{{\Gamma} \Rightarrow {\Delta, {A\lor B}}}
 \quad \frac{{\Gamma} \Rightarrow {\Delta, B}}{{\Gamma} \Rightarrow {\Delta, {A\lor B}}}
 \end{array}
\]

\[\begin{array}{lccclc}
\forall L & \displaystyle \frac{F(t),\Gamma \Rightarrow \Delta}{\forall x F(x),\Gamma \Rightarrow \Delta} 
& &&
\forall R & \displaystyle \frac{\Gamma \Rightarrow {\Delta, F(a)}}{\Gamma \Rightarrow {\Delta, \forall x F(x)}} 
\\[2ex]
\exists L & \displaystyle \frac{F(a),\Gamma \Rightarrow \Delta}{\exists x F(x),\Gamma \Rightarrow \Delta} 
& &&
\exists R & \displaystyle \frac{\Gamma \Rightarrow {\Delta, F(t)}}{\Gamma \Rightarrow {\Delta, \exists x F(x)}} 
\end{array}
\]


In \(\forall L\) and \(\exists R\), *t* is an arbitrary term. The
variable *a* in \(\forall R\) and \(\exists L\) is an
*eigenvariable* of the respective inference, i.e., *a* is
not to occur in the *lower sequent*.



Finally, we have the special *Cut Rule*

 

\[
\frac{\Gamma \Rightarrow {\Delta, A} \qquad {A, \Lambda} \Rightarrow \Theta}
{{\Gamma, \Lambda} \Rightarrow {\Delta, \Theta}} \tag\*{Cut}

\]


The formula *A* is called the *cut formula* of the
inference.



In the rules for logical operations, the formulae highlighted in the
premises are called the *minor formulae* of that inference,
while the formula highlighted in the conclusion is the *principal
formula* of that inference. The other formulae of an inference are
called *side formulae*. A *proof* (also known as a
*deduction* or *derivation*) \(\cD\) is a tree of
sequents satisfying the conditions that (i) the topmost sequents of
\(\cD\) are logical axioms and (ii) every sequent in \(\cD\) except
the lowest one is an upper sequent of an inference whose lower sequent
is also in \(\cD\). A sequent \(\Gamma \Rightarrow \Delta\) is
*deducible* if there is a proof having \(\Gamma \Rightarrow
\Delta\) as its bottom sequent.



The Cut rule differs from the other rules in an important respect.
With the rules for introducing connectives, one sees that every
formula that occurs above the line occurs below the line either
directly, or as a subformula of a formula below the line. That is also
true for the structural rules. (Here \(A(t)\) is counted as a
subformula, in a slightly extended sense, of both \(\exists xA(x)\)
and \(\forall xA(x)\).) But in the case of the Cut rule, the cut
formula *A* vanishes. Gentzen showed that such "vanishing
rules" can be eliminated.




Theorem 2.3 (Gentzen's
*Hauptsatz*) If a sequent \(\Gamma \Rightarrow \Delta\)
is deducible, then it is also deducible without the Cut rule; the
resulting proof is called *cut-free* or *normal*.




The secret to Gentzen's *Hauptsatz* is the symmetry of
left and right rules for all the logical connectives including
negation. The proof of the cut elimination theorem is rather intricate
as the process of removing cuts interferes with the structural rules.
It is contraction that accounts for the high cost of eliminating cuts.
Let \(\lvert \cD\rvert\) be the *height* of the deduction \(\cD\) and let
\(rank(\cD)\) be the *supremum* of the *lengths of cut
formulae* occurring in \(\cD\). Turning \(\cD\) into a cut-free
deduction of the same end sequent results, in the worst case, in a
deduction of height \(\cH(rank(\cD),\lvert \cD\rvert)\) where \(\cH(0,n)=n\) and
\(\cH(k+1,n)=4^{\cH(k,n)}\), yielding hyper-exponential growth.



The sequent calculus we have been discussing allows the proof of
classically, but not intuitionistically correct formulae, for example,
the law of excluded middle. An intuitionist version of the sequent
calculus can be obtained by a very simple structural restriction:
there can be at most one formula on the right hand side of the sequent
symbol \(\Rightarrow\). The cut elimination theorem is also provable
for this intuitionist variant. In either case, the *Hauptsatz*
has an important corollary that parallels that of the Normalization
theorem (for intuitionist logic) and expresses the subformula
property.




Corollary 2.4 (Subformula property) If
\(\cD\) is a cut-free proof of the sequent
\(\Gamma\Rightarrow\Delta\), then all formulae in \(\cD\) are
subformulae of elements in either \(\Gamma\) or \(\Delta\).




This Corollary has another direct consequence that explains the
crucial role of the *Hauptsatz* for obtaining consistency
proofs.




Corollary 2.5 (Consistency) A contradiction,
i.e., the empty sequent \(\emptyset \Rightarrow \emptyset\), is not
provable.





**Proof**: Assume that the empty sequent is provable;
then, according to the *Hauptsatz* it has a cut-free derivation
\(\cD\). The previous corollary assures us that only empty sequents
can occur in \(\cD\); but such a \(\cD\) does not exist since every
proof must contain axioms. \(\qed\)




The foregoing results are solely concerned with pure logic. Formal
theories that axiomatize mathematical structures or serve as formal
frameworks for developing substantial chunks of mathematics are based
on logic but have additional axioms germane to their purpose. If they
are of the latter kind, such as *first-order arithmetic* or
*Zermelo-Fraenkel set theory*, they will assert the existence
of *mathematical objects* and their properties. What happens
when we try to apply the procedure of cut elimination to theories?
Axioms are usually detrimental to this procedure. It breaks down
because the symmetry of the sequent calculus is lost. In general, one
cannot remove cuts from deductions in a theory **T** when the cut
formula is an axiom of **T**. However, sometimes the axioms of a
theory are of *bounded syntactic complexity*. Then the
procedure applies partially in that one can remove all cuts that
exceed the complexity of the axioms of **T**. This gives rise to
*partial cut elimination*. It is a very important tool in proof
theory. For example, it can be used to analyze theories with
restricted induction (such as fragments of **PA**; cf.
Sieg 1985). It also works very well if the axioms of a theory can be
presented as *atomic intuitionist sequents* (also called
*Horn clauses*), yielding the completeness of
*Robinson*'s *resolution method* (see Harrison
2009).



Using the *Hauptsatz* and its Corollary, Gentzen was able to
capture all of the consistency results that had been obtained prior to
1934 including Herbrand's, that had been called by Godel in
his 1933 "the most far-reaching" result. They had been
obtained at least in principle for fragments of elementary number
theory; in practice, Gentzen did not include the quantifier-free
induction principle. Having completed his dissertation, Gentzen went
back to investigate natural deduction calculi and obtained in 1935 his
first consistency proof for full first-order arithmetic. He
formulated, however, the natural calculus now in "sequent
form": instead of indicating the assumptions on which a
particular claim depended by the undischarged ones in its proof tree,
they are attached now to every node of the tree. The
"sequents" that are being proved are of the form \(\Gamma
\Rightarrow A\), where all the logical inferences are carried out on
the right hand side. This proof was published only in 1974; it was
subsequently analyzed most carefully in Tait 2015 and Buchholz 2015.
It was due to criticism of Bernays and Godel that Gentzen
modified his consistency proof quite dramatically; he made use of
transfinite induction, as will be discussed in detail in the next
section. Here we just mention that Bernays extensively discussed
transfinite induction in *Grundlagen der Mathematik II*. The
main issue for Bernays was the question, *is it still a finitist
principle?*--Bernays did not discuss, however, two other
aspects of Gentzen's work, namely, the use of structural
features of formal proofs for consistency proofs and the attempt of
gaining a constructive, semantic understanding of intuitionist
arithmetic. The former became crucial for proof theoretic
investigations; the latter influenced Godel and his functional
interpretation via computable functionals of finite
 type.[14]
 The two aspects together opened a new era for proof theory and
mathematical logic with the goal of proving the consistency of
analysis. We will see, how far current techniques lead us and what
foundational significance one can attribute to them.


## 3. Gentzen's Consistency Proof

 

Cut elimination fails for first-order arithmetic (i.e.,
**PA**), not even partial cut elimination is possible
since the induction axioms have unbounded complexity. Gentzen,
however, found an ingenious way of dealing with purported
contradictions in arithmetic. In Gentzen 1938b he showed how to effectively
transform an alleged **PA**-proof of an inconsistency
(the empty sequent) in his sequent calculus into another proof of the
empty sequent such that the latter gets assigned a smaller ordinal
than the former. Ordinals are a central concept in set theory as well
as in proof theory. To present Gentzen's work we shall first
discuss the notion of ordinal from a proof-theoretic point of
view.


### 3.1 Ordinals in Proof Theory

 

This is the first time we talk about the transfinite and ordinals in
proof theory. Ordinals have become very important in advanced proof
theory. The concept of an ordinal is a generalization of that of a
natural number. The latter are used for counting finitely many things
whereas ordinals can also "count" infinitely many things.
It is derived from the concept of an ordering \(\prec\) of a set
*X* which arranges the objects of *X* in order, one after
another, in such a way that for every predicate *P* on *X*
there is always a first element of *X* with respect to \(\prec\)
that satisfies *P* if there is at least one object in *X*
satisfying *P*. Such an ordering is called a
*well-ordering* of *X*. Certainly the usual less-than
relation on \(\bbN\) is a well-ordering. Here every number \(\ne 0\)
is the successor of another number. If one orders the natural numbers
\(>0\) in the usual way but declares that 0 is bigger than every
number \(\ne 0\) one arrives at another ordering of \(\bbN\).
Let's call it \(\prec\). \(\prec\) is also a well-ordering of
\(\bbN\). This time 1 is the least number with respect to \(\prec\).
However, 0 plays a unique role. There are infinitely many numbers
\(\prec 0\) and there is no number \(m\prec 0\) such that 0 is the
next number after *m*. Such numbers are are called limit numbers
(with respect to \(\prec\)).



In order to be able to formulate Gentzen's results from the end
of section 3.3, we have to "arithmetize" the treatment of
ordinals. Let us first state some precise definitions and a Cantorian
theorem.




Definition 3.1 A non-empty set *A*
equipped with a total ordering \(\prec\) (i.e., \(\prec\) is
transitive, irreflexive, and 

 

\[\forall x,y\in A\,[{x\prec y}\lor {x=y}\lor {y\prec x}])\]


is a *well-ordering* if every non-empty subset *X* of
*A* contains a \(\prec\)-least element, i.e.,

 

\[(\exists u\in X)(\forall y\in X)[{u\prec y}\lor {u=y}].\]


The elements of a well-ordering \((A,\prec)\) can be divided into
three types. Since *A* is non-empty there is least element with
respect to \(\prec\) which is customarily denoted by 0 or \(0\_A\).
Then there are elements \(a\in A\) such that there exists \(b\prec a\)
but there is no *c* between *b* and *a*. These are the
successor elements of *A*, with *a* being the successor of
*b*. An element \(c\in A\) such that \(0\prec c\) and for all
\(b\prec c\) there exists \(d\in A\) with \(b\prec d\prec c\) is said
to be a limit element of *A*.



In set theory a set is called *transitive* just in case all its
elements are also subsets. An *ordinal* in the set-theoretic
sense is a transitive set that is well-ordered by the elementhood
relation \(\in\). It follows that each ordinal is the set of
predecessors. According to the trichotomy above, there is a least
ordinal (which is just the empty set) and all other ordinals are
either successor or limit ordinals. The first limit ordinal is denoted
by \(\omega\).





Fact 3.2 Every well-ordering \((A,\prec)\)
is order isomorphic to a unique ordinal \((\alpha,\in)\).




Ordinals are traditionally denoted by lower case Greek letters
\(\alpha,\beta,\gamma,\delta,\ldots\) and the relation \(\in\) on
ordinals is notated simply by \(<\). If \(\beta \) is a successor
ordinal, i.e., \(\beta\) is the successor of some (necessarily unique)
ordinal \(\alpha\) we also denotes \(\beta\) by \(\alpha'\).
Another important fact is that for any family of ordinals \(\alpha\_i\)
for \(i\in I\) (*I* some set) there is a smallest ordinal,
denoted by \(\sup\_{i\in I}\alpha\_i\) that is bigger than every ordinal
\(\alpha\_i\).



The operations of addition, multiplication, and exponentiation can be
defined on all ordinals by using case distinctions and transfinite
recursion (on \(\alpha\)). The following states the definitions just
to convey the flavor: 

 

\[\begin{align}
 \beta+0 &= \beta & \beta+\alpha' &=(\beta+\alpha)' &\displaystyle \beta+\lambda &=\sup\_{\xi<\lambda}(\beta+\xi)\\
\beta\cdot 0 &= 0 & \beta\cdot \alpha' &=(\beta\cdot\alpha)+\beta &\displaystyle \beta\cdot \lambda &=\sup\_{\xi<\lambda}(\beta\cdot\xi)\\
\beta^ 0 &= 0' & \beta^{ \alpha'} &=\beta^{\alpha}\cdot \beta &\displaystyle \beta^\lambda &=\sup\_{\xi<\lambda}(\beta^\xi)
\end{align}\]


However, addition and multiplication are in general not
commutative.



We are interested in representing specific ordinals \(\alpha\) as
relations on \(\bbN\). In essence Cantor defined the first ordinal
representation system in 1897. Natural *ordinal representation
system*s are frequently derived from structures of the form 



\[\tag{2}
{\frakA} = \langle\alpha,f\_1,\ldots,f\_n,<\_{\alpha}\rangle
\]


where \(\alpha\) is an ordinal, \(<\_{\alpha}\) is the ordering of
ordinals restricted to elements of \(\alpha\) and the \(f\_i\) are
functions 

 

\[\tag{3}
f\_i:\underbrace{\alpha\times\cdots\times\alpha}\_{k\_i \textrm{ times}}
\longrightarrow \alpha
\]


for some natural number \(k\_i\). 

 

\[
 \bbA = \langle A,g\_1,\ldots,g\_n,\prec\rangle
\]


is a *computable* (or *recursive*)
*representation* of \(\frakA\) if the following conditions
hold:


1. \(A\subseteq\bbN\) and *A* is a computable set.
2. \(\prec\) is a computable total ordering on *A* and the functions
\(g\_i\) are computable.
3. \(\frakA \cong\bbA\), i.e., the two structures are
isomorphic.




Theorem 3.3 (Cantor 1897) For every ordinal
\(\beta>0\) there exist unique ordinals
\(\beta\_0\geq\beta\_1\geq\dots\geq\beta\_n\) such that 

 

\[\tag{4}\label{epsilon} \beta = \omega^{\beta\_0}+\ldots+\omega^{\beta\_n}.\]



The representation of \(\beta\) in (4) is called the *Cantor normal
form*. We shall write \(\beta \mathbin{=\_{\sCNF}}
\omega^{\beta\_1}+\cdots +\omega^{\beta\_n}\) to convey that
\(\beta\_0\geq\beta\_1\geq\dots\geq\beta\_k\).



The rather famous ordinal that emerged in Gentzen's consistency
proof of **PA** is denoted by \(\varepsilon\_0\). It
refers to first ordinal \(\alpha>0\) such that \((\forall
\beta<\alpha)\,\omega^{\beta}<\alpha\). \(\varepsilon\_0\) can
also be described as the least ordinal \(\alpha\) such that
\(\omega^{\alpha}=\alpha\).



Ordinals \(\beta<\varepsilon\_0\) have a Cantor normal form with
exponents \(\beta\_i<\beta\) and these exponents have Cantor normal
forms with yet again smaller exponents. As this process must
terminate, ordinals \(<\varepsilon\_0\) can be coded by natural
numbers. For instance a coding function 

 

\[{\Corner{\mathord{\,.\,}}}:\varepsilon\_0\longrightarrow \bbN\]


could be defined as follows: 

 

\[{\Corner{\alpha}} = 
\left\{\begin{array}{ll} 
0 
& \textrm{if } \alpha=0\\ 
\langle{\Corner{\alpha\_1}},\ldots,{\Corner{\alpha\_n}}\rangle 
& \textrm{if } \alpha \mathbin{=\_{\sCNF}} \omega^{\alpha\_1}+\cdots+\omega^{\alpha\_n} 
\end{array}\right.\]


where \(\langle k\_1,\cdots,k\_n\rangle\coloneqq
2^{k\_1+1}\cdot\ldots\cdot p\_n^{k\_n+1}\) with \(p\_i\) being the
*i*th prime number (or any other coding of tuples). Further
define: 

 

\[\begin{align}
A\_0 &{} \coloneqq \textrm{range of }\ {\Corner{\mathord{.} }} \\
{\Corner{\alpha}}\prec{\Corner{\beta}} &{} \mathbin{:\Leftrightarrow} \alpha<\beta \\ 
{\Corner{\alpha}} \mathop{\hat{+}} {\Corner{\beta}} &{} \coloneqq {\Corner{\alpha+\beta}} \\
{\Corner{\alpha}} \mathop{\hat{\cdot}} {\Corner{\beta}} &{} \coloneqq {\Corner{\alpha\cdot\beta}} \\
\hat{\omega}^{{\Corner{\alpha}}} &{} \coloneqq {\Corner{\omega^{\alpha}}}.\\
\end{align}\]


Then 

 

\[
 {\langle\varepsilon\_0,+,\cdot,\delta\mapsto \omega^{\delta},<\rangle}
\cong {\langle A\_0,\hat{+},\hat{\cdot},x\mapsto\hat{\omega}^{x},\prec\rangle}
.\]


\(A\_0,\hat{+},\hat{\cdot},x\mapsto\hat{\omega}^{x},\prec\) are
primitive recursive. Finally, we can spell out the scheme
PR-TI\((\varepsilon\_0)\) in the language of **PA**: 



\[
\forall x\, {\left[\forall y\, \left({y\prec x} \to {P(y)}\right) \to {P(x)}\right]} \to {\forall x\, {P(x)}}
\]


for all primitive recursive predicates *P*.



Given a natural ordinal representation system \(\langle
A,\prec,\ldots\rangle\) of order type \(\tau\) let
\(\PRA+\rTI\_{\qf}(<\tau)\) be **PRA** augmented by
quantifier-free induction over all initial (externally indexed)
segments of \(\prec\). This is perhaps best explained via the
representation system for \(\varepsilon\_0\) given above. There one can
take the initial segments of \(\prec\) to be determined by the
Godel numbers of the ordinals \(\omega\_0\coloneqq 1\) and
\(\omega\_{n+1}\coloneqq \omega^{\omega\_n}\) whose limit is
\(\varepsilon\_0\).




Definition 3.4 We say that a theory *T*
has *proof-theoretic ordinal* \(\tau\), written \(\lvert T\rvert =\tau\),
if *T* can be proof-theoretically reduced to
\(\PRA+\rTI\_{\qf}(<\tau)\), i.e., 

 

\[
 T \mathbin{\equiv\_{\Pi^0\_2}} \PRA+\rTI\_{\qf}(<\tau).
\]



Unsurprisingly, the above notion has certain intensional aspects and
hinges on the naturality of the representation system (for a
discussion see Rathjen 1999a: section 2.). 


### 3.2 Infinite Proofs

 

Gentzen's consistency proof for **PA** employs a
reduction procedure \(\cR\) on proofs *P* of the empty sequent
together with an assignment *ord* of representations for ordinals
to proofs such that \(\ord(\cR(P))< \ord(P)\). Here \(<\)
denotes the ordering on ordinal representations induced by the
ordering of the pertinent ordinals. For this purpose he needed
representations for ordinals \(<\varepsilon\_0\) where
\(\varepsilon\_0\) is the smallest ordinal \(\tau\) such that whenever
\(\alpha<\tau\) then also \(\omega^{\alpha}<\tau\) with
\(\alpha\mapsto \omega^{\alpha}\) being the function of ordinal
exponentiation with base \(\omega\). Moreover, the functions \(\cR\)
and *ord* and the relation \(<\) are computable (when viewed
as acting on codes for the syntactic objects), they can be chosen to
be primitive recursive. With \(g(n)= \ord(\cR^n(P))\), the
*n*-fold iteration of \(\cR\) applied to *P*, one has
\(g(0)>g(1)> g(2)> \ldots > g(n)\) for all *n*, which
is absurd as the ordinals \(<\varepsilon\_0\) are well-founded.
Hence **PA** is consistent.



Gentzen's proof, though elementary, was very intricate and thus
more transparent proofs were sought. As it turned out, the obstacles
to cut elimination, inherent to **PA**, could be overcome
by moving to a richer proof system, albeit in a drastic way by going
*infinite*. This richer system allows for proof rules with
infinitely many
 premises.[15]
 The inference commonly known as the \(\omega\)-*rule* consists
of the two types of *infinitary inferences*:

 

\[
\begin{align}
\frac{\Gamma \Rightarrow {\Delta, F(0)};\;
\Gamma \Rightarrow {\Delta,F(1)};\; 
\ldots; \Gamma \Rightarrow {\Delta,F(n)};\;
\ldots}
{\Gamma \Rightarrow {\Delta,\forall x\,F(x)}}
\tag\*{\(\omega R\)}
\\[1ex]
\frac{{F(0),\Gamma} \Rightarrow {\Delta};\;
 {F(1), \Gamma} \Rightarrow {\Delta};\;
\ldots; {F(n),\Gamma} \Rightarrow {\Delta};
\ldots}
{\exists x\,F(x), {\Gamma \Rightarrow \Delta} }
\tag\*{\(\omega L\)}
\end{align}\]


The price to pay will be that deductions become infinite objects,
i.e., *infinite well-founded trees*.



The sequent-style version of Peano arithmetic with the
\(\omega\)-*rule* will be denoted by \(\PA\_{\omega}\).
\(\PA\_{\omega}\) has no use for free variables. Thus free variables
are discarded and all *terms* will be closed. All formulae of
this system are therefore closed, too. The *numerals* are the
terms \(\bar{n}\), where \(\bar{0}=0\) and
\(\overline{n+1}=S\bar{n}\). We shall identify \(\bar{n}\) with the
natural number *n*. All terms *t* of \(\PA\_{\omega}\)
evaluate to a numeral \(\bar{n}\).



\(\PA\_{\omega}\) has all the inference rules of the sequent calculus
except for \(\forall R\) and \(\exists L\). In their stead,
\(\PA\_{\omega}\) has the \(\omega R\) and \(\omega L\) inferences. The
*Axioms* of \(\PA\_{\omega}\) are the following: (i)
\(\emptyset\Rightarrow A\) if *A* is a *true* atomic
sentence; (ii) \(B\Rightarrow \emptyset\) if *B* is a
*false* atomic sentence; (iii) \(F(s\_1,\ldots,s\_n)\Rightarrow
F(t\_1,\ldots,t\_n)\) if \(F(s\_1,\ldots,s\_n)\) is an atomic sentence and
the \(s\_i\) and \(t\_i\) evaluate to the same numerals,
respectively.



With the aid of the \(\omega\)-rule, each instance of the induction
scheme becomes logically deducible with an infinite proof tree. To
describe the cost of cut elimination for \(\PA\_{\omega}\), we
introduce the measures of *height* and *cut rank* of a
\(\PA\_{\omega}\) deduction \(\cD\). We will notate this by 



\[\cD \stile{\alpha}{k} \Gamma \Rightarrow \Delta.\]


The above relation is defined inductively following the buildup of the
deduction \(\cD\). For the *cut rank* we need the definition of
the *length*, \(\lvert A\rvert\) of a formula: 

 

\[
\begin{align}
\lvert A\rvert & =0 \textrm{ if } A \textrm{ is atomic; }\\
\lvert \neg A\_0\rvert & =\lvert A\_0\rvert +1; \\
\lvert A\_0\mathbin{\Box} A\_1\rvert & =\max(\lvert A\_0,A\_1\rvert)+1
\end{align}
\]


where \(\Box=\land,\lor,\to\); \(\lvert \exists x\,F(x)\rvert =\lvert \forall
x\,F(x)\rvert =\lvert F(0)\rvert +1\).



Now suppose the last inference *I* of \(\cD\) is of the form 



\[
\frac{
\begin{array}{c}
\cD\_0\\
{\Gamma\_0\Rightarrow \Delta\_0}
\end{array}
\ \ldots\ 
\begin{array}{c}
\cD\_n\\
{\Gamma\_n\Rightarrow \Delta\_n}
\end{array}
\ \ldots\
 n<\tau }
 {\Gamma\Rightarrow \Delta}
 I
\]


where \(\tau=1,2,\omega\) and the \(\cD\_n\) are the immediate
subdeductions of \(\cD\). If 

 

\[{\cD\_n \stile{\alpha\_n}{k} \Gamma\_n} \Rightarrow \Delta\_n\]


and \(\alpha\_n<\alpha\) for all \(n<\tau\) then 



\[{\cD \stile{\alpha}{k} \Gamma} \Rightarrow \Delta\]


providing that in the case of *I* being a *cut* with cut
formula *A* we also have \(\lvert A\rvert <k\). We will write
\({\PA\_{\omega} \stile{\alpha}{k} \Gamma} \Rightarrow \Delta\) to
convey that there exists a \(\PA\_{\omega}\)-deduction
\({\cD\stile{\alpha}{k} \Gamma}\Rightarrow \Delta\). The ordinal
analysis of **PA** proceeds by first unfolding any
**PA**-deduction into a \(\PA\_{\omega}\)-deduction: 



\[\tag{5}\label{einbett}
\textrm{If } {\PA \vdash \Gamma}\Rightarrow \Delta \textrm{ then }
 {\PA\_{\omega} \stile{\omega+m}{k} \Gamma} \Rightarrow \Delta
\]


for some \(m,k<\omega\). The next step is to get rid of the cuts.
It turns out that the cost of lowering the cut rank from \(k+1\) to
*k* is an exponential with base \(\omega\).




Theorem 3.5 (Cut Elimination for
\(\PA\_{\omega}\)) If \({\PA\_{\omega} \stile{\alpha}{k+1}
\Gamma} \Rightarrow \Delta\), then

 

\[
{\PA\_{\omega} \stile{\omega^{\alpha}}{k} \Gamma} \Rightarrow \Delta.
\]



As a result, if \({\PA\_{\omega} \stile{\alpha}{n} \Gamma}\Rightarrow
\Delta\), we may apply the previous theorem *n* times to arrive
at a cut-free deduction \({\PA\_{\omega} \stile{\rho}{0} \Gamma}
\Rightarrow \Delta\) with
\(\rho=\omega^{\omega^{\iddots^{\omega^{\alpha}}}}\), where the stack
has height *n*. Combining this with the result from
\((\ref{einbett})\), it follows that every sequent \(\Gamma\Rightarrow
\Delta\) deducible in **PA** has a cut-free deduction in
\(\PA\_{\omega}\) of length \(<\varepsilon\_0\). Ruminating on the
details of how this result was achieved yields a consistency proof for
**PA** from transfinite induction up to \(\varepsilon\_0\)
for elementary decidable predicates on the basis of finitist reasoning
(as described below).



Gentzen did not deal explicitly with infinite proof trees in his
second published proof of the consistency of **PA**
(Gentzen 1938b). However, in
the unpublished first consistency proof of Gentzen 1974 he aims at
showing that a proof of a sequent in first-order arithmetic gives rise
to a a well-founded reduction tree; that tree can be identified with a
cut-free proof in the sequent calculus with the \(\omega\)-rule. The
infinitary version of **PA** with the \(\omega\)-rule was
investigated by Schutte (1950). There remained the puzzle, how
Gentzen's work that used an ingenious method of assigning
ordinals to purported proofs of the empty sequent relates to the
infinitary approach. Much later work by Buchholz (1997) and others
revealed an intrinsic connection between Gentzen's assignment of
ordinals to deductions in **PA** and the standard one to
infinite deductions in \(\PA\_{\omega}\). In the 1950s infinitary proof
theory flourished in the hands of Schutte. He extended his
approach to **PA** to systems of ramified analysis to be
discussed below in
 section 5.2.



One last remark about the use of ordinals: Gentzen showed that
transfinite induction up to the ordinal \(\varepsilon\_0\) suffices to
prove the consistency of **PA**. Using the arithmetized
formalization of the proof predicate (see above, after
 Definition 1.3)
 and taking *k* as the numeral denoting the Godel number of
the formula \(0=1\), we can express the consistency of
**PA**, \(\Con (\PA)\), by the formula \(\forall x
\,\neg\proof\_{\PA}(x,k)\). To appreciate Gentzen's result it is
pivotal to note that he applied transfinite induction up to
\(\varepsilon\_0\) only for primitive recursive predicates (the latter
principle was denoted above by PR-TI\((\varepsilon\_0)\)). Otherwise,
Gentzen's proof used only finistist means. Hence, a more
accurate formulation of Gentzen's result is 

 

\[\tag{6}\label{picture}
\bF+\textrm{PR-TI}(\varepsilon\_0) \vdash \Con (\PA),\]


where **F**, as above, contains only finitistically acceptable
means. In his 1943 paper Gentzen also showed that this result is best
possible, as **PA** proves transfinite induction up to
any \(\alpha<\varepsilon\_0\). So one might argue that the
non-finitist part of **PA** is encapsulated in
PR-TI\((\varepsilon\_0)\) and therefore "measured" by
\(\varepsilon\_0\). \(\varepsilon\_0\) is also the proof-theoretic
ordinal of **PA** as specified in
 Definition 3.4.
 Gentzen hoped that results of this character could also be obtained
for stronger mathematical theories, in particular for analysis.
Hilbert's famous second problem asked for a direct consistency
proof of that mathematical theory. Gentzen wrote in 1938 that



> 
> 
> the most important [consistency] proof of all in practice, that for
> *analysis*, is still outstanding. (1938a [Gentzen 1969: 236]).
> 
> 
> 
> 



He actually worked on a consistency proof for analysis as letters 
(e.g. one to Bernays on 23.6.1935 translated in von Plato 2017: 240) and stenographic
notes from 1945 (e.g., Gentzen 1945) show. Formally, "analysis" was identified
already in Hilbert 1917/18 as a form of second order number theory.
Hilbert and Bernays developed mathematical analysis in a supplement of
the second volume of their "Grundlagen der Mathematik". We
take \(\bZ\_2\) as given in the following way. Its language extends
that of **PA** by an additional sort of variables
\(X,Y,Z,\ldots\) that range over sets of numbers and the binary
membership relation \(t\in X\). Its axioms are those of
**PA**, but the principle of proof by induction is
formulated as the *second order induction axiom* 



\[\forall X(0\in X\land\forall x(x\in X\rightarrow S(x)\in X) \rightarrow \forall x(x\in X)).\]


Finally, the axiom schema of *comprehension*,
**CA**, asserts that for every formula \({F}(u)\) of the
language of \(\bZ\_2\), there is a set \(X=\{u\mid {F}(u)\}\) having
exactly those numbers *u* as members that satisfy \({F}(u)\).
More formally, 

  

\[\label{CA}\tag{\(\bCA\)}
\exists X\forall u(u\in X\leftrightarrow{F}(u))
\]


for all formulae \({F}(u)\) in which *X* does not occur. That
\(\bZ\_2\) is often called "analysis" is due to the
realization (e.g., in Hilbert & Bernays 1939) that, via the coding
of real numbers and continuous functions as sets of natural numbers, a
good theory of the continuum can be developed from these axioms.



Modern analyses of "finitist mathematics" consider it as
situated between **PRA** and **PA**. When
arguing that Godel's second incompleteness theorem refutes
Hilbert's finitist program, von Neumann argued that finitist
mathematics is included in **PA** and, if not there,
undoubtedly in \(\bZ\_2\). So it is quite clear that a consistency
proof of \(\bZ\_2\) would use non-finitist principles or that the
pursuit of the consistency program would require an extension of the
finitist standpoint. In the next section we discuss briefly a variety
of extensions and elaborate two in greater detail.


## 4. Hilbert's Program, Extended

 

According to Bernays, the reductive result due to Godel and
Gentzen,
 Theorem 1.2,
 has a dramatic impact on the work concerned with Hilbert's
program. It opened in a very concrete and precise way the finitist
perspective to a broader "constructive" one. Hilbert
himself had taken such a step in a much vaguer way in his last paper
(Hilbert 1931b).
 Theorem 1.2
 showed, after all, that **PA** is contained in
**HA** via the negative translation. Since
**HA** comprises just a fragment of Brouwer's
intuitionism, the consistency of **PA** is secured on the
basis of the intuitionist standpoint. In a letter to Heyting of 25
February 1933, Gentzen suggested investigating the consistency of
**HA** since a consistency proof for classical arithmetic
had not been given so far by finitist means. He then continued



> 
> 
> If on the other hand, one admits the intuitionistic position as a
> secure basis in itself, i.e., as a consistent one, the consistency of
> classical arithmetic is secured by my result. If one wished to satisfy
> Hilbert's requirements, the task would still remain of showing
> intuitionistic arithmetic consistent. This, however, is not possible
> by even the formal apparatus of classical arithmetic, on the basis of
> Godel's result in combination with my proof. Even so, I am
> inclined to believe that a consistency proof for intuitionistic
> arithmetic, from an even more evident position, is possible and
> desirable. (quoted and translated in von Plato 2009: 672)
> 
> 
> 



Godel took a very similar position in December of 1933
(Godel 1995: 53). There he broadened the idea of a revised
version of Hilbert's program allowing constructive means that go
beyond the finitist ones without accepting fully fledged intuitionism;
the latter he considered to be problematic, in particular on account
of the impredicative nature of intuitionist implication. As to an
extension of Hilbert's position he wrote:



> 
> 
> But there remains the hope that in future one may find other and more
> satisfactory methods of construction beyond the limits of the system A
> [capturing finitist methods], which may enable us to found classical
> arithmetic and analysis upon them. This question promises to be a
> fruitful field for further investigations.
> 
> 
> 



In
 section 3.2
 we described Gentzen's considerations; in
 section 4.2
 we discuss Godel's as developed in the late 1930s. In
 section 4.1
 we *sketch* some other constructive positions.


### 4.1 Constructive Frameworks

 

A particularly appealing idea is to pursue Hilbert's program
relative to a constructive point of view and determine which parts of
classical mathematics are demonstrably consistent relative to that
standpoint (see Rathjen 2009 for pursuing this with regard to
Martin-Lof type theory). As one would suspect, there are
differing "schools" of constructivism and different layers
of constructivism. Several frameworks for developing mathematics from
such a point of view have been proposed. Some we will refer to in this
article (arguably the most important) are:


1. Arithmetical Predicativism.
2. Theories of higher type functionals.
3. Takeuti's "Hilbert-Gentzen finitist
standpoint".
4. Feferman's explicit mathematics.
5. Martin-Lof's intuitionistic type theory.
6. Constructive set theory (Myhill, Friedman, Beeson, Aczel).



At this point we will just give a very rough description of these
foundational views. A few more details, especially about their scope
on a standard scale of theories and proof-theoretic ordinals, will be
provided at the very end of
 section 5.3.



(a) Arithmetical Predicativism originated in the writings of
Poincare and Russell in response to the set-theoretic
paradoxes. It is characterized by a ban of impredicative definitions.
Whilst it accepts the completed infinite set of naturals numbers, all
other sets are required to be constructed out of them via an
autonomous process of arithmetical definitions. A first systematic
attempt at developing mathematics predicatively was made in
Weyl's 1918 monograph *Das Kontinuum* (Weyl 1918).



(b) Theories of higher type functionals comprise Godel's
*T* and Spector's extension of *T* via functionals
defined by bar recursion. The basic idea goes back to
Godel's 1938 lecture at Zilsel's (Godel 1995:
94). It was inspired by Hilbert's 1926 *Uber das
Unendliche*, which considered a hierarchy of functionals over the
natural numbers, not only of finite but also of transfinite type.



(c) To understand Takeuti's finitist standpoint it is important
to pinpoint the place where in a consistency proof a la Gentzen
the means of **PRA** are exceeded. Gentzen's proof
employs a concrete ordering \(\prec\) of type \(\varepsilon\_0\), it
uses an assignment of ordinals to proofs and provides a reduction
procedure on proofs such that any alleged proof of an inconsistency is
reduced to another proof of an inconsistency which gets assigned a
smaller element of the ordering. The ordering, the ordinal assignment
and the reduction procedure are actually primitive recursive and the
steps described so far can be carried out in a small fragment of
**PRA**. The additional principle needed to infer the
consistency of **PA** is the following:


* (\*)There are no
infinite elementary recursive sequences
\(\alpha\_0,\alpha\_1,\alpha\_2,\ldots\) such that \(\alpha\_{n+1}\prec
\alpha\_n\) holds for all *n*.



Takeuti refers to (\*) as the accessibility of \(\prec\). Note that
this is a weaker property than the well-foundedness of \(\prec\) which
refers to arbitrary sequences. There is nothing special about the case
of **PA** since any ordinal analysis of a theory *T*
in the literature can be made to fit this format. Thus
epistemologically (\*) is the fulcrum in any such consistency proof.
Takeuti's central idea (1987, 1975) was that we can carry out
*Gedankenexperimente* (thought experiments) on concretely given
(elementary) sequences to arrive at the insight that (\*)
 obtains.[16]




(d) Errett Bishop's novel (informal) approach to constructive
analysis (1967) made a great on impression on mathematicians with
constructive leanings. In it, he dealt with different kinds of
mathematical objects (numbers, functions, sets) as if they were given
by explicit presentations, each kind being equipped with its own
germane "equality" relation conceived in such a way that
operations on them would lead from representations to representations
respecting the equality relation. An important ingredient that made
Bishop's constructivism workable is the systematic use of
witnessing data as an integral part of what constitutes a mathematical
object. For instance, a real number comes with a modulus of
convergence while a function of real numbers comes equipped with a
modulus of (uniform) convergence. In his *explicit
mathematics*, Feferman (1975, 1979) aims (among other things) at
formalizing the core of Bishop's ontology. Explicit mathematics
is a theory that describes a realm of concretely and explicitly given
objects (a universe *U* of symbols) equipped with an operation
\(\bullet\) of application in such a way that given two objects
\(a,b\in U\), *a* may be viewed as a program which can be run on
input *b* and may produce an output \(a\bullet b\in U\) or never
halt (such structures are known as partial combinatory algebras or
Schonfinkel algebras). Moreover, some of the objects of *U*
represent sets of elements of *U*. The construction of new sets
out of given sets is either done explicitly by elementary
comprehension or by a process of inductive generation. If one also
adds principles to the effect that every internal operation (given as
\(\lambda x.a\bullet x\) for some \(a\in U\)) which is monotone on
sets possesses a least fixed point one arrives at a remarkably strong
theory (cf. Rathjen 1998, 1999b, 2002).



(e) Martin-Lof type theory is an intuitionist theory of dependent
types intended to be a full scale system for formalizing constructive
mathematics. Its origins of can be traced to *Principia
Mathematica*, Hilbert's *Uber das Unendliche*,
the natural deduction systems of Gentzen, taken in conjunction with
Prawitz's reduction procedures, and to Godel's
Dialectica system. It incorporates inductively defined data types
which together with the vehicle of internal reflection via universes
endow it with considerable consistency strength.



(f) Constructive set theory (as do the theories under (d) and (e))
sets out to develop a framework for the style of constructive
mathematics of Bishop's 1967 *Foundations of constructive
analysis* in which he carried out a development of constructive
analysis, based on informal notions of constructive function and set,
which went substantially further mathematically than anything done
before by constructivists. Where Brouwer reveled in differences,
Bishop stressed the commonalities with classical mathematics. What was
novel about his work was that it could be read as a piece of classical
mathematics as well.



The 'manifesto' of constructive set theory was most vividly
expressed by Myhill: 



> 
> 
> ... the argumentation of [Bishop 1967] looks very smooth and
> seems to follow directly from a certain conception of what sets,
> functions, etc. are, and we wish to discover a formalism which
> isolates the principles underlying this conception in the same way
> that Zermelo-Fraenkel set-theory isolates the principles underlying
> classical (nonconstructive) mathematics. We want these principles to
> be such as to make the process of formalization completely trivial, as
> it is in the classical case. (Myhill 1975: 347)
> 
> 
> 



Despite first appearances, there are close connections between the
approaches of (d)-(f). Constructive set theory can be
interpreted in Martin-Lof type theory (due to Aczel 1978) and
explicit mathematics can be interpreted in constructive set theory
(see Rathjen 1993b, in Other Internet Resources). Perhaps the closest
fit between (e) and (f), giving back and forth interpretations, is
provided by Rathjen & Tupailo 2006. Some concrete mathematical
results are found at the end of
 section 5.3.


### 4.2 The Dialectica Interpretation: Godel and Spector

 

Among the proposals for extending finitist methods put forward in his
1938 lecture at Zilsel's, Godel appears to have favored the
route via higher type functions. Details of what came to be known as
the Dialectica interpretation were not published until 1958
(Godel 1958) but the D-interpretation itself was arrived at by
1941. Godel's system \({T}\) axiomatizes a class of
functions that he called the *primitive recursive functionals of
finite type*. \({T}\) is a largely equational theory whose axioms
are equations involving terms for higher type functionals with just a
layer of propositional logic on top of that. In this way the
quantifiers, problematic for finists and irksome to intuitionists, are
avoided. To explain the benefits of the D-interpretation we need to
have a closer look at the syntax of \({T}\).




Definition 4.1 \({T}\) has a many-sorted
language in that each terms is assigned a type. Type (symbols) are
generated from 0 by the rule: If \(\sigma\) and \(\tau\) are types
then so is \(\sigma\to\tau\). Intuitively the ground type 0 is the
type of natural numbers. If \(\sigma\) and \(\tau\) are types that are
already understood then \(\sigma\to\tau\) is a type whose objects are
considered to be functions from objects of type \(\sigma\) to objects
of type \(\tau\). In addition to variables
\(x^{\tau},y^{\tau},z^{\tau},\ldots\) for each type \(\tau\), the
language of \({T}\) has special constants 0, \(\rsuc\),
\(\rK\_{\sigma,\tau}\), \(\rS\_{\rho,\sigma,\tau}\), and
\(\rR\_{\sigma}\) for all types \(\rho,\sigma,\tau\). The meaning of
these constants is explained by their defining equations.
\(\rK\_{\sigma,\tau}\) and \(\rS\_{\rho,\sigma,\tau}\) are familiar from
combinatory logic which was introduced by Schonfinkel in 1924 and
became more widely known through Curry's work (1930). 0 plays the role of the
first natural number while \(\rsuc\) embodies the successor function
on objects of type 0. The constants \(\rR\_{\sigma}\), called
*recursors*, provide the main vehicle for defining functionals
by recursion on \(\bbN\). Term formation starts with constants and
variables, and if *s* and *t* are terms of type
\(\sigma\to\tau\) and \(\sigma\), respectively, then \(s(t)\) is a
term of type \(\tau\). To increase readability we shall write
\(t(r,s)\) instead of \((t(r))(s)\) and \(t(r,s,q)\) instead of
\((t(r,s))(q)\) etc. Also \(\rsuc(t)\) will be shortened to
\(t'\). The defining axioms for the constants are the
 following:[17]


1. \(\neg t'=0\)
2. \(t'=r'\to t=r\)
3. \(\rK\_{\sigma,\tau}(s,t)=s\)
4. \({\rS}\_{\rho,\sigma,\tau}(r,s,t)= (r(t))(s(t))\)
5. \(\rR\_{\sigma}(f,g,0) = f\)
6. \(\rR\_{\sigma}(f,g,n')= g(n,\rR\_{\sigma}(f,g,n)).\)



The axioms of \({T}\) consist of the above defining axioms, equality
axioms and axioms for propositional logic. Inference rules are modus
ponens and the induction rule 

 

\[
\textrm{from } A(0) \textrm{ and } A(x) \to A(x') \textrm{ conclude }A(t)
\]


for *t* of type 0 and *x* not in \(A(0)\).




The first step towards the D-interpretation of Heyting arithmetic in
\({T}\) consists of associating to each formula *A* of arithmetic
a syntactic translation \(A^D\) which is of the form 




\[\tag{7}\label{D-Form} 
A^D \equiv {\exists x^{\sigma\_1}
\ldots
\exists x^{\sigma\_n} \forall y^{\tau\_1}
\ldots 
\forall y^{\tau\_m} A\_D(\vec{x},\vec{y})}
\]



with \(A\_D(\vec{x},\vec{y})\) being quantifier free. Thus \(A^D\) is
not a formula of \({T}\) but of its augmentation via quantifiers
\(\forall x^{\tau}\) and \(\exists y^{\tau}\) for all types \(\tau\).
The translation proceeds by induction on the buildup of *A*. The
cases where the outermost logical symbol of *A* is among
\(\land\), \(\lor\), \(\exists x\), \(\forall x\) are rather
straightforward. The crucial case occurs when *A* is an
implication \(B\to C\). To increase readability we shall suppress the
typing of variables. Let \(B^D\equiv \exists \vec{x}\, \forall
\vec{y}\, B\_D(\vec{x},\vec{y})\) and \(C^D\equiv {\exists \vec{u}\,
\forall \vec{v}\, C\_D(\vec{u},\vec{v})}\). Then one uses a series of
judicious equivalences to bring the quantifiers in \(B^D\to C^D\) to
the front and finally employs skolemization of existential variables
as follows: 

 

\[\begin{align}
\tag{i} \exists \vec{x}\,\forall \vec{y} B\_D(\vec{x},\vec{y})&\to \exists \vec{u}\,\forall \vec{v} C\_D(\vec{u},\vec{v})\\
\tag{ii} \forall \vec{x}[\,\forall \vec{y} B\_D(\vec{x},\vec{y})&\to \exists \vec{u}\,\forall \vec{v} C\_D(\vec{u},\vec{v})]\\
\tag{iii} \forall \vec{x}\,\exists\vec{u}[\,\forall \vec{y} B\_D(\vec{x},\vec{y})&\to \forall \vec{v} C\_D(\vec{u},\vec{v})]\\
\tag{iv} \forall \vec{x}\,\exists\vec{u}\,\forall \vec{v}[\,\forall \vec{y} B\_D(\vec{x},\vec{y})&\to C\_D(\vec{u},\vec{v})]\\
\tag{v} \forall \vec{x}\,\exists\vec{u}\,\forall \vec{v}\,\exists \vec{y}[B\_D(\vec{x},\vec{y})&\to C\_D(\vec{u},\vec{v})]\\
\tag{vi} \forall \vec{x}\,\exists\vec{u}\,\exists Y\,\forall \vec{v}[B\_D(\vec{x},Y(\vec{v}))&\to C\_D(\vec{u},\vec{v})]\\
\tag{vii}\exists U\,\exists Z\,\forall \vec{x}\,\forall \vec{v}[B\_D(\vec{x},Z(\vec{x},\vec{v}))&\to C\_D(U(\vec{x}),\vec{v})].
\end{align}\]


\(A^D\) is then defined to be the formula in (vii). Note, however,
that these equivalences are not necessarily justified constructively.
Only (i) \(\Leftrightarrow\) (ii) and (iii) \(\Leftrightarrow\) (iv)
hold constructively whereas (v) \(\Leftrightarrow\) (vi) and (vi)
\(\Leftrightarrow\) (vii) are justified constructively only if one
also accepts the axiom of choice for all finite types
(AC*ft*). Equivalences (ii) \(\Leftrightarrow\) (iii)
and (iv) \(\Leftrightarrow\) (v) use a certain amount of classical
logic known as the *principle of independence of premise*
(IP*ft*) and *Markov's principle*
(MP*ft*) for all finite types, respectively. At this
point \(A\mapsto A^D\) is just a syntactic translation. But amazingly
it gives rise to a meaningful interpretation of **HA** in
*T*.




Theorem 4.2 (Godel 1958) Suppose
\(\cD\) is a proof of *A* in **HA** and \(A^D\) as
in \((\ref{D-Form})\). Then one can effectively construct a sequence
of terms \(\vec t\) (from \(\cD\)) such that \({T}\) proves \(A\_D(\vec
t,\vec y\,)\).




If one combines the *D*-interpretation with the
Kolmogorov-Gentzen-Godel negative translation of
**PA** into **HA** one also arrives at an
interpretation of **PA** in \({T}\). Some interesting
consequences of the latter are that the consistency of
**PA** follows finitistically from the consistency of
\({T}\) and that every total recursive function of **PA**
is denoted by a term of \({T}\).



The three principles AC*ft*, IP*ft*
and MP*ft* which figured in the *D*-translation
actually characterize the *D*-translation in the sense that over
the quantifier extension of \({T}\) with intuitionistic logic, called
\(\bHA^{\omega}\), they are equivalent to the schema 

 

\[
C\leftrightarrow C^D
\]


for all formulae *C* of that theory. Principles similar to the
three above are also often validated in another type of computational
interpretation of intuitionistic theories known as
*realizability*. Thus it appears that they are intrinsically
related to computational interpretations of such theories.



A further pleasing aspect of Godel's interpretation is that
it can be extended to stronger systems such as higher order systems
and even to set theory (Burr 2000, Diller 2008). Moreover, it sometimes allows one to
extract computational information even from proofs of specific
classical theorems (see, e.g., Kohlenbach 2007). It behaves nicely
with respect to modus ponens and thus works well for ordinary proofs
that are usually structured via a series of lemmata. This is in
contrast to cut elimination which often requires a computationally
costly transformation of proofs.



Spector (1962) extended Godel's functional interpretation,
engineering an interpretation of \(\bZ\_2\) into *T* augmented via
a scheme of transfinite recursion on higher type orderings. This type
of recursion, called *bar recursion*, is conceptually related
to Brouwer's bar induction principle. (For a definition of bar
induction and a presentation of Spector's result see
 appendix C.)


## 5. Beyond Arithmetic: Subsystems of \(\bZ\_2\)

 

We described the system \(\bZ\_2\) of second order arithmetic already
at the end of section 3.2. It was viewed as the
"next"system to be proved consistent--after
first-order arithmetic **PA** had been shown to be. As we
mentioned \(\bZ\_2\) is also called "analysis", because it
allows the development of classical mathematical analysis: coding real
numbers and continuous functions as sets of natural numbers, a good
theory of the continuum can be developed from \(\bZ\_2\)'s
axioms. Indeed, Hermann Weyl showed in 1918 that a considerable
portion of analysis can be developed in small fragments of \(\bZ\_2\)
that are actually conservative over **PA**. The idea of
singling out the minimal fragment of \(\bZ\_2\) required to expose a
particular part of ordinary mathematics led in the 1980s to the
research program of *reverse mathematics*. However, before
discussing that program, we are going to proof-theoretic
investigations of \(\bZ\_2\) and its subsystems that have been a focal
point until the very early 1980s.


### 5.1 Takeuti's Fundamental Conjecture

 

After Gentzen, it was Gaisi Takeuti who worked on a consistency proof
for \(\bZ\_2\) in the late 1940s. He conjectured that Gentzen's
*Hauptsatz* not only holds for first order logic but also for
higher order logic, also known as simple type theory,
**STT**. This came to be known as Takeuti's
fundamental
 conjecture.[18]
 The particular sequent calculus he introduced was called a
generalized logic calculus, GLC (Takeuti 1953). \(\bZ\_2\) can be
viewed as a subtheory of GLC. In the setting of GLC the comprehension
principle **CA** is encapsulated in the right
introduction rule for the existential second-order quantifier and the
left introduction rule for the universal second-order quantifier. In
order to display these rules the following notation is convenient. If
\(F(U)\) and \(A(a)\) are formulae then \(F(\{v\mid A(v)\})\) arises
from \(F(U)\) by replacing all subformulae \(t\in U\) of \(F(U)\)
(with *U* indicated) by \(A(t)\). The rules for second order
quantifiers can then be stated as
 follows:[19]


 

\[\begin{array}{lcclc}
(\forall\_2\,\bL) &
\displaystyle \frac {{ F(\{v\mid A(v)\}) },\Gamma\Rightarrow \Delta}
{\forall X\,{F(X),\Gamma} \Rightarrow \Delta }
& & 
(\forall\_2\,\rR) & 
\displaystyle\frac {\Gamma\Rightarrow {\Delta, F(U)}}
{\Gamma\Rightarrow \Delta, {\forall X\,F(X) }}
 \\[2ex]
(\exists\_2\,\bL) & 
 \displaystyle \frac{F(U),\Gamma\Rightarrow \Delta}
{{ \exists X\,F(X)},\Gamma\Rightarrow \Delta }
 & &
(\exists\_2\,\rR) 
& 
\displaystyle \frac{\Gamma\Rightarrow \Delta,F(\{ v\mid A(v)\})} 
 {\Gamma\Rightarrow \Delta,{\exists X\,F(X) }}
 \end{array}
 \]


To deduce an instance \(\exists X\,\forall x\,[x\in X \leftrightarrow
A(x)]\) of **CA** just let \(F(U)\) be the formula
\(\forall x\,[x\in U \leftrightarrow A(x)]\) and observe that 



\[F(\{v\mid A(v)\})\equiv \forall x\,[A(x)\leftrightarrow A(x)], \]


and hence 

 

\[
 \begin{gather}
\vdots \\ 
\displaystyle \frac{\Gamma\Rightarrow \Delta, \forall x\,[A(x)\leftrightarrow A(x)]}
{\Gamma\Rightarrow \Delta, \exists X\,\forall x\,[x\in X \leftrightarrow A(x)]}
\tag{\(\exists\_2\,\rR\)}
\end{gather}
\]


As the deducibility of the empty sequent is ruled out if cut
elimination holds for GLC (or just the fragment GLC2
corresponding to \(\bZ\_2\)), Takeuti's Fundamental Conjecture
entails the consistency of \(\bZ\_2\). However note that it does not
yield the subformula property as in the first-order case since the
minor formula \(F(\{x\mid A(x)\})\) in \((\exists\_2\,\rR)\) and
\((\forall\_2\,\bL)\) may have a much higher (quantifier) complexity
than the principal formula \(\exists XF(X)\) and \(\forall XF(X)\),
respectively. Indeed, \(\exists XF(X)\) may be a proper subformula of
\(A(x)\) which clearly exhibits the impredicative nature of these
inferences and shows that they are strikingly different from those in
predicative analysis where a proper subformula property obtains.



In 1960a Schutte
developed a semantic equivalent to the (syntactic) fundamental
conjecture using partial or semi-valuations. He employed the method of
search trees (or deduction chains) to show that a formula *F*
that cannot be deduced in the cut-free system has a deduction chain
without axioms which then gives rise to a partial valuation *V*
assigning the value "false" to *F*. From the latter
he inferred that the completeness of the cut-free
 system[20]
 is equivalent to the semantic property that every partial valuation
can be extended to a total valuation (basically a Henkin model of
**STT**). In 1966 Tait succeeded in proving
cut-elimination for second order logic using Schutte's
semantic equivalent for that fragment. Soon afterwards, Takahashi
(1967) and Prawitz (1968) independently proved for full classical
simple type that every partial valuation extends to a total one,
thereby establishing Takeuti's fundamental conjecture. These
results, though, were somewhat disappointing as they were obtained by
highly non-constructive methods that provided no concrete method for
eliminating cuts in a derivation. However, Girard showed in 1971 that
simple type theory not only allows cut-elimination but that there is
also a terminating normalization
 procedure.[21]
 These are clearly very interesting results, but as far as instilling
trust in the consistency of \(\bZ\_2\) or **SST** is
concerned, the cut elimination or termination proofs are just circular
since they blatantly use the very comprehension principles formalized
in these theories (and a bit more). To quote Takeuti: 



> 
> 
> My fundamental conjecture itself has been resolved in a sense by Motoo
> Takahashi and Dag Prawitz independently. However, their proofs rely on
> set theory, and so it cannot be regarded as an execution of
> Hilbert's Program. (Takeuti 2003: 133) 
> 
> 
> 



Takeuti's work on his conjecture instead focused on partial
results. A major breakthrough that galvanized research in proof
theory, especially ordinal-theoretic investigations, was made by him
in 1967. In Takeuti 1967 he gave a consistency proof for
\(\Pi^1\_1\)-comprehension and thereby for the first time obtained an
ordinal analysis of an impredicative theory. For this Takeuti vastly
extended Gentzen's method of assigning ordinals (ordinal
diagrams, to be precise) to purported derivations of the empty
sequent. It is worth quoting Takeuti's own assessment of his
achievements.



> 
> 
> ... the subsystems for which I have been able to prove the
> fundamental conjecture are the system with \(\Pi^1\_1\) comprehension
> axiom and a slightly stronger system, that is, the one with
> \(\Pi^1\_1\) comprehension axiom together with inductive
> definitions.[...] I tried to resolve the fundamental conjecture
> for the system with the \(\Delta^1\_2\) comprehension axiom within our
> extended version of the finite standpoint. Ultimately, our success was
> limited to the system with provably \(\Delta^1\_2\) comprehension
> axiom. This was my last successful result in this area. (Takeuti 2003:
> 133)
> 
> 
> 




The subsystems of \(\bZ\_2\) that are alluded to in the above
discussion are now to be described. We consider the axiom schema of
\(\cC\)-*comprehension* for formula classes \(\cC\) which is
given by 

 

\[
\tag\*{\(\cC\Hy\bCA\)}
\Gamma\Rightarrow \exists X\forall u(u\in X\leftrightarrow{F}(u))
\]


for all formulae \({F}\in\cC\) in which *X* does not occur.
Natural formula classes are the *arithmetical formulae*,
consisting of all formulae without second order quantifiers \(\forall
X\) and \(\exists X\), and the \(\Pi^1\_n\)-*formulae*, where a
\(\Pi^1\_n\)-formula is a formula of the form \(\forall X\_1\ldots Q
X\_n\,A(X\_1,\ldots,X\_n)\) with \(\forall X\_1\ldots Q X\_n\) being a
string of *n* alternating set quantifiers, commencing with a
universal one, followed by an arithmetical formula
\(A(X\_1,\ldots,X\_n)\). Note that in this notation the class of
arithmetical formulae is denoted by \(\Pi^1\_0\).



Also "mixed" forms of comprehension are of interest, e.g.,


 

\[\tag\*{\(\Delta^1\_n{\Hy}\bCA\)}
\Gamma\Rightarrow \forall u\,[F(u)\leftrightarrow G(u)] \to \exists X\,\forall u\,[u\in X \leftrightarrow F(u)]
 \]


where \(F(u)\) is in \(\Pi^1\_n\) and \(G(u)\) in \(\Sigma^1\_n\).



One also considers \(\Delta^1\_n\) comprehension rules: 



\[
\frac{\emptyset \Rightarrow \forall u\,[F(u)\leftrightarrow G(u)]}
{\Gamma\Rightarrow \exists X\,\forall u\,[u\in X \leftrightarrow F(u)]}
\quad \quad\quad 
\begin{split}
\textrm{if } & F(u)\in\Pi^1\_n,\\
& G(u)\in\Sigma^1\_n
\end{split}
\tag\*{\(\Delta^1\_n{\Hy}\bCR\)} 
\]


For each axiom scheme \(\mathbf{Ax}\) we denote by \((\mathbf{Ax})\_0\)
the theory consisting of the basic arithmetical axioms plus the scheme
\(\mathbf{Ax}\). By contrast, \((\mathbf{Ax})\) stands for the theory
\((\mathbf{Ax})\_0\) augmented by the scheme of induction for all
\(\cL\_2\)-formulae. An example for these notations is the theory
\((\bPi^1\_1-\bCA)\_0\) which has the comprehension schema for
\(\bPi^1\_1\)-formulae.



In **PA** one can define an elementary injective pairing
function on numbers, e.g., \((n,m)\coloneqq 2^n\times3^m\). With the
help of this function an infinite sequence of sets of natural numbers
can be coded as a single set of natural numbers. The \(n^{th}\)
section of set of natural numbers *U* is defined by
\(U\_n\,\coloneqq \,\{m:\,(n,m)\in U\}\). Using this coding, we can
formulate a form of the axiom of choice for formulae \({F}\) in
\(\cC\) by 

 

\[\tag\*{\(\cC{\Hy}\bAC\)}
\Gamma\Rightarrow \forall x\exists Y{F}(x,Y)\rightarrow\exists Y\forall x{F}(x,Y\_x).
\]


The basic relations between the above theories are discussed in
Feferman and Sieg 1981a.


### 5.2 Predicative Theories

 

A major stumbling block for proving Takeuti's fundamental
conjecture is that in \((\forall\_2\bL)\) and \((\exists\_2\rR)\)
inferences the minor formula \(F(\{v\mid A(v)\})\) can have a much
higher complexity than the principal (inferred) formula \(QX\,F(X)\).
If, instead, one allowed these inferences only in cases where the
'abstraction' term \(\{v\mid A(v)\}\) had (in some sense) a
lower complexity than \(QX\,F(X)\), cut elimination could be restored.
To implement this idea, one introduces a hierarchy of sets (formally
represented by abstraction terms) whose complexity is stratified by
ordinal levels \(\alpha\), and a pertaining hierarchy of quantifiers
\(\forall X^{\beta}\) and \(\exists X^{\beta}\) conceived to range
over sets of levels \(<\beta\). This is the basic idea underlying
the ramified analytic hierarchy. The problem of which ordinals could
be used for the transfinite iteration led to the concept of
*autonomous progressions of theories*. The general idea of
progressions of theories is very natural and we shall consider it
first before discussing the autonomous versions.


#### 5.2.1 Progressions of theories: Completing the incomplete

 

As observed earlier, Hilbert attempted to overcome the incompleteness
of first-order arithmetic by introducing as axioms
\(\Pi^0\_1\)-statements all of whose instances had been finitistically
proved (Hilbert 1931a). In a way he modified the concept of a
"formal" theory by invoking finitist provability. Bernays,
in his letter to Godel of January 18, 1931 (Godel 2003:
86-88), proposed a *rule* of a more general form. He
indicated also that it would allow the elimination of the induction
principle--in exchange for dealing with infinite proofs.



These considerations among others raised the issue of what constitutes
a properly *formal* theory. Godel paid very special
attention to it when giving his Princeton Lectures in 1934. At the
very end he introduced the general recursive functions. This class of
number theoretic functions was shown to be co-extensional with
Church's l-definable ones by Church and Kleene. In
Church 1936 an "identification"
of effective
calculability and general recursiveness was proposed, what is usually
called *Church's thesis*. Turing, of course, proposed his
machine computability for a very similar purpose and proved its
equivalence to l-definability in an appendix to his
1936. Church
and Turing used their respective notion to establish the
undecidability of first-order logic. For Godel, this was the
background for formulating the incompleteness theorems in "full
generality" for all formal theories (containing a modicum of
number or set theory); see the Postscriptum
to the Princeton Lectures Godel wrote in 1964:



> 
> 
> In consequence of later advances, in particular of the fact that, due
> to A.M. Turing's work, a precise and unquestionably adequate
> definition of the general concept of formal system can now be given,
> the existence of undecidable arithmetical propositions and the
> non-demonstrability of the consistency of a system in the same system
> can now be proved rigorously for *every* consistent formal
> system containing a certain amount of finitary number theory.
> (Godel 1986: 369).
> 
> 
> 



The first incompleteness is proved for any such theory **T**, by
explicitly producing an unprovable yet true statement \(G\_\bT\). That
formula can then be added to **T** making \(\bT+G\_\bT\) a
"less incomplete" theory. Von Neumann had already
established the equivalence of \(G\_\bT\) with the consistency
statement for **T**, \(\Con (\bT)\); the latter expresses that
there is no proof in *T* of a blatantly false statement such as
\(0=1\). This gives then rise to an extension procedure leading from
**T** to \(\bT'\), namely (R1) \(\bT'=\bT+G\_\bT\).



Thus one might try to address the incompleteness of **T** by
forming a sequence of theories \(\bT=\bT\_0\subset
\bT\_1\subset\bT\_2\subset\ldots\) where \(\bT\_{i+1}=\bT\_i'\) and to
continue this into the transfinite. The latter can be achieved by
letting \(\bT\_{\lambda}=\bigcup\_{\alpha<\lambda}\bT\_{\alpha}\) for
limit ordinals l and \(\bT\_{\alpha+1}=\bT\_{\alpha}'\)
for successor ordinals \(\alpha+1\). However, the consistency
statement for \(\bT\_{\lambda}\), thus the provability predicate for
the theory, has to be expressed in the language of \(\bT\_{\lambda}\),
and one cannot simply use set theoretic ordinals. Furthermore, the
extensions of **T** are all supposed to be formal theories, i.e.,
the axioms have to be enumerable by recursive functions. To deal with
both issues at once, one has to deal with ordinals in an effective
way.



That is what Turing did in his Princeton dissertation (1939)
concerning, what he called, *ordinal logics*. There he
considers two ways of achieving the effective representation of
ordinals. The first way is via the set \(\rW\) of numbers *e* for
recursive well-orderings \(\leq\_e\), the second is provided by the
class of Church-Kleene notations for ordinals (Church and Kleene
1936) that used expressions in the l-calculus to describe
ordinals. The latter approach was then modified in Kleene 1938 to an
equivalent recursion-theoretic definition that uses numerical codes to
denote countable ordinals and is known as Kleene's
\({\cO}\).




Definition 5.1 A *computable* or
*recursive function* on the naturals is one that can be
computed by a Turing machine. The program of a Turing machine *M*
can be assigned a Godel number \({\Corner{M}}\). For natural
numbers \(e,n\), to convey that the Turing machine with Godel
number *e* computes a number *m* on input *n*, we use
the notation \(\{e\}(n)\) for *m*.



Kleene uses \({\rsuc}(a)\coloneqq 2^a\) as notations for successor
ordinals and and \({\rlim}(e)\coloneqq 3\cdot 5^e\) for limit
ordinals.



The class \({\cO}\) of ordinal notations, the partial ordering
relation \(\relLTcO\) between such notations, and the ordinal
\({\mid}{a}{\mid}\) denoted by \(a\in {\cO}\) are defined
simultaneously as follows:


1. \(0\in{\cO}\), and \({\mid}{0}{\mid} =0\).
2. If \(a\in{\cO}\) then \({\rsuc}(a)\in{\cO}\), \(a \relLTcO
{\rsuc}(a)\) and \({\lvert {\rsuc}(a)\rvert}={\lvert a\rvert}+1\).
3. If *e* is an index of a total recursive function and
\({\{e\}(n)} \relLTcO{\{e\}(n+1)}\) holds for all \(n\in{\bbN}\), then
\({\rlim}(e)\in{\cO}\), and \({\lvert {\rlim}(e)\rvert}=\sup\{{\lvert {\{e\}(n)}\rvert}\mid
n\in{\bbN}\}\).
4. If \(a \relLTcO b\) and \(b \relLTcO c\) then \(a \relLTcO
c\).




The first ordinal \(\tau\) such that there is no recursive
well-ordering of order type \(\tau\) is usually denoted by
\(\omega^{CK}\) in honor of Church and Kleene. It can be shown for the
above definition of \({\cO}\) that the recursive ordinals are exactly
those that have a notation in \({\cO}\).



When it comes to theories **T**, quite unlike to other areas of
logic (e.g., model theory), results as those presented in this section
depend not only on the set of axioms of **T**, but also on the way
they are presented. When talking about a theory **T** we assume
that **T** is given by a \(\Sigma^0\_1\)-formula \(\psi(v\_0)\) such
that *F* is an axiom of **T** just in case
\(\psi({\Corner{F}})\) holds; a \(\Sigma^0\_1\)-formula is of the form
\(\exists y\_1\ldots\exists y\_n\,R(y\_1,\ldots y\_n)\) with *R*
primitive recursive. This consideration together with Kleene's
\({\cO}\) allows us to build a transfinite hierarchy of theories based
on any suitable theory **T**. A *consistency progression*
based on **T** is a primitive recursive function \(n\mapsto
\psi\_n\) that associates with every natural number *n* a
\(\Sigma^0\_1\)-formula \(\psi\_n(v\_0)\) that defines \(\bT\_n\) such
that **PA** proves: (i) \(\bT\_0=\bT\); (ii)
\(\bT\_{{\rsuc}(n)}=\bT\_n'\), and (iii)
\(\bT\_{{\rlim}(n)}=\bigcup\_x\bT\_{\{n\}(x)}\). So, finally we can
formulate Turing's completeness result.




Theorem 5.2 For any true \(\Pi^0\_1\)
sentence *F* a number \(a\_{F}\in{\cO}\) can be constructed such
that \({{\mid}\,{a\_{F}}\,{\mid}}=\omega+1\) and \(\bT\_{a\_{F}}\vdash
F\). Moreover, the function \(F\mapsto a\_{F}\) is given by a primitive
recursive function.




At first glance Turing's theorem seems to provide some insight
into the nature of true \(\Pi^0\_1\)-statements. That this is an
"illusion" is revealed by the analysis of its simple proof
which is just based on the trick of coding the truth of *F* as a
member of \({\cO}\). The proof also shows that the infinitely many
iterated consistency axioms \(\Con (\bT\_0),\Con (\bT\_1),\ldots\) of
\(\bT\_{{{\rsuc}}({\rlim}(e))}\) are irrelevant for proving *F*.
As it turns out, the reason why one has to go to stage \(\omega+1\) is
simply that only at stage \(\omega\) a non-standard definition of the
axioms of \(\bigcup\_{n<\omega}\bT\_n\) can be introduced. More
details and other results on recursive progressions are discussed in
 Appendix B.
 Here let us just mention that one has considered other progressions
based on various extension procedures \(\bT \mapsto \bT'\) that
strengthen a given theory,
 notably:[22]


* (R2)\(\bT'=
\bT+\{\exists y\,\proof\_\bT(y,{\Corner{F}})\to F\mid F\)
closed\(\}\).
* (R3)\(\bT'=
\bT+\{\forall x\,\exists y\, \proof\_\bT(y,{\Corner{F(\bar{x})}})\to
\forall x F(x)\mid \textrm{ all } F(x)\) with at most *x*
free\(\}\).



(R2) is called an extension by the *local reflection
principle*, whereas (R3) uses the *uniform reflection
principle*. Feferman obtained in 1962 an amazing result that
strengthens Turing's result in a dramatic way.



Let \((\bT\_a)\_{a\in{\cO}}\) be a progression using the uniform
reflection principle with **PA** as the base theory
**T**. Then we have: for any true arithmetical sentence *F*
there is an \(a\in{\cO}\), such that \(\bT\_a\vdash F\). Moreover,
\(a\in{\cO}\) can be chosen such that \({{\mid}\,{a}\,{\mid}}\leq
\omega^{\omega^{\omega+1}}\).



For further discussion see
 Appendix B.
 Here we just note that the union of the \(\bT\_a\) is no longer a
formal theory.



In the foregoing progressions the ordinals remained external to the
theory. *Autonomous progressions of theories* are the proper
internalization of the general concept of progressions. In the
autonomous case one is allowed to ascend to a theory \(\bT\_a\) only if
one already has shown in a previously accepted theory \(\bT\_b\) that
\(a\in{\cO}\). This idea of generating a hierarchy of theories via a
boot-strapping process appeared for the first time in Kreisel 1960,
where it was proposed as a
way of characterizing finitism and predicativism in mathematically
precise way. In more formal terms, the starting point is a theory
\(\bT\_0\) which is accepted as correct and an extension procedure
\(\bT\mapsto\bT'\) which is viewed as leading from a correct
theory **T** to a more encompassing correct theory \(\bT'\).
Moreover, the language of these theories is supposed to contain a
formula \(\rAcc(x)\) such that provability of \(\rAcc(\bar{a})\) in a
correct theory entails that
 \(a\in{\cO}\).[23]
 Kreisel singled out two autonomous progressions of theories
\(\{{{\bF}}\_a\}\) and \(\{{{\bR}}\_a\}\) for finitism and
predicativity, respectively, and determined the least upper bound of
the \(\lvert a\rvert\) appearing in the first hierarchy to be the ordinal
\(\varepsilon\_0\) which is also the proof-theoretic ordinal of
**PA**. The determination of the least upper bound for
the predicative hierarchy \(\{{{\bR}}\_a\}\) was achieved independently
by Feferman (1964) and Schutte (1964, 1965). It turned out that
this ordinal can be expressed in a notation system developed by Veblen
that will be presented next.


#### 5.2.2 Stronger ordinal representations: The Veblen and Bachmann hierarchies

 

As we saw above, ordinals below \(\varepsilon\_0\) suffice for the
proof-theoretic treatment of **PA**. For stronger
theories segments larger than \(\varepsilon\_0\) have to be employed,
requiring new normal forms akin to Cantor's normal form. Ordinal
representation systems utilized by proof theorists in the 1960s first
emerged in a purely set-theoretic context more than 50 years earlier.
In 1904 Hardy wanted to "construct" a subset of \(\bbR\)
of size \(\aleph\_{1}\), the first uncountable cardinal. His method was
to represent countable ordinals via increasing sequences of natural
numbers and then to correlate a decimal expansion with each such
sequence. Hardy used two processes on sequences: (i) Removing the
first element to represent the successor; (ii) Diagonalizing at
limits. For example, if the sequence \(1,2,3,\ldots\) represents the
ordinal 1, then \(2,3,4,\ldots\) represents the ordinal 2 and
\(3,4,5,\ldots\) represents the ordinal 3 etc., while the
'diagonal' \(1,3,5,\ldots\) provides a representation of
\(\omega\). In general, if \(\lambda=\lim\_{n\in\bbN}\lambda\_n\) is a
limit ordinal with \(b\_{n1},b\_{n2},b\_{n3},\ldots\) representing
\(\lambda\_n<\lambda\), then \(b\_{11},b\_{22},b\_{33},\ldots\)
represents l. This representation, however, depends on the
sequence chosen with limit l. A sequence
\((\lambda\_n)\_{n\in\bbN}\) with \(\lambda\_n<\lambda\) and
\(\lim\_{n\in \bN}\lambda\_n=\lambda\) is called a *fundamental
sequence* for l. Hardy's two operations give
explicit representations for all ordinals \(<\omega^2\).



Veblen in 1908 extended the initial segment of the countable for which
fundamental sequences can be given effectively. The new tools he
devised were the operations of *derivation* and *transfinite
iteration* applied to *continuous increasing functions* on
ordinals.




Definition 5.4 Let \({\ON}\) be the class of
ordinals. A (class) function \(f:{\ON}\to{\ON}\) is said to be
*increasing* if \(\alpha<\beta\) implies
\(f(\alpha)<f(\beta)\) and *continuous* (in the order
topology on \({\ON}\)) if

 

\[
f(\lim\_{\xi<\lambda}\alpha\_{\xi})=\lim\_{\xi<\lambda}f(\alpha\_{\xi})
\]


holds for every limit ordinal l and increasing sequence
\((\alpha\_{\xi})\_{\xi<\lambda}\). *f* is called
*normal* if it is increasing and continuous.




The function \(\beta\mapsto \omega+\beta\) is normal while
\(\beta\mapsto \beta+\omega\) is not continuous at \(\omega\) since
\(\lim\_{\xi<\omega}(\xi+\omega)=\omega\) but
\((\lim\_{\xi<\omega}\xi)+\omega=\omega+\omega\).




Definition 5.5 The *derivative*
\(f'\) of a function \(f:{\ON}\rightarrow {\ON}\) is the function
which enumerates in increasing order the solutions of the equation
\(f( \alpha )= \alpha\), also called the *fixed points* of
*f*. 




If *f* is a normal function, \(\{\alpha:\,f(\alpha)=\alpha\}\) is
a proper class and \(f'\) will be a normal function, too.




Definition 5.6 Now, given a normal function
\(f:\ON \rightarrow \ON\), define a hierarchy of normal functions as
follows: 

  

\[\begin{align}
f\_{0}&=f \\
 f\_{\alpha +1}& =f\_{\alpha}'\\
f\_{\lambda}(\xi) &= \xi^{\textrm{th}} \textrm{ element of } \bigcap\_{\alpha<\lambda} \left(\textrm{Range of }
 f\_{\alpha}\right) \quad\mbox{ for }\lambda \textrm{ a limit ordinal}.
 \end{align}\]



In this way, from the normal function *f* we get a two-place
function, \(\varphi\_{f} ( \alpha , \beta )\coloneqq f\_{\alpha} ( \beta
)\). One usually discusses the hierarchy when \(f=\ell\), where
\(\ell( \alpha )=\omega^{\alpha}\). The least ordinal \(\gamma>0\)
closed under \(\varphi\_{\ell}\), i.e., the least ordinal \(>0\)
satisfying
\((\forall\alpha,\beta<\gamma)\;\varphi\_{\ell}(\alpha,\beta)<\gamma\)
is called \(\Gamma\_0\). It has a somewhat iconic status, in particular
since Feferman and Schutte determined it to be the least ordinal
'unreachable' by certain *predicative* means expressed
in terms of autonomous progressions of theories (defined in
 section 5.2).



Veblen extended this idea first to arbitrary finite numbers of
arguments, but then also to transfinite numbers of arguments, with the
proviso that in, for example \(\Phi\_{f} ( \alpha\_{0} , \alpha\_{1} ,
\ldots , \alpha\_{\eta} )\), only a finite number of the arguments
\(\alpha\_{\nu}\) may be non-zero. Finally, Veblen singled out the
ordinal \(E(0)\), where \(E(0)\) is the least ordinal \(\delta >
0\) which cannot be named in terms of functions \(\Phi\_{\ell} (
\alpha\_{0} , \alpha\_{1} , \ldots , \alpha\_{\eta} )\) with \(\eta <
\delta\), and each \(\alpha\_{ \gamma } < \delta\).



Though the "great Veblen number" (as \(E(0)\) is sometimes
called) is quite an impressive ordinal it does not furnish an ordinal
representation sufficient for the task of analyzing a theory as strong
as \(\Pi^1\_1\)-comprehension. Of course, it is possible to go beyond
\(E(0)\) and initiate a new hierarchy based on the function
\(\xi\mapsto E(\xi)\) or even consider hierarchies utilizing finite
type functionals over the ordinals. Still all these further steps
amount to rather modest progress over Veblen's methods. In 1950
Bachmann presented a new kind of operation on ordinals which dwarfs
all hierarchies obtained by iterating Veblen's methods. Bachmann
builds on Veblen's work but his novel idea was the systematic
use of *uncountable ordinals* to keep track of the functions
defined by diagonalization. Let \({\Omega}\) be the first uncountable
ordinal. Bachmann defines a set of ordinals \(\fB\) closed under
successor such that with each limit \(\lambda\in \fB\) is associated
an increasing sequence \(\langle
\lambda[\xi]:\,\xi<\tau\_{\lambda}\rangle\) of ordinals \(
\lambda[\xi] \in \fB\) of length \(\tau\_{\lambda}\leq\Omega\) and
\(\lim\_{\xi<\tau\_{\lambda}}\lambda[\xi]=\lambda\). A hierarchy of
functions \((\varphi^{\ssfB}\_{\alpha})\_{\alpha \in \fB}\) is then
obtained as follows:

 

\[\tag{8}\label{bachmann} \begin{align}
 {\varphi^{\ssfB}\_0 (\beta)} = \omega^{\beta} \quad
&
 {\varphi^{\ssfB}\_{\alpha+1}} = {\left(\varphi^{\ssfB}\_{\alpha}\right)'}
\\
 \varphi^{\ssfB}\_{\lambda} \textrm{ enumerates }
& \bigcap\_{\xi<\tau\_{\lambda}}(\mbox{Range of }\varphi^{\ssfB}\_{\lambda[\xi]})
&\kern-12pt \textrm{if } \lambda \textrm{ is a limit with } \tau\_{\lambda}<{\Omega} 
\\ 
 \varphi^{\ssfB}\_{\lambda}\textrm{ enumerates } 
& \{\beta< {\Omega} : \varphi^{\ssfB}\_{\lambda[\beta]}(0)=\beta\}
&\kern-10pt \textrm{if }\lambda \textrm{ is a limit with } \tau\_{\lambda}={\Omega}.
 \end{align}\]


After the work of Bachmann, the story of ordinal representations
becomes very complicated. Significant papers (by Isles, Bridge,
Pfeiffer, Schutte, Gerber to mention a few) involve quite
horrendous computations to keep track of the fundamental sequences.
Also Bachmann's approach was combined with uses of higher type
functionals by Aczel and Weyhrauch. Feferman proposed an entirely
different method for generating a Bachmann-type hierarchy of normal
functions which does not involve fundamental sequences. Buchholz
further simplified the systems and proved their computability. For
details we recommend the preface to Buchholz et al. 1981.


#### 5.2.3 Infinitary proofs for predicative theories

 

The ordinal that Feferman and Schutte determined as the least
upper bound for \(\{{{\bR}}\_a\}\) is \(\Gamma\_0\), the least non-zero
ordinal closed under the Veblen function
\(\alpha,\beta\mapsto\varphi\_{\alpha}(\beta)\). This was a genuine
proof-theoretic result with the tools coming ready-made from
Schutte's (1960b) monograph. There he had calculated the
proof-theoretic ordinals of the \({{\bR}}\_a\) as a function of
\(\lvert a\rvert\), using cut elimination techniques for logics with infinitary
rules (dubbed "semi-formal systems"). If
\(\lvert a\rvert =\omega^{\alpha}\) then \(\lvert {{\bR}}\_a\rvert =\varphi\_{\alpha}(0)\).
"Semi-formal" is a terminology employed by Schutte
and refers to the fact that this proof system has rules with
infinitely many premises, similar to the \(\omega\)-rule.




Definition 5.7 In the following we assume
that the ordinals come from some representation system. The language
of \(\bRA^\*\) is an extension of that of first order arithmetic. For
each ordinal \(\alpha\) and \(\beta>0\) it has free set variables
\(U\_0^\alpha,U^\alpha\_1,U^\alpha\_2\ldots\) of level \(\alpha\) and
bound set variables of level \(\beta\). The level,
\({\textrm{lev}(A)}\), of a formula *A* of \(\bRA^\*\) is defined
to be the maximum of the levels of set variables that occur in
*A*. Expressions of the form \(\{x\mid A(x)\}\) with \(A(u)\) a
formula will be called *abstraction terms*, their level being
the same as that of the formula \(A(u)\).



The inference rules of \(\bRA^\*\) comprise those of the sequent
calculus with the exception of \((\forall R)\) and \((\exists L)\)
which are replaced by those for the \(\omega\)-rule: \(\omega\)R and
\(\omega\)L. Below \(\fP\_{\beta}\) stands for the set of all
abstraction terms with levels \(<\beta\). The rules for the set
quantifiers are as follows: 

 

\[
\tag\*{\({\forall\_\beta\,\bL}\)}
\frac{F(P),\Gamma\Rightarrow \Delta,}
{\forall X^\beta\,F(X^\beta),\Gamma\Rightarrow \Delta}
\]\[

\tag\*{\({\forall\_\beta}\,\rR\)} \frac{\Gamma\Rightarrow \Delta, F(P)\
\textrm{ all } P\in{\fP}\_{\beta}} {\Gamma\Rightarrow \Delta, \forall
X^\beta\,F(X^\beta)} 

\]\[

 \tag\*{\({\exists\_\beta}\,\bL\)}
\frac{F(P),\Gamma\Rightarrow \Delta\ \textrm{ all } P\in{\fP}\_{\beta}}
{\exists X^\beta\,F(X^\beta),\Gamma\Rightarrow \Delta} 

\]\[

\tag\*{\({\exists\_\beta}\,\rR\)} \frac{\Gamma\Rightarrow \Delta,F(P)}
{\Gamma\Rightarrow \Delta, \exists X^{\beta} F(X^{\beta})} \]


where in \(\forall\_\beta\bL\) and \(\exists\_\beta\rR\), *P* is an
abstraction term of level \(<\beta\).




As per usual, the price one has to pay for rules with infinitely many
premises is that derivations become infinite (well-founded) trees. The
length of a derivation can then be measured by the ordinal rank
associated with the tree. One also wants to keep track of the
complexity of cuts in the derivation. The length we assign to a
formula *A*, \(\lvert A\rvert\), measures its complexity. It is an ordinal
of the form \(\omega\cdot \alpha+n\) where \(\alpha\) is the level of
*A* and \(n<\omega\). One then defines a notion of
derivability in \({{\bRA}}\), 

 

\[
\bRA^\*
\stile{\alpha}{\rho} \Gamma\Rightarrow \Delta
\]


where \(\alpha\) majorizes the transfinite length of the derivation
and \(\rho\) conveys that all cut formulae in the derivation have
length \(<\rho\).



Cut elimination works smoothly for \(\bRA^\*\), however, the prize one
has to pay can only be measured in terms of Veblen's \(\varphi\)
function. The optimal result is the so-called second cut elimination
theorem.




Theorem 5.8 (Second Cut Elimination Theorem)


 

\[
 \textrm{If } \bRA^\* \stile{\alpha}{\rho+\omega^\nu} \Gamma\Rightarrow \Delta \textrm{ then } \bRA^\*
 \stile{\varphi\_{\nu}(\alpha)}{\rho} \Gamma\Rightarrow \Delta
 \]



It entails of course the special case that \(\bRA^\*
\stile{\alpha}{\omega^\nu} \Gamma\Rightarrow \Delta\) yields \(\bRA^\*
\stile{\varphi\_{\nu}(\alpha)}{0} \Gamma\Rightarrow \Delta\), and thus,
as the latter deduction is cut-free, all cuts can be removed. Several
subtheories of \(\bZ\_2\) can be interpreted in \(\bRA^\*\), yielding
upper bounds for their proof-theoretic ordinals via
 Theorem 5.8.
 Here is a selection of such
 results:[24]





Theorem 5.9


1. \(\lvert (\Pi^1\_0{\Hy}\bCA)\_0\rvert =\varepsilon\_0\).
2. \(\lvert (\Pi^1\_0{\Hy}\bCA)\rvert =
\varphi\_2(0)=\varepsilon\_{\varepsilon\_0}\).
3. \(\lvert (\Delta^1\_1{\Hy}\bCR)\rvert = {\varphi}\_{\omega}(0)\).
4. \(\lvert (\Delta^1\_1{\Hy}\bCA)\rvert = \lvert (\Sigma^1\_1{\Hy}\bAC)\rvert =
{\varphi}\_{\varepsilon\_0}(0)\).




For the definitions of the theories in this theorem, see end of
 section 5.1.
 To obtain the results about theories in (iii) and (iv) it is somewhat
easier to first reduce them to systems of the form
\((\Pi^0\_1{\Hy}\bCA)\_{<\rho}\) as the latter have a straightforward
interpretation in \({{\bRA}}^\*\). Reductions of
\((\Delta^1\_1{\Hy}\bCR)\) to
\((\Pi^0\_1{\Hy}\bCA)\_{<\omega^{\omega}}\) and of
\((\Sigma^1\_1{\Hy}\bAC)\) to
\((\Pi^0\_1{\Hy}\bCA)\_{<\varepsilon\_0}\) are due to Feferman (1964)
and Friedman (1970),
 respectively.[25]




The investigation of such subsystems of analysis and the determined
effort to establish their mathematical power led to a research program
that was initiated by Friedman and Simpson some thirty years ago and
dubbed *Reverse Mathematics*. The objective of the program is
to investigate the role of set existence principles in ordinary
 mathematics.[26]
 The main question can be stated as follows:




Given a specific theorem \(\tau\) of ordinary mathematics, which set
existence axioms are needed in order to prove \(\tau\)?




Central to the above is the reference to what is called 'ordinary
mathematics'. This concept, of course, doesn't have a
precise definition. Roughly speaking, by ordinary mathematics we mean
main-stream, non-set-theoretic mathematics, i.e., the core areas of
mathematics which make no essential use of the concepts and methods of
set theory and do not essentially depend on the theory of uncountable
cardinal numbers.



For many mathematical theorems \(\tau\), there is a weakest natural
subsystem \({\bS}(\tau)\) of \(\bZ\_2\) such that \({\bS}(\tau)\)
proves \(\tau\). Very often, if a theorem of ordinary mathematics is
proved from the weakest possible set existence axioms, the statement
of that theorem will turn out to be provably equivalent to those
axioms over a still weaker base theory. Moreover, it has turned out
that \({\bS}(\tau)\) often belongs to a small list of specific
subsystems of \(\bZ\_2\) dubbed \(\RCA\_0\), \(\WKL\_0\), \(\ACA\_0\),
\(\ATR\_0\) and \(({\bPi}^1\_1{\Hy}{\bCA})\_0\),
 respectively.[27]
 The systems are enumerated in increasing strength. \(\ACA\_0\) is
actually the same theory as \((\Pi^1\_0{\Hy}\bCA)\_0\). The main set
existence axioms of \(\RCA\_0\), \(\WKL\_0\), \(\ACA\_0\), \(\ATR\_0\),
and \(({{\bPi}}^1\_1{\Hy}{\bCA})\_0\) are recursive comprehension, weak
Konig's lemma, arithmetical comprehension, arithmetical
transfinite recursion, and \(\bPi\_1^1\)-comprehension, respectively.
\(\ACA\_0\) is actually the same theory as \((\Pi^1\_0{\Hy}\bCA)\_0\).
For exact definitions of all these systems and their role in reverse
mathematics see Simpson 1999. Examples of mathematical statements
provable in \(\RCA\_0\) are the intermediate value theorem and the
Baire category theorem. Reversals for \(\WKL\_0\) are the Heine/Borel
covering lemma and the local existence theorem for solutions of
ordinary differential equations. Among the many reversals for
\(\ACA\_0\), \(\ATR\_0\), and \((\bPi^1\_1{\Hy}{\bCA})\_0\) one finds the
existence of maximal ideals in countable rings, Ulm's theorem,
and the Cantor-Bendixson theorem, respectively.



The proof-theoretic strength of \(\RCA\_0\) is weaker than that of
**PA** while \(\ACA\_0\) has the same strength as
**PA**. To get a sense of scale, the strengths of the
first four theories are best expressed via their proof-theoretic
ordinals:




Theorem 5.10


1. \(\lvert \RCA\_0\rvert =\lvert \WKL\_0\rvert =\omega^{\omega}\).
2. \(\lvert \ACA\_0\rvert =\varepsilon\_0\).
3. \(\lvert \ATR\_0\rvert =\Gamma\_0\).




\(\lvert (\bPi^1\_1\Hy\bCA)\_0\rvert\), however, eludes expression in the ordinal
representations introduced so far. This will require the much stronger
representation to be introduced in
 Definition 5.11.



There are important precursors of reverse mathematics. Weyl (1918)
started to develop analysis using a minimalist foundation (that
equates to \(\ACA\_0\)) whilst Hilbert and Bernays (1939) developed
analysis in second order arithmetic, whereby on closer inspection one
sees that all they used is \((\bPi^1\_1\Hy\bCA)\_0\). The first theorem
of genuinely reverse mathematics was established by Dedekind in his
essay *Stetigkeit und irrationale Zahlen* (1872). It states
that his continuity (or completeness) principle is equivalent to a
well-known theorem of analysis, namely, every bounded, monotonically
increasing sequence has a limit. He emphasizes, 



> 
> 
> This theorem is equivalent to the principle of continuity, i.e., it
> loses its validity as soon as we assume a single real number not to be
> contained in the domain \(\cR\) [of all real numbers, i.e., of all
> cuts of rational numbers]. (1872 [1996: 778]) 
> 
> 
> 



It is to bring out "the connection between the principle of
continuity and infinitesimal analysis" (1872 [1996: 779]).


### 5.3 Impredicative Subsystems and Generalized Inductive Definitions

 

Spector's (1962) functional interpretation of \(\bZ\_2\) via bar
recursive functionals was of great interest to proof theory. However,
it was not clear whether there was a constructive foundation of these
functionals along the lines of hereditarily continuous functionals
that can be represented by computable functions (akin to Kleene 1959;
Kreisel 1959) which would make them acceptable on intuitionistic
grounds. In 1963 Kreisel conducted a seminar the expressed aim of
which was to assay the constructivity of Spector's
interpretation (see Kreisel 1963). Specifically he asked whether an
intuitionistic theory of monotonic inductive definitions,
\(\bID^i\_1(\text{mon})\), could model bar recursion, or even more
specifically, formally capture a class of indices of representing
functions of these functionals. In a subsequent report the
seminar's conclusion was later summarized by Kreisel:



> 
> 
> ... the answer is negative by a wide margin, since not even bar
> recursion of type 2 can be proved consistent [from intuitionistically
> accepted principles]. (Kreisel in "Reports of the Seminar on the Foundations of Analysis,
> Stanford, Summer 1963", as quoted in Feferman 1998: 223)
> 
> 
> 
> 



He not only introduced theories of one inductive definition but also
of \(\nu\)-times transfinitely iterated inductive definitions,
\(\bID\_{\nu}\). Albeit it soon became clear that even the theories
\(\bID\_{\nu}\) couldn't reach the strength of \(\bZ\_2\) (in
point of fact, such theories are much weaker than the fragment of
\(\bZ\_2\) based on \(\Pi^1\_2\)-comprehension); they became the subject
of proof-theoretic investigation in their own right and occupied the
attention of proof theorists for at least another 15 years. One reason
for this interest was surely that the intuitionistic versions
corresponding to the accessible (i.e., well-founded) part of a
primitive recursive ordering are immediately constructively appealing
and a further reason was that they were thought to be more amenable to
direct proof-theoretic treatments than fragments of \(\bZ\_2\) or set
theories.



We shall not give a detailed account of the formalization of these
theories, but focus on the non-iterated case \(\bID\_1\) and its
intuitionistic version \(\bID\_1^i\) to convey the idea. A monotone
operator on \(\bbN\) is a map \(\Gamma\) that sends a set \(X\subseteq
\bbN\) to a subset \(\Gamma(X)\) of \(\bbN\) and is monotone, i.e.,
\(X\subseteq Y\subseteq \bbN\) implies \(\Gamma(X) \subseteq
\Gamma(Y)\). Owing to monotonicity, the operator \(\Gamma\)
will have a least fixed point \(I\_{\Gamma}\subseteq\bbN\), i.e.,
\(\Gamma( I\_{\Gamma})=I\_{\Gamma}\) and for every other fixed point
*X* it holds \(I\_{\Gamma} \subseteq X\).
Set-theoretically \(I\_{\Gamma}\) is obtained by iterating \(\Gamma\)
through the ordinals, 

 

\[
\begin{align}
\Gamma^0&=\emptyset,\\
\Gamma^1&=\Gamma(\Gamma^0),\\
\Gamma^{\alpha}&=\Gamma\left(\bigcup\_{\xi<\alpha}\Gamma^{\xi}\right).
\end{align}
\]


Monotonicity ensures (in set theory) that one finds an ordinal
\(\tau\) such that \(\Gamma(\Gamma^{\tau})=\Gamma^{\tau}\), and the
set \(\Gamma^{\tau}\) will be the least fixed point. If one adds a new
1-place predicate symbol *P* to the language of arithmetic, one
can describe the so-called positive arithmetical operators. They are
of the form 

 

\[
\Gamma\_A(X)=\{n\in\bbN\mid A(n,X)\}
\]


where \(A(x,P)\) is a formula of the language of **PA**
augmented by *P* in which the predicate *P* occurs only
 positively.[28]
 The syntactic condition of positivity then ensures that the operator
\(\Gamma\_A\) is monotone. The language of \(\bID\_1\) is an extension
of that of **PA**. It contains a unary predicate symbol
\(I\_A\) for each positive arithmetical operator \(\Gamma\_A\) and the
axioms 

 

\[\label{id1} 
\begin{align}
\tag{Id1} \forall x\,(A(x,I\_A)\rightarrow I\_A(x))\\
\tag{Id2} \forall x\,[A(x,F)\to F(x)]\to \forall x\,[I\_A(x)\to F(x)]
\end{align}
\]


where in (Id2) \(F(x)\) is an arbitrary formula of \(\bID\_1\) and
\(A(x,F)\) arises from \(A(x,P)\) by replacing every occurrence of
\(P(t)\) in the formula by \(F(t)\). Collectively these axioms assert
that \(I\_A\) is the least fixed point of \(\Gamma\_A\), or more
accurately the least among all sets of natural numbers definable in
the language of \(\bID\_1\). \(\bID\_1^i\) will be used to denote the
intuitionistic version. Its subtheory \(\bID\_{1}^{i}(\cO)\) is
obtained by just adding the predicate symbol \(I\_A\) and the
pertaining axioms (Id1) and (Id2), where \(\Gamma\_A\) is the operator
that defines Kleene's \(\cO\) (cf.
 Definition 5.1).



By a complicated passage through formal theories for choice sequences
it was known that the theory \(\bID\_{1}\) can be reduced to
\(\bID\_{1}^{i}(\cO)\). The first ordinal analysis for the theory
\(\bID\_{1}^{i}(\cO)\) was obtained by Howard (1972). Via the known
proof-theoretical reductions this entailed also an ordinal analysis
for \(\bID\_{1}\). The proof-theoretic ordinal of \(\bID\_{1}\) is the
*Bachmann-Howard ordinal*, which is denoted by
\({\psi\_{\sOmega\_{1}}(\varepsilon\_{\Omega\_1+1})}\) in the system of
 Definition 5.11.



As inductively defined sets can be the starting point of another
inductive definition, the procedure of inductively defining predicates
can be iterated along any well-ordering \(\nu\) in a uniform way. This
leads to the theories \(\bID\_{\nu}\) which allow one to formalize
\(\nu\)-times iterated inductive definitions, where \(\nu\) stands for
a primitive recursive well-ordering. If \(\nu\) is a well-ordering on
constructive grounds then also the \(\nu\)-times iterated version of
Kleene's \(\cO\) has a clear constructive meaning. As a result
the formal theories \({{\bID}}^i\_{\nu}(\cO)\) that embody this process
are constructively justified. The topic of theories of iterated
inductive definitions was flourishing at the 1968 conference on
Intuitionism and Proof Theory in Buffalo (see Kino et al. 1970). One
of the main proof-theoretic goals was to find a reduction of the
classical theories \(\bID\_{\nu}\) to their intuitionistic counterparts
\({{\bID}}^i\_{\nu}(\cO)\). This was all the more desirable because of
known reductions of important fragments of second order arithmetic to
theories of the former kind. Friedman (1970) had shown that the second
order system with the \(\Sigma \_2^1\)-axiom of choice can be
interpreted in the system
\(\hbox{($\Pi\_1^1$-CA)}\_{<{\varepsilon\_0}}\) of less than
\({\varepsilon\_0}\)-fold iterated \(\Pi\_1^1\)-comprehensions and
Feferman (1970a) had shown that less than \(\nu\)-fold iterated
\(\Pi\_1^1\)-comprehensions could be interpreted in the system 



\[
\bID\_{<\nu} \coloneqq \bigcup\_{\alpha<\nu}\bID\_{\alpha}
\]


for \(\nu=\omega^{\gamma}\) with \(\gamma\) limit. However, Zucker
(1973) showed that there are definite obstacles to a straightforward
reduction of the theories \(\text{ID}\_{\nu}\) for \(\nu > 1\) to
their intuitionistic cousins. Sieg (1977) attacked the problem by a
method adapted from Tait (1970) who had used cut elimination for an
infinitary propositional logic with formulae indexed over constructive
number classes to obtain a consistency proof for second order
arithmetic theory with the schema of \(\Sigma \_2^1\) dependent
choices. He achieved a reduction of \(\bID\_{<\nu}\) to
\(\bID\_{<\nu}^i(\cO)\) for limit \(\nu\) by carrying out the proof
theory for a system of \(\PL\_{\alpha}\) of propositional logic with
infinitely long conjunctions and disjunctions indexed over the
constructive number classes \(\cO\_{\alpha}\) for \(\alpha<\nu\)
inside \(\bID^i\_{\alpha+1}(\cO)\). As \(\bID\_{\alpha}\) can be reduced
to \(\PL\_{\alpha}\) this brought about the reduction. Ordinal analyses
for theories of iterated inductive definitions, first for finite and
then also for transfinite iterations, were obtained by Pohlers using
Takeuti's reduction procedure for \(\Pi\_1^1\)-comprehension (see
Pohlers 1975, 1977). Working independently, Buchholz (1977a) used a new type of rules, dubbed
\(\Omega\_{\mu+1}\)-rules to recapture these results without use of
Takeuti's methods. These rules are an extension of the
O-rule described in
 Definition C.3.


#### 5.3.1 Interlude: an ordinal representation system beyond Bachmann's

 

The ordinal representation systems encountered so far are not
sufficient for expressing the strength of theories of iterated
inductive definitions nor that of the strongest of the standard system
of reverse mathematics, \((\Pi^1\_1{\Hy}\bCA)\_0\). Therefore we
intersperse a brief account of how to proceed onwards, adumbrating the
main ideas.



Bachmann's bold move of using large ordinals to generate names
for small ordinals was a very important idea. To obtain ordinal
analyses of ever stronger theories one has to find new ways of
defining ordinal representation systems that can encapsulate their
strength. The latter goes hand in hand with the development of new cut
elimination techniques that are capable of removing cuts in
(infinitary) proof systems with strong reflection rules. Ordinal
representations, however, appear to pose a considerable barrier to
understanding books and articles in this research area. Nonetheless we
think that they are the best way to express the proof-theoretic
strength of a theory as they provide a scale by means of which one can
get a grasp of how much stronger a theory \(S\_1\) is than another
theory \(S\_2\) (rather than the bland statement that \(S\_1\) is
stronger than \(S\_2\)).



As an example we will introduce an ordinal representation system which
characterizes the theory \((\Pi^1\_1{\Hy}\bCA)+{{\BI}}\), following
Buchholz 1977b. It is
based on certain ordinal functions \(\psi\_{\sOmega\_n}\) which are
often called *collapsing functions*. The definition of these
functions, that is of the value \({\psi\_{\sOmega\_{n}}(\alpha)}\) at
\(\alpha\), proceeds by recursion on \(\alpha\) and gets intertwined
with the definition of sets of ordinals
\(C^{{\Omega\_{\omega}}}(\alpha,\beta)\), dubbed "Skolem
hulls" since they are defined as the smallest structures closed
under certain functions specified below.



Let \(\bbN^+\) be the natural numbers without 0. Below we shall assume
that \(\Omega\_n\) \((n\in\bbN^+)\) is a "large" ordinal
and that \(\omega<\Omega\_n <\Omega\_{n+1}\). Their limit,
\(\sup\_{n\in\bbN^+}\Omega\_n\), will be denoted by
\(\Omega\_{\omega}\).




Definition 5.11 By recursion on \(\alpha\)
we define: 

 

\[\begin{align}
C^{\Omega\_{\omega}}(\alpha,\beta) & = 
\left\{\begin{array}{l} \textrm{closure of } \beta\cup\{0,\Omega\_{\omega}\}\cup\{\Omega\_n\mid n\in\bbN^+\} \\
\textrm{under: }\\ 
+, (\xi\mapsto \omega^{\xi})\\
(\xi\longmapsto{\psi\_{\sOmega\_{n}}(\xi)})\_{\xi<\alpha}\textrm{ for } n\in\bbN^+
\end{array}\right. \\[1ex]
{\psi\_{\sOmega\_{n}}(\alpha)}&= \min\{\rho<\Omega\_n\mid\;C^{\Omega\_{\omega}}(\alpha,\rho)\cap\Omega\_n=\rho\}.
\end{align}\]



At this point it is not clear whether \({\psi\_{\sOmega\_{n}}(\alpha)}\)
will actually be defined for all \(\alpha\) since there might not
exist a \(\rho<\Omega\_n\) such that 

 

\[
C^{{\Omega\_{\omega}}}(\alpha,\rho)\cap\Omega\_n=\rho.
\]


This is where the "largeness" of \(\Omega\_n\) comes into
play. One (easy) way of guaranteeing this consists in letting
\(\Omega\_n\) be the \(n^{th}\) uncountable regular cardinal, that is
\(\Omega\_n\coloneqq \aleph\_n\). However, such strong set-theoretic
assumptions can be avoided. For instance, it suffices to let
\(\Omega\_n\) be the \(n^{th}\) recursively regular ordinal (which is a
countable ordinal) (see Rathjen 1993a).



To get a better feel for what \(\psi\_{\sOmega\_{n}}\) is doing, note
that if \(\rho={\psi\_{\sOmega\_{n}}(\alpha)}\), then
\(\rho<\Omega\_n\) and with \([\rho,\Omega\_n)\) being the interval
consisting of ordinals \(\rho\leq\alpha<\Omega\_n\) one has 



\[
[\rho,\Omega\_n)\cap C^{\Omega\_{\omega}} (\alpha,\rho) =\emptyset
\]


thus the order-type of the ordinals below \(\Omega\_n\) which belong to
the "Skolem hull" \(C^{{\Omega\_{\omega}}}(\alpha,\rho)\)
is \(\rho\). In more pictorial terms, \(\rho\) is said to be the
\(\alpha^{th}\) *collapse* of \(\Omega\_n\) since the order-type
of \(\Omega\_n\) viewed from within the structure
\(C^{{\Omega\_{\omega}}}(\alpha,\rho)\) is actually \(\rho\).



The ordinal representation system we are after is provided by the set


 

\[
C^{{\Omega\_{\omega}}}(\varepsilon\_{\Omega\_{\omega}+1},0)
\]


where \(\varepsilon\_{\Omega\_{\omega}+1} \) is the least epsilon number
after \(\Omega\_{\omega}\), i.e., the least ordinal
\(\eta>\Omega\_{\omega}\) such that \(\omega^{\eta}=\eta\). The
proof-theoretic ordinal of \((\Pi^1\_1{\Hy}\bCA)+{{\BI}}\) is
\({\psi\_{\sOmega\_{1}}(\varepsilon\_{\Omega\_{\omega}+1})}\). Although
the definition of the set
\(C^{{\Omega\_{\omega}}}(\varepsilon\_{\Omega\_{\omega}+1},0)\) and its
ordering is set-theoretic, it turns that it also has a purely
primitive recursive definition which can be given in a fragment of
**PRA**. Thus the set-theoretic presentation mainly
serves the purpose of a "visualization" of an elementary
well-ordering.



The pattern of definition exhibited in
 Definition 5.11
 continues for stronger systems, albeit only as a basic template since
for theories beyond the level of \((\Delta^1\_2{\Hy}\bCA)+{{\BI}}\)
substantially new ideas are required. Analogies between large
set-theoretic ordinals (cardinals) and recursively large ordinals on
the one hand and ordinal representation systems on the other hand can
be a fruitful source of inspiration for devising new representation
systems. More often than not, hierarchies and structural properties
that have been investigated in set theory and recursion theory on
ordinals turn out to have proof-theoretic counterparts.


#### 5.3.2 Assigning proof-theoretic ordinals

 

Using an extended version of the representation system from
 Definition 5.11
 if
 \(\nu>\omega\),[29]
 the outcome of all the work on the theories of inductive definitions
can be summarized by the following
 theorem.[30]





Theorem 5.12 For recursive \(\nu\), 



\[
\lvert \bID\_{\nu}\rvert = \lvert \bID^i\_{\nu}(\cO)\rvert = \psi\_{\sOmega\_\nu}(\varepsilon\_{\sOmega\_{\nu}+1}).
\]



A generalized treatment of theories of iterated inductive definitions
for arbitrary well-orderings and of autonomous iteration was carried
out in Rathjen 1988, 2010. These theories are stronger than
\((\Delta^1\_2{\Hy}\bCA)\) if \(\nu\geq\varepsilon\_0\).



Theorem 5.12
 played an important role in determining the exact strength of some
fragments of \(\bZ\_2\). The major ordinal-theoretic results pertaining
to subsystems of \(\bZ\_2\) of the pre-1980 area given in the next
 theorem.[31]




Theorem 5.13


1. \(\lvert (\Pi^1\_1{\Hy}\bCA)\_0\rvert =
\lvert \bID\_{<\omega}\rvert =\psi\_{\sOmega\_1}(\Omega\_{\omega})\)
2. \(\lvert (\Pi^1\_1{\Hy}\bCA)\rvert
=\psi\_{\sOmega\_1}(\Omega\_{\omega}\cdot\varepsilon\_0)\)
3. \(\lvert (\Pi^1\_1{\Hy}\bCA)+{{\BI}}\rvert =\lvert \bID\_{\omega}\rvert
=\psi\_{\sOmega\_1}(\varepsilon\_{\sOmega\_{\omega}+1})\)
4. \(\lvert (\Delta^1\_2{\Hy}\bCR)\rvert =
\psi\_{\sOmega\_1}(\Omega\_{\omega^{\omega}})\)
5. \(\lvert (\Delta^1\_2{\Hy}\bCA)\rvert =
\psi\_{\sOmega\_1}(\Omega\_{\varepsilon\_0})\)




The next challenge after \((\Delta^1\_2{\Hy}\bCA)\) was posed by the
theory \((\Delta^1\_2{\Hy}\bCA)+{{\BI}}\). Its treatment not only
required a considerably stronger ordinal representation system but
also coincided with a shift away from \(\cL\_2\) theories and theories
of iterated inductive definitions to a direct proof-theoretic
treatment of set theories. Pioneering work on the proof theory of set
theories is mainly due to Jager (1980, 1982). The analysis of
\((\Delta^1\_2{\Hy}\bCA)+{{\BI}}\) in Jager & Pohlers 1982
provides a particularly nice application of this new approach which
has been called *admissible proof theory*, owing to its concern
with theories extending Kripke-Platek set theory by axioms asserting
the existence of admissible sets (for some details see
 Appendix D.1).




Theorem 5.14 \(\lvert (\Delta^1\_2{\Hy}\bCA)+\BI\rvert =
\psi\_{\sOmega\_1}(\varepsilon\_{I+1})\)




The "*I*" in the foregoing notation is supposed to be
indicative of "*inaccessible cardinal*". Indeed,
the easiest way to build an extended ordinal representation system
sufficient unto this task (modeled on
 Definition 5.11)
 is to add an inaccessible *I*, close the Skolem hulls under
\(\xi\mapsto \Omega\_\xi\) for \(\xi<I\) and introduce collapsing
functions \(\psi\_{\pi}\) for all \(\pi\) of either form *I* or
\(\Omega\_{\xi+1}\).



The goal of giving an ordinal analysis of full second order arithmetic
has not been attained yet. For many years \(\Pi^1\_2\)-comprehension
posed a formidable challenge and the quest for its ordinal analysis
attained something of a holy grail status (cf. Feferman 1989). At
first blush it might be difficult to see why the latter comprehension
is so much more powerful than \(\Delta^1\_2\)-comprehension (plus
\({{\BI}}\)). To get a sense for the enormous difference, it seems
advisable to work in (admissible) set theory and consider a hierarchy
of recursively large ordinal notions wherein these comprehension
schemes correspond to the bottom and the top end of the scale,
respectively. That is discussed in
 Appendix D.
 Here we just mention a few reductions to "constructive"
frameworks. The reductions we have in mind, underlie a broadened view
of "constructivity". Constructive theories of functions
and sets that relate to Bishop's constructive mathematics as
theories like **ZFC** relate to Cantorian set theory have
been proposed by Myhill, Martin-Lof, Feferman and Aczel.
Among those are Feferman's constructive theory of operations and
classes, \(\bT\_0\) in 1975 and 1979, Martin-Lof's
intuitionistic type theory (1984) and constructive set theory,
especially Constructive Zermelo-Fraenkel Set Theory,
**CZF**, the latter also combined with the regular
extension axiom, **REA**. By employing an ordinal
analysis for set theory **KPi** which is an extension of
Kripke-Platek set theory via an axiom asserting that every set is
contained in an admissible set (see
 Appendix D)
 it has been shown that **KPi** and consequently
\((\Delta^1\_2{\Hy}\bCA)+{{\BI}}\) can be reduced to both of these
theories:




Theorem 5.15 (Feferman 1975; Jager
1983; Jager & Pohlers 1982; Rathjen 1993b)
\((\Delta^1\_2{\Hy}\bCA)+\BI\), **KPi**, \(\bT\_0\) and
**CZF**+**REA** are proof-theoretically
equivalent. In particular, these theories prove the same theorems in
the negative arithmetic fragment.





Theorem 5.16 (Rathjen 1993b; Setzer 1998)
The soundness of the negative arithmetic fragment of
\(\Delta^1\_2-\bCA+\BI\) and **KPi** is provable in
Martin-Lof's 1984 type theory.




A detailed account of these results has been given in section 3 of
Rathjen 1999a.


## 6. Epilogue

 

Proof theory has become a large subject with many specialized branches
that can be mathematically quite complex. So we have tried to present
developments close to the main artery of its body, starting with its
inception at the beginning of the twentieth century and ending with
results from the close of the century. The theorems mentioned at the
end of section 5 foreshadow investigations in the twenty-first century
that are presented in Rathjen (2018) and concern relationships
between Feferman's systems of explicit mathematics and
Martin-Lof type theories; the paper touches also on the
completely new developments of homotopy type theory (see Awodey 2012).
Some additional contemporary proof theoretic developments are
described in appendices
 D,
 E and
 F.
 The theme of
 Appendix E,
 the extraction of computational information from proofs in particular
formal theories, is the central topic of Schwichtenberg and
Wainer's 2012. They deal with theories of arithmetic and
analysis up to \((\Pi^1\_1{\Hy}\bCA)\_0\). Standard texts on proof
theory covering ordinal analysis are Takeuti 1985 and Schutte
1977. First steps into ordinal analysis are taken in Pohlers 2009.
Finally, some new directions of proof theoretic work are taken in
contributions to both Kahle and Rathjen 2015 and Jager and
Sieg 2018.



Let us also report on progress on the methodological issues the
finitist consistency program was to address. First of all, due to
quite a bit of important historical work, we have a much better grasp
of the evolution of the program in the 1920s and its roots in the
development toward modern structuralist mathematics in the nineteenth
century. The work of editing Hilbert's unpublished lecture notes
has opened a treasure of
 information.[32]
 The connections to the development in nineteenth century mathematics
are hinted at in
 Appendix A,
 but they are explored in greater depth, for example, in
Ferreiros 2008; Reck 2003, 2013; and the papers Sieg wrote on
Dedekind with Morris (forthcoming) and Schlimm (2005, 2017),
respectively. Secondly, as to the properly methodological issues, we
presented some broad considerations in
 section 4.1,
 namely, that consistency proofs should be given relative to
"constructive" theories. We did not make any remarks about
what is characteristic of a constructive perspective and why such a
perspective has not only a mathematical, but also a philosophical
point. There is, of course, a very rich literature. Let us point to
some informative sources: van Atten (2007) as defending
Brouwer's views, Martin-Lof (1984) as exposing the
philosophical motivation for his type theory, Feferman (1988, 2000)
discussing the foundational point of proof theory, Bernays (1976) as
presenting crucial aspects of an informed philosophy of mathematics,
and (Sieg 2013) as
explicating (the context for) his *reductive
structuralism*.



Back to proof theory: We have to admit that we neglected some
classical topics. One is the study of different proof systems and
their relationships going back to Gentzen's dissertation (1935).
In their *Basic Proof Theory*, Troelstra and Schwichtenberg
(2000) give an excellent selection, but some important calculi such as
the Schutte proof systems are not covered (see, for example,
Schutte 1960b, 1977). They also do not cover proof systems for
temporal and modal logic, neither are substructural logics
 presented.[33]




A second omission concerns Bounded Arithmetic, where feasibility
issues are a central focus: one studies formal theories with provably
recursive functions that form very small subclasses of the primitive
recursive ones. Indeed, the class of the provably total functions of
Buss' base theory is that of functions that can be computed in
polynomial time, and there was the hope that proof theoretic
investigations might contribute novel results in complexity theory. A
third omission concerns proof mining; that line of deep mathematical
investigations using proof theoretic tools was initiated by Kreisel
(1958, 1982) and Luckhardt (1989), but really perfected only by Kohlenbach
(2007). We hinted at the work of his school at the very end of
 section 4.1.



Proof theory, as we described it, deals primarily with formal proofs
or derivations. Hilbert aimed, however, as we pointed out in
 section 1,
 for a more general analysis of ordinary, informal mathematical
proofs. For Gentzen in his 1936, "the objects of proof theory
shall be the *proofs* carried out in mathematics proper" (p. 499). The aim of Hilbert and his
collaborators was undoubtedly to achieve a deeper mathematical and
conceptual understanding, but also to find general methods of proof
construction in formal calculi. This is now being pursued in the very
active area of using powerful computers for the interactive
verification of proofs and programs as well as the fully automated
search for proofs of mathematical
 theorems.[34]
 That can be pursued with a cognitive scientific purpose of modeling
mathematical reasoning (see Sieg 2010 and Ganesalingam & Gowers 2017). It is clearly
in the spirit of Hilbert who articulated matters in his second Hamburg
talk of 1927 as follows:



> 
> 
> The formula game ... has, besides its mathematical value, an
> important general philosophical significance. For this formula game is
> carried out according to certain definite rules, in which the
> technique of our thinking is expressed. These rules form a closed
> system that can be discovered and definitively stated.
> 
> 
> 



Then he continues with a provocative statement about the cognitive
goal of proof theoretic investigations.



> 
> 
> The fundamental idea of my proof theory is none other than to describe
> the activity of our understanding, to make a protocol of the rules
> according to which our thinking actually proceeds. (Hilbert 1927
> [1967: 475]) 
> 
> 
> 



It is clear to us, and it was clear to Hilbert, that mathematical
thinking does not proceed in the strictly regimented ways imposed by
an austere formal theory. Though formal rigor is crucial, it is not
sufficient to shape proofs intelligibly or to discover them
efficiently, even in pure logic. Recalling the principle that
mathematics should solve problems "by a minimum of blind
calculation and a maximum of guiding thought", we have to
investigate the subtle interaction between understanding and
reasoning, i.e., between introducing concepts and proving
theorems.