For completeness, we also follow the same overall strategy as we did for sentence logic. Starting with an initial tableau of sentences, we generate a new tableau the sentences of which make the sentences on the original tableau true. The sentences on the generated tableau are, on the whole, shorter than on the generating tableau. Roughly speaking, we eventually get down to minimal sentences which characterize an interpretation on which all the sentences of ancestor tableaux are true. But there will be some new wrinkles.
We have to say how quantified and negated quantified sentences will be treated on a tableau. For negated quantified sentences, we apply the rules of logical equivalence for negated quantifiers, pushing the negation sign through the quantifier and switching the quantifier. That will leave us with only quantified sentences, with no negation signs in front, with which we have to deal.
We will make a universally quantified sentence true by making all its substitution instances true. We will make an existentially quantified sentence true by making one substitution instance true. But we will have to make this substitution instance the assumption of a new subderivation so that we will be able to apply the 3E rule to contradictions to get 'A&-A' as the final conclusion of the outermost derivation.
These ideas get incorporated by extending the rules for sequential and branching generation:
R2' Sequential generation: Extend the statement of the rule with the following steps (to be applied before the instruction to reiterate remaining sentences).
a) If a sentence of the form -(3u)P(u) appears on the generating tableau, enter (Vu)-P(u) on the generated tableau.
b) If a sentence of the form -(Vu)P(u) appears on the generating tableau, enter (3u)-P(u) on the generated tableau.
c) If a sentence of the form (Vu)P(u) occurs on the generating tableau, enter on the generated tableau all the substitution instances formed with names which appear on the generating tableau. If no names appear on the generating tableau, pick one name arbitrarily and use it to form a substitution instance entered on the generated tableau. Also reiterate (Vu)P(u) on the generated tableau.
We must reiterate (Vu)P(u) on the generated tableau because, as you will soon see, new names can arise on later tableaux. These new names must be substituted into (Vu)P(u) to make (Vu)P(u) true for all its substitution instances. So we must carry (Vu)P(u) along on each tableau to have it for forming substitution instances any time that a new name arises.
R3' Branching generation: If any sentence of the form XVY occurs on the generating tableau, apply R3 exactly as stated. If no XVY occurs but there is a sentence of the form (3u)P(u) on the generating tableau, pick a New Name, that is, a name which does not appear anywhere on the generating tableau. Use the new name to form a substitution instance of (3u)P(u), and use this substitution instance as the assumption starting a new subderivation. Reiterate all other sentences on the generating tableau in the subderivation to complete the generated tableau, just as in R3.
As students of the tree method already know, these rules create a problem. Suppose that a sentence of the form (Vu)(3v)R(u,v) appears on a tableau. R2' tells us to enter at least one substitution instance, (3v)R(s,v), on the next tableau and to reiterate (Vu)(3v)R(u,v) itself. R3' will then tell us to start a new subderivation with R(s,t), t a new name. Of course, (Vu)(3v)R(u,v) also gets reiterated onto the subderivation. But now we will have to do the same thing all over again. The new name, t, will have to go into (Vu)(3v)R(u,v), giving a new existentially quantified sentence, . (3v)R(t,v), which will call for a new subderivation with yet another new name, which will have to go back into the reiterated (Vu)(3v)R(u,v). We are off and running in a chain of subderivations that will never end.
A first impulse is to wonder if the generation rules couldn't be written better, so as to avoid this problem. They can be written so as to avoid exactly this form of the problem, but it turns out that no matter how the rules are written, some problem with essentially the same import will arise. Indeed, proving this is a further important fact about logic.
Here is an overview of what the problem involves. The semantic tableau procedure provides a mechanical method for searching for a derivation 238 Interpretatwns, Soundness, and Completeness for Predicate Logic 154. Completeness for Predicate Logic Derivations 439 which establishes the validity of a given argument, or equivalently, a mechanical method for searching for an interpretation of a given finite set of sentences. In sentence logic, the method is guaranteed to terminate. A method which thus terminates is guaranteed to give a definite yes or no answer to the original question ('Is the argument valid?' or 'Is the initial set of sentences consistent?'). Such a method, guaranteed eventually to turn,up a yes or no answer, is called a Decision Procedure.
Now, here is the general form of our current problem. Given an exceedingly plausible assumption about what will count as a mechanical decision procedure, one can prove that there is no decision procedure for predicate logic. In our formulation we fail to get a decision procedure because we may get an infinite sequence of sub-sub . . . -sub-derivations. If our tableau procedure has failed to close at some stage, we may not be able to tell for sure whether that is because we just haven't pursued it far enough, or because it will go on forever. This is not just a weakness of our rules. One can prove that any sound and complete system of predicate logic will suffer in the same way. Roughly speaking, the problem arises from the requirement on the 3E rule, which we must have in order to ensure soundness.
Since there is no point in searching for better rules, we will have to see what we can make of our R2' and R3' in fashioning a completeness proof.
Consider a set of sentences, for example, just the sentence (Vu)(3v)R(u,v) for which our tableau procedure generates an infinite sequence of tableaux. We will need the fact that we can then, so to speak, draw an unending path through the nested sequence of subderivations. Koenig's lemma assures us that we can always do so. Refer back to the tree structure at the beginning of chapter 14 and imagine that each node represents a subderivation, beginning with the outermost derivation at the top node. Moving from one node to two nodes beneath represents the process of starting two new subderivations by working on a sentence of the form XVY. When we start one new subderivation by working on a sentence of the form (3u)P(u), we start one new node, that is, a "branch" with one rather than two new forks. When a subderivation closes, the corresponding path on the tree structure closes. Koenig's lemma tells us that if such a tree structure is infinite, then there is an infinite open path through the tree.
We now know that if a tableau derivation does not close (is infinite or does not have all its terminal tableaux closed) then there is an open path of subderivations through the derivation. The path might be finite or it might be infinite. Each such path provides an interpretation, which we will again call a Terminal Interpretation. But we want to characterize the idea of a terminal interpretation so that it will work for infinite as well as finite cases. Since an infinite path through a derivation has no terminal tableau, we cannot let the terminal interpretation simply be one provided by the terminal tableau.
Here's the recipe for the terminal interpretation represented by an infinite path. Collect all the names that occur on the path, and set up _a domain of objects, each one named by one of the names on the path, with no two names assigned to the same object. Then look at all the minimal sentences which appear on the path. If an atomic sentence letter appears, the interpretation will make it true. If an atomic sentence letter appears negated, the interpretation will make the atomic sentence letter false. If an atomic sentence of the form P(s) appears, the interpretation will make the predicate P true of the object named by s. Similarly, if -P(s) appears, the interpretation will make P false of the object named by s. Two and more place predicates are treated similarly. If this recipe fails to specify all the atomic facts of the interpretation, fill in the missing facts arbitrarily. In sum
D24: A Terminal Interpretation represented by an open path has as its names all the names which occur on the path and as its domain a set of objects, each named by exactly one of the names. The interpretation assigns truth values to atomic sentence letters and determines which predicates are true of which objects (pairs of objects, and so on) as described by the minimal sentences on the path. Any facts not so specified by the minimal sentences may be filled in arbitrarily.
Note, incidentally, that this recipe gives a consistent interpretation. Since the path is open, it cannot contain both an atomic sentence and its negation. So this recipe will not make an atomic sentence both true and false. That is, it will not both say and deny that a predicate is true of an object. The main work we need to do is to prove the analogy of lemma 18, namely
L37: The sentences of the initial tableau are all true in a terminal interpretation represented by an open path.
We prove this by proving that a terminal interpretation makes true all the sentences in all the tableaux along its path, arguing by induction on the length of the sentences.
We need to take a little care in saying what the length of a sentence is. To keep things initially simple, let us first consider a special case-analogous to our procedure in section 13-4: Suppose that 'v', '-', and the quantifiers are the only connectives occurring in any of the initial sentences. Then we can take the length of a sentence simply to be the number of connectives occurring in the sentence.
To carry out the inductive argument, suppose that we have an open path and a terminal interpretation, I, represented by that path. By the definition of a terminal interpretation, all atomic and negated atomic sentences, and so all sentences of length 0 or 1, along this path are true in I. 240 Zntcrpntafimu, Soundness, and Cmnpleteness for Predicate Logic 154. COrnpIctmess for Predicate Logic Derivorionr 241 For the inductive hypothesis, suppose that all sentences of length no greater than n along the path are true in I. Let X be a sentence of length n + 1. Suppose that X has the form -(YvZ). Then rule R2 for sequential generation tells us that -Y and -Z will both be on the path, since they will be on the tableau generated by the tableau on which -(YvZ) occurs. -Y and -Z are both shorter than -(YvZ), and the inductive hypothesis tells us that -Y and -Z are both true in I. Hence -(YvZ), that is, X, is true in I. When X has the form --Y the argument goes quite like the case of -(YvZ).
Next, we must consider X of the form YvW. Such X gives rise to two generated tableaux, one including Y and one including W. One of these generated tableaux must be on the open path. Suppose it is the one with Y. Since (by the inductive hypothesis) all sentences along this path with n or fewer connectives are true, Y, and so YvW, are true. If W rather than Y is on the path, the same argument applies. Suppose that X has the form (3u)P(u). Then rule R3' specifies that there is a subderivation along the path that includes a substitution instance, P(s), which the inductive hypothesis tells us is true in I. Definition D22 applies to tell us that then (3u)P(u), that is, X, is true in I.
Now suppose that X has the form (Vu)P(u). Rule R2' specifies that, for each tableau in which (Vu)P(u) appears, all its substitution instances formed with names in that tableau appear in the next sequentially generated tableau. (Vu)P(u) is also reiterated, so that any name which comes up will eventually get instantiated along the path. By the inductive hypothesis, all these substitution instances are true in I. Remember that in a terminal interpretation there is exactly one object named by each name, and we have just seen that all of these names eventually get used to form true substitution instances of (Vu)P(u). So lemma L32 applies to tell us that (Vu)P(u), that is, X, is also true in I.
Make sure that you understand how this last step in the inductive proof makes essential use of the fact that (Vu)P(u) is always reiterated, to ensure that when new names come up in later tableaux, they will always be used to instantiate (Vu)P(u).
We still need to consider sentences of the form -(3u)P(u) and -(Vu)P(u). Rule R2' applies to such sentences to produce sentences, respectively, of the form (Vu)-P(u) and (3u)-P(u). There might seem to be a problem here because -(-Ju)P(u) and (Vu)-P(u) have the same number of connectives, as do -(Vu)P(u) and (3u)-P(u). But we can still complete the inductive step. Suppose that -(-Ju)P(u) has n + 1 connectives apd appears on the path. R2' tells us that (Vu)-P(u), also having n + 1 connectives, also appears on the path. But we have already seen that the inductive hypothesis ensures us of the truth of (Vu)-P(u) in the terminal interpretation, I. Lemma L29 then tells us that -(3u)P(u) is also true in 1. Of course, the case for -(Vu)P(u) works the same way.
To complete the proof of L37 we must lift the restriction and allow sentences to include all the sentence logic connectives. This creates a new difficulty. For example, R2 instructs us to generate (X&Y)V(-X&-Y) from X=Y. But (X&Y)v(-X&-Y) has four more connectives than X=Y rather than fewer.
We can resolve this impasse by assigning weights to the connectives. I-', 'v', and the quantifiers are each worth one "point," '3' and '&' each get three "points," and '=' gets six "points." The length of a sentence is now just the number of these "points" added up for all the connectives in the sentence. (This technique can also be applied to arrange for -(3u)P(u) and -(Vu)P(u) to be longer than (Vu)-P(u) and (3u)-P(u).)
EXERCISE 15-23. Complete the inductive step of the argument for lemma L37 with all of the sentence logic connectives.
We have proved L37, the analogue of L18 needed for proving completeness for sentence logic derivations. The proof for sentence logic derivations also used L20, which says that if all terminal tableaux close, then 'A&-A' appears as the derivation's final conclusion. We must reformulate the statement ever so slightly because, with the possibility of infinite derivations, some paths might not have terminal tableaux. So we will say
D25: a semantic tableau derivation is Closed if all sequences of subderivations terminate in a closed tableau.
You will then prove the analogy of L20:
L38: If a semantic tableau derivation is closed, then 'A&-A' appears as the derivation's final conclusion.
The key to L20 is the inductive step, L21. Again, we only need to reformulate to accommodate our more specific definition of a closed tableau derivation:
L39: Let D be a closed semantic tableau derivation. Then, if all of D's subderivations of level i have 'A&-A' as their final conclusion, so do all the subderivations of level i + 1.
EXERCISE 15-24. Prove L39. You only need to check the inductive step for rule R3', involving subderivations started with a substitution instance of a sentence of the form (3u)P(u). Be sure you see how the new 444 Intcrprctation, Soundness, and Cinnpktcncss fm Predicate Logic 15-5. Cinn~~s, Identity, and Functions 443 name requirement in the statement of R3' functions~crucially in your proof.
If you now go back and read the short paragraph proving T7 and change just the words 'L18' and 'L20' to 'L37' and 'L38', you will see that we have a proof of T7, where the set of sentences Z may now include predicate logic sentences. T7 applies exactly as it did in section 12-3 to establish
T15 (Completeness for predicate logic derivations): For any finite set of sentences, Z, and any sentence X, if Z~X, then ZkX.
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.