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]
Brief summary:
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
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
|
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
Conditional
Development (⊃D)
|
...........A ⊃ B
..........↙.....↘
.......¬A.........B
|
Negated Conditional
Development (¬⊃D)
|
..........¬(A ⊃ B)
..............↓
..............A
..............↓
.............¬B
|
The rule on the right is to be interpreted as follows. If we have a formula ¬(A ⊃ B) at a node, then every branch that goes through that node is extended with two further nodes, one for A and one for ¬B. The rule on the left is interpreted similarly: if we have a formula A ⊃ B at a node, then every branch that goes through that node is split at its tip into two branches; one contains a node for ¬A; the other contains a node for B.(6)
A ⊃ B, B ⊃ C ⊢ A ⊃ C
A ⊃ B, B ⊃ C ⊢ A ⊃ C
| ||
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
|
A ⊃ B
↓
B ⊃ C
↓
¬(A ⊃ C)
↓
A
↓
¬C
↙ ↘
¬A B
↙ ↓ ↓ ↘
¬B C ¬B C
× × × ×
|
P
.
P
.
P
.
3¬⊃D
.
3¬⊃D
.
1⊃D
.
2⊃D
Valid
|
The first three formulas are the premises and negated conclusion. The next two formulas are produced by the rule for the negated conditional applied to the negated conclusion; the first split on the branch is produced by applying the rule for the conditional to the first premise; the next splits are produced by applying the same rule to the second premise. (Ignore the ‘×’s: we will come back to those in a moment.)(7)
A ⊃ B, B ⊃ C ⊢ A ⊃ C
| ||
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
|
A ⊃ B
↓
B ⊃ C
↓
¬(A ⊃ C)
↓
A
↓
¬C
↙ ↘
¬A B
× ↓ ↘
¬B C
× ×
|
P
.
P
.
P
.
3¬⊃D
.
3¬⊃D
.
1⊃D
.
2⊃D
Valid
|
Double Negation
Development (¬¬D)
|
............¬¬A
.............↓
.............A
|
Disjunction
Development (∨D)
|
...........A ∨ B
..........↙.....↘
........A.........B
|
Negated Disjunction
Development (¬∨D)
|
.........¬(A ∨ B)
.............↓
............¬A
.............↓
............¬B
|
Negated Conjunction
Development (¬∧D)
|
¬(A ∧ B)
↙ ↘
¬A ¬B
|
Conjunction
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
|
Intuitively, what a tableau means is the following. If we apply a rule to a formula, then if that formula is true in an interpretation, so are the formulas below on at least one of the branches that the rule generates. (Of course, there may be only one such branch.)(8)
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.(8)
A ⊃ B, B ⊃ C ⊢ A ⊃ C
| ||
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
|
A ⊃ B
↓
B ⊃ C
↓
¬(A ⊃ C)
↓
A
↓
¬C
↙ ↘
¬A B
↙ ↓ ↓ ↘
¬B C ¬B C
× × × ×
|
P
.
P
.
P
.
3¬⊃D
.
3¬⊃D
.
1⊃D
.
2⊃D
Valid
|
The second notion of validity is proof-theoretic. Validity is defined in terms of some purely formal procedure (that is, one that makes reference only to the symbols of the inference). We use the metalinguistic symbol ‘⊢’ for this notion of validity. In our case, this procedure will (mainly) be one employing tableaux. What distinguish different logics here are the different tableau procedures employed.(4)
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.5 (8-9)5. There may, in fact, be several completed trees for an inference, depending upon the order of the premises in the initial list and the order in which rules are applied. Fortunately, they all give the same result, though this is not entirely obvious. See 1.14, problem 5.(9)
A ⊃ B, B ⊃ C ⊢ A ⊃ C
⊢ ((A ⊃ B) ∧ (A ⊃ C)) ⊃ (A ⊃ (B ∧ C))
⊢((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
|
Note that when we find a contradiction on a branch, there is no point in continuing it further. We know that the branch is going to close, whatever else is added to it. Hence, we need not bother to extend a branch as soon as it is found to close. Notice also that, wherever possible, we apply rules that do not split branches before rules that split branches. Though this is not essential, it keeps the tableau simpler, and is therefore useful practically.(9)
No comments:
Post a Comment