Review of Practical Foundations of Mathematics

Roy Dykhoff
Bulletin of the LMS

This is a fascinating and rewarding book, an "account of the foundations of mathematics (algebra) and theoretical computer science, from a modern constructive viewpoint". It is intended for "students and teachers of computing, mathematics and philosophy".
Mathematicians are now rarely interested in the foundations of their subject, either because (they think) the foundations impinge little on their own specialisms, or because they appear too restrictive, or (even worse) because their justification seems to be philosophical rather than mathematical. For many, Zermelo-Fraenkel set theory (including a choice axiom, usually in the form of Zorn's lemma) seems to be adequate, with occasional appeals to a set/class distinction, the continuum hypothesis or large cardinal axioms if apparently required. The underlying logic should of course be classical, following Hilbert and his enthusiasm for Cantor's paradise rather than Brouwer and his allegedly obscurantist views. In particular, it has been argued by some and felt by many that constructive mathematics is too limitative: that the results are too weak and some of the proofs are too difficult.
Several events led to the need for an alternative point of view. The shift began with the 1967 work of Bishop on constructive mathematics (especially on real analysis, later extended [] in collaboration with Bridges), continued with the work of Grothendieck, Lawvere et al on topos theory [], followed by the work [] of Martin-Löf on predicative constructive type theory (both for its own sake, as a firm foundation for mathematics, and for its role in software development) and the work of logicians and computer scientists, such as Abramsky, Aczel, Hyland, Jung, Pitts, Plotkin and Scott, on the semantics [] of programming languages, in particular the theory of domains and the theory of non-well-founded sets []. One key idea here is that what mathematicians have traditionally done, and one thing that computer scientists need to do, is to construct algorithms as solutions to problems. So, what then is the right foundation for this constructional activity? Constable [], for example, points out that, for formalisation of automata theory, including decidability results, one requires a formal theory that includes primitive notions of computability, in order to avoid presupposing the very subject being introduced.
Taylor's answer, like Constable's, is a version of intuitionistic type theory, based on constructive logic, i.e. the standard intuitionistic restriction of classical logic by non-assertion of the law of excluded middle. Bishop and Bridges showed that in such a framework one can develop a lot of useful analysis, including for example an adequate theory of integration, constructive analogues to fixed point theorems and a theory of Hilbert spaces. Note in particular the 1997 work (see []) of Richman and Bridges giving a constructive proof of Gleason's Theorem on measures on the closed subspaces of a Hilbert space. (It had been argued by some philosophers that this theorem was constructively invalid and that this was fatal for the constructivist programme: but the constructively invalid result was in fact just a classical reformulation of the theorem.)
The present book's focus is, instead, on the algebra (in a broad sense, including lattices, posets and category theory) that can be developed on such a foundation. (But then, the category theory can also be used as a foundation in turn, and that is what the present book is really about.) The book began "as the prerequisites for another book (Domains and Duality)", which it is hoped will appear in due course. The book's chapters cover first-order reasoning, types and induction, posets and lattices, cartesian closed categories, limits and colimits, structural recursion, adjunctions, algebra with dependent types and the quantifiers.
Chapter 1, on "First Order Reasoning", is typically non-standard and interesting: many topics are covered here that are left out of conventional foundational treatments, such as the difference between equations and reduction rules, the theory of descriptions and heuristics for proof discovery. The emphasis is on natural deduction, for its closer correspondence with actual reasoning than the use of Frege-Hilbert systems (with lots of logical axioms but few inference rules): it also happens to correspond better with constructive logic than with classical logic, for which the unnatural rule of reductio ad absurdum is required. There is a section on automated deduction, including a welcome treatment of the important topic of uniform proofs, the logical basis for logic programming in languages like Prolog (which, incidentally, is based on constructive rather than classical logic). Unification is covered carefully, without alas any remark to the effect that it was advocated for automated deduction by Herbrand and Prawitz before popularised by Robinson's theory of resolution (1965). The final section, on classical and intuitionistic logic, includes a section on the axiom of choice: it is not clear how this, involving as it does existential quantification over relations, fits in a chapter on first-order logic, at least not in the absence of some set theory.
Chapter 2, on "Types and induction", presents a constructive version of type theory, embellished for allegedly historical reasons with the name of Zermelo. This leads to the Curry-Howard analogy between propositions and types, according to which every logical connective is also a type constructor (e.g. implication corresponds to the function type operator). Induction and recursion, including structural induction on lists, are studied carefully: the chapter concludes with higher-order logic, including the second-order polymorphic lambda calculus of Girard. There is a discussion of the interesting phenomenon that there is no continuous "square root" function defined on the unit circle in the complex plane, despite Brouwer's view that all such functions are continuous. (This view is not shared by all constructivists: [] for example argues that it depends on extra-mathematical considerations. One way out is, as Taylor observes, to distinguish between e.g. the real numbers and Cauchy sequences, their representatives.)
Chapter 3, on "Posets and Lattices", begins on the metamathematical study of the semantics of the type theory considered so far, with the simplest case-posets (i.e. categories where any two arrows with the same source and target are equal). There is a double purpose here: the use of posets such as Lindenbaum algebras generated by the provability relation between propositions, and the use of ordered sets (e.g. Scott domains) "to illustrate many of the phenomena of reasoning, especially about non-terminating computation": in other words, as a semantics for programming languages. Chapter 4, on "Cartesian Closed Categories", takes this further: propositions generalise to types, provability to proofs and the categories of the title thus arise as models of the simply typed lambda calculus, a primitive version of constructive type theory. The remaining chapters develop this point of view, culminating in dependent type theory (where types can be parametrised by variables ranging over some simpler type) as required for both mathematics and software specification. There are splendid examples of (octagonal) commuting diagrams, that test to their limit the LATEX macros devised by the author (and for which other authors have reason to be exceedingly grateful). This reviewer is amused that some of his 1970s work on partial products, abandoned in the 1980s as unfruitful, turns out to be a key concept in the semantics of dependent type theory. Finally, there is a brief discussion of the much neglected Axiom of Replacement.
Almost every section has historical asides, e.g. that the "Sheffer stroke" was discovered at least as early as 1764 by Ploucquet. Incidentally, the Sheffer stroke is an extreme instance of a minimalist tendency, to reduce everything to as few primitives as possible: but electronic engineers willingly use devices other than "nand gates", and it is no longer fashionable to try to reduce all of mathematics to logic, despite the resurgence of logicism in some philosophical circles. This tendency led to an over-emphasis on classical logic and thus to failure to observe the important connections, extensively studied in this book, between (intuitionistic) logic and type theory.
Each chapter has several pages of subtle, provocative and imaginative exercises, varying from the trivial to unsolved research problems. The book finishes with an excellent lengthy bibliography and a decent index.
The book has several weaknesses. First, by focusing on algebra rather than analysis, it gives heart to those who, despite the evidence from (e.g.) [] still insist that constructive mathematics is inadequate for real mathematics. Second, the word "Practical" in the title needs more careful justification: the foundations are indeed those that are needed in practice for applications of mathematics in, e.g. computer science: but the connection with practical algebra, in the form of algorithms to solve algebraic problems, in group theory or ring theory for example, is not made sufficiently clear. Third, there are (of course) mathematical errors, but this is not the place to consider them all. (A list is promised for the web site.) As a first example, there is a failure to distinguish carefully between truth and validity, e.g. in the explanation (p 43) of the preservation of validity by logical rules ("i.e. whenever the premises are true, so is the conclusion" [replace "true" by "valid"]) and in the definition, as "proof and truth ... coincide", of completeness of a proof theory (no, completeness is when provability coincides with validity, i.e. truth in every interpretation). That this matters is shown up by Gödel's incompleteness theorem, that provability in any formalisation of classical first-order arithmetic (or, equivalently, arithmetic validity-truth in all models of the formalisation) is not equivalent to truth in the standard model. A second example is the suggested proof (p.120) that the Axiom of Choice, AC, implies the Law of Excluded Middle, LEM. According to the constructive meaning of "exists" the presented version of AC is an easy theorem [] of predicative constructive type theory 1, where LEM fails to be valid. So the "proof" depends on something additional such as the (non-constructive) use of power sets or equivalence classes. Finally, this reviewer found it at first odd and then irritating that most cited authors were given familiar forenames, particularly when they were not used consistently, and were sometimes quite unfamiliar. The family and friends of L. Egbertus J. Brouwer would have been surprised to see him referred to as "Jan" rather than as "Bertus".
Despite these imperfections, the book has many strengths. Its main strengths are its breadth, its use of examples from an amazing spread of mathematics and its history, its exercises and its coverage of key ideas in categorical logic. In summary, it is a magnificent compilation of ideas and techniques: it is a mine of (well-organised) information suitable for the graduate student and experienced researcher alike. Novice graduate students will however need a lot of help in staying afloat. A copy should be at least in every university library (if only one could decide whether the mathematicians, the computer scientists, the logicians, the philosophers or perhaps even the linguists should pay for it): experts in the field will want their own copies. Further details (e.g. chapter outlines) may be found at the author's website: www.dcs.qmw.ac.uk/ ∼ pt. There is even an HTML version of the book itself: book-lovers will be pleased to hear that it is far from adequate, in the absence so far of adequate HTML representations of mathematical diagrams.

References

[]
Aczel, P., Non-well-founded sets, CSLI Lecture Notes 14, Stanford 1988.
[]
Bishop, E. and Bridges, D., Constructive Analysis, Springer-Verlag, 1985.
[]
Bridges, D., Can constructive mathematics be applied in physics?, Journal of Philosophical Logic 28, 1999, pp 439-453.
[]
Constable, R. L., Formalising Decidability Theorems About Automata, in "Computational Logic" (eds. U. Berger and H. Schwichtenberg), Springer-Verlag, 1999, pp 179-213.
[]
Johnstone, P., Topos Theory, Academic Press, 1977.
[]
Martin-Löf, P., Intuitionistic Type Theory, Bibliopolis (Naples), 1984.
[]
Pitts, A. and Dybjer, P., Semantics and Logics of Computation, CUP, 1997.

Footnotes:

1Reply: Martin-Löf's proof is correct, but whether what he proves is the Axiom of Choice is open to dispute: this depends on his interpretation of the existential quantifier, which I reject in Section 2.4 of the book.

This is www.PaulTaylor.EU/prafm/Dyckhoff-review.html and it was derived from prafm/Dyckhoff-review.tex which was last modified on 18 August 2006.