Review of Practical Foundations of Mathematics

Peter Johnstone
Zentralblatt für Mathematik

In 1971, Carl Linderholm published a book entitled Mathematics Made Difficult (Wolfe Publishing Ltd.; Zbl 217,1), in which he attempted to satirize the way in which (as he saw it) `abstract nonsense' was taking over the foundations of mathematics and making them incomprehensible. Nearly 30 years later, Paul Taylor has finally written the book of which Mathematics Made Difficult was a parody. That is not intended as a criticism of Practical Foundations of Mathematics; the reviewer has little sympathy with Linderholm's rather heavy-handed `humour', and is of the opinion that Taylor has written a splendid and highly enjoyable book. But the parallel between the two books is inescapable.
Taylor's book is both didactic and descriptive: it attempts to explain how mathematicians and informaticians (the latter being the author's appealing term for theoretical computer scientists) should view the foundations on which their work is based, but at the same time it attempts to tease out the logical structure underpinning the informal way in which mathematicians actually argue - both today and in previous eras of history. It is this latter feature which makes it very different from most books on the foundations of mathematics, but at the same time brings it closer to Linderholm's satire. (To take two examples, the detailed description of the history of the algorithm for solving the general cubic equation, and its presentation as a program in the semi-formal language developed by the author (p. 198), remind one irresistibly of the tribulations of M. Boulangiaire in chapter 3 of Mathematics Made Difficult. And the author's concern for Bo Peep's difficulties in counting her sheep, evidenced by Exercise 1.1 on p. 60, might have been lifted straight from Linderholm's discussion of whether one can use the same number-system for adding and for counting.)
Mention of exercises is a reminder that this book is, at least partly, intended as a textbook. What sort of students could benefit from courses based on it? The author's own suggestion is that `the first three chapters should be accessible to final year undergraduates in mathematics and informatics'; this is probably true, provided the mathematics undergraduates have rather more familiarity with programming languages (and the informaticians have more familiarity with non-discrete mathematics) than is usual. (And both groups would find the exercises pretty hard going.) It is, above all, beginning graduate students in both disciplines who will find this book most useful; it will prompt them to think seriously about the foundations of their subjects, and the relations between them, in a way that no other existing book (known to the reviewer) can achieve. Indeed, if it succeeds in becoming widely used and quoted (as it deserves to do), then it may bring about an altogether new level of understanding, by each of the two groups, of the way in which the other group thinks about the subject it studies.
At the heart of the book, not surprisingly, is category theory. It is therefore a little unexpected not to find a chapter headed `Introduction to Categories' or something of the sort; Chapter III on posets and lattices is immediately followed by a chapter entitled `Cartesian Closed Categories'. However, readers who are newcomers to category theory should not despair: Chapter IV does largely consist of an introduction to category theory (albeit a rather more condensed one than that found in most textbooks on category theory), and this together with Chapter V on `Limits and Colimits' will serve to introduce such readers to all the important concepts of the subject (except, rather oddly, for adjunctions, which are held back until Chapter VII, although adjoint functors between posets have been treated in Chapter III).
The author's other main theme is structural recursion, which forms the title of Chapter VI but which, like the categorical notion of adjoint functor, actually pervades the whole book. Chapter VI itself is a tour of various aspects of recursive definitions: free algebras, the general recursion theorem (formulated, in the style of Gerhard Osius, as a theorem about well-founded coalgebras), tail recursion, and Kuratowski-finiteness. But the thing which links all of these to each other, and to the categorical ideas which are omnipresent in the foundations of mathematics, is the notion of the syntactic category of a theory and the syntax/semantics adjunction. These topics are covered more fully in the last two chapters, which introduce the notions of dependent types, fibrations and the categorical notion of quantification. Although, in these later chapters, the going inevitably gets tougher (as befits the subject-matter), the author's style remains user-friendly without becoming imprecise: a student who works through to the end of the book will (rightly) feel a real sense of achievement, but there is no reason why he shouldn't get there if he perseveres.
The book's collection of references is splendidly eclectic; Taylor is extremely good at pointing out the (sometimes surprising) sources of ideas that most of us take for granted, and at finding apposite quotations to support his argument. Indeed, the reviewer suspects that many readers will gain more enjoyment from reading the footnotes than they do from the text of this book. (The reviewer's favourite footnote, a rare unattributed example, is on page 192.) Taylor's insistence on spelling out the forenames of cited authors, whenever he knows them, may at first seem irritating to a reader brought up on the tradition of initials-plus-surname, but one soon gets used to it. Indeed, by the time one reaches the Bibliography, one is tempted to wonder what crimes Godfrey Harold Hardy can have committed in Taylor's eyes, to cause him to be reduced to `G.H.'. (In this respect, if in no other, Taylor's book is inferior to Linderholm's!)

This is www.PaulTaylor.EU/prafm/Johnstone-review.html and it was derived from prafm/Johnstone-review.tex which was last modified on 14 February 2009.