.jpeg)
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
13.
Free Logics
13.3
Tableaux
Brief summary:
(13.3.1) The tableau rules for free logics are the same as for classical logic, except the rules for universal and particular instantiation are different. (Below I compile all the rules.)
| Double Negation Development (¬¬D) |
| ¬¬A ↓ A |
| Conjunction Development (∧D) |
| A ∧ B ↓ A ↓ B |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B) ↙ ↘ ¬A ¬B |
| Disjunction Development (∨D) |
| A ∨ B ↙ ↘ A B |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B) ↓ ¬A ↓ ¬B |
| Conditional Development (⊃D) |
| A ⊃ B ↙ ↘ ¬A B |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B) ↓ A ↓ ¬B |
| Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A B ¬B |
| Negated Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A ¬B B |
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
| Universal Instantiation Development (UI,D) |
| ∀xA ↙ ↘ ¬ℭa Ax(a)
where a is any constant on the branch (choosing a new constant only if there are none there already) |
| Particular Instantiation Development (PI,D) |
| ∃xA ↓ ℭc ↓ Ax(c)
where c is a constant new to the branch |
(6-8; 266; 291, with names and additional text at the bottom made by me)
(13.3.2) Priest next gives an example tableau for a valid inference. (13.3.3) Priest then gives a couple example tableaux for invalid inferences. (13.3.4) “To read off a counter-model from an open branch, we take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes.)” (p.268). And, E = v(ℭ). (13.3.5) Priest next provides a couple example counter-models.
[Tableau Rules for Free Logics]
[Tableau Example 1]
[Tableau Examples 2 and 3]
[Counter-Models]
[Counter-Model Examples]
Summary
[Tableau Rules for Free Logics]
[The tableau rules for free logics are the same as for classical logic, except the rules for universal and particular instantiation are different.]
[(ditto) (Below I compile all the rules.)
| Double Negation Development (¬¬D) |
| ¬¬A ↓ A |
| Conjunction Development (∧D) |
| A ∧ B ↓ A ↓ B |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B) ↙ ↘ ¬A ¬B |
| Disjunction Development (∨D) |
| A ∨ B ↙ ↘ A B |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B) ↓ ¬A ↓ ¬B |
| Conditional Development (⊃D) |
| A ⊃ B ↙ ↘ ¬A B |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B) ↓ A ↓ ¬B |
| Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A B ¬B |
| Negated Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A ¬B B |
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
| Universal Instantiation Development (UI,D) |
| ∀xA ↙ ↘ ¬ℭa Ax(a)
where a is any constant on the branch (choosing a new constant only if there are none there already) |
| Particular Instantiation Development (PI,D) |
| ∃xA ↓ ℭc ↓ Ax(c)
where c is a constant new to the branch |
(6-8; 266; 291, with names and additional text at the bottom made by me)
]
The tableaux for free logic are the same as those for classical logic, except that the rules of universal and particular instantiation are now formulated as follows:
ℭ
Universal Instantiation
Development (UI,D)
∀xA
↙ ↘
¬ℭa Ax(a)
where a is any constant on the branch (choosing a new constant only if there are none there already)
Particular Instantiation
Development (PI,D)
∃xA
↓
ℭc
↓
Ax(c)
where c is a constant new to the branch
(291, with names and additional text at the bottom made by me)
a is any constant on the branch (choosing a new constant only if there are none there already); c is a constant new to the branch.
(291)
[Tableau Example 1]
[Priest next gives an example tableau for a valid inference.]
[(ditto)]
Here is a tableau to demonstrate that ∀xPx, ∃xQx ⊢ ∃x(Px ∧ Qx).
∀xPx, ∃xQx ⊢ ∃x(Px ∧ Qx)
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
.
8.
.
9.
.
10.
∀xPx
↓
∃xQx
↓
¬∃x(Px ∧ Qx)
↓
∀y¬(Px ∧ Qx)
↓
ℭc
↓
Qc
↙ ↘
¬ℭc Pc
× ↙ ↘
¬ℭc ¬(Pc ∧ Qc)
× ↙ ↘
¬Pc ¬Qc
× ×
P
.
P
.
P
.
3¬∀
.
2PI
.
2PI
.
1UI
(7×5)
4UI
(7×5)
8¬∧
(9a×7b)
(9b×6)
valid
(enumeration and step accounting are my own and are probably mistaken)
The new rule for particular instantiation is applied at lines five and six. The new rule for universal instantiation is applied the first two times the tableau splits.
(292)
[Tableau Examples 2 and 3]
[Priest then gives a couple example tableaux for invalid inferences.]
[(ditto)]
Here are two more tableaux, showing that Pa ⊬ ∃xPx, and ⊬ ∃x(Px ∨ ¬Px).
Pa ⊬ ∃xPx
1.
.
2.
.
3.
.
4.
Pa
↓
¬∃xPx
↓
∀y¬Px
↙ ↘
¬ℭa ¬Pa
×
P
.
P
.
2¬∃
.
3UI
(4×1)
(open)
invalid
(enumeration and step accounting are my own and are probably mistaken)
⊬ ∃x(Px ∨ ¬Px)
1.
.
2.
.
3.
.
4.
.
5.
¬∃x(Px ∨ ¬Px)
↓
∀y¬(Px ∨ ¬Px)
↙ ↘
¬ℭa ¬(Pa ∨ ¬Pa)
↓
¬Pa
↓
¬¬Pa
×
P
.
1¬∃
.
2UI
.
3¬∨
.
3¬∨
(5×4)
(open)
invalid
(enumeration and step accounting are my own and are probably mistaken)
(292)
[Counter-Models]
[“To read off a counter-model from an open branch, we take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes.)” (p.268). And, E = v(ℭ).]
[Recall from section 12.4.8 how we construct counter-models:
To read off a counter-model from an open branch, we take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes.)
(p.268, section 12.4.8)
To this we add that E = v(ℭ).]
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)
[Counter-Model Examples]
[Priest next provides a couple example counter-models.]
[Priest will now construct counter-models for the two tableaux of section 13.3.3 above. The first one was:
| Pa ⊬ ∃xPx | ||
| 1. .
2. .
3. .
4. | Pa ↓ ¬∃xPx ↓ ∀y¬Px ↙ ↘ ¬ℭa ¬Pa × | P .
P .
2¬∃ .
3UI (4×1) (open) invalid |
(enumeration and step accounting are my own and are probably mistaken)
The open branch here is the left one. On that branch, there is only one constant, a, and since also Pa, we have: D = {∂a} = v(P). And since E = v(ℭ) (see section 13.3.4 above) and also since we have on the branch just ¬ℭa for the existence predicate, that gives us: E = φ = v(ℭ). We of course assign the constant as: v(a) = ∂a. So let us see if this makes the premises true but the conclusion not true. The inference is Pa ⊬ ∃xPx. The premise we assigned as true, because a is P. But recall the truth conditions for the quantifiers:
v(∀xA) = 1 iff for all d ∈ E, v(Ax(kd)) = 1 (otherwise it is 0)
v(∃xA) = 1 iff for some d ∈ E, v(Ax(kd)) = 1 (otherwise it is 0)
(p.291, section 13.2.4)
As we can see, in order for ∃xPx to be true, there needs to be something in the E set that is P. But we know that the E set is empty. That means the conclusion is not true even though the premise is true. Now let us take a look again at the second one:
| ⊬ ∃x(Px ∨ ¬Px) | ||
| 1. .
2. .
3. .
4. .
5. | ¬∃x(Px ∨ ¬Px) ↓ ∀y¬(Px ∨ ¬Px) ↙ ↘ ¬ℭa ¬(Pa ∨ ¬Pa) ↓ ¬Pa ↓ ¬¬Pa × | P .
1¬∃ .
2UI .
3¬∨ .
3¬∨ (5×4) (open) invalid |
(enumeration and step accounting are my own and are probably mistaken)
Here in the open branch on the left, we only have one constant, a. So: D = {∂a}. Regarding the existence predicate, we only have ¬ℭa. So: E = φ = v(ℭ). Of course v(a) = ∂a. But we have nothing that takes the predicate P, so: v(P) = φ. Let us check the formula, which is ⊬ ∃x(Px ∨ ¬Px). Since nothing takes the P predicate, we have the conclusion as not true.]
The counter-model determined by the open branch of the first tableau of 13.3.3 is as follows: D = {∂a} = v(P), E = φ = v(ℭ), and v(a) = ∂a. In the counter-model determined by the open branch of the second tableau, D = {∂a}, E = φ = v(ℭ), v(a) = ∂a, and v(P) = φ. It is easy to check that these work. Details are left as an exercise.
(293)
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