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

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

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

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

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

- 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*)=*x*_{1}. - 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*, apply orthogonality.*W*= >*B*→ Θ - 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.

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

- p. 380, proof of
Theorem 7.2.2[
*b*⇒*c*]: Putting*B*=*FX*. - p. 397, introduction to Section 7.5
(
**significantly wrong symbol**): μ =*U*·ε·*F*. - p. 403, Remark 7.5.12: V. Zöberlein.
- p. 415, Notation 7.7.3(b)
(
**significantly wrong symbol**):*Q*_{X}:*H*_{X}→*U*`*X*′.

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

- 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*=*id*_{S}. Show that*P*is a fibration. Find a fibration of posets that preserves neither ∧ not T.

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