You are here

Proof Theory

Gaisi Takeuti
Dover Publications
Publication Date: 
Number of Pages: 
BLL Rating: 

The Basic Library List Committee recommends this book for acquisition by undergraduate mathematics libraries.

[Reviewed by
Michael Berg
, on

Five years ago I had the pleasure of reviewing Menzler-Trott’s biographical study of Gerhard Gentzen, the main player on the scene in the early days of proof theory. The extensive review by Solomon Feferman of the book now under review, published in the Bulletin of the AMS in 1977 (Vol. 83, No. 3. p.351ff.), starts off by noting that the book’s author, Takeuti, “places himself squarely in the line of development of Hilbert and Gentzen,” and this of course brings everything pretty clearly into focus. What we are dealing with here is a well-defined and active area of mathematical logic, equipped with a solid genealogy, namely, what came about in the wake of Hilbert’s program aimed at proving the consistency of mathematics, the derailment thereof wrought by Gödel, and the subsequent partial reconquistas effected by, prominently among others, Gentzen.

Takeuti’s Proof Theory is split into three parts, respectively, “First Order Systems,” “Second Order and Finite Order Systems,” and “Consistency Problems,” and obviously provides a long trajectory into the field, taking one from the basics of formal mathematical logic (quickly enough: Schütte’s proof approach to the completeness of first order predicate calculus (due of course to Gödel) appears already on p.40), through what are still pretty hot topics (I’ll never tire of the amazing proof of the incompleteness of Peano Arithmetic, on p.79 ff), to rather deep waters, at least to a fellow-traveler like me.

For example, after dealing with “a consistency proof of P[eano] A[rithmetic]” at considerable length, right after a discussion of ordinals from a finitistic perspective (which is a lynchpin of Gentzen’s approach; see the aforementioned review by Feferman), Takeuti starts off his Part II with gusto, going at material specifically tailored to proof theoretic goals and therefore of a more specialized or idiosyncratic nature than what came before. Evidently this is where (post-) Gentzen-style methodology is both motivated and laid out: we encounter, e.g., Gentzen’s famous “cut-elimination” procedure and infinitary logic manifesting determinate logic with equality as a special case (“with heterogeneous quantifiers”). But these deep waters are unquestionably worth navigating: all of the preceding sets the stage for the third and last part of the book, devoted in its entirety to “Consistency Problems” — and rightly so, of course.

But that’s not all. The present work being the second edition of the book, dating to 1986, Takeuti appends four articles which “will give the reader a good idea of many different aspects of proof theory,” written by Georg Kreisel, Wolfram Pohlers, Stephen G. Simpson, and, indeed, the aforementioned Solomon Feferman (who provides “a personal report”). This is a marvelous set of additions to an already very important book in its field. And, happily, it’s now published by Dover at under $25.

Michael Berg is Professor of Mathematica at Loyola Marymount University in Los Angeles, CA.

Preface to the Second Edition
Part I. First Order Systems
1. First Order Predicate Calculus
2. Peano Arithmetic
Part II. Second Order and Finite Order Systems
3. Second Order Systems and Simple Type Theory
4. Infinitary Logic
Part III. Consistency Problems
5. Consistency Proofs
6. Some Applications of Consistency Proofs