3.13.4: Completeness for Derivations- Formal Details

To keep attention focused on the main ideas, I'm going to restrict consideration to sentences in which '-' and 'v' are the only connectives used. 404 Soundness and Completenesr for Sentence Logic DctiYotions 13-4. Completeness for Derivations: Fond Details 205 Once you understand this special case, extension to the other connectives will be very easy. As I mentioned, I will also carry out the proof only under the restriction that the initial set of sentences, Z, is finite. Chapter 14 will generalize the result to infinite sets, Z.

To help fix ideas, I'll start with a slightly more extended example. Skip over it now and refer back to it as an illustration as you read the details.

The method of semantic tableau derivations constitutes a way of testing a finite initial set of sentences for consistency. Here are the rules for generating such a derivation:

R1 Znicial Tabbau: The method begins by listing the sentences in the set to be tested as the premises of the derivation. This initial list constitutes the initial tableau.

Lines 1 and 2 in the example are an initial tableau.

Each further tableau (the Generabd Tableau) is generated from some prior tableau (the Generating Tableau) by one of two methods:

R2 Sequatial generation

a) Each line of the generated tableau is a new line of the same derivation as the generating tableau.

b) If a sentence of the form --X occurs on the generating tableau, enter X on the generated tableau.

c) If a sentence of the form -(XVY) occurs on the generating tableau, enter -X and -Y as separate lines on the generated tableau. -

d) Reiterate all remaining sentences of the generating tableau as new lines of the generated tableau.

Tableaux 2 and 3 in the example illustrate sequentially generated tableaux. c) is illustrated in the example by lines 3, 4, 6, 7, 8, and 9. d) is illustrated by lines 5 and 10. Note that the rule I apply for c), which I have called '-v', is a new derived rule, constituted by simply applying DM followed by &E.

R3 Branching generation:

a) If a sentence of the form XVY occurs on the generating tableau, start two new subderivations, one with assumption X and the other with assumption Y.

b) Reiterate all the remaining sentences of the generating tableau on each of the subderivations.

c) Each of the (initial parts of) the subderivations started by steps a) and b) constitutes a generated tableau.

Branching generation is illustrated in the example by tableaux 4, 5, 6, 7.

Tableaux 4, 6, and 7 illustrate what happens when both a sentence and the negation of a sentence appear on a tableau. No interpretation will make all the sentences on such a tableau true. So such a tableau will never provide an interpretation which will prove the original sentences consistent. We record this fact by extending the tableau by applying CD to derive 'A&-A'. We say that such a tableau is Closed and mark it with an ' x '.

We have applied CD to draw the explicit contradiction, 'A&-A', on closed tableaux because this contradiction will be helpful in deriving 2 06 Soundness and Completeness for Sentence Logic Derivations 134. Completeness for Derivations: Formal Details 207 'A&-A' in the outermost derivation. We will see that, if the original set of sentences is inconsistent, then all chains of tableaux will terminate with a closed tableau. Argument by cases will then allow us to export 'A&-A' from subderivations to outer derivations, step by step, until we finally get 'A&-A' as the final conclusion of the outermost derivation.

We make these ideas more precise with two further instructions:

R4: If both a sentence and the negation of the same sentence appear on a tableau, apply CD to derive 'A&-A' as the last line of the tableau, and mark the end of the tableau with an 'X ' to indicate that it is Closed. Do not generate any new tableaux from a closed tableau.

R5: If 'A&-A' appears on two subderivations, both generated by the same disjunction in the outer derivation, apply AC to write 'A&-A' as the final conclusion on the outer derivation.

Look again at tableaux 4, 6, and 7, as illustrations of R4. Lines 30 and 31 illustrate R5.

We now need to prove that semantic tableau derivations do what they are supposed to do. Here is the intuitive idea. We start with a set of sentences. The tableau procedure constitutes a way of determining whether or not this set is consistent. This works by systematically looking for all possible ways of making the original sentences true. If the systematic search turns up a way of making all the original sentences true (a model), then we know that the original set is consistent. Indeed, we will prove that if the original set is consistent, the procedure will turn up such an interpretation. Thus we know that if the procedure fails to turn up such an interpretation, the original set must be inconsistent. This is signaled by all chains of tableaux terminating with a closed tableau.

