Springer, NY, 2015, 561 pp.

**ACM CR categories:**

F.4.1 Mathematical logic - proof theory

K.2 History of computing - People

This book is the follow-on to the 2009 symposium in Leeds celebrating the centenary of the great German logician Gerhard Gentzen. It contains survey as well as technical chapters by highly respected proof theorists. It is of interest to logicians and computer scientists working in theorem proving, type theory, and proof complexity.

Gentzen, a student of David Hilbert's colleague Paul Bernays, started the field of proof theory after Kurt Gödel showed, in 1931, that Peano arithmetic (PA), the first-order theory of the natural numbers with addition and multiplication, could not prove its own consistency. Gentzen analyzed proofs; developed methods such as sequent calculus and natural deduction; and proved the cut elimination theorem, which allowed proofs to be put into normalized form.

From von Plato's chapter, based on recently uncovered documents,
I learned that Gentzen asked himself questions such as
"Where is the Gödel-point hiding?" Gentzen recursively assigned ordinals
to each reduced derivation, so that each proof rule led to a decrease in the
ordinal. Buchholz's chapter shows that his first proof
(which I did not know about) was criticized by Bernays and Gödel for
unjustifiably using induction on trees. In 1936, Gentzen directly used
induction on sets of quantifier-free formulae of the ordinal
ε_{0} to prove consistency.
(This ordinal is the supremum of the ordinals
{ω,ω^{ω},...}.)
He also proved, in 1943, that using induction for a lesser ordinal would not
suffice. Gödel called Gentzen a better logician than himself.
In 1958, Gödel gave a different consistency proof for PA using
functionals of finite type, which is known by the name of the journal
*Dialectica* in which this paper was published.

Gödel's original goal, and that of Gentzen until he died in a Czech
prison camp after World War II, was the consistency of analysis,
in logical terms, second-order Peano arithmetic (PA2), where the kind of
arguments used seemed unjustified to people like Hilbert working on the
foundations of mathematics. Ferreira has contributed a chapter on a 1962 proof
of the consistency of analysis by Clifford Spector, who also died young.
Spector pointed out that his proof, following Gödel's *Dialectica*
approach, relies on the consistency of a method called bar recursion.
Tait showed this consistency in 1971 without producing a measure of
proof-theoretic strength as Gentzen did, so there remains an open question.

I also enjoyed reading Rathjen's chapter on how Reuben Goodstein, in 1944,
produced from a descending sequence of ordinals below ε_{0}
a sequence of integers. The independence of the termination of such
sequences from PA was shown by Kirby and Paris in 1982;
Rathjen argues that such a proof was within Goodstein's reach.
Another enjoyable chapter by Meskens and Weiermann studies these sequences
as well as Hydra games: roughly speaking, the question is how fast
a fast-growing function must grow for a statement about it to be
unprovable in PA.