• Page 5, "if it occurs syntactically within G," should be "F" [Kwanghoon Choi]
• Page 33, Exercise 1.3: final \vee ("or") should be a \wedge ("and") [Eric]
• Page 49, Examples 2.21; page 50, Example 2.23: Line 3 of the first proof (and similarly for the others) is both unnecessary and not according to an inference rule listed in the book. Instead, split on line 2 and proceed.
• Chapter 4: Every use of T_\cons should be T_\cons^+ (the theory of acyclic lists).
• Page 66, top: In the final characteristic formula, F should be \neg F [Mathias Preiner]
• Page 68, Exercise 2.3 (e): \exists y. G should be \exists x. G to avoid capturing a free variable y in G
• Page 86, bottom: The axiom should specify that car(x) = x and cdr(x) = x [Roberto Sebastiani]
• Page 88: "where is has value w" should be "where it has value w" [ThanhVu Nguyen]
• Page 98, Example 4.2: \cons(d) should be d [Ben]
• Page 109, middle: "each possible formaulae" => "each possible formula" [Brandon]
• Page 109, Example 4.10: two instances of \vee should be \wedge (same issues as Exercise 1.3) [Zyad Hassan]
• Page 116, middle: should be "on the *right* half if a[m] < e and on the *left* half if a[m] > e" [Zyad Hassan]
• Page 136, bottom: Figure 5.22 should be referenced, not Figure 12.1 [Miquel Bertran]
• Page 151, Figure 5.25: "j" should be declared outside of the inner loop, and "t" should be included in r₁ and r₂
• Page 166, Figure 6.3: "a = a" in the construction of the qs instance should be "array = a"
• Page 167, Figure 6.4: the third row is incorrect, as the 5 and 6 are inverted [ThanhVu Nguyen]
• Page 188, bottom: x should be x' [Karl]
• Page 189, bottom: F should be F_4
• Page 197, top: F_5 actually has the form of a disjunction of such formulas [Yan Zhang]
• Page 202, second full paragraph: Every F_4 should be F_3
• Page 271, Example 10.3: Function and predicate symbols can evaluate arbitrarily on tuples of D_J elements that include at least one A element.
• Section 3.6, Chapter 11: The basic theory of arrays T_A should include an axiom schema asserting that the domain is infinite: for each positive integer n, forall x1, ..., xn. exists y. y != x1 && ... && y != xn. This schema is unnecessary for arrays with integer indices T_A^Z.
• Page 295, bottom: F should be F_3
• Page 305: Two additional axioms are required for the theory of hashtables: [Sebastien Bardin]
  • keys-put 2: \forall h,j,k,v. j \ne k \rightarrow (j \in keys(put(h,k,v)) \leftrightarrow j \in keys(h))
  • keys-remove 2: \forall h,j,k,v. j \ne k \rightarrow (j \not\in keys(remove(h,k,v)) \leftrightarrow j \not\in keys(h))