# The Development of Proof Theory

*First published Wed Apr 16, 2008*

The development of proof theory can be naturally divided into: the prehistory of the notion of proof in ancient logic and mathematics; the discovery by Frege that mathematical proofs, and not only the propositions of mathematics, can (and should) be represented in a logical system; Hilbert's old axiomatic proof theory; Failure of the aims of Hilbert through Gödel's incompleteness theorems; Gentzen's creation of the two main types of logical systems of contemporary proof theory, natural deduction and sequent calculus (see the entry on automated reasoning); applications and extensions of natural deduction and sequent calculus, up to the computational interpretation of natural deduction and its connections with computer science.

- 1. Prehistory of the notion of proof
- 2. Hilbert's old axiomatic proof theory
- 3. The unprovability of consistency
- 4. Natural deduction and sequent calculus
- 5. The consistency of arithmetic and analysis
- 6. Later developments in natural deduction
- 7. Later developments and applications of sequent calculus
- 8. The aims of proof theory
- Bibliography
- Related Entries

## 1. Prehistory of the notion of proof

Proof theory can be described as the study of the general structure
of mathematical proofs, and of arguments with demonstrative force as
encountered in logic. The idea of such demonstrative arguments, i.e.,
ones the conclusion of which follows necessarily from the assumptions
made, is central in Aristotle's *Analytica Posteriora*: a
deductive science is organised around a number of basic concepts that
are assumed understood without further explanation, and a number of
basic truths or axioms that are seen as true immediately. Defined
concepts and theorems are reduced to these two, the latter through
proof. Aristotle's account of proof as demonstrative argument fits
very well to the structure of ancient geometry as axiomatized in
Euclid. The specific form of
Aristotle's logic,
the theory of syllogism has instead, so it seems, almost nothing to
do with proofs in Euclidean geometry. These proofs remained intuitive
for more than two thousand years.

Before the work of Frege in 1879, no one seems to have maintained that there could be a complete set of principles of proof, in the sense expressed by Frege when he wrote that in his symbolic language, “all that is necessary for a correct inference is expressed in full, but what is not necessary is generally not indicated; nothing is left to guesswork.” (One might contend that Boole is an exception as far as classical propositional logic is concerned.) Even after Frege, logicians such as Peano kept formalizing the language of mathematical arguments, but without any explicit list of rules of proof. Frege's step ahead was decisive for the development of logic and foundational study. The contrast to the ancients is great: Aristotle gave a pattern for combining arguments, but the idea of a finite closed set of rules was, philosophically, beyond the dreams of anyone before Frege, with the possible exception of Leibniz.

As we know today, Frege's principles of proof are complete for classical predicate logic. Russell took up his logic, but used the notation of Peano, and thus formulated an axiomatic approach to logic. The idea was that the axioms express basic logical truths, and other logical truths are derived from these through modus ponens and universal generalization, the two principles Frege had identified. Mathematics was to be reduced to logic, so that its proofs would become presented in the same axiomatic pattern.

Frege's and Russell's approach to logic became the universally
accepted one, especially through the influence of Hilbert and his
co-workers in the 1920s. In the 19th century, Frege was a marginal
figure, and the algebraic approach to logic, as in Boole and
especially Ernst Schröder, was the dominant one. It is clear
that there was a good understanding of the principles of predicate
logic in this tradition, for how could there have been a
Löwenheim-Skolem theorem otherwise? Skolem found out about
Frege's logic through *Principia mathematica* only after having
worked out the theorem in his paper of 1920. The first section of
that paper, widely read because of the English translation in Van
Heijenoort's *From Frege to Gödel*, marks the end of the
algebraic tradition of logic that merged silently with lattice
theory. Other sections of the paper contain a remarkable beginning of
the analysis of proofs in lattice theory and in projective geometry:
Skolem considered the axioms of a mathematical theory from a purely
combinatorial and formal point of view, as means for producing
derivations of a formula from given formulas used as assumptions. It
was found out in the early 1990s that the part on lattice theory
contains the solution of a decision problem, called the word problem
for freely generated lattices, the known solution of which stemmed
from 1988! Skolem's terminology and notation in lattice theory are
those of Schröder and that is part of the reason why his work
was a lost opportunity for proof theory.

## 2. Hilbert's old axiomatic proof theory

Hilbert's book *Grundlagen der Geometrie* of 1899 set the stage
for the central foundational problems of mathematics of the early
decades of the 20th century. We can list these problems as follows:

- The formalization of a mathematical theory. This includes a choice of its basic objects and relations, and a choice of the axioms.
- A proof of the consistency of the axioms.
- The question of the mutual independence and completeness of the axioms.
- The decision problem: is there a method for answering any question that could be raised within the theory?

As to Hilbert's geometry, its attempted formalization fell short of
the ideal to which it gave birth. Hilbert found a much more important
field to which his “metamathematics” was to be applied,
namely arithmetic and analysis. The groundwork was a study of the
four foundational problems in axiomatic formulations of pure logic.
Propositional logic was thus formalized, found to be consistent and
complete, and decidable. The first results about predicate logic are
from 1915, when Leopold Löwenheim gave his version of what later
became the Löwenheim-Skolem theorem for predicate logic (see the
entry on
classical logic).
He also solved special cases of the decision problem. This
development was independent of the Frege-Russell tradition, and was
instead based on the algebraic approach to logic of Ernst
Schröder. Around 1920, the “Hilbert style” axiomatic
approach, as it is often called, was known to everyone and dominated
the logical scene; the algebraic approach merged almost without
notice with lattice theory. By 1928, in Hilbert and Ackermann's
*Grundzüge der theoretischen Logik*, an axiomatic formal
system for predicate logic was presented, together with the problem
of its completeness. The latter was solved by Gödel in 1929,
published a year later. The fourth foundational problem, the decision
problem for predicate logic, was shown to have a negative solution in
a short paper by Church in 1936, as a corollary to Gödel's
incompleteness theorem.

