Proof theory is one of the main branches in mathematical logic. Its original purpose was to secure the consistence of mathematics by finitary methods. This was part Hilbert’s program; the main goal was to show the correctness of mathematics using formal deductibility by means of a consistency proof. The principal requirement for the program to succeed was the use of finitary methods; in particular it should not use the principle of excluded middle. As is well known, the main objective of Hilbert’s program could not be attained, due to Gödel’s incompleteness theorems.
Proof theory has a technical mathematical aspect and a philosophical one, the latter specifically addressed to foundational problems and axiomatics. The book under review takes as its main point to challenge the reader by exhibiting the various instances where these aspects of its subject interact and influence each other. The ultimate, and ambitious, goal is to discuss and frame the nature of mathematical knowledge, its questions, answers, and the relations amongst them.
This goal also sets the style, so to speak, of the book: You will not find the usual set of definitions at the beginning (“a language is a finite alphabet …”, “a well-formed formula …”). Instead, you will find spirited discussions, historical remarks, small deviations, and the author’s opinions on the subjects being studied. In most of the standard expositions, almost all of these points are quickly swept under the carpet in order to get a clean, almost sterilized, presentation. As the author remarks, sometimes these points are not even seen, they are the “blind spots” that the title of the book refers to. The book retains the lively nature of its origin; it is more like a recording in front of an audience than an engineered recording in a studio.
I should point out, however, that the technical parts are also well covered. Gödel’s incompleteness theorem is discussed in the first chapter as well as the nature of incompleteness, undecidability and truth. Gentzen’s sequent calculus, cut-elimination and the Hauptsatz (the cut-rule is redundant in classical sequent calculus) appear in the first part of the book, which also includes a chapter on intuitionistic sequent calculus and Kripke models.
Lambda calculus, structured proof theory, the Curry-Howard correspondence, Martin-Löf theory and the interpretation in terms of Cartesian-closed categories are the main subjects of part II.
Part III, devoted to linear logic, starts with the closed monoidal category of coherent spaces and stable linear maps between them to set the framework for linear logic. After its interpretation, cut-elimination, completeness and the Hauptsatz are proved. This part ends with a chapter on proof-nets, a geometric device originally introduced by the author to represent the structure of a proof eliminating its irrelevant components.
Part IV focuses on another contribution of the author, ludics, an attempt to reconstruct a part of mathematical logic analyzing the interactions between the components of a proof using some sort of game-based interpretation (as the author puts it: “[If] logic is a sort of game, proofs are winning strategies”). The necessary sections on locations or loci are also included. For its applications to theoretical computer science, this is one of the most important parts of the book.
The last two parts of the book start with a quick trip to quantum logic, returning briefly to coherent spaces to show a link to the quantum world, as a finite-dimensional preamble to the methods of the geometry of interaction. This is also an original contribution of the author and takes its motivation from looking at proof-nets as some sort of special networks in a graph. To distinguish which networks are bona fide proof-nets, Girard introduced a criterion in terms of permutations or trips in this network and then reinterpreted this criterion as an operator in a corresponding Hilbert space. Girard’s main result in this context is the execution formula that encodes the cut-elimination process in terms of the corresponding operator. This approach is further generalized interpreting proofs as bounded operators in a suitable Hilbert space. Then, execution or cut-elimination becomes a solution of a linear equation, the so-called feedback equation.
There are several excellent textbooks and monographs in proof theory, from K. Schütte’s Proof Theory (Springer, 1977) and G. Takeuti’s Proof Theory (Elsevier, 1987) to W. Pohlers’ Proof Theory: The First Steps into Impredicativity (Springer, 2008). Girard’s book is welcome addition to the literature, with a fresh and playful approach, well suited for an author that gave us ludics and positive skunks as illustrations.
Felipe Zaldivar is Professor of Mathematics at the Universidad Autonoma Metropolitana-I, in Mexico City. His e-mail address is email@example.com.
Part I. The basics
Part II Around Curry-Howard
Part III. Linear logic
Part IV. Polarised interpretations
Part V. Iconoclasm
Part VI. Geometry of interaction