Priest (3.3) An Introduction to Non-Classical Logic, ‘Tableaux for Normal Modal Logics’, 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

 

3.

Normal Modal Logics

 

3.3

Tableaux for Normal Modal Logics

 

 

 

 

Brief summary:

(3.3.1) To make tableaux for other normal modal logics, we will add rules regarding the R accessibility relation. (3.3.2) The tableaux for the different normal modal logics take rules reflecting the properties of the accessibility relations that characterize them.

Tableaux Rules for Kρ, Kσ, and Kτ
ρ . ↓ iri . . “ρrD”	σ irj ↓ jri . . “σrD”	τ irj jrk ↓ .irk . “τrD”

(3.3.3) In the first tableau example for normal modal logics, we learn that □p ⊃ p is valid in Kρ but not in K; thus Kρ is a proper extension of K. (3.3.4) In Priest’s second example, we learn that p ⊃ □◊p is not valid in K but it is valid in Kσ, thus Kσ is a proper extension of K. (3.3.5) In the third of Priest’s examples, we learn that □p ⊃ □□p is not valid in K but it is valid in Kτ, thus Kτ is a proper extension of K. (3.3.6) For compound systems, we must apply the rules for each restriction. When making the tableau, we should apply the ◊-rule first. Then secondly we compute and add all the needed new facts about r that then arise. Lastly we should backtrack whenever necessary to apply the □-rule in cases of r where it is required. (3.3.7) We make counter-models by assigning worlds in accordance with the i numbers on an open branch, r relations in accordance with the irj formulations, p,i formulations as  v_wi(p) = 1, ¬p,i formulations as v_wi(p) = 0, and if neither of those two cases show for some p, we can assign it any value we want. (3.3.8) These tableaux are both sound and complete.

 

 

 

 

 

Contents

 

3.3.1

[Adding Accessibility Rules for Other Normal Modal Logic Tableaux]

 

3.3.2

[Rules for Kρ, Kσ, and Kτ]

 

3.3.3

[Tableau example 1: Kρ (Reflexive)]

 

3.3.4

[Tableau example 2: Kσ (Symmetrical)]

 

3.3.5

[Tableau example 3: Kτ  (Transitive)]

 

3.3.6

[Tableau example 4: Kστ (Symmetrical and Transitive)]

 

3.3.7

[Counter-Models]

 

3.3.8

[Soundness and Completeness of the Normal Modal Tableaux]

 

 

 

 

 

Summary

 

3.3.1

[Adding Accessibility Rules for Other Normal Modal Logic Tableaux]

 

[To make tableaux for other normal modal logics, we will add rules regarding the R accessibility relation.]

 

[In section 2.4 we examined the tableaux rules for modal logic. And in section 3.2 we learned the semantics for normal modal logics, with many of them being fashioned by adding constraints to the accessibility relation of the interpretations. Now we will extend the tableaux rules so that they work for these other normal modal logics, and this will primarily involve rules involving the R accessibility relation.]

The tableau rules for K can be extended to work for other normal systems as well. Essentially, this is done by adding rules which introduce further information about r on branches. Since this information comes into play when the rule for □ is applied, the effect of this is to increase the number of applications of that rule.

(38)

[contents]

 

 

 

3.3.2

[Rules for Kρ, Kσ, and Kτ]

 

[The tableaux for the different normal modal logics take rules reflecting the properties of the accessibility relations that characterize them.]

 