Hilbert and his school, with Bernays, Ackermann and von Neumann as
foremost, as well as young Herbrand in France, pursued the
metamathematical study of arithmetic in the latter part of the 1920s.
Hilbert developed a method for the study of consistency problems,
called the
epsilon substitution method,
to deal with the quantifiers. He felt that indirect inferences with
quantifiers in cases with an infinity of objects were the crucial
point of consistency proofs and needed a justification. Say, if the
assumption that all natural numbers have the property *P*
leads to an impossibility, the existence of a number with the
contrary property not-*P* can be inferred. The central problem
was thus to justify the use of classical logic in mathematical
proofs, arithmetical ones in the first place. Ackermann was very
close to a solution towards the end of the 1920s and optimism reigned
in the Hilbert school. Then, of course, the unexpected happened when
Gödel proved the impossibility of a complete formalization of
elementary arithmetic, and, as it was soon interpreted, the
impossibility of proving the consistency of arithmetic by finitary
means, the only ones judged “absolutely reliable” by
Hilbert.

## 3. The unprovability of consistency

After Gödel had made public the incompleteness of arithmetic in September 1930, von Neumann found that the consistency of arithmetic would be among the Gödelian unprovable propositions. Alas, Gödel had made the same discovery so von Neumann never published his proof. He did, however, conjecture in correspondence with Gödel the unprovability of the consistency of arithmetic and therefore of mathematics as a whole, in some absolute sense.

In 1932–33, Gödel and Gentzen found independently of each other a translation from classical Peano arithmetic to intuitionistic Heyting arithmetic. Specifically, it shows that if a contradiction is provable in the former, it is provable in the latter. Then the consistency of intuitionistic arithmetic would guarantee also the consistency of classical arithmetic. This result was a surprise: as mentioned, Hilbert had thought that the “transfinite” indirect existence proofs would be the part of arithmetic that needs to be secured of contradiction. By Gödel's and Gentzen's result, already intuitionistic arithmetic contained principles that went beyond finitary reasoning. A letter Gentzen wrote to Heyting on 25 February 1933 summarizes the situation as follows:

A consistency proof by finite means has … not succeeded so far, so that this original aim of Hilbert has not been achieved. 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 Gödel'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 also desirable.

The last-mentioned was the goal Gentzen had set to himself early in 1932, when in a letter to his old teacher Hellmuth Kneser he wrote:

I have set as my specific task to find a proof of the consistency of logical deduction in arithmetic… The task becomes a purely mathematical problem through the formalization of logical deduction. The proof of consistency has been so far carried out only for special cases, for example, the arithmetic of the integers without the rule of complete induction. I would like to proceed further at this point and to clear at least arithmetic with complete induction. I am working on this since almost a year and hope to finish soon, and would then present this work as my dissertation (with Prof. Bernays).

## 4. Natural deduction and sequent calculus

In pursuing his consistency program, Gentzen set as his first task
the analysis of purely logical deduction, to be extended later to
arithmetic and analysis. In his thesis *Untersuchungen über
das logische Schliessen* (Investigations into Logical Inference,
under the supervision of Bernays, accepted in June 1933 and published
in two parts in 1934–35), he states that he set as his task the
analysis of mathematical proofs as they occur in practice. Hilbert's
lecture in Hamburg in 1930 is one obvious source of inspiration for
this venture. The first observation is that actual proofs are not
based on axioms expressed in a logical language, as in Hilbert's
axiomatic proof theory. The most typical feature is instead that
theorems make their claims under some assumptions. The assumptions
are analyzed into parts and the conclusion is also analyzed into
parts until these two analyses meet and a proof can be synthesized.
The latter analysis proceeds by what Gentzen called introduction
rules: they give sufficient conditions for deriving a proposition of
a given form. For example, to derive a conjunction A&B, it is
sufficient to derive the conjuncts *A* and *B*
separately. The inference is given formally as in the rule

AB

A&B&I

Assumptions, instead, are analyzed into their components through elimination rules that give, by and large, immediate consequences of the assumptions. For example, a conjunction used as an assumption can be decomposed into its constituents, as in the rules

A&B

A&E _{1}

A&B

B&E _{2}

Gentzen developed and studied the system of natural deduction during
1932, and had arrived by September 1932 at a calculus of natural
deduction (ND for short) that is standard today. By this time, he had
noticed that if an introduction, say a derivation of
*A*&*B* from *A* and *B* separately,
is followed by the corresponding elimination, say a derivation of
*A*, the formula *A*&*B* constitutes a local
maximum, a “hillock”, that can be eliminated. He also
called such hillocks “detours”, and what is now called a
detour conversion removes such unnecessary pairs of
introduction-elimination steps. The result of the steps of
“normalization” is a derivation in “normal
form”.

