7.8.1. Finding finite structures

To complete the discussion of the adequacy of the system of derivations for generalizations, we will look a little more closely at the reasons why it is not decisive. There are two aspects to the problem, one concerning universals alone and another concerning their interaction with functors. The infinitely developing derivations displayed earlier are enough to show us that our system is not decisive, but the failure of decisiveness in these derivations does not run very deep and can be overcome by a relatively small adjustment to our rules. Different adjustments are needed to handle universals and functors, and we will consider the case of universals first.

The rule UG directs us to reach a universal goal ∀x θx by trying to close a gap whose goal is an instance θa for some independent term a. Although we need to close such a gap to show that the universal goal can be reached, this gap need not point us toward the only way of dividing the original gap. When we are constructing general arguments we are checking for counterexamples to generalizations. Thus, for a general argument to go through, we must show that there is no counterexample of any sort; it is not enough to show that the things we are already speaking of are not counterexamples.

However, to show that a general argument fails, a counterexample of any sort, new or old, will do; and a structure dividing a gap between resources and an instance of the universal for an old term would be enough to show that the universal is not entailed by those resources. This means that, in a negative use of derivations, there is some reason for considering gaps whose goals are instances for old terms. We can refine our analysis of entailment to take account of this by making the planning rule for universals more elaborate. The alteration makes derivations cumbersome in practice; but, even if we do not put it put into actual use, it can help to focus attention on deeper reasons for failure of decisiveness.

The revised rule is Supplemented Universal Generalization (UG+); it is shown in Figure 7.8.1-1. The rule UG+ alters UG by adding further new gaps in which we try to conclude instances of the universal not only for a new term but also for terms already appearing in the gap. Adding these new gaps will certainly make it no easier to show that an entailment holds. And they make it no harder either: anything that can be shown for the independent term a can be shown for any term, so if that gap closes, all the others will, too. The function of the added gaps is instead to help us show that an entailment fails while using as few terms as possible. The new gaps provide new directions in which we may search for a path that not only remains open but reaches a dead end.

The derivation at the right shows the effect of the first rule when it is applied to one of the examples of 7.7.3. The first gap in this derivation has reached a dead end. Its only active resources are the initial premise and Raa, and neither is exploitable. In the case of the universal premise, this is because it has already been exploited for the term a, which is the only term ever appearing in this gap.

The gap describes a structure whose referential range contains one value, and the predicate R will be true of the pair consisting of this value and itself. The initial premise—which says that there is no value that is related to nothing by R—is thus true in this structure, showing that the reductio entailment ∀x ¬ ∀y ¬ Rxy ⊨ ⊥ fails.

A planning rule for universal goals is one way we can be led to introduce and unending series of terms. Another way we have seen occurs when a universal quantifier binds a variable occurring in a compound term. When such a generalization is instantiated, a new compound terms can be introduced into the derivation, leading to still further instantiation. We could avoid such further instantiation if the new compound term was in the same alias set as a term for which the universal had already been instantiated, so we can investigate the possibility of avoiding an infinitely developing gap by trying to put new compound terms in already existing alias sets.

On this approach, when we introduce a new compound term that does not automatically become part of an already existing alias set, we also look at ways of identifying the new compound term with existing terms, at least one from each alias set. We will say that in doing this we are securing the term. Of course, it may be that no identification with existing terms is consistent with our resources. We allow for this possibility by adding a gap in which we make no assumptions about the new term.

The rule shown in Figure 7.8.1-2 can be used to secure terms. We suppose in turn that a compound term is a co-alias of each of a series of unanalyzed terms already in the gap and also pursue the development of the gap without new assumptions. Fullest investigation of the possibilities comes if we include at least one term from each alias set. We will call this rule Securing a Term (ST). Nothing in the statement of this rule requires that the term μ be new, but that is the only use that we are interested in now.

Although the application of ST would often be quite awkward, it makes short work of the first of the examples from 7.7.3.

│∀x Rx(fx) a:1 ├─ 1 UI │Ra(fa) │ ││fa = a a—fa │├─ ││○ Ra(fa), fa = a ⊭ ⊥ │├─ ││⊥ 2 │ ││(unfinished) │├─ ││⊥ 2 ├─ 2 ST │⊥

Having introduced the term fa through the instantiation at stage 1, we have the alias sets {a} and {fa}. We consider securing fa by identifying it with the term a. The first gap has then reached a dead end because the universal has already been exploited for a member of its single alias set. There is a second unfinished gap that merely represents the continuation of the gap after stage 1 with no added assumption about the identity of the term fa. The structure described by the dead-end gap is one whose range has a single member named by the term a, which stands in the relation R to itself. The single reference value of this structure is the only possible input and output for the functor f.