Looking for help with number 8 in bold down below.

1. The hurdle we face for extending our proof of completeness to quantifier formulas is that we might not be able to develop their tableau completely. Indeed, there may be no end to applying the rules of development for universal formulas on the right and existential formulas on the left, since they can be applied to a single formula without duplication by using different name letters. For starters, then, we need to come up with a new understanding of a tableaus being fully developed.

2. Imagine the following three-step procedure for developing formulas in a tableau with quantifier formulas:

(1) First, we systematically apply all the rules for the regular truth functors until they develop into their atomic constituents or into quantifier formulas.

(2) We then systematically apply all the undeveloped one shot rules requiring the introduction of new name letters (those for existential on the left and universal on the right), including especially any such formula that might have just been uncovered in step 1.

(3) We then apply those continuously applicable or blanket rules (for universal on the left and existential on the right) for all the names that appear on a branch, including especially those that might have just been introduced by the application of the one shot rules.

We then repeat this three-step process upon those formulas that resulted from the application of these quantifier rules. And we repeat this process again and again until there are no further developments at any given stage.

[Note: If we happen to have an infinite set of premises, we can modify this procedure by adding a single new premise at the beginning of each distinct stage. The result will be a non-terminating process, though one by which we can still assure that every single formula gets developed at some stage or another.]

3. So for the time being, let us suppose that this process eventually terminates, and that it results in an open path. Once again, our task is to construct from this path an interpretation that will verify all the formulas on the left, and falsify all the formulas on the right. Since we are now dealing with quantifier formulas, an interpretation for these formulas needs to consist of a domain of objects, an assignment of denotations for the names on the path, and an assignment of extensions to the predicates and relations appearing on that path.

4. Our interpretation, call it I, is actually quite intuitive. The domain will be a set of objects {ThingA, ThingB, ThingC, } corresponding to (and respectively denoted by) each of the name letters a,b,c that appear in the formulas along that open path. Thus every object in the domain will be denoted by one, and only one, name letter, and every name letter will have an object that it denotes. Moreover, we determine predicate extensions by looking to the atomic formulas lying along the path. Specifically, if an atomic formula (e.g., Fcb) appears on the left side of the path, then we include the objects denoted by its name letters in the extension of the predicate ( in the extension of F). If an atomic formula appears on the right, we simply make sure that the objects it denotes does NOT belong in the extension of its predicate letter. Any other atomic formulas can be settled willy-nilly.

5. It is really quite easy to verify that this interpretation I will do the work that we demand of it that is, that it verifies all the formulas on the left, and makes false all those on the right. This is immediately evident for all the atomic formulas, for our interpretation stipulates that it will be true if it appears on the left and false if it appears on the right. The justification for all the truth functors is exactly as before. And so we now turn to the quantifier formulas. Once again, our overall proof is one by induction, and our inductive hypothesis is that all formulas shorter than the one we are considering is true on I if they appear on the left hand side of the path, and false on I if they are on the right. From this, we want to show that all quantifier formulas will be true on I if they are on the left and false on I if the are on the right.

6. So lets first consider an existential formula, (x), on the left. This is one of our one-shot rules, and step 2 of our procedure above for developing tableaus ensures that it will have been developed at some stage in the process by placing (/x) on the left. But (/x) is a shorter formula than (x), and so by our inductive hypothesis, (/x) must be true on I. But since this is so, its easy to see that there must be some object in the domain, namely the one denoted by , such that if we had a name for it, , (/x) must be true. And so (x) must be true on I as well, which is just what we want to show.

7. Now consider a universal quantifier, (x), appearing on the left. This is one of our continuous rules covered by step 3 of our procedure for developing tableaus, which stipulates that for every name letter appearing on this branch, there is a corresponding instantiation of (x) with the letter , which also appears on the left. But these instantiations are all shorter than (x), and so they must be true on I. Moreover, since each and every object in Is domain is denoted by some name or another appearing on the branch, it follows that there will be no way to find an object in the domain such that if we were to assign a name (it), I will assign (it/x) any value other than true. Thus (x) must be true on I as well.

8. The two quantifier rules on the right proceed along similar lines. Go ahead and try!

9. Our final wrinkle concerns those cases in which our new procedure for developing trees would go on without end. This would occur, for instance, when you have an existential formula embedded within a universal formula on the left (this is sometimes called an AE formula), or when you have a universal formula embedded within an existential formula on the right. In both cases, when we apply our rules of development to a continuous formula, we wind up uncovering a new formula that demands we apply a one-shot rule of development to it. And the new name introduced by applying this one-shot rule in turn requires that we apply the continuous rule once again, uncovering a new one-shot formula, and so on, without end. So what do we do?

10. Simple; we adopt a strategy much like we did with infinite sequents. Since we are assuming that we cannot close off the tableau, we envision a path in which each and every formula along it is eventually developed, and that blanket rules for quantifier formula are eventually applied for each and every name that appears on the path. Notice that the procedure for systematically developing formulas outlined above actually does this. Every existential on the left and universal on the right will get developed in step 2 of the same stage at which it is uncovered. And for every name that ever appears on an open path, there will be a corresponding instantiation of every universal on the left and existential on the right, either immediately following the introduction of that continuous formula or the introduction of that name. Then from this never-closing path, we follow once more our rules for constructing interpretations that will eventually verify each and every formula that ever appears on the left of that path (and falsify all those on the right). The result will be an interpretation with an infinite domain, but thats no real problem, since for each name that ever gets introduced along the path (hence, each object in the interpretations domain) the appropriate continuous rules will have been applied immediately upon its introduction.