Implication is perhaps more typical of ND than conjunction: to derive
*A*⊃*B*, one temporarily assumes *A*, then
tries to derive *B*. If this succeeds, the temporary
assumption is closed or “discharged” when the conclusion
to *A*⊃*B* is made, as in the schematic derivation

[ A]

.

.

.

B

A⊃B

⊃I

In the other direction, *A*⊃*B* can be eliminated
if a derivation of *A* has been found, for then *B* can
be concluded:

A⊃BA

B⊃E

If rule ⊃I is followed by ⊃E, there is a non-normality that
is removed by a detour conversion: a derivation of *B* (and
what follows after it) is constructed by taking the derivation of the
minor premiss *A* of the elimination rule and the derivation
of *B* from the assumption *A* in the introduction.
These two pieces are combined together into a derivation of
*B* that does not have the detour formula
*A*⊃*B*. In Gentzen's thesis, all assumptions are
in the end closed by implication introductions, but nowadays one
considers also derivations that leave a collection of formulas as
open assumptions.

Looking at the rules of conjunction and implication, one notes that the premisses (the formulas immediately above the inference line) are subformulas of the conclusion in the I-rules, whereas it is the other way around in the E-rules. Gentzen noticed that in normal derivations, this property of single steps is inherited by the whole derivation, in the sense that all formulas are subformulas of the conclusion. This result gave as a byproduct a decision method for intuitionistic propositional logic. Another corollary was a syntactic proof of consistency: if a contradiction is provable, anything is provable, but an atomic formula, say, has no proof: if it has a proof, it has a normal proof, but no E-rules apply to an atomic formula, and no I-rule concludes it either.

Gentzen's idea was to extend natural deduction to a system of arithmetic by the addition of a rule that corresponds to the principle of complete induction. Consistency would then follow from the normalization of derivations and the subformula property. By early 1933, Gentzen realized that this proof strategy would not go through: the induction rule is schematic and has an infinity of instances, with no bound on the complexity of the induction formulas. It would be impossible to restrict these formulas in advance, thus no subformula property can hold. After this failure, Gentzen took verbatim out of his early thesis manuscript the translation from classical to intuitionistic arithmetic and submitted it as a paper in March 1933, but withdrew the paper after hearing of Gödel's publication of the result.

Gentzen wrote that he was unable to prove a normalization theorem for
a classical system of ND. He therefore invented another logical
calculus that he called sequent calculus (*Sequenzenkalkul*,
literally “calculus of sequences”) and made it the
central topic of his thesis. The name of the calculus comes from the
representation of assumptions of a derivation as a list. The word
“sequent” used as a noun is a suggestion of Kleene's in
his *Introduction to Metamathematics* (1952, p. 441), taken up
in many languages in the form of purely invented words.

Sequent calculus, SC for short, can be seen as a formal representation of the derivability relation in natural deduction. A sequent consists of a list Γ of formulas, an arrow (in Gentzen, later also other markers have been used), and one formula as a conclusion. The list gives the assumptions the conclusion depends on in a derivation, in a local notation where in ND they are found in the leaves of a derivation tree. Gentzen also generalized sequents so that they have, instead of one conclusion, a list of possible cases after the arrow. This novelty led to the first satisfactory formulation of a proof system for classical logic. Gentzen's SC rules for conjunction and implication are, with commas separating elements in lists:

Conjunction

Γ →Δ,AΓ → Δ,B

Γ→Δ,A&BR&

A,Γ→Δ

A&B,Γ→ΔL& _{1}

B,Γ→Δ

A&B,Γ→ΔL& _{2}Implication

A,Γ→Δ,B

Γ→Δ,A⊃BR⊃

Γ →Θ,AB,Δ→Λ

A⊃B,Γ,Δ→Θ,ΛL⊃

This is not the place to explain the details of ND and SC (but see
the entry on
automated reasoning).
Gentzen formulated the latter, denoted LK, so that it gave an
intuitionistic calculus, denoted LJ, as a special case, the one in
which the conclusion is a list of at most one case. He then proved
the analogue of the normalization theorem for the classical calculus,
the calculus and the proof carefully formulated so that the result
for the intuitionistic calculus was a special case of the one for the
classical calculus. In LJ and LK, L stands for
“logistic”, a term by which Gentzen refers to the
axiomatic calculi of logic of Frege, Russell, and Hilbert and
Bernays. In such calculi, each line in a derivation is correct in
itself, i.e., a logical truth, whence the term. The letters K and J
come from the German words *klassisch* and
*intuitionistisch*. (The latter should thus be I, but older
German uses for upper case I also the writing J.)

Gentzen called the analogue of normalization by the unimaginative
name of *Hauptsatz*, “main theorem”. The standard
terminology today is “cut elimination theorem” All of the
logical rules of SC have the subformula property in a very immediate
sense: each formula in a premiss is a formula or subformula in the
conclusion. The rule for combining derivations, analogous to the one
explained above for the case of detour conversions in ND, is called
“cut”. In it, a formula *A* appears as a case in a
first premiss and as an assumption in a second premiss. In the
conclusion, this formula has disappeared and the assumptions of the
two premisses collected together:

Γ →AA,Δ→C

Γ,Δ→CCut

