An Introduction to Substructural Logics | Errata
Places: Main | Solutions | Links | Errata | Comments | Author
This page will contain information about all errors in An Introduction to Substructural Logics. If you find errors in the book you should check this page first and then if the error has not been reported here, please send an email indicating the error to Greg.Restall@mq.edu.au with “ISL: Errata” in the subject field. Your help will be appreciated not only by me, but also by the other readers of the book.

I'm grateful to the following people who have submitted errata: AE Antony Eagle; BG Brendan Gillon; CK Chris Kane; DDV Dave De Vidi; DS David Scarratt; DmS Dmitry Shkatov; GW Graham Wrightson; HY Hongseok Yang; JCB JC Beall; LH Lloyd Humberstone; MN Matti Nykänen; MW Michael Warren; NC Neus Castells.

Errors by Chapter

  1. Introduction

    Part I: Proof Theory

  2. 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(l-m) if l > m, not b(m-l) if l > m as it's written.
      Thanks DS
    • Page 15, footnote 5, sentence 2 should read: "For example, written words of English are well-ordered 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
  3. 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
  4. Hilbert Systems
    • Page 73, line -2. This is a terrible error. The last axiom on this line should not be (A -> C) & (B -> C) -> (A -> B v C) but should be (A -> C) & (B -> C) -> (A v B -> C)
      Thanks HY
    • page 85, proof of AoB -> C |- A->(B->C). This "proof" is completely wrong up to the consecution (AoB -> C);(A;B) |- C. Replace the top of the proof with 
                            A |- A  B |- B
                      --------------
AoB -> C |- AoB -> C    A;B |- AoB
----------------------------------
      (AoB -> C);(A;B) |- C
      and you have a genuine proof.
      Thanks NC
    • Page 87, line 19. In this proof I say Sigma |- t & A -> B. This doesn't make any sense, as I haven't defined |- as a relationship between sets and single formulas. I should say Sigma |-_H t & A -> B.
      Thanks HY
  5. 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
  6. Gentzen Systems
    • Page 110, in the first two displayed proofs, all the commas should be semicolons.
      Thanks DmS
  7. Formulas as Types, Proofs as Terms
    • Page 138, line 2: The rule should contact to N[x:=M].
      Thanks MN
    • Page 138, second proof fragment. It should read 
                    Sigma(x:A;y:B)|-N:C/\D
              ------------------------
Delta|-M:AoB  Sigma(x:A;y:B)|-fst(N):C
--------------------------------------
Sigma(Delta)|-let M be xoy in fst(N):C
      Thanks MN

    Part II: Propositional Structures

  8. 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 co-finite.
      Thanks DDV
  9. Manipulating Propositional Structures
  10. 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

  11. 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
  12. Frames II: Logics without Distribution
  13. Frame Constructions

    Part IV: Decidability and Undecidability

  14. Decision Procedures
    • Page 321, line 15: "a product of the first m primes" should be "a product of the first k primes".
      Thanks MN
  15. Undecidability
    • Page 327, line 7: "where" should be "Where"
      Thanks MN
    Part V: Coda
  16. Using Substructural Logics
    • Page 343, line 14: "these are world" should be "these are worlds".
      Thanks DDV
Places: Main | Solutions | Links | Errata | Comments | Author
This page is maintained by Greg Restall. Last modified May 17, 2002