Jean-Yves Girard’s The Blind Spot: Lectures on Logic is an exposition of proof theory, challenging established notions and inviting reconsideration of the nature of mathematical knowledge. Intended for postgraduate students and researchers in logic, this work transcends mere technical exposition to engage with the philosophical underpinnings of logic itself, dissecting the relationship between questions and answers, and the implicit versus the explicit in mathematical discourse.
At the heart of Girard’s treatise lies the relation between the known and the unknown, the expressible and the inexpressible. He embarks on this intellectual journey by revisiting Gödel’s incompleteness theorems of 1931, highlighting the inherent limitations of formal systems in capturing the totality of mathematical truths. Gödel’s paradox serves as a catalyst for Girard’s deeper inquiry into the asymmetry between questions and their answers—a dynamic where answers are perpetually incomplete in relation to the questions that give rise to them.
Building upon this foundation, Girard goes into the paradigms introduced by Gerhard Gentzen’s cut-elimination techniques from 1935. Cut-elimination, a cornerstone of proof theory, becomes a pivotal theme as Girard navigates through various logical frameworks. He examines settings such as sequent calculus, natural deduction, lambda calculi, and category-theoretic compositions. Each of these frameworks serves as a lens through which Girard investigates the process of explicitation—the transformation of implicit knowledge into explicit form.
A significant portion of the book is devoted to the geometry of interaction (GoI), a concept Girard pioneered. GoI represents a radical shift in understanding logical operations, interpreting them through the lens of operator inversion in von Neumann algebras. This approach redefines the traditional perception of mathematical language, which is often seen as a mere reflection of preexisting reality. Instead, Girard proposes that logical operations possess an intrinsic procedural meaning. Operators within GoI are invertible not because they adhere to predetermined constructs, but because the very rules of logic are designed to ensure invertibility. This perspective positions logic as an active participant in the construction of mathematical reality, rather than a passive descriptor.
Girard’s discourse extends to a critical examination of the notion of truth and its presumed durability. He challenges the reader to distinguish between imperfect (perennial) and perfect modes of truth, suggesting that the infinite should be understood as the unfinished or the perennial. This line of thought leads to a contemplation of the very nature of perenniality and its potential impermanence. Through this questioning, Girard hints at a logical foundation for algorithmic complexity, proposing that the procedures we use to engage with infinity are themselves sources of complexity.
The book does not shy away from confronting the historical and philosophical contexts that have shaped modern logic. Girard reflects on the evolution of logic throughout the 20th century, critiquing its tendency towards totalitarianism in various forms, including the so-called “linguistic turn.” He argues that this shift led to an excessive formalism, where logic became entangled in bureaucratic protocols and lost touch with its mathematical and philosophical roots. This critique extends to specific domains such as model theory and set theory, where Girard perceives a detachment from meaningful mathematical structures in favor of overly simplistic or counterintuitive representations.
One of the recurring themes in Girard’s lectures is the concept of the “blind spot”—the aspects of logic and mathematics that remain unseen or unacknowledged due to inherent biases or limitations in our perspectives. He uses this metaphor to highlight how certain logical systems, such as quantum logic or modal logics like S5, fail to address fundamental inconsistencies because they operate within a framework that overlooks crucial procedural considerations. By bringing these blind spots to light, Girard encourages a re-evaluation of accepted logical principles and the development of more robust systems that account for these hidden complexities.
In exploring the dichotomy between essentialism and existentialism, Girard offers a nuanced analysis of their respective influences on the philosophy of mathematics. Essentialists, who view mathematical entities and truths as pre-existing and immutable, are contrasted with existentialists, who emphasize the constructed and procedural nature of mathematical knowledge. Girard aligns himself more closely with the existentialist viewpoint, advocating for a perspective that recognizes the dynamic and interactive processes that give rise to mathematical understanding.
This exploration leads Girard to critically assess foundational projects in logic and mathematics, such as set theory, Hilbert’s program, and Brouwer’s intuitionism. He examines set theory’s essentialist underpinnings and its reliance on concepts like actual infinity and the comprehension schema, which led to paradoxes like Russell’s antinomy. Girard discusses how subsequent refinements, such as Zermelo’s restrictions leading to ZF set theory, attempted to address these issues but still reflect an essentialist mindset.
Turning to Hilbert’s formalist project, Girard unpacks the ambition to ground mathematics in a finitary, formal system that prioritizes consistency over existential proofs. He critiques this approach for its reductionist tendencies and its ultimate inability to provide a satisfactory foundation for mathematical knowledge, especially in light of Gödel’s incompleteness theorems.
Brouwer’s intuitionism is presented as an alternative that challenges the essentialist and formalist traditions by rejecting the law of excluded middle in the context of the infinite and emphasizing the primacy of mathematical constructions over abstract existence claims. Girard acknowledges the strengths of intuitionism, particularly its recognition of the procedural aspects of mathematical truth, while also noting the difficulties it faces due to its radical departure from classical logic.
Throughout The Blind Spot, Girard consistently emphasizes the importance of procedural explanations in logic and mathematics. He argues that the durability of mathematical truths should not be assumed but rather examined through the lens of the processes that produce them. This perspective leads to a reconsideration of concepts like infinity, which Girard suggests should be understood as representing the unfinished or the ongoing, rather than a completed totality.
Girard’s work is characterized by its depth and originality, challenging readers to engage with complex ideas that bridge mathematics, logic, philosophy, and even touches of physics and computer science. His critique of the historical development of logic invites a rethinking of established doctrines and encourages the pursuit of new frameworks that better capture the procedural and dynamic nature of mathematical knowledge.
The Blind Spot is more than a collection of lectures on proof theory, it is a profound philosophical inquiry into the very foundations of how we understand and practice mathematics. Girard’s insights compel mathematicians, logicians, and philosophers alike to confront the limitations of traditional approaches and to explore the possibilities that emerge when we embrace a procedural and existential perspective on logic.
This book shows Girard’s position as one of the world’s leading proof theorists, offering a transformative vision that has the potential to reshape our understanding of logic and mathematics in the 21st century. It is a challenging read, demanding a high level of engagement from its audience, but the rewards are commensurate with the effort, providing rich material for reflection and further research in the foundations of mathematical thought.
Simon Gros 
Leave a comment