Priest (9.3) Introduction to Non-Classical Logic, ‘Tableaux for K4’, summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[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 K₄

 

 

 

 

Brief summary:

(9.3.1) We will formulate the tableau procedures for K₄ 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 K₄ 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 w_i 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.)

 

 

 

 

 

Contents

 

9.3.1

[Sources of the Tableaux for K₄]

 

9.3.2

[Tableau Formulation]

 

9.3.3

[Tableau Rules for the Extensional Connectives (∧, ∨ and ¬)]

 

9.3.4

[Tableau Rules for the Conditional (→)]

 

9.3.5

[Example 1: Valid]

 

9.3.6

[Example 2: Invalid]

 

9.3.7

[Countermodels]

 

9.3.8

[The Soundness and Completeness of the Tableaux]

 

 

 

 

 

Summary

 

9.3.1

[Sources of the Tableaux for K₄]

 

[We will formulate the tableau procedures for K₄ by modifying those for FDE.]

 

[In the previous section (9.2), Priest gave the semantics for K₄, 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 K₄ by modifing the tableau system for FDE that we used in section 8.3.]

A tableau system for K₄ 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)

[contents]

 

 

 

 

9.3.2

[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 A₁, ... , A_n ⊢ B , we start with an initial list of the form:

A₁,+

.

.

.

A_n,+

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)

[contents]

 

 

 

 

9.3.3

[Tableau Rules for the Extensional Connectives (∧, ∨ and ¬)]

 

[The tableau rules for the extensional connectives (∧, ∨ and ¬) in K₄ 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 (K₄), 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)

[contents]

 

 

 

 

9.3.4

[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)

[contents]

 

 

 

 

 

9.3.5

[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)

[contents]

 

 

 

 

 

9.3.6

[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)

[contents]

 

 

 

 

 

9.3.7

[Countermodels]

 

[We make countermodels from open branches in the following way: “There is a world w_i 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:

xxxw₀xxxxxxxw₁

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 w_i 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:

xxxw₀xxxxxxxw₁

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 w_0. But ¬q is true at w₁, and ¬p is not true there. Hence, ¬q → ¬p is not true at w₀.

(166)

[contents]

 

 

 

 

 

9.3.8

[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.

[contents]

 

 

 

 

 

 

 

 

 

 

From:

 

Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.

 

 

.

 

Priest (2.4) An Introduction to Non-Classical Logic, ‘Modal Tableaux,’ summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[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 v_wi(p) = 1. And for nodes of the form ¬p, i, we assign v_wi(p) = 0. If there are neither of these two, then v_wi(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.

 

 

 

 

Contents

 

2.4.1

[Node Structures of Modal Tableaux]

 

2.4.2

[Modal Tableaux Initial Set-Up]

 

2.4.3

[World Inheritance]

 

2.4.4

[Tableaux Rules for Modal Operators. (All Rules Given in Total).]

 

2.4.5

[Branch Closing]

 

2.4.6

[Tableaux Examples]

 

2.4.7

[Counter-Models]

 

2.4.8

[Counter-Model Example]

 

2.4.9

[Soundness and Completeness of the Tableaux]

 

 

 

 

 

 

 

Summary

 

2.4.1

[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.³

(24)

3. I will avoid using r as a propositional parameter where this might lead to confusion.

(24)

[contents]

 

 

 

 

 

2.4.2

[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.⁵

(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)

[contents]

 

 

 

 

2.4.3

[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)

[contents]

 

 

 

 

2.4.4

[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)

[contents]

 

 

 

 

2.4.5

[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.)⁴

(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)

[contents]

 

 

 

2.4.6

[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)

[contents]

 

 

 

 

2.4.7

[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 v_wi(p) = 1. And for nodes of the form ¬p, i, we assign v_wi(p) = 0. If there are neither of these two, then v_wi(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, w_i; w_iRw_j iff irj occurs on the branch; for every propositional parameter, p, if p, i occurs on the branch, v_wi(p) = 1, if ¬p, i occurs on the branch, v_wi(p) = 0 (and if neither, v_wi(p) can be anything one wishes).

(27)

[contents]

 

 

 

 

 

2.4.8

[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 = {w₁, w₂, w₃}

w₁Rw₂, w₁Rw₃, w₃Rw₃

v_w1(p) = 0, v_w1(q) = 0;

v_w2(p) = 1, v_w2(q) = 1,

v_w3(p) = 1, v_w3(q) = o,

It was diagramed as:

xxxxxxxxxxxxw₂xxpxxq

xxxxxxxxxx↗

¬px¬qxxw₁

xxxxxxxxxx↘x↷

xxxxxxxxxxxxw₃xxpxx¬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 = {w₁, w₂, w₃,w₄}

w₀Rw₁, w₁Rw₂, w₀Rw₃, w₃Rw₄

v_w1(p) = 1, v_w1 (q) = x;

v_w2(p) = x, v_w2(q) = x;

v_w3(p) = x, v_w3(q) = 0;

v_w4(p) = x, v_w4(q) = x;

(27)

And it can be depicted as:

xxxxxxxxxxxxw₂

xxxxxxxxx↗

xxxxxxw₁xxp

xxx↗

w₀

xxx↘x

xxxxxxw₃xx¬q

xxxxxxxxx↘

xxxxxxxxxxxxw₄

(page 27)

Priest then shows how we can check that the counter-model works (see p.27 for the details).

[contents]

 

 

 

2.4.9

[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.

 

 

 

 

 

.