# Errata to Practical Foundations of Mathematics

### 19 August 2000

First, I apologise to Heinrich Kleisli, Dito Pataraia, Maria Cristina Pedicchio, Dietmar Schumacher and V. Zöberlein for my mistakes in their names on pages 179, 403, 533, 540, 563, 566 and 572.

## Introduction

• p. x before Acknowledgements: topics in the mechanics of symbolic logic using the methods of category theory.
• p. xi: Ruth Horner died the very week that the book went to press, and Doris Wilson died during the following year.

## 1  First Order Reasoning

• p. 1, para 2: characteristic instead of remarkable - this seems to be a pretty good definition of the mathematical sciences.
• p. 7, Lemma 1.1.5: correctly forbids x to be free in a, because the substitution [a/x]*u is meant to result in a term that doesn't involve x. See Definition 4.3.11(b) for why.
• p. 17, Definition 1.2.10(a) (broken sentence structure): by at most one thing, i.e. any two (∀) solutions are equal (cfExample 1.8.2):
• p. 34, Remark 1.5.9: so the sign (positive or negative) of the influence of φ depends on whether it lies behind an odd or even number of implications.
• p. 37, Lemma 1.6.3, proof box, line 6 (significantly wrong symbol): should be ∃y.γ∧φ[y] in the left-hand box; for clarity, I have put (γ∧φ)∨… and …∨(γ∧ψ) in the right-hand box too.
• p. 60, Exercise 1.1: moved it from a pile ... [Hint: Exercise 3.63.] (I now think that the Schröder-Bernstein theorem is the proof of this, which will of course add fuel to Peter Johnstone's fire.)

## 2  Types and Induction

• p.93, before Remark 2.4.10: The failure of the disjunction property seems to mean that classical logic has no constructive interpretation.

## 3  Posets and Lattices

• p. 128, Warning 3.1.4: Any irreflexive relation < [insert "(∀x. x/ < x)"] can in fact be recovered from ( < )∪(=)
• p. 128: Example 3.1.6(c): The composite of two monotone functions (or of two antitone ones) is monotone.
• p. 132: Example 3.2.5(h) (misleading remark): Example 6.6.3(f) shows that ℑ ⊂ {⊥,T} can only be regarded as finite if it's decidable.
• p. 133: mark on plate in Example 3.2.8, near the right.
• p. 143, Definition 3.4.10 (misleading remark): the remark about being intermediate is a bit misleading, so the footnote on page 502 has been changed, but not this remark.
• p. 144, intro to Section 3.5 (significantly wrong word): the sum of posets or dcpos.
• p. 160, second paragraph of Remark 3.7.12: Cf [Con76, p. 66] (This was essentially the point of John Conway's "Mathematicians' Liberation Movement".)
• p. 162: "Modal logic has medieval and even ancient roots" belongs after Definition 3.8.2.
• p. 162, before Example 3.8.3(b'): but the second, partial correctness.
• p. 165: mark on plate in middle of Theorem 3.8.11(a).
• p. 176, Exercise 3.19 (significantly wrong word): posets or dcpos.
• p. 179, Exercise 3.45: Dito Pataraia.

## 4  Cartesian Closed Categories

• p. 238, after Proposition 4.8.3 (significantly wrong word): naturality, not normality.
• p. 243, Definition 4.8.15(c) (significantly wrong word): the right end of the first cell is the left end of the second.

## 5  Limits and Colimits

• p. 275, penultimate paragraph of Definition 5.5.1: The bottom row f the rectangle ... products. Then ...
• final paragraph (significantly wrong symbol): if c then
• p. 285 Corollary 5.6.12 (significantly wrong symbol): v(y)=x1.
• p. 288, Lemma 5.7.3: use W instead of K, for just this lemma, as it's about coequalisers in general rather than kernels. Conversely, given equal W = > B→ Θ, apply orthogonality.
• p. 290, diagram for Lemma 5.7.6(e) (significantly wrong symbol): (German) f;m and z;n instead of f;n and z;m.
• p. 295, Remark 5.8.4(e): The lifting property is not unique, but there's no room to insert this.

## 6  Structural Recursion

• p. 342, Remark 6.5.6: [Knu68, vol. 1, pp. 353-5] explains how to store the equivalence relation.
• p. 346, Example 6.6.3(f): a subset of a finite set is finite iff it is complemented cf. Example 3.2.5(h).
• p. 346, after Remark 6.6.4: the ambiguity in the usage of the word "law" mentioned in Definition 1.2.2.
• p. 350, Corollary 6.6.12: {⊥,T} is a join-semilattice; the unique join-homomorphism taking all singletons to T maps everything else there except ∅.
• p. 358, Remark 6.7.14: It is probably true in the concrete case of ordinals in Pos and Set that a sh-coalgebra is well founded in the sense of Definition 6.3.2 iff < is a well founded relation (Definition 2.5.3). Inability to formulate the abstract result for ordinals in A and C where there is an adjunction F −| U is the reason why I have not finished [Tay96b].
• p. 362, Exercise 6.23 (significantly wrong symbol): TΘ instead of T(Γ×Θ) at the top right of the diagram.

## 8  Algebra with Dependent Types

• p. 436, diagram for Example 8.1.12: the arrows marked [^(f)][^(x)] and [^(g)][^(z)] should have double arrowheads, but this hasn't been changed.

## 9  The Quantifiers

• p. 472 Notation 9.1.3: mark on plate near "Note that nothing we did in Chapter VIII".
• p. 480, Example 9.2.5, last paragraph: I find this example very confusing as the main one used to demonstrate.
• p. 487, Remark 9.3.1: several marks on the plate.
• p. 489, Remark 9.3.3, last line of the dotted proof box (significantly wrong symbol): [a/x, b/y]*f:θ.
• p. 491, Corollary 9.3.9: Our Frobenius law follows as a corollary.
• p. 502, Example 9.4.11(d) (misleading remark): The closed point of the Sierpi\'nski space does classify closed subsets intuitionistically. Any point of this space can be expressed as the join of a directed diagram taking only ⊥ and T as values, whilst (the dual of) the equation in Exercise 9.57 characterises support classifiers [Tay98].
• pp 505, after Corollary 9.4.16 (misleading treatment): Beware that, whilst our approach to the Beck-Chevalley condition does ensure that pullbacks of >-|>-maps are >-|>-maps, such pullbacks need not always exist in the category of locally compact spaces.
• p. 506, Section 9.5: In fact the formal rules also suggest that we should view comprehension as forming types or contexts from contexts.
• p. 519, Proposition 9.6.13[c⇒]: The infinitary version of Example 2.1.7 (rather than of its converse Exercise 2.14).
• p. 523, Exercise 9.4 (the one and only falsity): Thomas Streicher sent me a simple counterexample to the claim that fibrations preserve pullbacks. I have replaced the exercise with Let C and S be categories with pullbacks and P:CS a functor that preserves them. Suppose that P −| T with P·T=idS. Show that P is a fibration. Find a fibration of posets that preserves neither ∧ not T.

## Bibliography

• [BHPRR66] Essays on the foundations of mathematics.

This is www.PaulTaylor.EU/Practical-Foundations/errata.html and it was derived from prafm/errata.tex which was last modified on 22 July 2007.