Errors by Chapter
 Introduction
Part I: Proof Theory
 Ifs, Ands and Ors
 Page 13, line 10. The "or" really ought to be a "nor".
Thanks BG
 Page 15, displayed definition. The second
clause should be b(lm) if l >
m, not b(ml) if l >
m as it's written.
Thanks DS
 Page 15, footnote 5, sentence 2 should read: "For example, written words of English are wellordered by the
dictionary ordering."
Thanks MW
 Page 16, Lemma 2.9. I need the assumption
that the A_i and B_j are
formulas too, in order to prove the lemma.
Thanks DS
 Page 18, line 3. The sigma notation there
should have a superscripted n not an
l.
Thanks JCB
 Page 16, Lemma 2.9. I need the assumption
that the A_i and B_j are
formulas too, in order to prove the lemma.
Thanks DS
 Page 18, lines 13 and 3. That should be
"connectives of arity m" not
"connectives of arity i".
Thanks DS
 Page 23, last displayed proof. If you take
the order of premises in a proof to matter,
then the top of this proof should have its
premises switched.
Thanks DmS
 Page 24, second last sentence. It should
end "is still an instance of the rule," not "is
still an inference of the rule."
Thanks DS
 Page 30, Definition 2.27. Omit the "is" in
"is left residuates".
Thanks DS
 Page 31, line 3 from bottom. "can find a
proof of A > B" should be "can
find a proof of A  B".
Thanks DmS
 Page 32, line 7. The annotation on the rule
should be (>E).
Thanks AE
 page 32, line 3 from bottom: It should be
"in systems with K, we can...", rather
than "in systems with K' we can".
Thanks AE
 Page 34, Figure 2.1, Line 9. (vI) should
be (vE).
Thanks DS
 page 37, line 8: Peirce's law should be
(p > q) > p  p.
Thanks AE
 Page 38, line 2. That should be "This is
almost a proof of Y(X)B" not "This
is almost a proof of Y(A)B".
Thanks DS
 Page 40, Table 2.4: DBBlP' should be DBB'lP.
Thanks CK
 Page 40, line 7. There is an extraneous
right parenthesis. Delete it.
Thanks DS
 Page 45, Exercise {2.6}. There is no
doubt that F  F o A and F  A o
F are facts but they aren't
“important fusion facts.” I meant
to write “F o A  F and A o
F  F.” (I use F in HTML
for the upside down T in the text).
 Page 45, Exercise {2.7}. The implication
facts are written as T  A > T
and F > A  F The “F
> A  F” is in error. It
should be “T  F >
A”.
Thanks LH
 Page 45, Exercise {2.13}. "implication
rules" should be "elimination rules".
Thanks DS
"their rules" should really be "its rules". Thanks DDV
 Page 46, Exercises {2.16} and {2.17} are
much more interesting if you ask in which
logics are A < T and A <
t equivalent to A respectively
(not T and t, which is what
is written).
Thanks DS
 Modalities
 Page 49, Proof of Lemma 3.6. The leaves of the left displayed proof
should both read []A & []B  []A & []B. The next steps are
conjunction elimination steps to []A & []B  []A and []A &
[]B  []B. I was being naughty and not paying attention to the
actual natural deduction rules.
 Page 57, Left premise of the last fusion introduction step in the last
proof: the second turnstile should be a fusion.
Thanks DS
 Page 61, line 13. The last word should be "action" not "type".
Thanks DS
 Page 65, Lemma 3.27. The proofs don't follow the rules I gave. The
first line for the left proof is the premises for the second
proof, and vice versa! Then the proofs follow using the rules of
Definition 3.18.
Thanks DS
 Page 67, line 14. The middle arrow in the formula should be a
turnstile.
Thanks DS
 Page 67, Definition 3.37. We only need to specify one of the negation
rules, not both, given that the negation is de Morgan.
Thanks DS
In addition, the first negation rule there should be (~I;E), not (~I;~E). Thanks MW
 Page 68, First proof. The 0  t ought be t 
t.
Thanks DS
 Page 68, line 5: "particfular" should, of course, be "particular".
Thanks MW
 Page 68, After the proof. "tied the intensional structure": "to"
ommitted.
Thanks DS
 Page 69, The second proof is botched. Replace the rightmost
leaf with "A;B  AoB" and delete the second line of the proof.
Thanks DS
 Page 70, Exercise {3.4} is completely garbled. It should ask you to
find negation or structural rules necessary (and sufficient) to prove
 A > B  ~B > ~A
 ~B > ~A  A > B
 A > ~A  ~A
 ~T  F
 ~(A > F)  ~A > F
 ~(A > A)  F
Thanks HY
 Hilbert Systems
 Theories
 Page 90, Definition {5.6}. T is
