# Practical Foundations of Mathematics

Published in 1999 by
**Cambridge University Press**,
**ISBN 0-521-63107-6**.
Dewey Decimal Classification: 510-dc21.
Library of Congress Classification: QA 39.2.T413; Card number 98-39472.
British Library Shelf marks: 3015.9915 59 and YC.1999.b.5463.
Sales to 31 December 2005: 1311.
Volume **59** in the series
*Cambridge Studies in Advanced Mathematics*.
This series also includes books by
Peter Johnstone
and by
Jim Lambek and Phil Scott.
## Buy it online

**From the publisher, CUP: ** in the
UK or the
USA.
**From bookshops: **
Amazon
(UK)
(USA),
Blackwell's,
Barnes & Noble,
Powell's
or W H Smith.
**Via Price Comparison Sites: **
Abebooks,
Best Book Buys,
FetchBook,
Froogle (=Google)
(UK)
(USA) or
Pricegrabber.
## Read it online

The **18-page Synopsis** in DVI
or HTML
has links into the full text, on-line in HTML.
This crude HTML translation only includes the narrative and simpler
mathematical formulae, not the diagrams.
It was generated by TTH.
The bibliography is intended to list survey works,
texbooks and books with extensive bibliographies of their own
(to take the interested reader further afield as quickly as possible),
and intend to remove papers which only state the result which is
already treated in my book.
## Corrections

Two mathematically significant but localised errors have been found:
- p. 342, Lemma 6.5.7:
The unification algorithm need not terminate if the "occurs check"
fails, for example
*x* = *a* *b* *x*, *y* = *b* *a* *y*, *x* = *a* *y*.
The whole section needs to be reorganised,
as the "occurs check" is currently introduced after this Lemma,
- p. 523, Exercise 9.4:
Thomas Streicher sent me a simple counterexample to the claim that
fibrations preserve pullbacks.
The exercise was replaced by another similar one in the 2000 reprint.

Some other corrections were made in the 2000 reprint,
and there are a few more now.
## Back cover blurb (from the 2000 reprint)

*Practical Foundations* collects the methods of construction of
the objects of twentieth century mathematics, teasing out the logical
structure that underpins the informal way in which mathematicians
actually argue.
Although it is mainly concerned with a framework essentially
equivalent to intuitionistic ZF, the book looks forward to more subtle
bases in categorical type theory and the machine representation of
mathematics. Each idea is illustrated by wide-ranging examples, and
followed critically along its natural path, transcending disciplinary
boundaries between universal algebra, type theory, category theory,
set theory, sheaf theory, topology and programming.
The first three chapters will be essential reading for the design of
courses in discrete mathematics and reasoning, especially for the
"box method" of proof taught successfully to first year informatics
students.
Chapters IV, V and VII provide an introduction to categorical logic.
Chapter VI is a new approach to term algebras, induction and
recursion, which have hitherto only been treated either naively or
with set theory. The last two chapters treat dependent types,
fibrations and the categorical notion of quantification, proving in
detail the equivalence of types and categories.
The twin themes of structural recursion adjoint functors pervade the
whole book. They are linked by a new construction of the syntactic
category of a theory.
Students and teachers of computing, mathematics and philosophy will
find this book both readable and of lasting value as a reference work.

*From Peter Johnstone's review for Zentralblatt*:
This book deserves to become widely used and quoted, and will bring
about an altogether new level of understanding, by mathematicians and
informaticians, of how the other group thinks.
Although, in the later chapters, the going inevitably gets tougher,
the author's style remains user-friendly without becoming imprecise.
Taylor is extremely good at pointing out the (sometimes surprising)
sources of ideas that most of us take for granted.
A splendid and highly enjoyable book.
## Reviews

## Used in seminars or lecture series

*The links in the remaining sections of this page were collected
somewhat hurriedly from the first 150 out of over 800 links listed
by
Google.
I would be very pleased to hear of other relevant links, especially
to Masters' courses that have used the book.*

BRICS (DK),
Clemson (USA),
UNL (PT),
Texas.
## Cited in book lists

Algebraic Set Theory,
Frank Atanassow
(again),
BRICS,
Arthur Buchsbaum,
Peter Cameron,
Paolo Caressa,
Category Theory 101 Wiki,
Drexel Math Forum,
Adam Eppendahl,
Excite,
Functional Mathematics,
Haskell Bookshelf,
Haskell Wiki,
Hypography,
R B Jones,
Daikoku Manabu,
Just Pasha,
Psyche,
Joseph Kiniry,
Greg Lavender,
Paul-André Melliès,
Qoolsqool Algebra,
RU.math,
Alexander Sakharov,
Siddartha,
Salvador Vera,
UFRGS (PT),
Google Directory on Logic and Foundations,
## Web searches

Google Book Search,
CiteSeer,
Google and
Google Scholar.
This is
`www.PaulTaylor.EU/prafm/index.html`
and it was derived from `prafm/webpage.tex`
which was last modified on 14 February 2009.