.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 distracting mistakes, because I have not finished proofreading.]
Summary of
Graham Priest
An Introduction to Non-Classical Logic: From If to Is
Part I
Prop0sitional Logic
8
First Degree Entailment
8.3
Tableaux for FDE
Brief summary:
The tableaux for First Degree Entailment will allow us to evaluate arguments for validity. The rules are modeled after those of classical logic, but are made more complex with the inclusion of a new addition to the formulations, namely, after each formula, we add a comma and then + for true ones and − for false ones, like:
p,+
and
¬p,−
We set up the tableaux to test for valid inference by first stacking the premises and lastly the negated conclusion. We then use the tableau rules to develop the branches until we can determine them as being either open or closed.
| Double Negation Development, True (¬¬D,+) |
| ¬¬A,+ ↓ A,+ |
| Double Negation Development, False (¬¬D,−) |
| ¬¬A,− ↓ A,− |
| Conjunction Development, True (∧D,+) |
| A ∧ B,+ ↓ A,+ B,+ |
| Conjunction Development, False (∧D,−) |
| A ∧ B,− ↙ ↘ A,− B,− |
| Negated Conjunction Development, True (¬∧D,+) |
| ¬(A ∧ B),+ ↓ ¬A ∨ ¬B,+ |
| Negated Conjunction Development, False (¬∧D,−) |
| ¬(A ∧ B),− ↓ ¬A ∨ ¬B,− |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+ ↙ ↘ A,+ B,+ |
| Disjunction Development, False (∨D,−) |
| A ∨ B,- ↓ A,- B,- |
| Negated Disjunction Development, True (¬∨D, +) |
| ¬(A ∨ B),+ ↓ ¬A ∧ ¬B,+ |
| Negated Disjunction Development, False(¬∨D, -) |
| ¬(A ∨ B),- ↓ ¬A ∧ ¬B,- |
Braches close when they contain nodes of the form A,+ and A,−. Open branches indicate counter-models: to any p,+, we assign pρ1; and to any ¬p,+ we assign pρ0. And we make no other assignments than that. This technique will make the premises true and the conclusion not true, when it is an invalid inference. The tableaux are sound and complete.
[The FDE Tableaux as Modified Classical Tableaux]
[+ and – Symbols]
[Validity Set-Up]
[Tableaux Rules for FDE]
[Branch Closing]
[Example of a Valid Inference]
[An example of an Invalid Inference]
[Countermodels from Open Branches]
[Demonstration of the Branch Technique]
[Soundness and Completeness of the Tableaux]
Summary
[The FDE Tableaux as Modified Classical Tableaux]
[The tableaux for FDE are modified from those of classical logic.]
[Recall from section 1.4 the tableaux rules for classical logic. For my own purposes, I called them developments, and I used the names and symbols from David Agler’s Symbolic Logic. (See section 4.2 of Agler’s text.) The following comes from the brief summary of section 1.4 of the current text:
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).(See entry on section 1.4.)
] Priest will now modify the tableaux for classical propositional calculus to obtain the tableaux for First Degree Entailment (FDE).
Tableaux for FDE can be obtained by modifying those for the classical propositional calculus as follows.
(144)
[+ and – Symbols]
[After each true formula we write a comma then +, and after each false, −.]
[In the classical tableaux, we never designated the formulas as being either true or false. Here we will.]
Each entry of the tableau is now of the form A, + or A, −. Intuitively, A, + means that A is true, A, − means that it isn’t. As we noted in 8.2.4, and as with intuitionist logic (6.4.1), ¬A,+ no longer means the same, intuitively, as A,−.
(144)
[Validity Set-Up]
[To test for valid inference, we set up the tree by first stacking the premises and lastly the negated conclusion.]
[Recall from Agler’s Symbolic Logic section 4.6.5 that an argument is valid if the set of propositions made of the premises and the negated conclusion makes a closed tree. Here was an example for:
P→Q, P ⊢ Q
(Agler, Symbolic Logic, p.149)
.] To test for valid inference, we set up the tree such that the premises and the negated conclusion are stacked:
To test the claim that A1, ... , An ⊢ B , we start with an initial list of the form:
A1,+
.
.
.
An,+
B,−
(Priest, 144)
[Tableaux Rules for FDE]
[We develop the tableaux by means of a set of rules where we always designate the truth value of the formula and distinguish them by those means too.]
[In the following we give the tableaux rules, as noted from section 1.4, I for my own purposes called them developments, and I used the names and symbols from David Agler’s Symbolic Logic. (Again, see section 4.2 of Agler’s text.)
| Double Negation Development, True (¬¬D,+) |
| ¬¬A,+ ↓ A,+ |
| Double Negation Development, False (¬¬D,−) |
| ¬¬A,− ↓ A,− |
| Conjunction Development, True (∧D,+) |
| A ∧ B,+ ↓ A,+ B,+ |
| Conjunction Development, False (∧D,−) |
| A ∧ B,− ↙ ↘ A,− B,− |
| Negated Conjunction Development, True (¬∧D,+) |
| ¬(A ∧ B),+ ↓ ¬A ∨ ¬B,+ |
| Negated Conjunction Development, False (¬∧D,−) |
| ¬(A ∧ B),− ↓ ¬A ∨ ¬B,− |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+ ↙ ↘ A,+ B,+ |
| Disjunction Development, False (∨D,−) |
| A ∨ B,- ↓ A,- B,- |
| Negated Disjunction Development, True (¬∨D, +) |
| ¬(A ∨ B),+ ↓ ¬A ∧ ¬B,+ |
| Negated Disjunction Development, False(¬∨D, -) |
| ¬(A ∨ B),- ↓ ¬A ∧ ¬B,- |
Let us go through the reasoning behind them.
| Conjunction Development, True (∧D,+) |
| A ∧ B,+ ↓ A,+ B,+ |
Suppose that A ∧ B. That could only be so if both A and B are true. Thus we can derive A as true and B as true.
| Conjunction Development, False (∧D,−) |
| A ∧ B,− ↙ ↘ A,− B,− |
Now suppose that A ∧ B is false. Then either (or both) are false.
| Disjunction Development, True (∨D,+) |
| A ∨ B,+ ↙ ↘ A,+ B,+ |
Now suppose that A ∨ B is true. That that means at least one of the two disjuncts needs to be true.
| Disjunction Development, False (∨D,−) |
| A ∨ B,- ↓ A,- B,- |
Now suppose is A ∨ B false. That means both disjuncts need to be false. Priest then writes:
The other rules are also easy to remember, since ¬(A ∧ B) and ¬A∨¬B have the same truth values in FDE, as do ¬(A ∨ B) and ¬A∧¬B, and ¬¬A and A. (De Morgan’s laws and the law of double negation, respectively.)
(145)
Let us work out the truth values here for the first pairing, using what was said in section 8.2.:
¬(A ∧ B)ρ???
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬(A ∧ B) Configuration one:
Aρ1
Bρ1
A ∧ Bρ1
¬(A ∧ B)ρ0
¬A∨¬B Configuration one:
Aρ1
Bρ1
¬Aρ0
¬Bρ0
¬A∨¬Bρ0
[Thus for configuration one, both are 0]
¬(A ∧ B) Configuration two:
Aρ1
Bρ0
A ∧ Bρ0
¬(A ∧ B)ρ1
¬A∨¬B Configuration two:
Aρ1
Bρo
¬Aρ0
¬Bρ1
¬A∨¬Bρ¬A∨¬Bρ1
[Thus for configuration two, both are 1]
¬(A ∧ B) Configuration three:
Aρo
Bρ1
A ∧ Bρ0
¬(A ∧ B)ρ1
¬A∨¬B Configuration three:
Aρ1
Bρo
¬Aρ0
¬Bρ1
¬A∨¬Bρ1
[Thus for configuration three, both are 1]
¬(A ∧ B) Configuration four:
Aρo
Bρ0
A ∧ Bρ0
¬(A ∧ B)ρ1
¬A∨¬B Configuration four:
Aρ0
Bρo
¬Aρ1
¬Bρ1
¬A∨¬Bρ1
[Thus for configuration four, both are 1]
¬(A ∧ B) Configuration five:
Aρ1
Aρo
Bρ1
A ∧ Bρ0
A ∧ Bρ1
¬(A ∧ B)ρ1
¬(A ∧ B)ρ0
¬A∨¬B Configuration five:
Aρ1
Aρo
Bρ1
¬Aρ0
¬Aρ1
¬Bρ0
¬A∨¬Bρ1
¬A∨¬Bρ0
[Thus for configuration five, both are 1 and 0]
¬(A ∧ B) Configuration six:
Aρ1
Aρo
Bρ0
A ∧ Bρ0
A ∧ Bρ0
¬(A ∧ B)ρ1
¬A∨¬B Configuration six:
Aρ1
Aρo
Bρ0
¬Aρ0
¬Aρ1
¬Bρ1
¬A∨¬Bρ1
[Thus for configuration six, both are 1]
¬(A ∧ B) Configuration seven:
Aρ1
Bρ1
Bρ0
A ∧ Bρ0
A ∧ Bρ1
¬(A ∧ B)ρ1
¬(A ∧ B)ρ0
¬A∨¬B Configuration seven:
Aρ1
Bρ1
Bρ0
¬Aρ0
¬Bρ0
¬Bρ1
¬A∨¬Bρ1
¬A∨¬Bρ0
[Thus for configuration seven, both are 1 and 0]
¬(A ∧ B) Configuration eight:
Aρ0
Bρ1
Bρ0
A ∧ Bρ0
¬(A ∧ B)ρ1
¬A∨¬B Configuration eight:
Aρ0
Bρ1
Bρ0
¬Aρ1
¬Bρ0
¬Bρ1
¬A∨¬Bρ1
[Thus for configuration eight, both are 1]
¬(A ∧ B) Configuration nine:
Aρ1
Aρ0
Bρ1
Bρ0
A ∧ Bρ0
A ∧ Bρ1
¬(A ∧ B)ρ1
¬(A ∧ B)ρ0
¬A∨¬B Configuration nine:
Aρ1
Aρ0
Bρ1
Bρ0
¬Aρ0
¬Aρ1
¬Bρ0
¬Bρ1
¬A∨¬Bρ1
¬A∨¬Bρ0
[Thus for configuration nine, both are 1]
(I am not sure if we do something for neither value. Maybe it is like this, and let us first recall the evaluation rules:)
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬(A ∧ B) Configuration ten:
Bρ1
A ∧ Bρ[no such relation]
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ[no such relation]
¬A∨¬B Configuration ten:
Bρ1
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬Aρ[no such value]
¬Bρ0
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ[no such value]
[Thus for configuration ten, both are not valued]
¬(A ∧ B) Configuration eleven:
Bρ0
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ0
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ1
¬A∨¬B Configuration eleven:
Bρ0
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬Aρ[no such value]
¬Bρ1
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ[no such value]
[Thus for configuration eleven, both are not valued]
¬(A ∧ B) Configuration twelve:
Bρ1
Bρ0
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ0
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ1
¬A∨¬B Configuration twelve:
Bρ1
Bρ0
¬Aρ[no such value]
¬Bρ0
¬Bρ1
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ1
[Thus for configuration twelve, both are 1]
¬(A ∧ B) Configuration thirteen:
[Neither has any value]
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ[no such value]
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ[no such value]
¬A∨¬B Configuration thirteen:
[Neither has any value]
¬Aρ[no such value]
¬Bρ[no such value]
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ[no such value]
[Thus for configuration thirteen, both are not valued]
¬(A ∧ B) Configuration fourteen:
Aρ1
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ[no such value]
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ[no such value]
¬A∨¬B Configuration fourteen:
Aρ1
¬Aρ0
¬Bρ[no such value]
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ[no such value]
[Thus for configuration fourteen, both are not valued]
¬(A ∧ B) Configuration fifteen:
Aρ0
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ0
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ1
¬A∨¬B Configuration fifteen:
Aρ0
¬Aρ1
¬Bρ[no such value]
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ1
[Thus for configuration fifteen, both are 1]
¬(A ∧ B) Configuration sixteen:
Aρ1
Aρ0
A ∧ Bρ1 iff Aρ1 and Bρ1
A ∧ Bρ0 iff Aρ0 or Bρ0
A ∧ Bρ0
¬Aρ1 iff Aρ0
¬Aρ0 iff Aρ1
¬(A ∧ B)ρ1
¬A∨¬B Configuration sixteen:
Aρ1
Aρ0
¬Aρ1
¬Aρ0
¬Bρ[no such value]
A ∨ Bρ1 iff Aρ1 or Bρ1
A ∨ Bρ0 iff Aρ0 and Bρ0
¬A∨¬Bρ1
[Thus for configuration sixteen, both are 1]
[Thus for all configurations, both take the same values.]
(I realize there are mistakes and omissions, but I just wanted to see how it all plays out.) We can imagine then doing the same thing for ¬(A ∨ B) and ¬A∧¬B, and ¬¬A and A. Given these equivalences, we can see how the other evaluations would follow.]
[See rules given above]
The first two rules speak for themselves: if A ∧ B is true, A and B are true; if A ∧ B is not true, then one or other of A and B is not true. Similarly for the rules for disjunction. The other rules are also easy to remember, since ¬(A ∧ B) and ¬A∨¬B have the same truth values in FDE, as do ¬(A ∨ B) and ¬A∧¬B, and ¬¬A and A. (De Morgan’s laws and the law of double negation, respectively.)
(145)
[Branch Closing]
[Braches close when they contain nodes of the form A,+ and A,−.]
A branch here is closed not if there is a formula and its negation, but rather if there is a true and a false valued formula.
Finally, a branch of a tableau closes if it contains nodes of the form A,+ and A,−.
(145)
[Example of a Valid Inference]
[We make an example to illustrate how the rules work for a valid inference.]
We will now do the following formula as an example. [For my own convenience, I will follow a pattern like in Agler’s Symbolic Logic section 4.1.1, but I of course can be making many mistakes, so please use Priest’s text primarily.]
¬(B ∧ ¬C) ∧ A ⊢ (¬B ∨ C) ∨ D
| ¬(B ∧ ¬C) ∧ A ⊢ (¬B ∨ C) ∨ D | ||
| 1. . 2. . 3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. .
11. | ¬(B ∧ ¬C) ∧ A,+ . (¬B ∨ C) ∨ D,− . ¬(B ∧ ¬C),+ . A,+ . ¬B∨¬¬C,+ . ¬B ∨ C,− . D,− . ¬B,− . C,− ↙ ↘ ¬B,+ ¬¬C,+ . × C,+ x ×
| P .
P .
1∧D,+ .
1∧D,+ .
3¬∧D,+ .
2∨D,- .
2∨D,- .
6∨D,- .
6∨D,- .
5∨D,+
10¬¬D,+
. Valid |
(based on p.145)
The third and fourth lines come from the first, by the rule for true conjunctions. The next line comes from the third by De Morgan’s laws. The next two lines come from the second by the rule for untrue disjunctions, which is then applied again, to get the next two lines. The branching arises because of the rule for true disjunctions, applied to line five. The left | branch is now closed because of ¬B,− and ¬B,+; an application of double negation then closes the righthand branch.
(145-146)
[An example of an Invalid Inference]
[We make an example to illustrate how the rules work for an invalid inference.]
We will now show this invalidity:
p ∧ (q ∨¬q) ⊬ r
| p ∧ (q ∨¬q) ⊬ r | ||
| 1. .
2. .
3. .
4. .
5. | p ∧ (q ∨ ¬q),+ . r,− . p,+ . q ∨ ¬q,+ ↙ ↘ q,+ ¬q,+ | P .
P .
1∧D,+ .
1∧D,+
4∨D,+ |
(based on p.146)
[Countermodels from Open Branches]
[Open branches indicate counter-models. To any p,+, we assign pρ1; and to any ¬p,+ we assign pρ0.]
The next part reads:
Counter-models can be read off from open branches in a simple way. For every parameter, p, if there is a node of the form p,+, set pρ1; if there is a node of the form ¬p,+, set pρ0. No other facts about ρ obtain.
(146)
[I may not follow, but let us consider how this might work. Perhaps the idea is that each open branch can serve to indicate a counterexample. Let us take the left branch from above, and let us try to set the values accordingly.
pρ1
qρ1
rρ?
Is this a countermodel for the inference proposed in
p ∧ (q ∨¬q) ⊬ r
? Recall from section 8.2.8 that:
Semantic consequence is defined, in the usual way, in terms of truth preservation, thus:
Σ ⊨ A iff for every interpretation, ρ, if Bρ1 for all B ∈ Σ then Aρ1
(144)
As we will see in section 8.3.9 below, we assign no value to r (maybe that is what “No other facts about ρ obtain” means, but I am not sure) and thus it is shown to be invalid as the premises are true and the conclusion not true.]
[Demonstration of the Branch Technique]
[The open branch technique makes the premises true and the conclusion not true.]
Priest then explains what we noted above in section 8.3.8 about how the counter-model technique works in that example.
Thus, the counter-model defined by the righthand branch of the tableau in 8.3.7 is the interpretation ρ, where pρ1 and qρ0 (and no other relations hold). It is easy to check directly that this interpretation makes the premises true and the conclusion untrue.
(146)
[Soundness and Completeness of the Tableaux]
[The tableaux are sound and complete.]
Later we prove that the tableaux are sound and complete:
The tableaux are sound and complete with respect to the semantics. This is proved in 8.7.1–8.7.7.
(146)
From:
Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.
Also cited:
Agler, David. 2013. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman & Littlefield.
.
No comments:
Post a Comment