Practical Foundations of Mathematics

Paul Taylor

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:
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.