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 ε₀ 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 (PA₂), 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 ε₀ 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, this is the question of how fast a fast-growing function must grow for a statement about it to be unprovable in PA.