When we extend trees for sentence logic to predicate logic, we add four new rules: 3, -3, V, and -V. Roughly speaking, what we need to do is to check that these rules are downwardly and upwardly correct. There is, however, a complication: infinite trees.
Before going further, please review section 8-4. In sentence logic every tree ends, including all open trees. That is because we need to work on each sentence only once, and when working on a sentence the sentences on the output list are all shorter than the input sentence. But in predicate logic we may have to work on sentences of the form (Vu)(3v)R(u,v) more than once. When we instantiate (Vu)(3v)R(u,v) with a name, s, we get an existentially quantified sentence, (3v)R(s,v). When we apply 3 to this sentence, we must use a new name, t, which we must then substitute back into (Vu)(3v)R(u,v), producing another existentially quantified sentence, which will produce another new name, and so on.
The overall tree strategy still works as before: We make longer sentences true by making shorter sentences true, until we get to minimal sentences which describe an interpretation. The process may now go on forever, but we can still think of infinite open paths as describing interpretations in which all sentences on the paths are true.
Because trees can be infinite, we need to reconsider what is involved in a finished tree. We do not need to revise our definition, D9, but we do need to make sure that if a tree does not close in a finite number of steps that it can be finished in the sense given by D9. That is, we must make sure that there is some systematic way of applying the rules which guarantees that, for each sentence to which a rule can be applied, eventually the rule is applied.
Here's a system which supplies the guarantee. We segment our work on a tree into stages. At stage n we work only on sentences that appear on lines 1 through n. Stage n continues until all sentences on lines 1 through n which can be checked have been checked and until all names occurring in lines 1 through n have been substituted into all universally quantified sentences occurring in lines 1 through n. Of course, at the end of stage n, the tree may have grown to many more than n lines. But that does not matter. Every checkable sentence occurs by some line, n, and so will eventually get checked by this process, and every name and every universally quantified sentence occurs by some line n, so every universally quantified sentence will eventually be instantiated by every name. Of course, this system is not efficient. But efficiency is not now the point. We want to show that there is a system which is guaranteed not to leave anything out.
The next point to establish is that if a tree is infinite it has an infinite open branch. Koenig's lemma tells us that if a tree is infinite, it has an infinite branch, and since closed branches are finite, this infinite branch must be open.
Open branches, infinite or finite, describe interpretations in pretty much the way they do for sentence logic. Given an open branch, collect all the names that occur on the branch and set up a domain of objects, I each one named by one of the names on the branch, with no two names assigned to the same object. Then let the minimal sentences on the branch specify what is true of what. Atomic sentence letters are treated as in sentence logic. If an atomic sentence of the form P(s) appears on the branch, in the branch's interpretation P is true of s. If an atomic sentence of the form -R(s,t) appears, then in the branch's interpretation R is false of the pair of objects named by s and t (in that order). And so on. The minimal sentences will generally fail to specify all atomic facts. The unspecified facts may be filled in arbitrarily.
For sentence logic we formulated rule correctness in terms of any interpretation: Any interpretation which makes an input sentence true makes at least one output list true. And any interpretation which makes an output list true makes the input sentence true. This won't work for quantified sentences.
For upward correctness of the V rule, consider some sentence, (Vu)P(u), and some interpretation, I, in which there are more objects than are named on an open branch. Even if all of the output sentences of the V rule-that is, even if all of the substitution instances of (Vu)P(u) which appear on this branch-are true in I, (Vu)P(u) might not be true in I. To be true in I, (Vu)P(u) must be true for all objects in I, whether the object concerned has a name or not.
For downward correctness we need the following: Given an interpretation in which the first n lines of a branch are true, there is an interpretation which makes true all of these sentences as well as the sentences in an output list resulting from applying a rule. But for the 3 rule, not just any interpretation in which the first n lines, including (3u)P(u), are true will serve. Such an interpretation might not have a name for an object which makes (3u)P(u) true. Worse, the interpretation might have such a name but the resulting substitution instance might conflict with another sentence already on the branch.
This last problem is what necessitated the new name rule, and it is essential that you understand how that requirement fits in here. Suppose that our branch already has '(3x)Bx' and '-Ba' and that the interpreta- 232 Interpretdionr, Soundness, and Compkteness for Predicate Logic 15-2. Soundness and Compkteness for Trees 233 tion, I, which makes these two sentences true has just one name, 'a', and two objects, the first, named by 'a', which is not B and the second, which has no name in I and is B. This I is a consistent interpretation for '(3x)Bx' and '-Ba', but we cannot use it in forming a substitution instance which shows '(3x)Bx' to be true. We must extend or change our interpretation by assigning a new name, 'b', to the unnamed object. Then the truth of '(3x)Bx' is made explicit by including 'Bb' on the branch.
The new name feature of the 3 rule ensures that we always proceed in the way just described. When it comes time to describe downward correctness of the 3 rule, the downward correctness must be given a corresponding description. As in the last example, the I which makes the initial sentences on the branch true may not have the required new name. Or I may have the name but, since the name does not occur in any of the sentences so far considered on the branch, the name could refer to the wrong object. (Think of lemma 25 in making sure you understand this last point.) For lack of the right name referring to the right object, the I which makes true the first n sentences on a branch may not also make true the substitution instance which comes by applying the 3 rule with its new name requirement. But there will always be an s-variant of I, I,, resulting by assigning the new name s to the right object, which will make true (3u)P(u)'s substitution instance, P(s). Since s is new to the branch, lemma 25 guarantees that all the prior sentences in the branch will still be true in I,.
The foregoing remarks should motivate the following revisions of Dl5 and Dl 6:
D15': A tree method rule is Downwardly Correct iff it meets the following condition for all interpretations, I, and all line numbers, n: Suppose that I is an interpretation which makes true all sentences along a branch from lines 1 through n. Suppose that the input sentence for the rule lies on this branch, on one of the lines 1 through n, and the sentences on the output lists lie on the lines immediately succeeding n. Then there is an s-variant of I which makes true all of the sentences on the original branch, lines 1 through n, and also all of the sentences on at least one of the output lists.
D 16': A tree method rule is Upwardly Cmect iff in any interpretation, I, which is described by an open branch, if all the sentences on an output list on that branch are true in I, then the input sentence is true in I.
Note that upward correctness concerns only interpretations which are described by the open branch in question.
Before checking rule correctness, we need to clarify what is to count as the output list for an application of the V rule. For upward correctness, the output list resulting when V is applied to (Vu)P(u) includes all the substitution instances of (Vu)P(u) on the finished branch. For downward correctness the output list includes only those substitution instances on the branch as it exists just after the V rule is applied to (Vu)P(u) but before any further rules are applied.
You can now proceed to check downward and upward correctness of the quantifier rules.
EXERCISES 15-13. Using lemma L29, show that the rules -3 and -V are downwardly and upwardly correct according to D15' and D16' (though, for these two rules, the difference with Dl5 and Dl6 is inessential). 15-14. Prove that the 3 rule is upwardly correct. You only need apply definition D22. 15-15. Prove that the V rule is upwardly correct. You need to apply lemma L32. 15-16. Prove that the 3 rule is downwardly correct. You need lemmas L25 and L27. Note carefully the role of the new name requirement in your proof. 15-17. Prove that the V rule is downwardly correct. You need lemma L31. Don't forget to treat the case in which V applies to a sentence on a branch with no names. This case will require L25.
We have now done all the real work in proving downward and upward adequacy:
T10: The truth tree method for predicate logic is downwardly adequate.
T11: The truth tree method for predicate logic is upwardly adequate.
Given the revised definitions of upward rule correctness, the proof of upward adequacy works pretty much as it does for sentence logic. Downward adequacy requires some change, in ways which I have already indicated. Suppose that an initial set of sentences has a model. For sentence logic we showed that each time we applied a rule there is at least one extension of the initial segment of a branch all the sentences of which are true in the original model. Now we show instead that each time we apply a rule there is at least one extension of the initial segment of a branch all the sentences of which are true in an s-variant of the model for the prior branch segment. D15' has been designed to make the inductive proof of this statement straightforward.
EXERCISES 15-18. Prove downward adequacy for predicate logic trees. 15-19. Prove upward adequacy for predicate logic trees. To extend the proof of section 12-2, you will need to revise the definition of 254 Interpretations, Soundness, and Cornpkteness for Predicate Logic 15-3. Soundess for Predicate Logic Derivations 235 'length of a sentence'. The natural alternative is to let the length of a predicate logic sentence be the number of predicates and connectives. But on this definition the input and output sentences of the -3 and -V rules have the same length. With a little care you can still do the induction with this definition. Or you can define length by letting an initial negation followed by a quantifier count as three units of length and letting each occurrence of '=' count as two units.
T10 and T11, downward and upward adequacy, immediately give
T12: The truth tree method for predicate logic is sound.
T13: The truth tree method for predicate logic is complete.
in exactly the way they do for sentence logic.
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.