Thus, cut is the only rule that makes a formula
“disappear” in a derivation. Gentzen showed that
instances of the rule of cut can be eliminated from derivations by
permuting them upward until they reach points at which the derivation
starts. In ND, the starting points are assumptions, in SC they are
“initial sequents” of the form
*A* → *A* in which the assumption
formula *A* is at the same time the conclusion. A cut with
such a sequent as one premiss has the other premiss equal to the
conclusion and can therefore be deleted.

After the proof of cut elimination, Gentzen had no use for the proof of normalization for intuitionistic natural deduction. He gave the first handwritten version of his thesis, with the detailed proof of normalization (equivalent to some 13 printed pages) to Bernays, but the latter seems never to have realized what he had in his hands. The proof, among the papers of Bernays in Zurich, was discovered by the present author in February 2005 and is now available in an English translation (Gentzen 2008).

## 5. The consistency of arithmetic and analysis

After his thesis work on ND and SC for pure logic, Gentzen continued
his plan of proving the consistency of arithmetic. The result was
ready by December 1934. What this very first proof was, is not known
in detail. However, a letter to Bernays from 1938 indicates that the
proof that Gentzen wrote down by the summer of 1935 was not this
original one, but a second proof. This second proof was criticized by
Bernays and Gödel who discussed it during their Atlantic voyage
to Princeton in September 1935. Gentzen's idea in the proof was as
follows: first, take the conjunction-negation-universal
quantification fragment of natural deduction as the logic used in the
formalization of arithmetic. Then write each rule instance so that
the premisses and conclusion have the open assumptions listed at
left, with an arrow separating the conclusion, so, as sequents. This
variant of ND is now called ND in SC style. Consider a sequent
Γ **→** *C*. If its
conclusion is an atomic formula, it is an equation between numbers.
In the worst case it is false, so then consider the list of
assumptions. If one assumption is a conjunction, replace it by a
conjunct of your choice, if a universal quantification, by an
instance. If it is a negation ¬*A*, replace the conclusion
by *A*. If at any stage of this “reduction
process” the conclusion of a sequent is a compound formula, you
have to consider any conjunct or any instance of universal
quantification as a possible conclusion. In case of negation
¬*A* as a conclusion, move *A* to the assumption
part and replace the conclusion by 0=1. Gentzen shows that by
proceeding in this way under the assumption that the sequent in
question is derivable, either a true equation is found as a
conclusion, or a false equation as an assumption. Thus, there are no
derivable sequents with all assumptions true and the conclusion
false.

It was unclear to Gödel and Bernays what the proof assumed; they thought it assumed what is known in intuitionistic mathematics as the fan theorem, but this was false. Termination of Gentzen's reduction procedure can be proved instead by induction on well-founded trees (“bar-induction”), a principle that was used by Gentzen on intuitive grounds. Anyway, the result of the criticism was that Gentzen changed without further ado the proof into a third proof that uses the now famous principle of transfinite induction up to the first epsilon-number. This induction was presented through a coding that used decimal numbers. The concrete result of the changes for Gentzen's paper published in 1936 was not good, however: the logical calculus was changed midway in an article of seventy-odd pages that became very difficult to read. Therefore Gentzen gave yet another, by the present count fourth proof of the consistency of arithmetic in 1938, this time based on the classical sequent calculus LK of 1933. As mentioned, correspondence with Bernays indicates that he thereby returned to the proof method that had led to success in 1934. The use of transfinite induction is made clearly visible in the 1938 paper through an ordinal notation. Such induction principles on Cantor's “second number class” are discussed in detail in Hilbert's 1926 lecture “Über das Unendliche” (“On the infinite”), a paper Gentzen referred to.

One would have thought that that was that, but Gentzen had reason to
produce even a fourth proof of the consistency of arithmetic, in his
last paper published in 1943 but written before the war in 1939. He
extended Peano arithmetic through transfinite ordinals and made the
transfinite induction principle part of this extended calculus. Then
he showed directly that transfinite induction up to the first
epsilon-number ε_{0} is expressible but not provable
in the system. Gödel's incompleteness theorem is thus proved in
a completely different way. The idea of the proof is, in brief terms,
as follows: first it is laid down what it means to derive transfinite
induction to a specific ordinal number in the system. Secondly,
ordinal numbers below ε_{0} are associated to
derivations. These are called “values”. It is then shown
that if transfinite induction to an ordinal number is derivable, this
ordinal number cannot be greater than the value of the derivation.
Therefore transfinite induction to ε_{0} is not
derivable.

Since the induction principle can be expressed but not proved in ordinary arithmetic, a formula unprovable in Peano arithmetic is found. An easy consequence of Gentzen's version of the incompleteness theorem is the consistency of Peano arithmetic, because anything would be provable in an inconsistent system. Contrary to Gödel's “artificial” unprovable formula that was obtained through a coding of the arithmetized provability predicate, Gentzen's transfinite induction principle is a principle of “ordinary” mathematics.

Gentzen's last proof determined the “proof-theoretic ordinal” of Peano arithmetic, namely the one that is needed to prove consistency, with the property that nothing less would suffice. The work marked the beginning of ordinal proof theory. It was without doubt the most remarkable foundational achievement in arithmetic after Gödel's incompleteness theorems, but is still largely unknown — one can find many books about Gödel's theorems that do not even mention Gentzen.