Priest now gives the rules for certain normal modal logics. [Recall the constraints from section 3.2.3:

ρ (rho), reflexivity: for all w, wRw.

σ (sigma), symmetry: for all w₁, w₂, if w₁Rw₂, then w₂Rw₁.

τ (tau), transitivity: for all w₁, w₂, w₃, if w₁Rw₂ and w₂Rw₃, then w₁Rw₃.

η (eta), extendability: for all w₁, there is a w₂ such that w₁Rw₂.

(p.36, section 3.2.3)

Priest will give the rules for the first three, and we see the fourth in the next section.

 

Tableaux Rules for Kρ, Kσ, and Kτ
ρ . ↓ iri . . “ρrD”	σ irj ↓ jri . . “σrD”	τ irj jrk ↓ .irk . “τrD”

 

| (We come to the rule for η in the next section.) The rule for ρ means that if i is any integer on the tableau, we introduce iri. It can therefore be applied to world 0 after the initial list, and, thereafter, after the introduction of any new integer. The other two rules are self-explanatory. Note that if the application of a rule would result in just repeating lines already on the branch, it is not applied. Thus, for example, if we apply the σ-rule to irj to get jri, we do not then apply it again to jri to get irj. The following three subsections give examples of tableaux for Kρ, Kσ and Kτ , respectively.

(38, with my naming additions)

[contents]

 

 

 

3.3.3

[Tableau example 1: Kρ (Reflexive)]

 

[In the first tableau example for normal modal logics, we learn that □p ⊃ p is valid in Kρ but not in K; thus Kρ is a proper extension of K.]

 

Here is Priest’s first tableau example (recall the other rules from section 2.4.4):

⊢_Kρ □p ⊃ p

⊢Kρ □p ⊃ p
1. . 2. . 3. . 4. . 5.	¬(□p ⊃ p),0 ↓ 0r0 ↓ □p,0 ↓ ¬p,0 ↓ p,0 ×	P . 1ρrD . 1¬⊃D . 1¬⊃D . 2,3□rD (4)

(39, with naming and enumeration added)

The last line is obtained from □p, 0, since 0r0. Since □p ⊃ p is not valid in K (2.12, problem 2(o)), this shows that Kρ is a proper extension of K. (That is, Kρ is not exactly the same as K.)

(39, boldface mine)

[contents]

 

 

 

 

3.3.4

[Tableau example 2: Kσ (Symmetrical)]

 

[In Priest’s second example, we learn that p ⊃ □◊p is not valid in K but it is valid in Kσ, thus Kσ is a proper extension of K.]

 

Here is Priest’s second tableau example (again, we refer to the other rules from section 2.4.4):

⊢_Kσ p ⊃ □◊p

⊢Kσ p ⊃ □◊p
1. . 2. . 3. . 4. . 5a. 5b. . 6. . 7. . 8. . .	¬(p ⊃ □◊p),0 ↓ p,0 ↓ ¬□◊p,0 ↓ ◊¬◊p,0 ↓ 0r1 ¬◊p,1 ↓ 1r0 ↓ □¬p,1 ↓ ¬p,0 ×	P . 1¬⊃D . 1¬⊃D . 3¬□D . 4◊rD 4◊rD . 5aσrD . 5b¬◊D . 6,7□rD (2)

(39, with naming and enumeration added.)

The last line follows from the fact that □¬p, 1, since 1r0. Since p ⊃ □◊p is not valid in K (2.12, problem 2(t)), this shows that Kσ is a proper extension of K.

(39, boldface mine)

[contents]

 

 

 

3.3.5

[Tableau example 3: Kτ  (Transitive)]

 

[In the third of Priest’s examples, we learn that □p ⊃ □□p is not valid in K but it is valid in Kτ, thus Kτ is a proper extension of K.]

 

Here is Priest’s third tableau example (again, refer to the other rules in section 2.4.4):

⊢_Kτ □p ⊃ □□p

⊢Kτ □p ⊃ □□p
1. . 2. . 3. . 4. . 5a. 5b. . 6. . 7a. 7b. . 8. . 9. . .	¬(□p ⊃ □□p),0 ↓ □p,0 ↓ ¬□□p,0 ↓ ◊¬□p,0 ↓ 0r1 ¬□p,1 ↓ ◊¬p,1 ↓ 1r2 ¬p,2 ↓ 0r2 ↓ p,2 ×	P . 1¬⊃D . 1¬⊃D . 3¬□D . 4◊rD 4◊rD . 5b¬◊D . 6◊rD 6◊rD . 5a,5bτrD . 2,8□rD (7b)

(40, with naming and enumeration added.)

When we add 1r2 to the tableau because of the ◊-rule, we already have 0r1; hence, we add 0r2. Since □p holds at 0, an application of the rule for □ immediately closes the tableau. Since □p ⊃ □□p is not valid in K (2.12, problem 2(r)), this shows that Kτ is a proper extension of K.

(40, boldface mine)

[contents]

 

 

 

3.3.6

[Tableau example 4: Kστ (Symmetrical and Transitive)]

 

[For compound systems, we must apply the rules for each restriction. When making the tableau, we should apply the ◊-rule first. Then secondly we compute and add all the needed new facts about r that then arise. Lastly we should backtrack whenever necessary to apply the □-rule in cases of r where it is required.]

 

Priest now explains how to do tableaux for normal modal logics with compound restrictions. (I will quote in the entirety as it is well explained in the original):

For ‘compound’ systems, all the relevant rules must be applied. There may be some interplay between them. To keep track of this, adopt the following procedure. New worlds are normally introduced by the ◊-rule. Apply this first. Then compute all the new facts about r that need to be added, and add them. Finally, backtrack if necessary and apply the □-rule wherever the new r facts require it. The procedure is illustrated in the following tableau, demonstrating that ⊢_Kστ ◊p ⊃ □◊p. For brevity’s sake, we write more than one piece of information about r on the same line.

 

⊢Kστ ◊p ⊃ □◊p
1. . 2. . 3. . 4a. 4b. . 5. . 6. . 7a. 7b. . 8. . 9. . 10. . 11. . 12. . .	¬(◊p ⊃ □◊p),0 ↓ ◊p,0 ↓ ¬□◊p,0 ↓ 0r1 p,1 ↓ 1r0,1r1,0r0 ↓ ◊¬◊p,0 ↓ 0r2 ¬◊p,2 ↓ 2r0, 2r2, 1r2, 2r1 ↓ □¬p,2 ↓ ¬p,2 ↓ ¬p,1 ↓ ¬p,0 ×	P . 1¬⊃D . 1¬⊃D . 2◊rD 2◊rD . 4a,5στD . 3¬□D . 6◊rD 6◊rD . 5,7a,8στrD . 7b¬◊D . 8,9□rD . 8,9□rD . 8,9□rD (11×4b)

The line ◊¬◊p, 0 requires the construction of a new world, 2, with an application of the ◊-rule. This is done on the next two lines. We then add all the new information about r that the creation of world 2 requires. 2r0 is added because of symmetry; 2r2 is added because of transitivity and the fact that we have 2r0 and 0r2; 1r2 is added because of transitivity and the fact that we have 1r0 and 0r2; similarly, 2r1 is added because of transitivity. Symmetry and transitivity require no other facts about r. In constructing a tableau, it may help to keep track of things if one draws a diagram of the world structure, as it emerges.

(40-41, with naming and enumeration added to the tableau. Page break comes in the middle of the tableau)

[contents]

 

 

 

3.3.7

[Counter-Models]

 

[We make counter-models by assigning worlds in accordance with the i numbers on an open branch, r relations in accordance with the irj formulations, p,i formulations as  v_wi(p) = 1, ¬p,i formulations as v_wi(p) = 0, and if neither of those two cases show for some p, we can assign it any value we want.]

 

[Recall from section 2.4.7 how counter-models are formed:

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

(p.27, section 2.4.7)

Priest now explains how to do it with the inclusion of the extra r information in our alternate normal modal logics.]

Counter-models read off from an open branch of a tableau incorporate the information about r in the obvious way. Thus, consider the following tableau, which shows that ⊬_Kρσ □p ⊃ □□p.

 

⊬Kρσ □p ⊃ □□p
1. . 2. . 3. . 4. . 5. . 6. . 7a. 7b. . 8. . 9. . 10. . 11a. 11b. . 12. . .	¬(□p ⊃ □□p),0 ↓ 0r0 ↓ □p,0 ↓ ¬□□p,0 ↓ p,0 ↓ ◊¬□p,0 ↓ 0r1 ¬□p,1 ↓ 1r1, 1r0 ↓ p,1 ↓ ◊¬p,1 ↓ 1r2 ¬p,2 ↓ 2r2, 2r1	P . 1ρrD . 1¬⊃D . 1¬⊃D . 2,3□rD . 4¬□D . 6◊rD 6◊rD . 7ρσrD . 5,7a□rD . 7b¬□D . 10◊rD 10◊rD . 11,ρσrD (open)

The counter-model is ⟨W, R, v⟩, where W = {w₀,w₁,w₂}, R is such that w₀Rw₀, w₁Rw₁, w₂Rw₂, w₀Rw₁, w₁Rw₀, w₁Rw₂ and w₂Rw₁, and v is such that | v_w0(p)  = v_w1(p) = 1, v_w2(p) = 0. In pictures:

↷xxxx↷xxxx↷

w_ox⇄xw₁x⇄xw₂

pxxxxpxxxx¬p

(41-42, with naming and enumeration added to the tableau)

[contents]

 

 

 

3.3.8

[Soundness and Completeness of the Normal Modal Tableaux]

 

[These tableaux are both sound and complete.]

 

Priest notes lastly that: “The tableau systems above are all sound and complete with respect to their respective semantics. The proof of this can be found in 3.7” (42).

[contents]

 

 

 

 

From:

 

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

 

 

 

 

 

.