The procedure accomplishes these aims by resolving the original sentences into simpler and simpler sentences which enable us to see what must be true for the original set to be true. Each new tableau consists of a set of sentences, at least some of which are shorter than previous sentences. If all of the generated tableau's sentences are true, then all of the sentences on the generating tableau will be true. For a sequentially generated tableau, the new sentences give us what has to be true for the sentences on the generating tableau to be true. When we have branching generation, each of the two new tableaux gives one of the only two possible ways of making all sentences of the generating tableau true. In this way the procedure systematically investigates all ways in which one might try to make the original sentences true. Attempts that don't work end in closed tableaux.

We need to work these ideas out in more detail. We will say that A tableau is a

Tenninul Tableau if it has not generated any other tableau, and no rule for tableau generation applies to it.

It can happen that no rule applies to a tableau for one of two reasons: The tableau can be closed. Or it might be open but have only minimal sentences (atomic or negated atomic sentences). We will discuss these two - cases separately.

First we will prove

L18: An open terminal tableau describes an interpretation in which all sentences of the initial tableau are true.

An open terminal tableau has only minimal sentences, none of which is the negation of any other. The interpretation such a tableau specifies is the one which makes all its sentences true, that is, the assignment of t to all the tableau's unnegated atomic sentences and f to the atomic sentences which appear negated on the tableau. Let's call such an interpretation a Tminul Interpretation, for short.

Our strategy will be to do an induction. Suppose we are given an open terminal tableau, and so the terminal interpretation, I, which it specifies. The fact that all the sentences of the terminal tableau are true in 1 provides our basis step. For the inductive step you will show that instructions for constructing a tableau derivation guarantee that if all the sentences of a generated tableau are true in an interpretation, then all the sentences of the generating tableau are true in the same interpretation. Thus all the sentences of the tableau which generated the terminal tableau will be true in I. In turn, that tableau's generator will have all its sentences true in I. And so on up. In short, induction shows that all the Ancestors of the open terminal tableau are true.

To fill in the details of this sketch, you will first prove the inductive step:

L19: If tableau Tp is generated from tableau TI and all sentences of T, are true in interpretation I, then all the sentences of TI are also true in I.

EXERCISE 13-11. Prove L19.

Since the proof of L18 will be inductive, we need to specify more clearly the sequence of cases on which to do the induction:

A terminal tableau's generator will be called the tableau's first Ancestor. In general, the i + 1st ancestor of a terminal tableau is the generator of the ith ancestor.

We will do the induction starting from a 0th case, namely, the terminal tableau. The ith case will be the terminal tableau's ith ancestor.

We are now ready to prove L18. Suppose we are given a semantic tableau derivation, with an open terminal tableau. This tableau specifies an interpretation, I, in which all the terminal tableau's sentences are true. The inductive property is: The nth ancestor of the terminal tableau has all its sentences true in I. The terminal tableau provides the basis case. By L19, if the nth ancestor of the terminal tableau has all its sentences true in I, then so does the n + 1st ancestor. Then, by induction, all the terminal tableau's ancestors have all their sentences true in I, which includes the derivation's initial tableau, as required to prove L18.

I have now said all I need about tableau derivations which terminate with one or more open tableaux. What happens if all the terminal tableaux are closed? In a word, rule R5 applies repeatedly until, finally, 'A&-A' appears as the final conclusion of the outermost derivation:

L20: If in a semantic tableau derivation all the terminal tableaux are closed, then 'A&-A' appears as the derivation's final conclusion.

We will prove this with another induction.

We need a sequence of cases on which to do the induction. The natural choice is the level or depth of subderivations, as measured by the number of nested scope lines. But we want to start with the deepest level of subderivation and work our way back out. So we need to reverse the ordering: The first level of subderivations will be the deepest, the second will be the subderivations one level less deep, and so on. More exactly defined

Given a tableau derivation, let k be the largest number of nested scope lines on the derivation (including the outermost scope line). The Inverted Level of each subderivation is k less the number of scope lines to the left of the subderivation.

(I will henceforth omit the word 'inverted' in 'inverted level'.) The key to the proof will be the inductive step:

L21: Let D be a semantic tableau derivation in which all terminal tableaus are closed. Then, if all of D's subderivations of level n have 'A&-A' as their final conclusion, so do all the subderivations of level n + 1.

(I construe 'subderivation' broadly to include the outermost derivation, a sort of null case of a subderivation.)

EXERCISE 13-12. Prove L2 1. I

