# Errata to Practical Foundations of Mathematics

### 22 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. 4, Remark 1.1.1: The simplest operation on trees is substitution of another term for a variable. A copy of the expression-tree for the new term is made for each occurrence of the variable, and attached to the tree in its place. If there are many occurrences, the new term and its own variables are proliferated, but if there are none the new term disappears.

• 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. 9, Definition 1.1.9: In fact ... In this book we make (not make make) no systematic distinction.

• p. 17, Definition 1.2.10(a) (broken sentence structure): by at most one thing, so that 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 f 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.g\landf[y] in the left-hand box; for clarity, I have put (g\landf)Ú¼ and ¼Ú(g\landy) in the right-hand box too.

• p. 50, Remark 1.7.9(b): f[x] without an arrow under the x.

• p. 60, Exercise 1.1: She found a stick or a pebble for (to name'') each individual sheep, and moved it from a pile outside the pen to another inside. Any one object (not necessarily the sheep's own name''). [Hint: cf 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.)

• pp 60-1, Exercise 1.5: Show how to express a Turing machine as a system of reduction rules.

## 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\not < 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 again 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 a complemented subset.

• p. 133: mark on plate in Example 3.2.8, near the right.

• p. 143, Definition 3.4.10 (misleading remark): The type 2/W of truth values is playing a topological role here, in which the point T is open and ^ is closed. As such, 2/W is called the Sierpinski space and will be written S. As with R, in this book we shall avoid questions that rely on the intuitionistic nature of this space (see the footnote on page 502). (The remark about being intermediate'' is misleading, as 2/W is indeed the set of points of the Sierpinski space intuitionistically.)

• 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\rightrightarrows B® Q, 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 \prec 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\dashv U is the reason why I have not finished [Tay96b].

• p. 362, Exercise 6.23 (significantly wrong symbol): TQ instead of T(G×Q) 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:q.

• p. 491, Definition 9.3.6: the slanted pullback symbol has been made parallel with the relevant map.

• p. 491, Corollary 9.3.9: Our Frobenius law follows as a corollary.

• p. 502, Example 9.4.11(d) (misleading remark): Although ^ Î 2/W doesn't classify subsets in Set intuitionistically, in Sp the closed point of the Sierpinski space does classify closed subsets. Any point of S 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 again >-|>-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 and not types.

• 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:C®S a functor that preserves them. Suppose that P\dashv T with P·T = idS. Show that P is a fibration. Find a fibration of posets that preserves neither \land nor T.

## Bibliography

• [BHPRR66] Essays on the foundations of mathematics.