Errata to Practical Foundations of Mathematics
Paul Taylor
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
(cf. Example 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.
7 Adjunctions
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:C→S 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.