History and philosophy of constructive type theory (Q1396584)

The book under review introduces the reader to Martin-Löf's Constructive Type Theory (henceforth CTT in short) from a philosophical and historical perspective. The motivation is twofold: since the end of the eighties, almost all Martin-Löf's papers deal with the philosophical aspects of type theory and there is no systematic discussion of its conceptual aspects. Similarly, the complex evolution of the theory is only sketchily touched in the literature. As to the content of the book, it is organized in four chapters. The first chapter focusses on the latest version (1995) of CTT which is available to the author, and it fills out almost one half of the whole book. It is in itself a self-contained monograph, yielding an overview of the basic ideas and principles underlying the theory. Great attention is paid to variants and hosts of comments and historical notes pervade the text. This shows the scholarship of the author, but it sometimes makes a smooth reading of the text not that easy. The second chapter, though more compact, is devoted to a bulk of philosophical and metatheoretical considerations about the 1995 version, mainly a discussion of identity (semantical identity, syntactical identity, etc.), the nature of judgements (distinction between analytic and synthetic in the light of type theory). While the logic of analytic judgments is decidable and complete, it is no more the case if you suppress the information concerning proof-objects and you deal with synthetic judgments. The incompleteness and undecidability results are then reinterpreted in the light of this distinction. The chapter ends with a comparison between CTT and the traditional viewpoints in the foundations of mathematics. The third chapter deals with the history of CTT in a proper sense from its birth (1970) to 1995, but it is structured according to the development of the basic features of the theory, which include, among others, the fixing up of the forms of judgment, the concept of type and its distinction from sets, the search for an alternative semantical approach (by contrast with the metamathematical one), the understanding of type theory as a working mathematical language, and its subsequent extensions motivated by constructive mathematics and computer science (e.g. universes, W-types), the identity issue, the question of reflection (i.e. iterating the construction of universes of higher and higher types). Finally, the appendix deals with the (temporary) tension between type theoretic and logical foundations, arising from the technical possibility of modelling parts of CTT into logical theories of proposition and truth, due to Aczel and Smith. The final chapter explores the sources of CTT within the history of logic from 1880 to 1970. The first section investigates how CTT is related to the main conceptions of logic of the last century: logic as universal language à la Frege/Russell vs. logic as calculus (in the light of the algebraic tradition and later of the metamathematical approach). The author claims that, while the second paradigm has become dominant, CTT has recovered essential features of the first tradition. The second section links CTT with technical developments of proof theory, mainly the Gentzen-Prawitz work on natural deduction, the Curry-Howard isomorphism, its extension to infinitary typed lambda calculus and infinitary intuitionistic propositional logic, the Tait-Girard method of computability predicates for proving strong normalization. In the conclusion the author underlines that the book is open ended, since CTT is still an ongoing enterprise. Future investigations are promised touching upon the relations of CTT with Husserl, Frege, Brouwer, Bolzano, Brentano, etc. The inspiration of the book and its motivation explain certain omissions. As the author himself warns us, no attempt is made to cover the applications of CTT to linguistics and computer science, and little emphasis is given to metamathematical investigation. Also, CTT is understood as a predicative theory of types in the sense of Martin-Löf; so no treatment is given of alternative approaches, like impredicative systems and generalizations thereof, from Girard's system F to the theory of constructions. The author adopts Martin-Löf's type theory as a benchmark for evaluating several issues pertaining to the philosophy of logic and mathematics in a wider sense. But he has a hard task in front of him, as CTT has a rather intricate conceptual and technical apparatus. We believe the book is a useful tool, especially for those who already have a working knowledge of CTT and are willing to reflect on its conceptual foundations. Indeed, for philosophers CTT represents an appealing bridge between phenomenology and analytical philosophy within the domain of philosophy of mathematics. We regret that the book -- dense as it is -- has no appropriate analytical /subject/name index.