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.