by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic and Semantics, entry directory]
[Graham Priest, entry directory]
[Priest, Introduction to Non-Classical Logic, entry directory]
[The following is summary of Priest’s text, which is already written with maximum efficiency. Bracketed commentary and boldface are my own, unless otherwise noted. I do not have specialized training in this field, so please trust the original text over my summarization. I apologize for my typos and other unfortunate mistakes, because I have not finished proofreading, and I also have not finished learning all the basics of these logics.]
Summary of
Graham Priest
An Introduction to Non-Classical Logic: From If to Is
Part I
Propositional Logic
2.
Basic Modal Logic
2.4.
Modal Tableaux
Brief summary:
(2.4.1) Tableaux in modal logic take the same branching node structure as those for propositional logic. However, the nodes themselves have a different structure, and there are two possible ones. {1} A, i, where A is a formula and i is a natural number indicating the world in which the formula holds, or {2} irj, where i is a natural number for a world that accesses world j, also given as a natural number (the r stays as r). (2.4.2) We test for validity by setting the premises to true in world 0 and the negation of the conclusion to true in world 0. (2.4.3) The tableaux rules for modal logic are the same as for non-modal propositional logic, except we indicate the worlds involved, and the branches inherit the world indicators from above (they are listed below with the new ones). (2.4.4) There are four new tableaux rules for modal operators. (Here we list all rules together):
| Double Negation Development (¬¬D) |
| ¬¬A,i ↓ A,i |
| Conjunction Development (∧D) |
| A ∧ B,i ↓ A,i B,i |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B),i ↓ ¬A ∨ ¬B,i |
| Disjunction Development (∨D) |
| A ∨ B,i ↙ ↘ A,i B,i |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B),i ↓ ¬A,i ↓ ¬B,i |
| Conditional Development (⊃D) |
| A ⊃ B,i ↙ ↘ ¬A,i B,i |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B),i ↓ A,i ↓ ¬B,i |
| Negated Necessity Development (¬□D) |
| ¬□A,i ↓ ◊¬A,i |
| Negated Possibility Development (¬◊D) |
| ¬◊A,i ↓ □¬A,i |
| Relative Necessity Development (□rD) |
| □A,i irj ↓ A,j
(both □A,i and irj must occur somewhere on the same branch, but in any order or location) |
| Relative Possibility Development (◊rD) |
| ◊A,i ↓ irj A,j
(j must be new: it cannot occur anywhere above on the branch) |
(24)
(2.4.5) Branches close when there are contradictions in the same world. (2.4.6) Priest provides examples to show how the tableaux are made. (2.4.7) We make counter-models using completed open branches. We assign worlds in accordance with the i numbers. We assign R relations in accordance with irj formulations. And nodes of the form p, i we assign vwi(p) = 1. And for nodes of the form ¬p, i, we assign vwi(p) = 0. If there are neither of these two, then vwi(p) can be given any value we want. (2.4.8) Priest shows how to make a counter-model with an example. (2.4.9) These tableaux are both sound and complete.
[Node Structures of Modal Tableaux]
[Modal Tableaux Initial Set-Up]
[World Inheritance]
[Tableaux Rules for Modal Operators. (All Rules Given in Total).]
[Branch Closing]
[Tableaux Examples]
[Counter-Models]
[Counter-Model Example]
[Soundness and Completeness of the Tableaux]
Summary
[Node Structures of Modal Tableaux]
[Tableaux in modal logic take the same branching node structure as those for propositional logic. However, the nodes themselves have a different structure, and there are two possible ones. {1} A, i, where A is a formula and i is a natural number indicating the world in which the formula holds, or {2} irj, where i is a natural number for a world that accesses world j, also given as a natural number (the r stays as r).]
We will now learn the tableaux rules for modal logic, which “are similar to those for propositional logic (1.4)” (24). At each node we will write something taking one of two structures. {1} There may be a formula and a natural number, with a comma between them. Suppose i stands for a natural number and A for a formula. For this structure, then, it would be given as A, i. The natural number in this and in the follow case stands for different possible worlds. Or {2} there may be an indication of world accessibility, written under the form irj, where in actual cases the r will remain as r, but the i and j will be natural numbers standing for worlds, with the sequence meaning that world i accesses world j.
Tableaux for modal logic are similar to those for propositional logic (1.4), except for the following modifications. At every node of the tree there is either a formula and a natural number (0, 1, 2,. . .), thus: A, i; or something of the form irj, where i and j are natural numbers. Intuitively, different numbers indicate different possible worlds; A, i means that A is true at world i; and irj means that world i accesses world j.3
(24)
3. I will avoid using r as a propositional parameter where this might lead to confusion.
(24)
[Modal Tableaux Initial Set-Up]
[We test for validity by setting the premises to true in world 0 and the negation of the conclusion to true in world 0.]
[Recall from section 1.4.5 that a tableau is “complete iff every rule that can be applied has been applied” (p.8). And recall from section 1.4.6 that
A branch is closed iff there are formulas of the form A and ¬A on two of its nodes; otherwise it is open. A closed branch is indicated by writing an × at the bottom. A tableau itself is closed iff every branch is closed; otherwise it is open.
(p.8, section 1.4.6)
And finally, recall from section 1.4.7 that:
A is a proof-theoretic consequence of the set of formulas Σ (Σ ⊢ A) iff there is a complete tree whose initial list comprises the members of Σ and the negation of A, and which is closed. We write ⊢ A to mean that φ ⊢ A, | that is, where the initial list of the tableau comprises just ¬A. ‘Σ ⊬ A’ means that it is not the case that Σ ⊢ A.5
(pp.8-9, section 1.4.7)
One example is the following. We want to show that:
⊢ ((A ⊃ B) ∧ (A ⊃ C)) ⊃ (A ⊃ (B ∧ C))
We negate the conclusion, and we try to see if there is a completed, closed tree. That means we apply all the rules possible to develop the tree at least to closures, and if we find contradictions along all branches, we deem it valid. As we can see, it is valid.
| ⊢((A ⊃ B) ∧ (A ⊃ C)) ⊃ (A ⊃ (B ∧ C)) | ||
| 1. . . 2. 3. 4. 5. 6. 7. . 8. . 9. . 10. | ¬(((A ⊃ B) ∧ (A ⊃ C)) ⊃ (A ⊃ (B ∧ C))) . (A ⊃ B) ∧ (A ⊃ C) ¬(A ⊃ (B ∧ C)) (A ⊃ B) (A ⊃ C) A ¬(B ∧ C) ↙ ↘ ¬B ¬C ↙ ↓ ↓ ↘ ¬A B ¬A B × × × ↓ ↘ ¬A C × × | P .. .
1¬⊃D 1¬⊃D
2∧D 2∧D 3¬⊃D 3¬⊃D .
7¬∧D .
4⊃D .
5⊃D Valid |
(p.9, section 1.4.8)
It seems now Priest is explaining how to text for validity, because he now writes:]
Second, the initial list for the tableau comprises A, 0, for every premise, A (if there are any), and ¬B, 0, where B is the conclusion.
(24)
[World Inheritance]
[The tableau rules for modal logic are the same as for non-modal propositional logic, except we indicate the worlds involved, and the branches inherit the world indicators from above.]
[Priest says that the tableaux rules for formulas built-up using truth-functional connectives are the same as with non-modal propositional logic, with one exception: whatever world-numbers we assign to a formula are inherited by the descendants below in the branch. In section 2.4.4 below, we give these rules for connectives in additional to those for modal operators.]
Third, the rules for the truth-functional connectives are the same as in non-modal logic, except that the number associated with any formula is also associated with its immediate descendant(s). Thus, the rule for disjunction, for example, is:
A ∨ B, i
↙ ↘
A, i B, i
(24)
[Tableaux Rules for Modal Operators. (All Rules Given in Total).]
[There are four new tableaux rules for modal operators.]
[Priest now adds for tableaux rules for the modal operators. Below I list what I think would be the complete list. To all of them I have added names, so that I can better follow the reasoning at work in the tableaux. But they are not Priests. For the connectives, they structures are based on those from section 1.4, and the names are borrowed from David Agler’s Symbolic Logic section 4.2. The names for modal logic rules are completely invented by me. Sorry about that, but I do not know yet anything more conventional.]
| Double Negation Development (¬¬D) |
| ¬¬A,i ↓ A,i |
| Conjunction Development (∧D) |
| A ∧ B,i ↓ A,i B,i |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B),i ↓ ¬A ∨ ¬B,i |
| Disjunction Development (∨D) |
| A ∨ B,i ↙ ↘ A,i B,i |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B),i ↓ ¬A,i ↓ ¬B,i |
| Conditional Development (⊃D) |
| A ⊃ B,i ↙ ↘ ¬A,i B,i |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B),i ↓ A,i ↓ ¬B,i |
| Negated Necessity Development (¬□D) |
| ¬□A,i ↓ ◊¬A,i |
| Negated Possibility Development (¬◊D) |
| ¬◊A,i ↓ □¬A,i |
| Relative Necessity Development (□rD) |
| □A,i irj ↓ A,j
(both □A,i and irj must occur somewhere on the same branch, but in any order or location) |
| Relative Possibility Development (◊rD) |
| ◊A,i ↓ irj A,j
(j must be new: it cannot occur anywhere above on the branch) |
(24)
[Branch Closing]
[Branches close when there are contradictions in the same world.]
In modal tableaux, we close a branch when we find a contradiction in one particular world.
Finally, a branch is closed iff for some formula, A, and number, i, A, i and ¬A, i both occur on the branch. (It must be the same i in both cases.)4
(25)
4. It is not obvious, but, as in the propositional case, every tableau of the kind we are dealing with here is finite.
(25)
[Tableaux Examples]
[Priest provides examples to show how the tableaux are made.]
Priest now gives some examples, enumerated (i), (ii), and (iii):
(i) □(A ⊃ B) ∧ □(B ⊃ C) ⊢ □(A ⊃ C)
| □(A ⊃ B) ∧ □(B ⊃ C) ⊢ □(A ⊃ C) | ||
| 1. . 2. . 3. . 4. . 5. . 6a. 6b. . 7. . 8. . 9. . 10. . 11. . 12. | □(A ⊃ B) ∧ □(B ⊃ C), 0
↓ ¬□(A ⊃ C), 0 ↓ □(A ⊃ B), 0 ↓ □(B ⊃ C), 0 ↓ ◊¬(A ⊃ C), 0 ↓ 0r1 (1) ¬(A ⊃ C), 1 (1) ↓ A, 1 ↓ ¬C, 1 ↓ A ⊃ B, 1 (2) ↓ B ⊃ C, 1 (2) ↙ ↘ ¬A, 1 B, 1 × ↓ ↘ ¬B, 1 ¬C, 1 × ×
| P . P .
1∧D . 1∧D .
2¬□D . 5◊rD 5◊rD . 6b¬⊃D . 6b¬⊃D . 3,6a□rD .
4,6a□rD .
9⊃D (7) 10⊃D (11)(8) |
(25, with naming and enumeration added)
The lines marked (1) are obtained by applying the rule for ◊ to the line immediately above them. Note that in applying the rule for ◊, a number new to the branch must be chosen. The lines marked (2) are the results of two applications of the rule for □ to the conjuncts of the premise. Note that the rule for is applied to numbers already on the branch.
(25)
Example 2:
(ii) ⊢ ◊(A ∧ B) ⊃ (◊A ∧ ◊B)
| ⊢ ◊(A ∧ B) ⊃ (◊A ∧ ◊B)) | ||
| 1. . 2. . 3. . 4. . 5. . 6a. 6b. . 7. . 8. . 9. .
| ¬(◊(A ∧ B) ⊃ (◊A ∧ ◊B)),0
↓ ◊(A ∧ B),0 ↓ ¬(◊A ∧ ◊B),0 ↙ ↘ ¬◊A,0 ¬◊B,0 ↓ ↓ □¬A,0 □¬B,0 ↓ ↓ 0r1 0r1 (1) A ∧ B,1 A ∧ B,1 (1) ↓ ↓ A,1 A,1 ↓ ↓ B,1 B,1 ↓ ↓ ¬A,1 ¬B,1 (2) × ×
| P . 1¬⊃D .
1¬⊃D . 3¬∧D .
4¬◊D . . 5◊rD . 6b∧D . 6b∧D . 5,6a□rD (7)(8) |
(25-26, with naming and enumeration added)
The lines marked (1) result from an application of the rule for ◊ to the formula at the second node of the tableau. The line marked (2) results from applications of the rule for □ to □¬A, 0 (left branch) and □¬B, 0 (right branch).
(26)
Example 3:
(iii) ⊬ (◊p ∧ ◊¬q) ⊃ ◊□◊p
| ⊬ (◊p ∧ ◊¬q) ⊃ ◊□◊p | ||
| 1. . 2. . 3. . 4. . 5. . 6. . 7a. 7b. . 8. . 9. . 10a. 10b. . 11. . 12a. 12b. . 13. . 14. . 15a. 15b. . 16.
| ((◊p ∧ ◊¬q) ⊃ ◊□◊p),0
↓ ◊p ∧ ¬◊q,0 ↓ ¬◊□◊p,0 ↓ ◊p,0 ↓ ◊¬q,0 ↓ □¬□◊p,0 (1) ↓ 0r1 (2) p,1 (2) ↓ ¬□◊p,1 (3) ↓ ◊¬◊p,1 ↓ 1r2 ¬◊p,2 ↓ □¬p,2 ↓ 0r3 (4) ¬q,3 (4) ↓ ¬□◊p,3 (5) ↓ ◊¬◊p,3 ↓ 3r4 ¬◊p,4 ↓ □¬p,4 | P . 1¬⊃D .
1¬⊃D . 2∧D .
2∧D . 3¬◊D . 4◊rD 4◊rD . 6,7a□rD . 8¬□D . 9◊rD 9◊rD . 3¬◊D . 5◊rD 5◊rD . 6,12a□r . 13¬□D . 14◊rD 14◊rD . 15b¬◊D |
(26, with naming and enumeration added)
The lines marked (2) result from an application of the rule for ◊ to the fourth line of the tableau. The lines marked (4) result from an application | of the same rule to the fifth line of the tableau. Note that, as the example shows, when we apply the rule for ◊, we may have to go back and apply the rule for □ again, to the new world (number) that has been introduced. Thus, the line marked (3) results from a first application of the rule to line (1). Line (5) results from a second application. For this reason, if one is ticking nodes to show that one has finished with them, one should never tick a node of the form □A, since one may have to come back and use it again.
(26-27)
[Counter-Models]
[We make counter-models using completed open branches. We assign worlds in accordance with the i numbers. We assign R relations in accordance with irj formulations. And nodes of the form p, i we assign vwi(p) = 1. And for nodes of the form ¬p, i, we assign vwi(p) = 0. If there are neither of these two, then vwi(p) can be given any value we want.]
Priest next explains how to make counter-models from completed open tableaux. [It seems to be the following. (Perhaps we can look exclusively at one branch for all of the following steps, but I am not sure.) First we list all the worlds for the counter-model. We look to see what numbers are in the branch, and they indicate the different worlds, which we then list. For every accessibility indication in the branch we designate a corresponding R relation for the worlds in question. To assign values to propositional parameters, if we have any nodes of the form p, i, then we assign it true for that indicated world, and if we have ¬p, i, then we assign it false for that world. If there is neither the one nor the other form for p on the branch, we can assign it any value we please.]
Counter-models can be read off from an open branch of a tableau in a natural way. For each number, i, that occurs on the branch, there is a world, wi; wiRwj iff irj occurs on the branch; for every propositional parameter, p, if p, i occurs on the branch, vwi(p) = 1, if ¬p, i occurs on the branch, vwi(p) = 0 (and if neither, vwi(p) can be anything one wishes).
(27)
[Counter-Model Example]
[Priest shows how to make a counter-model with an example.]
[Recall from section 2.3.7 the way that interpretations are depicted visually. From our brief summary of that section: “We can diagram the interpretation by giving each world it place in the diagram, where the formulations that are true in it are listed, and by using arrows to indicate world accessibility.” Priest gave an example:
W = {w1, w2, w3}
w1Rw2, w1Rw3, w3Rw3
vw1(p) = 0, vw1(q) = 0;
vw2(p) = 1, vw2(q) = 1,
vw3(p) = 1, vw3(q) = o,
It was diagramed as:
xxxxxxxxxxxxw2xxpxxq
xxxxxxxxxx↗
¬px¬qxxw1
xxxxxxxxxx↘x↷
xxxxxxxxxxxxw3xxpxx¬q
] Priest will now give a counter-model for example iii in section 2.4.5. [For convenience, let us copy it here.
| ⊬ (◊p ∧ ◊¬q) ⊃ ◊□◊p | ||
| 1. . 2. . 3. . 4. . 5. . 6. . 7a. 7b. . 8. . 9. . 10a. 10b. . 11. . 12a. 12b. . 13. . 14. . 15a. 15b. . 16.
| ((◊p ∧ ◊¬q) ⊃ ◊□◊p),0
↓ ◊p ∧ ¬◊q,0 ↓ ¬◊□◊p,0 ↓ ◊p,0 ↓ ◊¬q,0 ↓ □¬□◊p,0 (1) ↓ 0r1 (2) p,1 (2) ↓ ¬□◊p,1 (3) ↓ ◊¬◊p,1 ↓ 1r2 ¬◊p,2 ↓ □¬p,2 ↓ 0r3 (4) ¬q,3 (4) ↓ ¬□◊p,3 (5) ↓ ◊¬◊p,3 ↓ 3r4 ¬◊p,4 ↓ □¬p,4 | P . 1¬⊃D .
1¬⊃D . 2∧D .
2∧D . 3¬◊D . 4◊rD 4◊rD . 6,7a□rD . 8¬□D . 9◊rD 9◊rD . 3¬◊D . 5◊rD 5◊rD . 6,12a□r . 13¬□D . 14◊rD 14◊rD . 15b¬◊D |
(26, with naming and enumeration added)
]
W = {w1, w2, w3,w4}
w0Rw1, w1Rw2, w0Rw3, w3Rw4
vw1(p) = 1, vw1 (q) = x;
vw2(p) = x, vw2(q) = x;
vw3(p) = x, vw3(q) = 0;
vw4(p) = x, vw4(q) = x;
(27)
And it can be depicted as:
xxxxxxxxxxxxw2
xxxxxxxxx↗
xxxxxxw1xxp
xxx↗
w0
xxx↘x
xxxxxxw3xx¬q
xxxxxxxxx↘
xxxxxxxxxxxxw4
(page 27)
Priest then shows how we can check that the counter-model works (see p.27 for the details).
[Soundness and Completeness of the Tableaux]
[These tableaux are both sound and complete.]
Priest notes lastly that: “The tableaux just described are sound and complete with respect to the semantics. The proof is given in 2.9” (27).
From:
Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.
.
No comments:
Post a Comment