7.7.3. Thoroughness

We are going to be talking quite a bit about infinitely developing gaps, so it would be good to look at one. Two examples are shown below. The first illustrates a possibility mentioned in 7.5.3: the exploitation of a universal may introduce a term that immediately provides an opportunity for applying UI again. The second derivation shows that something similar can happen even without functors. Notice that the pattern of stages 1-4 in the second is repeated in stages 5-8 with the terms b and c playing the roles originally created by a and b, respectively; and this pattern is repeated again in 9-12 with the roles played by c and d. Clearly this process could continue forever.

│∀x Rx(fx) a:1, fa:2, f(fa):3, ...
├─
1 UI │Ra(fa)
2 UI │R(fa)(f(fa))
3 UI │R(f(fa))(f(f(fa)))
│⋮
├─
│⊥
│∀x ¬ ∀y ¬ Rxy a:1, b:5, c:9, ...
├─
1 UI ¬ ∀y ¬ Ray
│ⓑ
│││Rab
││├─
5 UI │││ ¬ ∀y ¬ Rby
│││
│││ │ⓒ
│││ │││Rbc
│││ ││├─
9 UI │││ │││ ¬ ∀y ¬ Rcy
│││ │││
│││ │││ │ⓓ
│││ │││ │││Rcd
│││ │││ ││├─
│││ │││ │││ ...
│││ │││ ││├─
│││ │││ │││⊥ 12
│││ │││ │├─
12 RAA │││ │││ ││¬ Rcd 11
│││ │││ ├─
11 UG │││ │││ │∀y ¬ Rcy 10
│││ ││├─
10 CR │││ │││⊥ 8
│││ │├─
8 RAA │││ ││¬ Rbc 7
│││ ├─
7 UG │││ │∀y ¬ Rby 6
││├─
6 CR │││⊥ 4
│├─
4 RAA ││¬ Rab 3
├─
3 UG │∀y ¬ Ray 2
├─
2 CR │⊥

We will see in 7.8.1 that a change in our rules would enable us to develop the initial gap in these derivations in a way that would produce dead-end open gaps, but we will see also (in 7.8.2) that in a derivation with certain additional premises such gaps would close, leaving only the ones shown here. So these gaps are good examples of the problem we face. And they are also examples of its solution; for, if they are continued into infinity in the same way, anything that can be done to develop them will be done at some stage in their development—each resource that can be exploited will be exploited (and, in the case of universals, as often as possible using terms appearing in the gap) and each goal will be planned for. So these illustrate the sort of paths we describe as fully developing. Our aim is to show that our system is thorough, that any derivation will either close or generate a fully developing path, one which will be either end in a dead-end open gap or continue as an infinitely developing path like the ones shown here.

In order to have a thorough system, we must rule out the possibility that a gap is developed infinitely without all possible rules being applied. For example, if either derivation above had A ∧ ¬ A as a second premise, it could be closed—but only if we got around to exploiting this resource and did not ignore the possibility of closing the gap as we exploited other resources. Nothing in the way our rules are stated prevents such oversights, so our system is not thorough as it stands. What we need is a way of organizing the application of the rules that will insure that we eventually apply every rule that we can.

Let us say that a sentence is exploitable in a gap when there is some exploitation rule for it that may be applied to develop that gap. To be exploitable, a sentence must first of all be among the active resources. But a universal resource may be active without being exploitable. This will happen when there are closed terms appearing in the gap but the universal is inactive for all of them. Other sorts of active resources may fail to be exploitable, either permanently or temporarily—such as atomic sentences or sentences that cannot be exploited while the gap has an active goal. Our aim is to manage the development of gaps so that no exploitable resource is left unexploited.

The only reason there is any difficulty here is that exploiting a universal can introduce new ways of exploiting it and other universals, so we are never forced to turn our attention to other tasks. Accordingly, we will manage the development of a derivation by setting an arbitrary limit on the exploitation of universals and gradually relax it as a path develops. We begin by doing all we can to develop a derivation except that we exploit universal resources only for terms in our initial premises and conclusion. Then we take all the terms that have appeared in a path in the course of this development and add them as admissible terms. Again we do all we can to develop each path of a derivation using the enlarged group of terms admissible for it, and so on. Let us call each round of development before enlarging the group of admissible terms, a cycle. Although a universal may not be exploited for each term in the gap at the completion of any given cycle, it will be exploited for all such terms during the next cycle. And the limit on the terms that may be used to exploit universals in a given cycle insures that the current cycle will not continue forever.

Now, if we survey the full development of a derivation, which may proceed to infinity, we have three possibilities: (i) all gaps close, (ii) at some point we find an open gap that cannot be either closed or developed further, or (iii) there is a path that is developed unceasingly. For, if the first two possibilities are not realized, we know that at each stage some gap is open and can be developed further; and it can be shown to follow that there is some path that is open at all stages. To know that our system is thorough, we must know that we have exploited resources and planned for goals as often as possible in cases (ii) and (iii) and have had no opportunity to close the gap. In case (ii) this is obvious, for otherwise the gap could have been developed further or closed. And the procedure above insures that there is a full application of the rules also in case (iii).

The way of organizing the application of rules that has been used here to establish thoroughness is not intended for actual use. It has been stated in a way that makes its effects are easy to see, but this does not make it easy to apply or make it an efficient way of completing derivations that do not go on forever. In practice, we will simply aim at the fullest planning for goals and the fullest exploitation of the broadest range of resources. So the system as we use it will be thorough not simply because of the rules governing its use but in part because of the way we in fact use it; that is, it will be thorough because we are thorough in our use of it.

Glen Helman 25 Aug 2005