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 distracting mistakes, because I have not finished proofreading. I have added my own terminology, abbreviations, and structures to the tableaux and to their rules, following David Agler’s
Symbolic Logic, so that I can more readily grasp the reasoning involved in them. Any mistakes made there are my own; see Priest’s text for the original and certainly correct renditions.]
Summary of
Graham Priest
An Introduction to Non-Classical Logic: From If to Is
1. Classical Logic and the Material Conditional
1.4. Tableaux
Brief summary:
We construct structures called tableaux to test for certain properties of arguments and formulas, especially validity and proof-theoretic consequence. The tableau has a structure of branches from a root down to tips. The structure can be displayed in the following way:
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
Nodes are the dots. The top node is the root, and those at the bottom are the tips. A branch is a path starting from the root and descending through a series of arrows as far as it can go.
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
To use the tableaux for validity (proof-theoretic consequence), we will need to place the premises (if there are any) on a single branch along with the negation of the conclusion. This beginning set-up is called the initial list. We then proceed to develop the branches using various transformational rules, namely:
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
|
“A tableau is complete iff every rule that can be applied has been applied” (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). Furthermore: “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” (8-9). Thus in this way we can use the tableau to test for proof-theoretic consequence(validity). If a branch closes, we do not need to develop it further. For practical convenience, we should try to make the tableau as simple as possible. One way to do this is by using non branch splitting rules before branch splitting ones. And, after applying a rule to a formula, it helps to place a tick mark next to it in order to signal that we may forget it.
Summary
1.4.1
[A tableaux has a structure of branches from a root down to tips.]
Priest will describe the structure of tableaux, which will be used to evaluate certain properties of formulas and sequents. They take the following form:
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
Nodes are the dots. The top node is the root, and those at the bottom are the tips. “Any path from the root down a series of arrows as far as you can go is called a branch” (6). [For example:
∙
|
↓
|
∙
|
↙ ↘
|
∙ ∙
|
↓ ↙ ↘
|
∙ ∙ ∙
|
1.4.2
[To use the tableaux to test inferences (or formulas) for validity, we will need to place the premises (if there are any) on a single branch along with the negation of the conclusion. This beginning set-up is called the initial list. We then begin to develop the branches using various transformational rules.]
Priest then explains how we use tableaux to test inferences for validity. We do so by beginning with “a single branch at whose nodes occur the premises (if there are any) and the negation of the conclusion” (6). [Note, if there are no premises, then we are perhaps testing for the validity of a formula. See
section 7.3.6 and
section 1.3.4.] This first single branch with the premises and the negation of the conclusion is called the
initial list (6). Then, we develop the tableau by using rules that extend the branches. We begin with the rules for the conditional. [Note, I will modify Priest’s presentation in accordance with David Agler’s system, because I am not clever enough to follow the operations used in a tableau when the rule names are omitted. With that in mind, I will give the rules names that more or less follow the pattern in Agler’s
Symbolic Logic. See
section 4.2.]
Conditional
Development (⊃D)
|
...........A ⊃ B
..........↙.....↘
.......¬A.........B
|
Negated Conditional
Development (¬⊃D)
|
..........¬(A ⊃ B)
..............↓
..............A
..............↓
.............¬B
|
Priest writes with regard to the above schemas:
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)
1.4.3
[To test for validity, we fully develop the tree branches (coming from the initial list) and see if all the branches close.]
Priest then shows how we can use these rules to test the validity of the sequent:
A ⊃ B, B ⊃ C ⊢ A ⊃ C
[Note, in the following I will add line numbers and rule abbreviations, in the style of Agler. See Agler’s
Symbolic Logic,
section 4.1.1.] [We are looking to find contradictions along all branches, where we place an ‘×’ to mean that it is closed. Priest returns to this idea later.]
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
|
Priest writes:
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)
[Note. We are not here discussing how branches close off. But I wonder about the ¬B on the left-most branch in line 7. I do not see in that branch a B, which would contradict the ¬B and close the branch. Later in section 1.4.6 we see that the reason it closes is because that branch has A and ¬A. And then in section 1.4.8 we learn that we do not need to continue developing once we reach a contradiction. So we might also develop this tree as:
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
|
]
1.4.4
[There are developmental rules for all the other connectives as well.]
Priest then provides the rules for the other connectives. [Again, I am making up my own names and abbreviations so that I can list the rules in the trees.]
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
|
Priest writes:
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)
1.4.5
[“A tableau is complete iff every rule that can be applied has been applied.”]
We say that a tableau is “complete iff every rule that can be applied has been applied” (8). Branches in some tableau might be infinite. [I am not sure, but I assume that means they cannot be complete.]
1.4.6
[“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.”]
Priest then defines other properties of branches and tableaux:
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)
Priest then notes that our tableau from before is closed, for: “the leftmost branch contains A and ¬A; the next contains A and ¬A (and C and ¬C); the next contains B and ¬B; the rightmost contains C and ¬C.” (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
|
1.4.7
[“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.”]
[Recall from
section 1.1.6 the notion of proof-theoretic validity:
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)
In section 1.4.3 above, we examined an argument. For the initial list, we had the premises along with the negated conclusion. We then applied a purely formal procedure that developed the initial list down branches of transformation, finding contradiction along all the branches. We defined a complete tableau as one where every developmental rule that can be applied has been applied. This seems to be similar to Agler’s term “fully decomposed tree” (see his
Symbolic Logic section 4.2.1). In Agler’s technique for testing for proof-theoretic validity, we do not need to fully decompose the tableau. Instead, we try to find contradictions as soon as possible so to close branches without needing to develop beyond what is necessary to close them. (In the next section, Priest will say the same thing. Perhaps the idea is that we can close the branch early, because we know that were it completed, it would still be closed. Thus a tableau with early-closed branches can still be considered to be virtually a closed and completed tree.)] In a given set of formulas (which might be a set containing just one formula), a particular formula is a proof-theoretic consequence of the other formulas if and only if the tableau with the premises and negated conclusion produces a complete and closed tree. [In the case of a singular formula, it would be the proof-theoretic consequence of no other formulas, meaning that simply by negating it, this produces a complete and closed tree.]
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)
1.4.8
[We can use the tableau to test for proof-theoretic consequence. If a branch closes, we do not need to develop it further. For practical convenience, we should try to make the tableau as simple as possible. One way to do this is by using non branch splitting rules before branch splitting ones.]
Since the tree in 1.4.3 is a complete and closed tableau, that means:
A ⊃ B, B ⊃ C ⊢ A ⊃ C
Priest will now show that
⊢ ((A ⊃ B) ∧ (A ⊃ C)) ⊃ (A ⊃ (B ∧ C))
In this tableau, we save space by omitting the vertical arrows, where the branch does not divide. [Again I add line numbers and rule justifications, which may be incorrect. Please consult the original text.] As there is just this formula, we will negate it and look to see if it creates a complete and closed tree. It does, so 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
|
Priest writes:
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)
1.4.9
[After applying a rule to a formula, it helps to place a tick mark next to it in order to signal that we may forget it.]
When developing our tableaux, it can be very useful to place a tick or checkmark beside the formulas that have already been developed by some rule. This allows us to forget about it and instead work on the formulas developed from it (9).
Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.
.
