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
9.
Logics with Gaps, Gluts and Worlds
9.3
Tableaux for K4
Brief summary:
(9.3.1) We will formulate the tableau procedures for K4 by modifying those for FDE. (9.3.2) Nodes in our possible worlds FDE tableaux take the “form A,+i or A,−i, where i is a natural number.” To test for validity, we compose our initial list by formulating our premise nodes as “B,+0” and our conclusion as “A,−0”. “A branch closes if it contains a pair of the form A,+i and A,−i” (164). (9.3.3) The tableau rules for the extensional connectives (∧, ∨ and ¬) in K4 are the same as for FDE except “i is carried through each rule.”[Below I include the conditional rules from the next section. Note that the rules for double negation and disjunction are not in the text and are probably mistaken.]
| Double Negation Development, True (¬¬D,+) |
| ¬¬A,+i ↓ A,+i |
| Double Negation Development, False (¬¬D,−) |
| ¬¬A,−i ↓ A,−i |
| Conjunction Development, True (∧D,+) |
| A ∧ B,+i ↓ A,+i B,+i |
| Conjunction Development, False (∧D,−) |
| A ∧ B,−i ↙ ↘ A,−i B,−i |
| Negated Conjunction Development, True (¬∧D,+) |
| ¬(A ∧ B),+i ↓ ¬A ∨ ¬B,+i |
| Negated Conjunction Development, False (¬∧D,−) |
| ¬(A ∧ B),−i ↓ ¬A ∨ ¬B,−i |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+i ↙ ↘ A,+i B,+i |
| Disjunction Development, False (∨D,−) |
| A ∨ B,-i ↓ A,-i B,-i |
| Negated Disjunction Development, True (¬∨D, +) |
| ¬(A ∨ B),+i ↓ ¬A ∧ ¬B,+i |
| Negated Disjunction Development, False(¬∨D, -) |
| ¬(A ∨ B),-i ↓ ¬A ∧ ¬B,-i |
| Conditional Development, True (→D,+) |
| A → B,+i ↙ ↘ A,-j B,+j .
j is every number that occurs on the branch |
| Conditional Development, False (→D,−) |
| A → B,-i ↓ A,+j B,-j .
j is a new number |
| Negated Conditional Development, True (¬→D, +) |
| ¬(A → B),+i ↓ A,+j ¬B,+j .
j is a new number |
| Negated Conditional Development, False(¬→D, -) |
| ¬(A → B),-i ↙ ↘ A,-j ¬B,-j .
j is every number that occurs on the branch |
(165, titles for the rules are my own additions)
(9.3.4) To the above rules we add those for the conditional [see the rules just above, where they were moved to.] (9.3.5) Priest then gives a tableau example showing a valid inference. (9.3.6) Priest next gives an example of an inference that is not valid. (9.3.7) We make countermodels from open branches in the following way: “There is a world wi for each i on the branch; for propositional parameters, p, if p,+i occurs on the branch, set pρwi1; if ¬p,+i occurs on the branch, set pρwi0. ρ relates no parameter to anything else” (166). (9.3.8) (It can be proven that the possible worlds FDE tableaux are sound and complete with respect to the semantics.)
[Sources of the Tableaux for K4]
[Tableau Formulation]
[Tableau Rules for the Extensional Connectives (∧, ∨ and ¬)]
[Tableau Rules for the Conditional (→)]
[Example 1: Valid]
[Example 2: Invalid]
[Countermodels]
[The Soundness and Completeness of the Tableaux]
Summary
[Sources of the Tableaux for K4]
[We will formulate the tableau procedures for K4 by modifying those for FDE.]
[In the previous section (9.2), Priest gave the semantics for K4, which is a possible worlds semantics combined with First Degree Entailment (FDE). Now our task is the tableau rules. Recall from section 3.5.5 that normal modal logic S5 is another name for Kυ, and in section 3.5.3 Priest gives the tableau rules for S5 by making slight modifications to those for modal logic. Priest says now that in the same was as this, we can formulate the tableau system for K4 by modifing the tableau system for FDE that we used in section 8.3.]
A tableau system for K4 can be obtained by modifying the system for FDE of 8.3, in the same way that the tableau system for classical propositional logic is modified in order to obtain one for Kυ (3.5.3).
(164)
[Tableau Formulation]
[Nodes in our possible worlds FDE tableaux take the “form A,+i or A,−i, where i is a natural number.” To test for validity, we compose our initial list by formulating our premise nodes as “B,+0” and our conclusion as “A,−0”. “A branch closes if it contains a pair of the form A,+i and A,−i” (164).]
[Recall from section 8.3.2 that FDE tableaux have the symbols + and – coming after the formulas to indicate whether the formula is true or not. And recall from section 2.4.1 that after the formulas we write numbers (or when as variables, as lowercase letters starting with i) indicating the world that the formula holds in. We will now combine these conventions such that we indicate the world and whether or not it is true in that world, by combining the + or the – (truth value) symbols with the lower-case letter (world) symbols. Thus if we write A,+i, that intuitively means that formula A is true in world i. The tableaux will test for validity, of course. So recall from section 2.4.2 that for modal tableaux, “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” (p. 24). Intuitively, we are setting it up so that all the premises are set for true in world 0 and the negation of the conclusion is set for true in world 0 also. And in FDE tableaux (recall from section 8.3.3), we set the premises to true and the conclusion false, using the plus/minus symbols:
To test the claim that A1, ... , An ⊢ B , we start with an initial list of the form:
A1,+
.
.
.
An,+
B,−
(p.144, section 8.3.3)
In our possible worlds FDE, we will combine these conventions. We set premises to +0 (true in world 0) and the conclusion to −0 (not true in world 0). A branch in a tableaux normally closes when there is something like a contradiction along it. So in our case, a branch closes when along it is a pair of nodes of the form A,+i and A,−i (in other words, if we find a formula that is both true and not true in the same world).]
A node now has the form A,+i or A,−i, where i is a natural number. The initial list comprises a node of the form B,+0 for every premise, B, and A,−0, where A is the conclusion. A branch closes if it contains a pair of the form A,+i and A,−i.
(164)
[Tableau Rules for the Extensional Connectives (∧, ∨ and ¬)]
[The tableau rules for the extensional connectives (∧, ∨ and ¬) in K4 are the same as for FDE except “i is carried through each rule.”]
[Recall from section 8.3.4 the FDE tableau rules for double negation, conjunction, and disjunction. Priest says that they are the same as for possible worlds FDE (K4), except “i is carried through each rule.” Priest provides the rules for conjunction, but I will guess them for double negation and disjunction too. Now, more specifically, Priest says that the rules are the same for the “extensional connectives,” which in section 9.2.3 he says are ∧, ∨ and ¬. So I am not entirely sure if there is a rule here for double negation; but I am guessing it is ok, because the FDE semantics rule for negation in section 8.2.6 toggles the 1/0 value.
| Conjunction Development, True (∧D,+) |
| A ∧ B,+i ↓ A,+i B,+i |
| Conjunction Development, False (∧D,−) |
| A ∧ B,−i ↙ ↘ A,−i B,−i |
(165)
| Negated Conjunction Development, True (¬∧D,+) |
| ¬(A ∧ B),+i ↓ ¬A ∨ ¬B,+i |
| Negated Conjunction Development, False (¬∧D,−) |
| ¬(A ∧ B),−i ↓ ¬A ∨ ¬B,−i |
| Double Negation Development, True (¬¬D,+) |
| ¬¬A,+i ↓ A,+i |
| Double Negation Development, False (¬¬D,−) |
| ¬¬A,−i ↓ A,−i |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+i ↙ ↘ A,+i B,+i |
| Disjunction Development, False (∨D,−) |
| A ∨ B,-i ↓ A,-i B,-i |
| Negated Disjunction Development, True (¬∨D, +) |
| ¬(A ∨ B),+i ↓ ¬A ∧ ¬B,+i |
| Negated Disjunction Development, False(¬∨D, -) |
| ¬(A ∨ B),-i ↓ ¬A ∧ ¬B,-i |
]
The rules for the extensional connectives are exactly the same as those of 8.3.4 for FDE, except that i is carried through each rule. | Thus, for example, the rules for ∧ are:
Conjunction
Development, True (∧D,+)
A ∧ B,+i
↓
A,+i
B,+i
Conjunction
Development, False (∧D,−)
A ∧ B,−i
↙ ↘
A,−i B,−i
(164-165, titles for the rules are my own additions)
[Tableau Rules for the Conditional (→)]
[To the above rules we add those for the conditional.]
[Priest then gives the rules for the conditional.]
The rules for the conditional are as follows:
| Conditional Development, True (→D,+) |
| A → B,+i ↙ ↘ A,-j B,+j .
j is every number that occurs on the branch |
| Conditional Development, False (→D,−) |
| A → B,-i ↓ A,+j B,-j .
j is a new number |
| Negated Conditional Development, True (¬→D, +) |
| ¬(A → B),+i ↓ A,+j ¬B,+j .
j is a new number |
| Negated Conditional Development, False(¬→D, -) |
| ¬(A → B),-i ↙ ↘ A,-j ¬B,-j .
j is every number that occurs on the branch |
(165, titles for the rules are my own additions)
In the rules that split the branch, j is every number that occurs on the branch. In the other two rules, j is a new number.
(165)
[Example 1: Valid]
[Priest then gives a tableau example showing a valid inference.]
[Priest gives an example that involves transitivity, which is valid.]
Example: A → B, B → C ⊢ A → C:
A → B, B → C ⊢ A → C
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
A → B,+0
↓
B → C,+0
↓
A → C,–0
↓
A,+1
↓
C,–1
↙ ↘
A,–1 B,+1
× ↓ ↘
¬B,–1 C,+1
× ×
P
.
P
.
P
.
3→–
.
3→–
.
1→+
(6×4)
2→+
(7×6)
(7×5)
Valid
(enumeration and step accounting are my own and are probably mistaken)
The fourth and fifth lines are obtained by applying the rule for untrue → to the third line. The two splits are then obtained by applying the rule for true → to the first and second lines respectively.
(165)
[Example 2: Invalid]
[Priest next gives an example of an inference that is not valid.]
[The next tableau example is invalid. For this one, we need to keep in mind that for the conditional, “In the rules that split the branch, j is every number that occurs on the branch. In the other two rules, j is a new number” (165, section 9.3.4 above). See lines 5 and 6 where where we must repeat the rule for both worlds.]
Example: p → q ⊬ ¬q → ¬p:
p → q ⊬ ¬q → ¬p
1.
.
2.
.
3.
.
4.
.
5.
.
6.
p → q,+0
↓
¬q → ¬p,–0
↓
¬q,+1
↓
¬p,–1
↙ ↘
p,–0 q,+0
↙ ↓ ↓ ↘
p,–1 q,+1 p,–1 q,+1
P
.
P
.
2→–
.
2→–
.
1→+
.
1→+
(open)
Invalid
(166, enumeration and step accounting are my own and are probably mistaken)
[Countermodels]
[We make countermodels from open branches in the following way: “There is a world wi for each i on the branch; for propositional parameters, p, if p,+i occurs on the branch, set pρwi1; if ¬p,+i occurs on the branch, set pρwi0. ρ relates no parameter to anything else” (166).]
[We make counter-models from open branches in the following way. For every i number, we designate a world with that number. We then look for propositional parameters. Ones that are non-negated and true in a world we set them in the countermodel to true in that world. Likewise, for any negated propositional parameter that is true in a world, we set that unnegated parameter to zero in that world. So let us consider the propositional parameters in the left-most branch: p,–1; p,–0; ¬p,–1; ¬q,+1. (Note, I have not figured out how we obtain the model yet working strictly with the rules. Priest writes, “for propositional parameters, p, if p,+i occurs on the branch, set pρwi1; if ¬p,+i occurs on the branch, set pρwi0.” Suppose we just follow the rules as they are here. Then our counter-model would simply be that q is false in world 1, because ¬q,+1 is the only one on the branch with a + sign, and the rules as they are given only stipulate for + sign formulations. And maybe also we would add that by the negation rule, ¬q is true in world 1. But I do not know how to get the p values yet in the example. There “+A indicates that A is true; −A indicates that it is untrue.” And on the basis of the left-most branch (p,–1; p,–0; ¬p,–1; ¬q,+1) we are to produce:
xxxw0xxxxxxxw1
xxx−pxxxxxx−p
xxxxxxxxxxx−¬p
xxxxxxxxxxx+¬q
So this is saying that p is untrue in world 0 and in world 1 (perhaps because p never gets a + sign in either world. But then why is q’s value not indicated for world 0? Is it because it has no effect anyway on the calculation?). And in world 1, why do we not have −q? We set it to 0, which means it is untrue? Instead we have +¬q. How did we get that on the basis of the rules? I can only think that we are applying a negation operation on the established value of q as false). I am going to make a very wild guess on these matters. We exclude the q from world 0 and world 1, for the following reason. Our formula is:
p → q ⊬ ¬q → ¬p
as we can see, since we established that p is untrue in both worlds, then p → q is true in both worlds, regadless of q’s value (which is false in world 1). And the reason why we do not write −q for world 1 is that it would have no bearing on the calculus. However, we can use the negation rule to get +¬q, which does have bearing. To finish the calculation, we would need the value for ¬p. We can derive it by noting that since p is neither true nor false, its value does not toggle, and it stays untrue. So in the conclusion, we have that the antecedent is true in world 1 but the consequent not true. This means that the conclusion as a conditional is 0 in world 1. And given the definition for the conditional, it will be 0 in world 0 too, I think maybe. With these parts of the model being established, we have that in every world where the premise is true, the conclusion is not true. And hence it is invalid. Chances are this is horribly wrong (I have revised it once already).]
Counter-models are read off from open branches of tableaux in the natural way. There is a world wi for each i on the branch; for propositional parameters, p, if p,+i occurs on the branch, set pρwi1; if ¬p,+i occurs on the branch, set pρwi0. ρ relates no parameter to anything else. Thus, the counter-model defined by the leftmost branch of the tableau of 9.3.6 may be depicted thus:
xxxw0xxxxxxxw1
xxx−pxxxxxx−p
xxxxxxxxxxx−¬p
xxxxxxxxxxx+¬q
(+A indicates that A is true; −A indicates that it is untrue.) At every world, p is untrue. Hence, p → q is true at w0. But ¬q is true at w1, and ¬p is not true there. Hence, ¬q → ¬p is not true at w0.
(166)
[The Soundness and Completeness of the Tableaux]
[It can be proven that the possible worlds FDE tableaux are sound and complete with respect to the semantics.]
[Priest ends by noting that:]
The tableaux are sound and complete with respect to the semantics. This is proved in 9.8.1–9.8.7.
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