We are now ready to prove L20. Let D be a semantic tableau derivation in which all terminal tableaux are closed. Our inductive property will be: All the subderivations of level n have 'A&-A' as their final conclusion. Ai level 1 all subderivations have no sub-subderivations. So all of the subderivations must end in terminal tableaux. By assumption, all of these are closed. So the inductive property holds for level 1. L21 gives the inductive step. By induction, the derivations at all levels conclude with 'A&-A', which includes the outermost derivation.

We are at long last ready to prove T7. Suppose that Z, a finite set of sentences, is inconsistent. (Note that, if inconsistent, Z must have at least one sentence.) Make the sentences of this set the first tableau of a semantic tableau derivation. Suppose that the derivation has an open terminal tableau. Then, by L18, there is an interpretation which makes true all the sentences in Z. But this is impossible since Z is supposed to be inconsistent. Therefore all terminal tableaux are closed. Then L20 tells us that the derivation terminates with 'A&-A', so that ZkA&-A, as was to be shown.

We have one more detail to complete. My proof of T7 is subject to the restriction that 'v' and '-' are the only connectives which appear in any of the sentences. We easily eliminate this restriction by exchanging sentences with other connectives for logical equivalents which use 'v' and '-' instead. At each stage we deal only with the main connective or, for negated sentences, with the negation sign and the main connective of the negated sentence. We rewrite rule R2 for sequential generation to read:

R2 Sequential generation:

a) Each line of the generated tableau is a new line of the same derivation as the generating tableau.

b) If a sentence of the form --X occurs on the generating tableau, enter X on the generated tableau.

c) If a sentence of the form -(XvY) occurs on the generating tableau, enter both -X and -Y as separate lines on the generated tableau.

d) If a sentence of the form X&Y occurs on the generating tableau, enter both X and Y as separate lines on the generated tableau.

e) If a sentence of the form X>Y occurs on the generating tableau, enter -XvY on the generated tableau.

f) If a sentence of the form XEY occurs on the generating tableau, enter (X&Y)v(-X&-Y) on the generated tableau.

g) If a sentence of the form -(X&Y) occurs on the generating tableau, enter -XV-Y on the generated tableau.

h) If a sentence of the form -(X>Y) occurs on the generating tableau, enter both X and -Y as separate lines on the generated tableau.

i) If a sentence of the form -(X=Y) occurs on the generating tableau, enter (X&-Y)v(-X&Y) on the generated tableau.

j) Reiterate all remaining sentences of the generating tableau as new lines of the generated tableau.

We could provide a more complicated version of R2 which would produce more efficient tableau derivations, but it's not worth the effort since true efficiency is only obtained with the truth tree method. In the next exercises you will show that the proof for the special case, using only the connectives 'v' and '-', extends to the general case covered by our reformulated R2.

EXERCISES Generalizing the proof of T7 only requires checking three points. 13-13. I argued that a tableau derivation always comes to an end because each new tableau shortens at least one sentence of the previous tableau. This argument no longer works, at least not as just stated. Show that tableau derivations, with sentences using any sentence logic connectives and the new rule R2, always come to an end. 13-14. Check that when all terminal tableaux close, a tableau derivation created using the new rule R2 is a correct derivation. You will have to prove two new derived rules, one for biconditionals and one for negated biconditionals.

13-15. Reprove lemma L19 for our fully general tableau derivations.

13-16. Explain why the proof of completeness in this section shows that the primitive sentence logic derivation rules of chapter 5 (volume I) are complete for sentence logic.

CHAPTER CONCEPTS

As a check on your mastery of this material, review the following ideas to make sure you understand them clearly:

a) Rule Soundness

b) Sentence Rule

c) Subderivation Rule

d) Semantic and Syntactic Inconsistency

e) Semantic Tableau Derivation (or Tableau Derivation)

f) Tableau

g) Initial Tableau

h) Generating Tableau

i) Generated Tableau

j) Sequential Generation

k) Branching Generation

I) Derived Rule -v

m) Closed Tableau

n) Minimal Sentence

o) Terminal Tableau

p) Terminal Interpretation

q) Ancestors of a Tableau

Contributors and Attributions

• Paul Teller (UC Davis). The Primer was published in 1989 by Prentice Hall, since acquired by Pearson Education. Pearson Education has allowed the Primer to go out of print and returned the copyright to Professor Teller who is happy to make it available without charge for instructional and educational use.