# 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
L^{A}T_{E}X 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:

^{1}Reply: 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.