The blind spot. Lectures on logic. (English) Zbl 1238.03045

Girard, Jean-Yves

Zürich: European Mathematical Society (EMS) (ISBN 978-3-03719-088-3/hbk). xiii, 537 p. (2011).

What a wonderful fresh breeze this book is, coming from the Mediterranean Calanques, blowing its potent winds over the cemeteries of dead ideas hoping for a revival of proof theory as a major player in a new iconoclastic approach to Foundations and perhaps even to computing. Jean-Yves Girard has written the manifesto for a revolution to come. He definitely is one who sees what he sees and says it loud and clear.
This book is the English translation of a series of lectures on proof theory given by Jean-Yves Girard at Università Roma Tre (Department of Philosophy) in the Fall of 2004. The last three chapters of the book are completely rewritten for the English translation, thus taking into account the latest developments. The book addresses mathematicians, computer scientists, physicists, philosophers and linguists. It must be said that the technical parts of the book are refreshingly illuminating and quite rigorous. On the other hand, the philosophical comments that are scattered throughout the book, and that are heavily present in the first part of the book, are definitely in the making and not very convincing at this stage. This is not to say that they are there for no good reason; the author of the book is one of the most important logicians of this century, one who has had more novel ideas than many others put together. However, it seems that it will take some time for the philosophical ideas in the book to crystallize into beacons, showing us the way.
We now describe the organization of the book and proceed to give a chapter-by-chapter synopsis.
The book is divided into six parts: (I) The basics (4 chapters), (II) Around Curry-Howard (3 chapters), (III) Linear logic (4 chapters), (IV) Polarised interpretation (4 chapters), (V) Iconoclasm (3 chapters), and (VI) Geometry of interaction (3 chapters). The book ends with a piece entitled “Envoi. The phantom of transparency”. The book has a very detailed index and a not very long bibliography, in particular work on categorical models for geometry of interaction is not mentioned at all! The first two parts can be used for a graduate course on proof theory where one can add a bit more to the categorical denotational semantics, whereas Parts III and IV can be used in a graduate course on linear logic and geometry of interaction. Parts V and VI (perhaps including some chapters from Parts III and IV for background) can form a very interesting seminar or research course on one of the most exciting research topics in the proof theory of linear logic and more potently in computational complexity from a proof-theoretical point of view where techniques and tools from the geometry of interaction program can be brought to play potentially significant roles.
Chapter 1 gives a brief critical account of the history of logic from the late 18th century to our times with a projection of some possible directions along which logic might evolve in the future. The main thrust of this chapter is the existence/essence dichotomy where essentialism accounts for the belief that all is already there and one just represents the archetypes, versus existentialism where things get perpetually reconstructed. The dichotomy is at the heart of typing (see Section 6F.) It is clear that the author adopts an existentialist view point throughout the book. The rest of the chapter discusses Hilbert’s project, Brouwer’s project , Gödel and after.
Chapter 2 discusses Gödel’s first and second incompleteness theorems and revisits Hilbert’s program in the face of these theorems.
Chapter 3 discusses the syntactical aspects of predicate logic with a brief mention of Hilbert-style systems versus the sequent calculus of Gentzen. It then gives a lucid account of Gentzens’s cut-elimination theorem (Hauptsatz). This is followed by a discussion of semantic aspects of predicate logic, and of infinitary proof theory.
Chapter 4 presents the intuitionistic logic and the systems LJ and NJ. The natural deduction systems NJ and LJ are also discussed in this chapter. This is followed by a brief discussion of logic programming and Kripke semantics.
Chapter 5 is the first chapter of Part II of the book and discusses the proofs-as-functions paradigm and the Curry-Howard isomorphism which is of great importance in at least the proof-theoretical view of computation and complexity.
Chapter 6 discusses Girard’s System F and its normalization theorem.
Chapter 7 is on category-theoretic interpretation of logic and discusses the perhaps most important class of categories of use in logic, namely Cartesian closed categories. It should be noted that the first section of this chapter gives a panoramic view of Girard’s thinking of logic and its stratification into multiple underground layers: \(-1, -2, -3\). This is a very important section to be read by anyone who wishes to understand the whole structure behind the book and the thinking of its author.
Chapter 8 is the first chapter of Part III of the book where the first model of Linear Logic (LL), namely coherent spaces, are discussed and shown to form a Cartesian closed category.
Chapter 9 introduces linear logic and shows how one can construct a denotational model for it using coherent spaces and linear functions. The classification of connectives of LL into perfect and imperfect is introduced and a brief discussion of \(*\)-autonomous categories, the categorical denotational models of the multiplicative fragment of LL, is also given.
Chapter 10 gives the phase semantics (provability semantics) for LL, proves the completeness theorem for this model and continues the discussion of perfect/imperfect connectives alluded to in Chapter 9. A discussion of focalization is also included in this chapter.
Chapter 11 introduces proof-nets, a syntax for LL and proves the sequentialization theorem (correctness criteria for proof-nets).
Chapter 12 is the first chapter of Part IV and it discusses the important notion of polarization. It also gives a discussion of game-related interpretations and relates to geometry of interaction (Chapter 19) and ludics.
Chapter 13 is a natural follow up from the previous chapter and takes on the more recent work by the author on designs and behaviours which prepares the reader for ludics.
Chapter 14 continues the discussion of the preceding chapter and introduces ludics: an attempt to reconstruct logic ex nihilo.
Chapter 15 discusses the exponential connectives where the author believes lies the actual blind spot of logic, where the door is opened to infinity, to perenniality. This chapter also includes a discussion of the Banach space denotational semantics for LL.
Chapter 16 is the first chapter of Part V of the book, perhaps one of the most exciting parts, where one finds a continuous flow of brave new iconoclastic ideas. The challenge of imperfect part of logic, of infinity is addressed in this chapter. A brief discussion of Light Linear Logic (LLL) and Elementary Linear Logic (ELL) is also given.
Chapter 17 introduces probabilistic and quantum coherent spaces and delves into a long introduction to \(C^*\)-algebras as preparation for the chapters to come in this and the next part of the book, especially those on the geometry of interaction. The author strongly believes that the mathematical setting of operator algebras is the most appropriate framework for studying and explaining logic.
Chapter 18 revisits proof-nets and the correctness criterion which is where the ideas on Geometry of Interaction (GoI) where initially conceived. It also gives a discussion of non-commutative logic.
Chapter 19 is the first chapter of the last part of the book and constitutes the most recent work by the author. The so-called feedback equation is discussed in this chapter and an excellent introduction to the first GoI is also given here. The feedback equation is naturally related to the notion of trace in categories (the work of Joyal-Street-Verity) and one could have added such a discussion here, but this is not included!
Chapter 20 discusses von Neumann algebras, the notion of factors and that of trace in a von Neumann algebra; it also discusses the Fuglede-Kadison determinant as preparation for the last chapter of the book.
Chapter 21 is the last chapter of the book and perhaps the most difficult for logicians to follow, but it is the belief of the reviewer that this is also the most exciting, novel and promising chapter of the book. The author brings together all the gadgets of factors, trace and determinants to build the newest version of the GoI. One of the most interesting and perhaps controversial concepts introduced here is the notion of subjective truth.
Envoi, which concludes the book, is a semi-philosophical and semi-technical overview of most of the topics discussed in the book, all viewed from the perspective of the “phantom of transparency”: the belief in the existence of an explicit and immediate world beyond perception, which in logic translates into semantics.

Reviewer: Esfandiar Haghverdi (Bloomington)

MSC:

03Fxx	Proof theory and constructive mathematics
03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03-03	History of mathematical logic and foundations
03A05	Philosophical and critical aspects of logic and foundations
03B10	Classical first-order logic
03B15	Higher-order logic; type theory (MSC2010)
03B47	Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B70	Logic in computer science
03F03	Proof theory in general (including proof-theoretic semantics)
03F05	Cut-elimination and normal-form theorems
03F07	Structure of proofs
03F52	Proof-theoretic aspects of linear logic and other substructural logics
03G30	Categorical logic, topoi
18C50	Categorical semantics of formal languages
18D15	Closed categories (closed monoidal and Cartesian closed categories, etc.)

Keywords:

classical logic; linear logic; geometry of interaction; proof theory; polarized logic; Curry-Howard isomorphism