7.5.4. Adding instances

The implementation of the laws for universal quantifiers is fairly straightforward if we use derivations only in a positive way—i.e., use them only to show that entailments hold. Discussion of their use to show that entailments fail will be postponed until 7.7. Also, as already noted, we will consider only the unrestricted universal. Rules for restricted universals present no special difficulties, and, like the principles for the restricted universal discussed above, they can be seen as simply abbreviations for combinations of rules for the unrestricted universal and the conditional.

The exploitation rule for universals, which we will call Universal Instantiation (UI), is shown in Figure 7.5.4-2. It can be used to add any instance of the universal as a further resource, annotating the universal to indicate the term for which an instance was added.

Although we record the use of this rule alongside the universal, the universal resource is not rendered completely inactive. The rule provides only a partial exploitation, extracting the content of the universal only for the single term τ. Since a universal does not bring with it any definite set of instances, it will never be rendered completely inactive, no matter how often this rule is used. Still, each use of the rule does exploit the universal for one term, and we record this by noting both the stage number and the term for which the universal has been exploited.

This information is used (much in the way we have used marking by stage numbers) to judge when a universal is active for a given term. To be active for a given term in a gap, a universal must be available in the gap and must not have been exploited for the term in the course of narrowing the gap. Specifically, an available universal is inactive for τ in a gap if it is marked by a pair τ:n and all scope lines to the left of some resource or goal entered at stage n continue unbroken to the left of the gap. Although an available universal is always active, it may not be active for all terms, and a term for which we apply the exploitation rule above should be one for which the universal is still active.

As we will see in 7.7.4, it is legitimate to limit the use of this rule to terms appearing in the available resources and goals of the gap. These are the same terms from which we form alias sets and it will be enough to exploit a universal for at least one term from each alias set.

Occasionally, no terms will appear in the initial premises and conclusion and none will be introduced by other rules. When this is so, the exploitation rule above may be used to introduce a new unanalyzed term into the derivation. For example, the premises and conclusion of the following derivation above contain no terms at all, so there would be no way of beginning it if we did not instantiate one of them for a new term.

	│∀x Fx	a:1
	│∀x ¬ Fx	a:2
	├─
1 UI	│Fa	(3)
2 UI	│¬ Fa	(3)
	│●
	├─
3 Nc	│⊥

This is the only sort of case in which instances need be added for terms new to the gap being developed.

That we ever instantiate for terms new to the gap reflects the assumption built into our system that there is at least one reference value. The derivation above shows one consequence of this assumption—namely, that Everything is finished and Everything is unfinished are inconsistent. Clearly, if there is anything at all, then these two sentences cannot both be true. On the other hand, if we were to drop the assumption that there is something, both sentences could be true. For generalizations are false only when they have counterexamples; and, in a world in which there was nothing, there would be nothing to serve as a counterexample to either Everything is finished or Everything is unfinished. The assumption that there is something is perhaps the only assumption typically regarded as part of deductive logic that might also be regarded as factual.

At the other extreme, use of UI even to instantiate for terms already in the gap can introduce new terms when we instantiate generalizations containing functors. For example, instantiating ∀x P(fx) for the term a will give us P(fa), which contains the term fa. This new term may be used also to instantiate the generalization, giving us P(f(fa)), which contains the term f(fa)—and so on. As we will see in 7.7, this is one aspect of a general feature of the deductive logic for generalizations that will sometimes keep a derivation from ever reaching an end. That is not our concern now, but the possibility of going on forever in the application of rules shows that we can no longer wait to apply rules fully before checking to see if a gap closes. And, because a large number of applications of instantiation may be possible, it is wise to select, from among the terms with which we might instantiate a generalization, those that seem most likely to help us close a gap.

The following derivation keeps universal instantiation to a minimum required to close its gap. Only the main quantifier is removed with each use of UI, so three uses are required to reach the bare predication Rabc. Only two more are needed to reach Racc but three would have been required to reach a second predication, such as Rccc, that had a different term in the first place after R.

	│∀x ∀y ∀z Rxyz	a:1
	├─
1 UI	│∀y ∀z Rayz	b:2, c:4
2 UI	│∀z Rabz	c:3
3 UI	│Rabc	(6)
4 UI	│∀z Racz	c:5
5 UI	│Racc	(6)
6 Adj	│Rabc ∧ Racc	(7)
	│●
	├─
7 QED	│Rabc ∧ Racc

On the other hand, a full use of instantiation for the terms appearing in the conclusion would have lead to 3 + 3×3 + 3×3×3 = 39 uses of UI (i.e., three to exploit the premise for a, b, and c, three more exploitations for each of the three resources that result, and finally three more for each of the nine resources added in that way). A derivation is not damaged by extra uses of UI any more than it is damaged by using Ext to add conjuncts that are not needed later. But, while adding all conjuncts as resources whenever a conjunction was exploited presented no practical problem, using UI in all ways possible can lead to unmanageably large derivations even for premises that are fairly simple.