Gödel had, it seems, not thought of giving a consistency proof of arithmetic through the use of non-finitary but still constructive principles. In the late thirties, at least from 1938 on, he developed as a response to Gentzen's proof his own special interpretation of intuitionistic logic and arithmetic, what came to be known as the Dialectica interpretation. It uses computable functionals to interpret the proofs of intuitionistic arithmetic. Gödel published the interpretation only in 1958, even though he had presented it in lectures in 1941. It is unknown if he discussed the matter when he met Gentzen in December 1939.

At the request of Bernays, Ackermann reproduced Gentzen' proof in terms of Hilbert's epsilon-calculus in 1940. Ackermann's paper was the starting point of Kreisel's 1951 “no-counterexample” interpretation of arithmetic. It was a surprise when the publication of Gödel's collected papers brought to light his “Zilsel-lecture” in Vienna in 1938: he outlines there this interpretation as a reformulation of Gentzen's 1935 proof. (The matter is discussed in great detail in Tait (2005) who himself had worked on the no-counterexample interpretation and its extension to analysis in the 1960s.)

The next obvious task in proof theory, after the proof of the
consistency of arithmetic, was to prove the consistency of analysis,
i.e., of the theory of real numbers. Gentzen did some work in this
direction, but was then assigned to military service in the fall of
1939. (He observed and reported the type, number, and direction of
aircraft that flew above the town of Brunswick, until he was hit by a
nervous breakdown in early 1942.) From 1943 on he resumed the work on
analysis, but the difficulties intrinsic to the topic were great, as
were the practical difficulties of life caused by the war. Analysis
was to be formulated as a system of second-order arithmetic, which
means that quantification is extended over number-theoretic
predicates or, equivalently, over sets of natural numbers.
Second-order number theory is used in Gentzen's last paper, published
in 1943, in which it is briefly shown that the principle of
transfinite induction up to ε_{0} is derivable in
second-order number theory.

More than half a century has passed with no constructive proof of the consistency of full second-order arithmetic in sight. Early pioneers in this field included Kurt Schütte and Gaisi Takeuti. The former created in 1951 an infinitary sequent calculus to present consistency proofs in a perspicuous way, the latter instead used a more traditional Gentzen-style calculus.

In the current research in the proof theory of second-order
arithmetic, one studies what are known as subsystems of second-order
arithmetic. The strongest results as of today are, in a very brief
outline, the following: let *X* range over number-theoretic
predicates. A formula such as *X(x)* states that *x*
has the property expressed by *X*. We can now use first- and
second-order logic
to form compound formulas such as
∀*X*(*X*(*x*) ∨ ¬
*X*(*x*)). The collection of natural numbers for which
such a formula with one universal second-order quantifier holds is
called a Π^{1}_{1}-set (in this case, the whole of
the natural numbers). More generally, a comprehension axiom is of the
form ∃*X*(∀*x* *X*(*x*)
⊃ *B*(*x*)). If the formula *B* has no
second-order quantifiers, the axiom gives what is called arithmetic
comprehension or ACA. If *B* can have the form
∀*Y*∃*Z* *C*(*x*) with no
other second-order quantifiers, the special case of
Π^{1}_{2}-comprehension is obtained. Consistency
proofs for a subsystem of second-order arithmetic with
Π^{1}_{2}-comprehension have been given by
Toshiyasu Arai and Michael Rathjen in the mid-1990s.

## 6. Later developments in natural deduction

