## 18 Jan 2018

### Priest (8.3) Introduction to Non-Classical Logic, ‘Tableaux for FDE [First Degree Entailment]’, summary

[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 1; and to any ¬p,+ we assign 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.

Contents

8.3.1

[The FDE Tableaux as Modified Classical Tableaux]

8.3.2

[+ and – Symbols]

8.3.3

[Validity Set-Up]

8.3.4

[Tableaux Rules for FDE]

8.3.5

[Branch Closing]

8.3.6

[Example of a Valid Inference]

8.3.7

[An example of an Invalid Inference]

8.3.8

[Countermodels from Open Branches]

8.3.9

[Demonstration of the Branch Technique]

8.3.10

[Soundness and Completeness of the Tableaux]

Summary

8.3.1

[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)

[contents]

8.3.2

[+ 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)

[contents]

8.3.3

[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)

[contents]

8.3.4

[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)ρ???

¬1 iff 0

¬0 iff 1

A1 iff 1 and 1

A0 iff 0 or 0

A1 iff 1 or 1

A0 iff 0 and 0

¬(A B)  Configuration one:

1

1

A Bρ1

¬(A B)ρ0

¬A∨¬B Configuration one:

1

1

¬0

¬0

¬A∨¬0

[Thus for configuration one, both are 0]

¬(A B)  Configuration two:

1

0

A Bρ0

¬(A B)ρ1

¬A∨¬B Configuration two:

1

o

¬0

¬1

¬A∨¬¬A∨¬Bρ1

[Thus for configuration two, both are 1]

¬(A B)  Configuration three:

o

1

A Bρ0

¬(A B)ρ1

¬A∨¬B Configuration three:

1

o

¬0

¬1

¬A∨¬1

[Thus for configuration three, both are 1]

¬(A B)  Configuration four:

o

0

A Bρ0

¬(A B)ρ1

¬A∨¬B Configuration four:

0

o

¬1

¬1

¬A∨¬1

[Thus for configuration four, both are 1]

¬(A B)  Configuration five:

1

o

1

A Bρ0

A Bρ

¬(A B)ρ1

¬(A B)ρ0

¬A∨¬B Configuration five:

1

o

1

¬0

¬1

¬0

¬A∨¬1

¬A∨¬0

[Thus for configuration five, both are 1 and 0]

¬(A B)  Configuration six:

1

o

0

A Bρ0

A Bρ

¬(A B)ρ1

¬A∨¬B Configuration six:

1

o

0

¬0

¬1

¬1

¬A∨¬1

[Thus for configuration six, both are 1]

¬(A B)  Configuration seven:

1

1

0

A Bρ0

A Bρ

¬(A B)ρ1

¬(A B)ρ0

¬A∨¬B Configuration seven:

1

1

0

¬0

¬0

¬1

¬A∨¬1

¬A∨¬0

[Thus for configuration seven, both are 1 and 0]

¬(A B)  Configuration eight:

0

1

0

A Bρ0

¬(A B)ρ1

¬A∨¬B Configuration eight:

0

1

0

¬1

¬0

¬1

¬A∨¬1

[Thus for configuration eight, both are 1]

¬(A B)  Configuration nine:

1

0

1

0

A Bρ0

A Bρ1

¬(A B)ρ1

¬(A B)ρ0

¬A∨¬B Configuration nine:

1

0

1

0

¬0

¬1

¬0

¬1

¬A∨¬1

¬A∨¬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:)

¬1 iff 0

¬0 iff 1

A1 iff 1 and 1

A0 iff 0 or 0

A1 iff 1 or 1

A0 iff 0 and 0

¬(A B)  Configuration ten:

1

A Bρ[no such relation]

¬1 iff 0

¬0 iff 1

¬(A B)ρ[no such relation]

¬A∨¬B Configuration ten:

1

¬1 iff 0

¬0 iff 1

¬[no such value]

¬0

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬[no such value]

[Thus for configuration ten, both are not valued]

¬(A B)  Configuration eleven:

0

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ0

¬1 iff 0

¬0 iff 1

¬(A B)ρ1

¬A∨¬B Configuration eleven:

0

¬1 iff 0

¬0 iff 1

¬[no such value]

¬1

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬[no such value]

[Thus for configuration eleven, both are not valued]

¬(A B)  Configuration twelve:

1

0

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ0

¬1 iff 0

¬0 iff 1

¬(A B)ρ1

¬A∨¬B Configuration twelve:

1

0

¬[no such value]

¬0

¬1

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬1

[Thus for configuration twelve, both are 1]

¬(A B)  Configuration thirteen:

[Neither has any value]

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ[no such value]

¬1 iff 0

¬0 iff 1

¬(A B)ρ[no such value]

¬A∨¬B Configuration thirteen:

[Neither has any value]

¬[no such value]

¬[no such value]

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬[no such value]

[Thus for configuration thirteen, both are not valued]

¬(A B)  Configuration fourteen:

1

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ[no such value]

¬1 iff 0

¬0 iff 1

¬(A B)ρ[no such value]

¬A∨¬B Configuration fourteen:

1

¬0

¬[no such value]

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬[no such value]

[Thus for configuration fourteen, both are not valued]

¬(A B)  Configuration fifteen:

0

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ0

¬1 iff 0

¬0 iff 1

¬(A B)ρ1

¬A∨¬B Configuration fifteen:

0

¬1

¬[no such value]

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬1

[Thus for configuration fifteen, both are 1]

¬(A B)  Configuration sixteen:

1

0

A1 iff 1 and 1

A0 iff 0 or 0

A Bρ0

¬1 iff 0

¬0 iff 1

¬(A B)ρ1

¬A∨¬B Configuration sixteen:

1

0

¬1

¬0

¬[no such value]

A1 iff 1 or 1

A0 iff 0 and 0

¬A∨¬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)

[contents]

8.3.5

[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)

[contents]

8.3.6

[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)

[contents]

8.3.7

[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)

[contents]

8.3.8

[Countermodels from Open Branches]

[Open branches indicate counter-models. To any p,+, we assign 1; and to any ¬p,+ we assign 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 1; if there is a node of the form ¬p,+, set 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.

1

1

?

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 1 for all B ∈ Σ then 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.]

[contents]

8.3.9

[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 1 and 0 (and no other relations hold). It is easy to check directly that this interpretation makes the premises true and the conclusion untrue.

(146)

[contents]

8.3.10

[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)

[contents]

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.

.