2.4.3. Attachment rules

When discussing the minimal soundness of QED in 2.3.2, we saw that it would be legitimate for a rule to close a gap when its goal is not among its active resources—or even among the active resources of its ancestor gaps—provided it is entailed by available resources. We will not employ such a sweeping rule but we will extend the use of QED (and later rules which use inactive resources) by rules which add to the available resources of a gap without changing either its active resources or its goal.

An example is the following way of developing a gap, which we will call Adjunction:

The added conjunction functions as a lemma so this rule represents a way of using lemmas but it has a number of special features both by comparison with a rule like LFR and by comparison with other rules we have seen.

The lemma φ ∧ ψ does not lie to the right of a new scope line, as it does in the second gap introduced by LFR, for two reasons. First, we have not branched the gap so the added resource is available throughout the gap. And, second, we do not need to mark this new resource off as an added assumption because it is entailed by those already present.

Notice also that we treat this rule not as a way to plan for our goal but simply as a way to add resources. However, it does not exploit resources in order to add others and the X to the right of φ ∧ ψ is intended to indicate that this resource need not be exploited further. One way to think about this is to suppose that φ ∧ ψ has been introduced as something already exploited. That is, although it need not have been a once active but exploited resource (and there would be no point in adding it if it was) it has a status similar to such resources.

Adjunction is one example of a group of rules we will refer to as attachment rules. Any such rule R will exhibit the following general pattern.

Since the lemma is not an active resource, the proximate argument of child gap is the same as the parent’s proximate argument so safety and (utter) soundness hold as they would for a gap that is completely unchanged.

The only question raised by such a rule concerns its impact on the (minimal) soundness of rules like QED that use merely available resources. The fact that the added resource is entailed by available resources means that, if we extend the available resources beyond once active ones only by using attachment rules, all resources available in a gap will be entailed by the active resources of the gap together with the active resources of its ancestors. Any interpretation that divides a gap and all its ancestors will then make all available resources true, and this will be enough for us to establish the soundness of rules using available resources. (To rehearse the argument for QED again: if the goal of a gap is among its available resources no interpretation can divide it and all its ancestors because, to do this, an interpretation would need to make its goal false while making not only its active resources but all its available resources true, and this is impossible when the goal is among the available resources.)

Although, as in the case of LFR, the most important constraint on the use of attachment rules will be good sense, a rule like Adj clearly raises questions about decisiveness since the lemma it introduces is more complex than the premises it is based on. This increased complexity will be typical of attachment rules and is the reason for their name. Apart from good sense, the requirement that the lemma be a component of a goal or active resource is a natural one since such cases will represent the most valuable instances of attachment rules. Here, though, we need to remember that a sentence is a component of itself and one common use of these rules will be to introduce the goal itself as an available resource in order to apply QED to close the gap.

The following derivation is a simple example of this in the case of Adj.

With two uses of Cnj, we would not have needed Adj and, with two uses of Adj, we would not have needed Cnj; but it is this sort of mixed use of the two that brings us closest to typical patterns of explicit deductive argument.