Anne Troelstra and Helmut Schwichtenberg
Basic Proof Theory.
Cambridge Tracts in Theoretical Computer Science, no 43.
Cambridge University Press 1996, Cambridge, New York and Melbourne.
xi + 343 pp.

This book is, as stated on the cover, "an introduction to the basic ideas of structural proof theory,..., with cut elimination and normalization as central tools". It is intended to fill the gap between introductory books and text books (such as Kleene's 1952 classic) and the advanced monographs such as those by Sch"utte, Takeuti, Pohlers and Girard. 

Structural proof theory, as conceived here, is the study of sequent calculi (i.e. Gentzen calculi) and natural deduction systems, as initiated by Gentzen in the 1930s. Attention is given both to provability and to the proofs, as mathematical objects, themselves. 

Chapter 1 gives some basic information about various formal systems, including the typed \lambda-calculus and typed combinatory logic: it sets the stage for the rest of the book by illustrating, for implicational logic, various systems treated more thoroughly later: Gentzen-style ``G-systems'', Gentzen/Prawitz-style natural deduction (``N-systems''), and Frege-Hilbert style ``H-systems''. Chapter 2 looks in more detail at N-systems and H-systems; Chapter 3 treats several G-systems, with a progression from G1 (weakening and contraction explicit) through G2 (weakening built-in, contraction explicit) to G3 (weakening and contraction built into the logical rules, following ideas of Kleene and Dragalin). Use of multisets rather than sets builds the exchange rule into the notation. Classical, intuitionistic and minimal logic are all considered, organised with a systematic terminology. 

Chapter 4 treats cut elimination, the core of structural proof theory; thus, it shows that Cut is an admissible rule in some of the G-systems mentioned above. (The proof is incorrect: a new version is available in the list of corrections.)  Interpolation and definability theorems are proved for various cut-free systems. A further calculus, now called G4ip, in the progression of G-systems for intuitionistic propositional logic, is presented, following work by various authors; this has a termination property, and is thus even better for root-first proof search than G3(ip). 

Chapter 5  covers the (hyper-exponential) costs of cut elimination, giving also the improved bounds for intuitionistic propositional calculus found by Hudelmaier, for an inversion-rule strategy; it also proves the standard permutation theorems (of Curry and Kleene) for classical and intuitionistic predicate sequent calculi.  

Chapter 6 covers normalisation of various typed lambda calculi, illustrating Tait's method of computability predicates and giving Orevkov's examples for which normalisation generates hyperxponentially deep normal proofs. 

Chapter 7 expounds the connections between Gentzen systems and resolution, partly following ideas of Mints. It includes a careful (and thus useful) treatment of idempotent substitutions and unification. 

Chapter 8 is a detailed treatment of basic categorical logic, giving the categorical semantics of the (extensional) typed lambda calculus (with connectives for product and function types, but not, alas, for sum types). This leads on to the work of Mints and Soloviev on coherence problems in category theory.

Chapter 9 is an introduction to the proof theory of modal and linear logics, a welcome supplement (in the first case) to the extensive material elsewhere on their model theory. Of modal logics, only S4 is covered in any detail, along with the G"odel-Kolmogorov embedding of Int into S4 both for its own sake and as a means to study the Girard embedding of Int into classical linear logic. The notation of Troelstra (rather than Girard) is used for linear logic; cut elimination is proven for some G-systems for linear logic, and proof nets are characterised as the inductive proof structures, following the argument in Danos' thesis. There is (regrettably) no coverage of the conceptually basic topics of sequentialisation and cut-elimination for proof nets, covered however by Troelstra in his book on linear logic.  

In chapter 10 the emphasis moves from these purely ``logical'' calculi to the proof theory of arithmetic. There is a clear treatment of ordinal notations, followed by standard results about subsystems of arithmetic with induction restricted to low-level formulae, leading up to the unprovability of a Gšdel sentence for a minimal first-order arithmetic system and the undefinability of arithmetical truth for PA.  Finally, chapter 11 gives a brief introduction to second-order intuitionistic logic, Girard's "System F" and second-order Heyting arithmetic. 

Each chapter is well-equipped with exercises, historical notes and references. There is a good bibliography, list of symbols and notations,  and index. Troelstra maintains a (lengthy) list of corrections, available from his web page "http://www.wins.uva.nl/~anne": this review is therefore not the place for details of ``mistakes''. 

Readers who suspect that proof theory is not just the study of certain formal systems, showing that this calculus is equivalent to that calculus (and that each admits the Cut rule...), but has connections with deep philosophical and mathematical issues (such as Hilbert's programme), will be disappointed; it is not that kind of book, despite the material in the last two chapters. Nevertheless, this is a most useful book, coherently presenting a wide range of material, almost all with origins in Gentzen's work 60 years ago.  The style is clear and attractive; the layout and typography are excellent (unlike some earlier volumes in the Cambridge Tracts in TCS). The book is at a level accessible to, and should (with the correction list) be required reading for, most graduate students of logic (and many students of theoretical computer science). Those working in automated deduction, logic programming, category theory, type theory, lambda calculus or functional programming will all find material here of interest.  



Roy Dyckhoff (St Andrews)