At the time when Gentzen worked out his system of natural deduction, Stanislaw Jaskowski was also developing a logical system for reasoning with assumptions. Formulas in derivations are arranged in a linear succession, but Jaskowski's paper of 1934 remained fragmentary and without substantial results such as a subformula property. The linear variant of natural deduction is followed in many pedagogical expositions of elementary logic (sometimes called “Fitch systems”). Gentzen found Jaskowski's work by June 1936, when both were in Münster, and considered its linear arrangement of formulas an improvement, a “liberation from the straitjacket of the tree form”, into one that reflects “the linearity of thinking” (the former from unpublished notes, the latter from Gentzen's thesis).

The system of natural deduction lay mostly dormant for some thirty
years, until the thesis of Dag Prawitz of 1965, *Natural Deduction:
A Proof-Theoretical Study*. The order in which Prawitz presented
the normalization theorem was different from the one in Gentzen's
early thesis manuscript. Prawitz gave first a normalization theorem
and subformula property for a system of natural deduction for
classical logic. This system contains no disjunction or existence. In
a second stage, he considered intuitionistic natural deduction for
the full language of predicate logic and reduced its normalization to
the deletion of detour convertibilities as in the fragment of
classical logic. When Gentzen's proof of normalization came to light
in 2005, Prawitz said, in conversation with the present author, that
it is clear that Gentzen knew the result, because the remarks in the
printed thesis are so suggestive.

In the late 1960s, *strong* normalization became an issue:
Prawitz, using previous work of William Tait and Jean-Yves Girard,
proved in 1971 that non-normalities in a derivation can be converted
in any order, with a terminating normalization process and a unique
normal derivation as a result. Gentzen seems not to have noticed the
latter, but seems to have thought rather the contrary, by the failure
of this property for the elimination of cuts in sequent calculus.

At about the same time as strong normalization was studied, the
*Curry-Howard* correspondence emerged. Curry had observed in his
work on combinatory logic in the late 1950's the analogy between
implication elimination in natural deduction and functional
application. The idea was as old as intuitionistic logic: by the
“BHK-explanation” of the connectives and quantifiers (for
Brouwer-Heyting-Kolmogorov), the forms of propositions in
intuitionistic logic express prescriptions on how to prove those
propositions: a conjunction *A*&*B* is proved by
proving *A* and *B* separately, a disjunction
*A*∨*B* by proving one of *A* and *B*,
and an implication *A*⊃*B* by showing how to
convert any proof of *A* into some proof of *B*, and so
on. These explanations come very close to the introduction rules of
natural deduction, but it remains unknown what their effect on
Gentzen's thought was.

The Curry-Howard correspondence, from a paper by William Howard of
1969, but published only in 1980, is based on the
“formulas-as-types” principle, or in another jargon, on
the “propositions-as-sets” principle. A proposition is
thought of as its set of proofs. Truth of a proposition corresponds
to the non-emptyness of the set. Proofs of
*A* ⊃ *B* are now functions from (proofs
of) *A* to (proofs of) *B* and
*A* ⊃ *B* itself the set of such
functions. Thus, if *f* :
*A* ⊃ *B* and *a* : *A*,
then functional application gives *f*(*a*) :
*B*. The reverse, corresponding to the introduction of an
implication, is captured by the principle of functional abstraction
of Alonzo Church's λ-calculus.

The Curry-Howard correspondence has made intuitionistic natural
deduction part of the computer science curriculum: it gives a
computational semantics for intuitionistic logic in which
computations, and the executions of programs more generally, are
effected through normalization. A proof of an implication
*A* ⊃ *B*, say, is a program that
converts data of type *A* into an output of type *B*.
The construction of an object (proof, function, program) *f*
of the type *A* ⊃ *B* ends with an
abstraction. When an object *a* of type *A* is fed into
*f* as an argument, the resulting expression is not normal,
but has a form that corresponds to an introduction followed by an
elimination. Normalization now is the same as the execution of the
program *f*. The use of intuitionistic logic is not tied to
any intuitionistic philosophy of mathematics, but is just a
systematic guarantee for the termination of the execution of computer
programs.

## 7. Later developments and applications of sequent calculus

Gentzen's doctoral thesis marked the birth of structural proof theory, as contrasted to the old axiomatic proof theory of Hilbert. A remarkable step ahead in the development of systems of sequent calculus was taken by Oiva Ketonen in his doctoral thesis of 1944. Ketonen, a student of mathematics and philosophy in Helsinki, went to Göttingen in 1938 to study proof theory with Gentzen — being the closest to a student the latter ever had. The connection seems to have been established by Ketonen's philosophy professor Eino Kaila who had met Gentzen in 1936 in Münster. Ketonen recollected later that Gentzen was “a sympathetic young man of few words” who gave him an introduction to the proof-theoretical systems and results. Ketonen's best-known discovery is a sequent calculus for classical propositional logic the logical rules of which are all invertible, meaning that whenever a sequent is of a form that matches the conclusion of a logical rule, the corresponding premisses, defined uniquely from the given sequent and the rule, are also derivable. The reverse is immediate (just apply the rule). Rules L& and L⊃, for example, are modified into

A,B,Γ→Δ

A&B,Γ→ΔL&

Γ →Δ,AB,Γ→Δ

A⊃B,Γ→ΔL⊃

There is just one left rule for conjunction (and dually just one right rule for disjunction). The left implication rule has what are called “shared contexts”: the assumptions and cases in the conclusion, except for the formula with the connective, are repeated identically in both premisses. Ketonen's idea was to define a system of proof search: one starts from a given sequent to be derived, chooses a formula in it, and writes the premisses of a rule that can conclude the given sequent. By invertibility, the question of derivability is replaced by one or two equivalent questions of derivability on simpler sequents. The new rules are needed to ensure uniquely defined premisses in such “root-first” decomposition.

Ketonen's proof of invertibility of the logical rules of his sequent
calculus used the structural rule of cut. Later Kurt Schütte
(1950) and Haskell Curry (1963) gave direct proofs of invertibility,
the latter with the explicit result that the inversions are *height
preserving*: if a given sequent is derivable in at most *n*
steps, the premisses in a rule that can conclude that sequent also
have a derivation in at most *n* steps.

How much of Ketonen's work stems from suggestions on the part of
Gentzen remains unknown, because no correspondence has been found.
Ketonen writes in the preface of his thesis that “Dr. G.
Gentzen of Göttingen directed me towards the problem area of
this work”. The thesis was Ketonen's only original work in
logic, saved from oblivion by a long review that Bernays wrote of it
for *The Journal of Symbolic Logic* in 1945.

One person who knew Ketonen's calculus in the late 1940s was Evert
Beth. When Beth later, in 1955, presented his well-known tableau
calculus, he seems to have forgotten the origin of the tableau
calculus as a reformulation of the one of Ketonen, but refers instead
to Kleene's influential *Introduction to Metamathematics* of
1952. Kleene had taken up Ketonen's calculus from the Bernays review
and also treated intuitionistic sequent calculus in which
invertibility is more restricted than in the classical calculus. With
Kleene's book, Gentzen's sequent calculi became generally known and
accessible.

Kleene's work of the early 1950's also pioneered a remarkable
development in sequent calculus, namely the
“contraction-free” classical and intuitionistic calculi
today denoted by *G3c* and *G3i*. These calculi have the
property that none of Gentzen's original “structural
rules” are needed. The rule of “weakening” permits
the addition of superfluous cases and assumptions, and the rule of
“contraction” the deletion of one copy of a formula if
two were present in a list, as in

WeakeningContraction

Γ →Δ

A,Γ→ΔWk

A,A,Γ→Δ

A,Γ→ΔCtr

Analogous rules permit weakening and contraction in the right,
succedent parts of sequents. Weakening is made an eliminable rule by
letting initial sequents have the form
*A*,Γ **→** Δ,
*A* instead of Gentzen's
*A* → *A*. Contraction is likewise made
eliminable by a suitable formulation of the rules. The import is that
in root-first proof search, no rules need be applied that would
produce a duplication of a formula in a premiss. Without this result,
non-termination of proof search would not follow.

The classical calculus has the property, mentioned above, of
height-preserving invertibility of its logical rules. Albert Dragalin
refined in the late 1970's the calculus into one in which the
structural rules are moreover “height-preserving
admissible”, meaning that whenever the premiss of such a rule
is derivable, the conclusion is derivable without the rule and with
at most the same size (maximum number of rule instances in a
derivation branch) of derivation. This property has profound effects
on cut elimination: in permuting cut up, Gentzen had to restore the
original contexts (the Γ's and Δ's) through weakenings
and contractions. With the height-preserving admissibility of these
rules, the size of a derivation does not increase when the rules are
applied. Dragalin gave also an intuitionistic multisuccedent calculus
with the same type of admissibility of the structural rules.
Troelsta, finally, gave in the textbook *Basic Proof Theory*
(2000, first ed. 1996) a single-succedent intuitionistic calculus
with height-preserving admissibility of weakening and contraction.
The contraction-free sequent calculi are powerful tools for the
analysis of formal derivations. Many difficult research results in
logic become just exercises through the control over the structure of
proofs that the *G3*-calculi permit.

The earliest application of sequent calculus in mathematics was in the proof theory of arithmetic, in Gentzen's thesis and in a decisive way in the 1938 proof of the consistency of arithmetic. Troelstra mentions Ketonen's work as “an early analysis of cutfree proofs in Gentzen calculi with axioms; but he considers the form of cutfree derivations in the pure calculus where axioms are present in the antecedent of the sequents derived” (Troelstra and Schwichtenberg 2000, p. 142). The axioms that Ketonen considers are those of projective and affine geometry, the former taken from Skolem's 1920 paper discussed in the first section above. Ketonen wanted to formulate Skolem's formal rules of proof within sequent calculus. However, Ketonen's work was mostly known only through its review by Bernays and only the logical part on sequent calculus was explained in detail there.

A second way to apply the sequent calculus is to let sequents that
begin derivation branches have, in addition to initial sequents, also
the form **→** *A*, in which *A*
is an axiom, or an instance of a universal axiom. Now, by Gentzen's
“extended Hauptsatz”, cuts in derivations can be permuted
up until one of their premisses is an axiom, but these cuts on axioms
remain. Another, newer method is to convert axioms into extra rules
that are added to the logical rules of sequent calculus, with full
cut elimination maintained (as explained in the book of Negri and von
Plato, chapter 6, and in Troelstra and Schwichtenberg's book, chapter
4.7).

## 8. The aims of proof theory

To what extent has proof theory achieved its original aims? For Hilbert, the aims were a complete clarification of the foundational problems through finitary proofs of consistency, etc, aims in which proof theory failed. Hilbert in his program was not interested in the study of mathematical proofs in themselves, but only in clearing the central foundational problems (and then to forget about them). A recently found note by Hilbert gives a different picture: the note states that Hilbert wanted to add as a 24th and last problem in his famous Paris list of open mathematical problems of 1900 the development of “a theory of proof methods in mathematics”. This was before his metamathematical program for the development of a proof theory emerged.

For Gentzen, the aims were, along with those of Hilbert, to understand the structure of mathematical proofs. This program was a complete success as far as pure logic and arithmetic are concerned. The methods of sequent calculus, especially, permit the analysis of proofs with profound results. The grand aim of proof theory, a proof of the consistency of analysis as in Hilbert's second Paris problem, has not been carried through but is not excluded, either.

Some understanding of the notion of proof is necessary for any
mathematician, if for nothing else, then at least for the
communicability of mathematical results: publication rests on the
understanding that proofs can be made as explicit as to be routinely
checkable for correctness. However, proof theory has so far not
become a practical tool for the working mathematician; the
applications in mathematics have been rather isolated cases. Recent
work on formalizing mathematical proofs with computerized systems,
called *proof editors*, may gradually change this picture.

Proof theory has created new aims outside traditional mathematics, especially in connection with computer science. Topics such as the verification of correctness of computer programs are an outgrowth of proof theory. Natural deduction has led to the Curry-Howard correspondence and to connections with functional programming, and sequent calculus is often used in systems of automatic proof search, as in logic programming.

## Bibliography

**Introductions to proof theory**:

- Negri, S. and von Plato, J.
*Structural Proof Theory*, Cambridge 2001. - Takeuti, G.
*Proof Theory*, North-Holland, 2nd ed, 1987. - Troelstra, A. and Schwichtenberg, H.
*Basic Proof Theory*, Cambridge, 2nd ed. 2000. - The
*Handbook of Proof Theory*(Sam Buss ed., 1998) contains reviews of specialized topics in proof theory.

**Original papers** (in order of first publication):

*Hilbert*: The central papers are found in English translation
in Van Heijenoort's *From Frege to Gödel*, Harvard 1967.
Consult, for the influence on Gentzen, also:

- Hilbert, D. Die Grundlegung der elementaren
Zahlenlehre,
*Mathematische Annalen*, vol. 104, pp. 484–494, 1931.

*Skolem*: The papers in logic are found in *Selected Works
in Logic*, ed. Fenstad 1970. Therein, pp. 103–136:

- Skolem, T. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze, nebst einem Theoreme über dichte Mengen, (original 1920).

*Gentzen*: The published papers can be found in English
translation in *The Collected Papers of Gerhard Gentzen* ed.
Szabo, 1969. The proof of normalization is in:

- Gentzen, G. The normalization of derivations,
*The Bulletin of Symbolic Logic*, vol. 14, pp. 245–257, 2008.

Other original material from Gentzen cited or referred to above is
from the biography *Logic's Lost Genius: The Life and Work of
Gerhard Gentzen*, by Eckart Menzler-Trott, American Mathematical
Society 2007.

- Gödel. K.
*Collected Papers I–V*, Oxford 1986–2003. - Jaskowski, S. On the rules of supposition in formal logic, (original 1934), in S. McCall, ed,
*Polish Logic 1920–1939*, pp. 232–258, Oxford 1967. - Ackermann, W. Zur Widerspruchsfreiheit der
Zahlentheorie,
*Mathematische Annalen*, vol. 117, pp. 162–1940, 940. - Ketonen, O.
*Untersuchungen zum Prädikatenkalkül*, (Annales Acad. Sci. Fenn, Ser. A.I. 23), 1944. - Schütte, K. Schlussweisen-Kalküle der
Prädikatenlogik,
*Mathematische Annalen*, vol. 122, pp. 47–65, 1950. - Schütte, K. Beweistheoretische Erfassung der unendlichen
Induktion in der Zahlentheorie,
*Mathematische Annalen*, vol. 122, pp. 369–389, 1951. - Kreisel, G. On the interpretation of non-finitist proofs: Part
I,
*The Journal of Symbolic Logic*, vol. 16, pp. 241–267, 1951. - Kleene, S.
*Introduction to Metamathematics*, North-Holland 1952. -
Beth, E.
*Semantic entailement and formal derivability*, Mededelingen der Koninklijke Nederlandse Akademie van wetenschappen, afd. letterkunde, vol. 18, no. 13, 1955. - Curry, H.
*Foundations of Mathematical Logic*, original 1963, Dover reprint 1977. - Prawitz, D.
*Natural Deduction: A Proof-Theoretical Study*, 1965, Dover reprint with a new preface 2006. - Prawitz, D. Ideas and results in proof theory, in J. Fenstad,
ed,
*Proceedings of the Second Scandinavian Logic Symposium*, pp. 235–308, North-Holland 1971. -
Howard, W. The formulae-as-types notion of construction, in J. Seldin
and J. Hindley, eds,
*To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, pp. 480–490, Academic Press 1980. - Dragalin, A.
*Mathematical Intuitionism: Introduction to Proof Theory*, American Mathematical Society 1988. - Rathjen, M. Recent advances in ordinal analysis;
Π
^{1}_{2}-CA and related systems,*The Bulletin of Symbolic Logic*, vol. 1, pp. 468–485, 1995.

**Secondary literature**:

- Bernays, P. Betrachtungen zum Sequenzen-kalkul,
in
*Contributions to Logic and Methodology in Honor of J. M. Bochenski*, pp. 1–44, North-Holland 1965. - Bernays, P. On the original Gentzen consistency proof for number
theory, in J. Myhill et al., eds,
*Intuitionism and Proof Theory*, pp. 409–417, North-Holland 1970. - Feferman, S. Highlights in proof theory, pp. 11–31 in V. Hendricks et al., eds.
- Hendricks, V. et al., eds,
*Proof Theory: History and Philosophical Significance*, Kluwer 2000. - von Plato, J. In the shadows of the Löwenheim-Skolem theorem: early combinatorial analyses of mathematical proofs,
*The Bulletin of Symbolic Logic*, vol. 13, pp. 189–225, 2007. - von Plato, J. From Hilbert's programme to Gentzen's programme (appendix in Menzler-Trott 2007).
- von Plato, J. Gentzen's logic, in
*Handbook of the History and Philosophy of Logic*, vol. 5, Elsevier, in press. - Smorynski, C. Hilbert's programme, (appendix in Menzler-Trott 2007).
- Tait, W. Gödel's reformulation of Gentzen's first consistency
proof for arithmetic: the no-counterexample interpretation,
*The Bulletin of Symbolic Logic*, vol. 11, pp. 225–238, 2005. - Troelstra, A. and Schwichtenberg, H.
*Basic Proof Theory*, Cambridge, 2nd ed. 2000), the historical notes at the end of each chapter.

## Related Entries

Boole, George | computability and complexity | epsilon calculus | Frege, Gottlob | Gödel, Kurt: incompleteness theorem | Hilbert, David: program in the foundations of mathematics | logic: classical | logic: intuitionistic | logic: second-order and higher-order | Peano, Giuseppe | proof theory | reasoning: automated | Russell, Bertrand | set theory