Additional errata to Practical Foundations of Mathematics
Paul Taylor
19 August 2006
The following corrections should be made to the 2000 reprint,
which itself corrected these mistakes.
1 First Order Reasoning
- p. 4, Remark 1.1.1, para 3:
maybe object instead of record nowadays.
- p. 6, Definition 1.1.4:
structural recursion, not induction.
- p. 7, Lemma 1.1.5:
on the right hand side of the second displayed formula,
add an asterisk, making
[[a/x]*b/y]*[a/x]*t.
- p. 47, Remark 1.7.4:
We put [(b)\vec] [not [(a)\vec]] for [(x)\vec].
2 Types and Induction
3 Posets and Lattices
4 Cartesian Closed Categories
5 Limits and Colimits
- p. 292, Section 5.8:
Categories of algebras inherit this good behaviour from Set
for quotients of congruences...
- p. 294, Proposition 5.8.3:
... and so it is the E class of the image factorisation.
6 Structural Recursion
- p. 342, Remark 6.5.6:
It should explain how the equivalence class is stored.
Also, in (c), should have y in place of x′.
- p. 342, Lemma 6.5.7:
significant mathematical error:
the algorithm need not terminate if the "occurs check" fails,
for example consider x = a b y, y = b a x, x=a y.
- p. 344, Section 6.6, 4th para:
add cross reference to Theorem 5.6.9.
Also, 5th paragraph should mention Richard Dedekind.
- p. 361, Exercise 6.22: subscripts?
7 Adjunctions
8 Algebra with Dependent Types
9 The Quantifiers
Bibliography
- L.E.J.' Brouwer was known as Bertus.
- The date of Bart Jacobs' thesis is 18 September 1991.
- p. 543, [Law66] Bill Lawvere, for consistency.
This is
www.PaulTaylor.EU/Practical-Foundations/errata2.html
and it was derived from prafm/errata2.tex
which was last modified on 30 May 2008.