~consistent if for no A is
both A in T and ~A in T.
Thanks HY
 Page 93, Definition 5.13: w
squaresuperset x should be w
squaresuperset y
Thanks DS
 Page 103, Exercise {5.9}, line 2 should start: "certain logics", not "certain with logics".
Thanks MW
 p. 93, second line: "neither ... nor", not "either ... or"
Thanks MP
 p. 93, definition 5.13: "if and only if v [subsethood symbol] x and w [subsethood symbol] y"
Thanks MP
 p. 95, third and fourth line: "it follows then that..."
Thanks MP
 p. 95, Proof for Corollary 5.19: "extending <T, {A}>" (brackets are missing)
Thanks MP
 Gentzen Systems
 Page 110, in the first two displayed
proofs, all the commas should be semicolons.
Thanks DmS
 Page 114, The mingle rule at the bottom of this page is stronger,
than the converse contraction form of mingle just above it. The text
labels it equivalent.
Thanks RD and SS
 Page 118, section 6.2, in the description of definition of 6.10. The bottommost derivation should have D as the consequent, since the C has been cut away.
Thanks PC
 Page 120, Lemma 6.14 has an extra 'then' inserted after "for all subformulae B
of A and for all consecutions C' and D'…"
Thanks SS
 Page 124, near the bottom there is a parenthetical remark
that says "(with just ~ and \lnot as structure)" but it should have
sharp and flat rather than the formula connectives. Further up that
page, the description of sharp and flat says only that they toggle
polarity from antecedent to consequent, when it needs to include the
other direction as well.
Thanks SS
 Formulas as Types, Proofs as Terms
Part II: Propositional Structures
 Defining Propositional Structures
 Page 158, Line 2. It should be the "strict order corresponding to <="
not the "partial order corresponding to <=".
Thanks DS
 Page 159, First proof. Should be "3 is not less than or equal to 2"
not "3 is not less than or equal to 4".
Thanks DS
 Page 160, line 14: The sentence "It is the bottom element ..." should read "An element
F is a bottom element of an ordering if and only if F <= a for every a."
(Note that F is the ascii for the upside down T symbol which looks like __.)
Thanks MN
 Page 163, line 12. Should be "(3 & 1) v (3 & 2) = F v 2 = 2",
not "(3 & 1) v (3 & 2) = T v 2 = 2".
Thanks DS
 Page 163, the definition of arbitrary joins and meets are mixed up.
Change the big Vee for the big Wedge and vice versa!
Thanks DS
 Page 165, Example 8.21. It should state that n' <= m
never, not that n' <= m when n < m.
Thanks DS
 Page 166, What I call "right conditionals" here are "left to right" in
Chapter 2, and even, "left" conditionals further on, in page 30! Oops!
Thanks DS
 Page 167, Definition 8.29 point 4. The second wedge should be deleted
in "wedge not wedge X".
Thanks DS
 Page 177, line 5: The union of two finite sets is finite, not cofinite.
Thanks DDV
 Manipulating Propositional Structures
 Categories
 Page 219: First commutative diagram, B x G should be B x C.
Thanks MW
 Page 220, line 2: A missing right parenthesis after C^op.
Thanks MW
 Page 223, final displayed rules: [B>C] should be [B=>C].
Thanks MW
 Page 225, Definition 10.30 (Adjoint Pairs): It should read
“G:D > C” rather than “G:D >
D.”
Thanks GW
Part III: Frames
 Frames I: Logics with Distribution
 Page 237, line 5: This sentence should read "So, if p is established at stage x, then p is
also established any later stage.".
Thanks DDV
 Page 240, line 7: "relative in a a simple way": delete one "a".
Thanks MW
 Page 241, line 9: "affect" should be "effect".
Thanks DDV
 Page 245, line 3 of Example 11.13: It should be "b = c, e = a and d = f", not "b = c, e = a and d = f".
Thanks MW
 Page 247, the first full sentence should read "In other words, x is of type A > B if and only if
whenever given an input of type A, its output is of type B".
Thanks DDV
 Page 249, lines 12 and 13: Strictly speaking the condition should be
forall x,x1,x2(SR(Y;X) > SR(X;Y)) and not its converse.
Thanks MW
 Page 252, line 4: The last "X" should be an "x".
Thanks MW
 Page 259, Theorem 11.37: Delete ", then" and replace by "."
Thanks DDV
 Frames II: Logics without Distribution
 Frame Constructions
Part IV: Decidability and
Undecidability
 Decision Procedures
 Page 321, line 15: "a product of the first m primes" should be "a product of the first k primes".
Thanks MN
 Undecidability
 Page 327, line 7: "where" should be "Where"
Thanks MN
Part V: Coda
 Using Substructural Logics
 Page 343, line 14: "these are world" should be "these are worlds".
Thanks DDV
