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 II:
Quantification and Identity
16.
Necessary Identity in Modal Logic
16.2
Necessary Identity
Brief summary:
(16.2.1) We will now define the identity predicate in a quantified normal modal logic. (16.2.2) “The denotation of the identity predicate is the same in every world, w, of an interpretation: vw(=) = {⟨d, d⟩ : d ∈ D}. ” (350). (16.2.3) There are three tableau rules for identity (see below).
| Principle of Identity Development (=D) |
| . ↓ a = a,i
(You can always add a line of the form a = a,i) |
| Substitutivity of Identicals (SI,D) |
| a = b,i ↓ Ax(a),i ↓ Ax(b),i
(where A is any atomic sentence distinct from a = b.) (Note: the world index on every line is the same, so substitution is licensed only within a world.) |
| Identity Invariance Rule (IIR,D) |
| a = b,i ↓ a = b,j
(where j is any world parameter on the branch distinct from i) |
(350, with names and additional text at the bottom made by me)
(16.2.4) Priest next gives two example tableaux for valid formulas in VK(NI), which is a variable domain system with necessary identity. And, “For future reference, we will call the formula ∀x∀y(x = y ⊃ □x = y) NI (Necessary Identity)” (351). (16.2.5) Priest next gives an example tableau for an invalid formula. (16.2.6) “Counter-models are read off from open branches as usual. In particular, where there is a bunch of lines of the form a = b, 0, b = c, 0, etc., a single denotation is provided for all the constants” (352). (16.2.7) Priest next gives an example counter-model.
[The Identity Predicate in Quantified Normal Modal Logic]
[Defining the Identity Predicate]
[The Three Identity Tableau Rules]
[Example Tableaux 1 and 2. NI (Necessary Identity)]
[Example Tableau 3]
[Counter-Models]
[Example Counter-Model]
Summary
[The Identity Predicate in Quantified Normal Modal Logic]
[We will now define the identity predicate in a quantified normal modal logic.]
[(ditto). (See section 12.5.1).]
Assume that we are dealing with any quantified (constant or variable domain) normal modal logic (without the Negativity Constraint). As in the classical case (12.5.1), we now distinguish one of the binary predicates as the identity predicate.
(350)
[Defining the Identity Predicate]
[“The denotation of the identity predicate is the same in every world, w, of an interpretation: vw(=) = {⟨d, d⟩ : d ∈ D}. ” (350).]
[(ditto). (See section 12.5.2).]
The denotation of the identity predicate is the same in every world, w, of an interpretation: vw(=) = {⟨d, d⟩ : d ∈ D}.
(350)
[The Three Identity Tableau Rules]
[There are three tableau rules for identity (see below).]
[The first two of the three rules of identity are the same as in section 12.5.3, only now with world designations:
| Principle of Identity Development (=D) |
| . ↓ a = a,i
(You can always add a line of the form a = a,i) |
| Substitutivity of Identicals (SI,D) |
| a = b,i ↓ Ax(a),i ↓ Ax(b),i
(where A is any atomic sentence distinct from a = b.) (Note: the world index on every line is the same, so substitution is licensed only within a world.) |
(350, with names and additional text at the bottom made by me)
The third rule is the Identity Invariance Rule (IIR):
| Identity Invariance Rule (IIR,D) |
| a = b,i ↓ a = b,j
(where j is any world parameter on the branch distinct from i) |
(350, with names and additional text at the bottom made by me)
]
There are three tableau rules for identity. The first two are exactly as in the classical case (12.5.3), modulo an appropriate world parameter:
Principle of Identity
Development (=D)
.
↓
a = a,i
(You can always add a line of the form a = a,i)
Substitutivity of Identicals (SI,D)
a = b,i
↓
Ax(a),i
↓
Ax(b),i
(where A is any atomic sentence distinct from a = b.)
(Note: the world index on every line is the same, so substitution is licensed only within a world.)
(350, with names and additional text at the bottom made by me)
– where, recall, A is any atomic sentence other than a = b. Note that in SI, the world index on every line is the same, so substitution is licensed only within a world. The third rule is the following:
Identity Invariance Rule (IIR,D)
a = b,i
↓
a = b,j
(where j is any world parameter on the branch distinct from i)
(350, with names and additional text at the bottom made by me)
where j is any world parameter on the branch distinct from i. I will call this the Identity Invariance Rule (IIR).
(350)
[Example Tableaux 1 and 2. NI (Necessary Identity)]
[Priest next gives two example tableaux for valid formulas in VK(NI), which is a variable domain system with necessary identity. And, “For future reference, we will call the formula ∀x∀y(x = y ⊃ □x = y) NI (Necessary Identity)” (351). ]
[Recall from section 16.1.2 that:
If S is any system of logic without identity, S(NI) will denote the system augmented by necessary identity, and S(CI) will denote the system of logic augmented by contingent identity.
(p.349, section 16.1.2)
We will be working now with a system called VK(NI). That means the system is augmented by necessary identity. I think that means it is identity as defined above in section 16.2.2 and especially section 16.2.3. The important idea there was that identity does not vary between worlds. The next thing to note is that the system in question is VK. Recall from section 15.3 that VK is a variable domain quantification modal logic system. What was notable about it is that the domain of quantification remains the same for all worlds, however, the valuation function v assigns for each world its own subset of the domain of existing things. We will now do tableaux in VK(NI), but the problem is that we have not yet summarized the sections where the rules are given for it. So let us try to reconstruct them for our purposes here, and later we may go back to do the whole sections in question. In section 15.4.1 (p.331), we learn that the tableau rules are modified from CK, which is a constant domain system. In section 14.3.1 (pp.309-310) we learn that the tableaux for CK are modified from those of K. We can start there. From what I understand from section 14.3.1, we will obtain the CK tableaux by using the K ones in section 2.4.4 (p.24) and adding quantifier rules from section 14.3.1 (p.310), which are like those for classical logic, section 12.4.1 (p.266); however, instead of the two instantiation rules given there (in section 14.3.1), we swap them with the ones given in section 15.4.1 (p.331). I probably having something here wrong, but for now let us just lay out the rules as such, including the identity rules from section 16.2.3 above:
| 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) |
(p.24, section 2.4.4)
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
(p.266, section 12.4.1)
| Universal Instantiation Development (UI,D) |
| ∀xA,i ↙ ↘ ℭa,i Ax(a),i
where a is any constant on the branch. (If there are not any, we select one at will.) |
| Particular Instantiation Development (PI,D) |
| ∃xA,i ↓ ℭc,i ↓ Ax(c),i
where c is any constant that does not occur so far on the branch. |
(p.331, section 15.4.1)
| Principle of Identity Development (=D) |
| . ↓ a = a,i
(You can always add a line of the form a = a,i) |
| Substitutivity of Identicals (SI,D) |
| a = b,i ↓ Ax(a),i ↓ Ax(b),i
(where A is any atomic sentence distinct from a = b.) (Note: the world index on every line is the same, so substitution is licensed only within a world.) |
| Identity Invariance Rule (IIR,D) |
| a = b,i ↓ a = b,j
(where j is any world parameter on the branch distinct from i) |
(350, with names and additional text at the bottom made by me)
With those as a possible set of rules we should use, see the example tableaux below for valid formulas where we try to apply them.]
Here are tableaux to demonstrate that ⊢VK(NI) ∀x∀y(x = y ⊃ □x = y), and ⊢VK(NI) ∀x∀y(x ≠ y ⊃ □x ≠ y). Clearly, the tableaux work in a similar way in VKt(NI), when □ is replaced by [F] or [P]. Since the variable domain logics are sub-logics of the corresponding constant domain logics (15.4.7, 15.5.5), these inferences are valid in all constant and variable domain quantified modal logics. It is the validity of these formulas that give this notion of identity its name: all true statements of identity or difference are necessarily | true (true for all future/past times). For future reference, we will call the formula ∀x∀y(x = y ⊃ □x = y) NI (Necessary Identity).
ditto)]
| ⊢VK(NI) ∀x∀y(x = y ⊃ □x = y) | ||
| 1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. .
11. .
12. .
13. | ¬∀x∀y(x = y ⊃ □x = y),0 ↓ ∃x¬∀y(x = y ⊃ □x = y),0 ↓ ℭa,0 ↓ ¬∀y(a = y ⊃ □a = y),0 ↓ ∃y¬(a = y ⊃ □a = y),0 ↓ ℭb,0 ↓ ¬(a = b ⊃ □a = b),0 ↓ a = b,0 ↓ ¬□a = b,0 ↓ ◊¬a = b,0 ↓ 0r1 ↓ ¬a = b,1 ↓ a = b,1 ×
| P .
1¬∀ .
2PI .
2PI .
4¬∀ .
5PI .
5PI .
7¬⊃ .
7¬⊃ .
9¬□ .
10◊r .
10◊r .
8,11IRR (13×12)
valid |
(enumeration and step accounting are my own and are probably mistaken)
The last line is obtained by applying the IIR from line eight.
| ⊢VK(NI) ∀x∀y(x ≠ y ⊃ □x ≠ y) | ||
| 1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. .
11. .
12. .
13. .
14. | ¬∀x∀y(x ≠ y ⊃ □x ≠ y),0 ↓ ∃x¬∀y(x ≠ y ⊃ □x ≠ y),0 ↓ ℭa,0 ↓ ¬∀y(a ≠ y ⊃ □a ≠ y),0 ↓ ∃y¬(a ≠ y ⊃ □a ≠ y),0 ↓ ℭb,0 ↓ ¬(a ≠ b ⊃ □a ≠ b),0 ↓ a ≠ b,0 ↓ ¬□a ≠ b,0 ↓ ◊¬a ≠ b,0 ↓ 0r1 ↓ ¬a ≠ b,1 ↓ a = b,1 ↓ a = b,0 ×
| P .
1¬∀ .
2PI .
2PI .
4¬∀ .
5PI .
5PI .
7¬⊃ .
7¬⊃ .
9¬□ .
10◊r .
10◊r .
12¬¬ .
13,11 IRR (14×8)
valid |
(enumeration and step accounting are my own and are probably mistaken)
Again, the last line is obtained by applying the IIR
(350-351)
[Example Tableau 3]
[Priest next gives an example tableau for an invalid formula.]
[We will now do an example tableau in CK(NI), which is a constant domain system with necessary identity. Given what we said above in section 16.2.4, I will guess that the rules we will use could be the following:
| 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) |
(p.24, section 2.4.4)
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
(p.266, section 12.4.1)
| Universal Instantiation Development (UI,D) |
| ∀xA,i ↓ Ax(a),i
where a is any constant on the branch. (If there are not any, we select one at will.) |
| Particular Instantiation Development (PI,D) |
| ∃xA,i ↓
where c is any constant that does not occur so far on the branch. |
(p.331, section 15.4.1)
| Principle of Identity Development (=D) |
| . ↓ a = a,i
(You can always add a line of the form a = a,i) |
| Substitutivity of Identicals (SI,D) |
| a = b,i ↓ Ax(a),i ↓ Ax(b),i
(where A is any atomic sentence distinct from a = b.) (Note: the world index on every line is the same, so substitution is licensed only within a world.) |
| Identity Invariance Rule (IIR,D) |
| a = b,i ↓ a = b,j
(where j is any world parameter on the branch distinct from i) |
(350, with names and additional text at the bottom made by me)
Let us apply these rules for the tableau example below.]
Here is another tableau to show that ⊬CK(NI) □∀x∀y((Sax ∧ Say) ⊃ x ≠ y):
| ⊬CK(NI) □∀x∀y((Sax ∧ Say) ⊃ x ≠ y) | ||
| 1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. .
11. .
12. .
13. .
14. | ¬□∀x∀y((Sax ∧ Say) ⊃ x ≠ y),0 ↓ ◊¬∀x∀y((Sax ∧ Say) ⊃ x ≠ y),0 ↓ 0r1 ↓ ¬∀x∀y((Sax ∧ Say) ⊃ x ≠ y),1 ↓ ∃x¬∀y((Sax ∧ Say) ⊃ x ≠ y),1 ↓ ¬∀y((Sab ∧ Say) ⊃ b ≠ y),1 ↓ ∃y¬((Sab ∧ Say) ⊃ b ≠ y),1 ↓ ¬((Sab ∧ Sac) ⊃ b ≠ c),1 ↓ Sab ∧ Sac,1 ↓ ¬b ≠ c,1 ↓ Sab,1 ↓ Sac,1 ↓ b = c,1 ↓ b = c,0
| P .
1¬□ .
2◊r .
2◊r .
4¬∀ .
5PI .
6¬∀ .
7PI .
8¬⊃ .
8¬⊃ .
9∧ .
9∧ .
10¬¬ . 3,13IRR (open)
invalid |
(enumeration and step accounting are my own and are probably mistaken)
(352)
[Counter-Models]
[“Counter-models are read off from open branches as usual. In particular, where there is a bunch of lines of the form a = b, 0, b = c, 0, etc., a single denotation is provided for all the constants” (352).]
[We will now make a counter-model, which is done in the “usual way.” As we have not been summarizing the previous sections, I am not entirely sure I know what way that is. But for now, I will use our most recent method, from section 13.3.4:
To read off a counter-model from an open branch of a tableau, the procedure is exactly as for classical logic, and E = v(ℭ). Since every object in D has a name in the interpretation, and given the definition of E, 13.2.6 assures us that to check that v(∃xA) = 1, we just have to show that v(Ax(c)) = 1 for some c such that ℭc is on the branch; and to check that v(∀xA) = 1, we just have to show that v(Ax(c)) = 1 for every constant, c, such that ℭc is on the branch.
(292, section 13.3.4)
But as in section 12.5.9and 13.6.5, we only need a single denotation for all identical constants in a world.]
Counter-models are read off from open branches as usual. In particular, where there is a bunch of lines of the form a = b, 0, b = c, 0, etc., a single denotation is provided for all the constants, as in 12.5.9and 13.6.5. (The 0 could, in fact, be any line number, because of the IIR.)
(352)
[Example Counter-Model]
[Priest next gives an example counter-model.]
[(ditto)]
Thus, in the counter-model given by the tableau of 16.2.5, W = {w0, w1}, w0Rw1, D = {∂a, ∂b}, v(a) = ∂a, v(b) = v(c) = ∂b, and vw1 (S) = {⟨∂a, ∂b ⟩}. In a picture:
_______________xxxxxxxxxxxxxxxx______________
|xSxxx∂axxx∂bx|xxxxxxxxxxxxxxx|xSxxx∂axxx∂bx|
|x∂axx×xxxx×xx|xxxwoxx→xxw1xxx|x∂axx×xxxx√xx|
|x∂bxx×xxxx×xx|xxxxxxxxxxxxxxx|x∂bxx×xxxx×xx|
_______________xxxxxxxxxxxxxxxx______________
I leave it as an exercise to check that this interpretation works.
(352)
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