# Additional errata to Practical Foundations of Mathematics

### 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].

## 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?

## 9  The Quantifiers

• p. 478, Proposition 9.2.3: ... and whose morphisms [plural] act as the identity ...

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