Book Excerpts:
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.
The book is an account of the foundations of mathematics (algebra) and
theoretical computer science, from a modern constructive viewpoint. It is intended, amongst other things, to provide a bridge between the use of logic underlying mathematical constructions and its abstract study in disciplines such as the
lambda calculus,
predicate calculus,
type theory and
universal algebra. It began as the prerequisites for another book (Domains and Duality), so it contains very little domain theory itself, but it does treat the fundamental issues of the semantics of programming languages.
Mathematical and computing issues are interwoven. For example the classifying category for an algebraic theory is defined as a declarative programming language, which is in turn illustrated by the solution of
cubic equations.
Category theory plays a major role in the book, but the abstract concepts are introduced on a "need to know" basis. Emphasis is placed on how functoriality, naturality, uniqueness, universality and pullback-stability carry the force of the constructions and properties (such as invariance under substitution), rather than allowing the reader to think that these are merely bureaucratic side conditions. Wherever possible, the poset analogues of categorical results are given first.
Excluded Middle is avoided, being largely irrelevant to algebra and category theory (these are often done "inside a topos"). However just as it is easier to teach a baby to swim before it has learnt the fear of water, so it is simpler to be constructive from the beginning with naive set theory than to recover it later with
Kripke models or
Grothendieck toposes.
Every result has been taken apart, sharpened, polished and re-assembled, so most of the sections contain material which is in some way original, and much of it could have been published individually. However much of the value of the book is that it deliberately blurs distinctions between disciplines, resolving numerous apparent conflicts of viewpoint which would never have been considered so thoroughly if they had been treated separately.
Intended Audience:
Students and teachers of computing, mathematics and philosophy should find this book both readable and of lasting value as a reference work.
Review(s):
Roy Dyckhoff,
University of St Andrews
:) "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."