# 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 **S**et*
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.