2.4.4. Attachment rules

The second sort of case in which use of a lemma is bound to safe is one in which it is clearly entailed by the available resources. A principle justifying that use would take the following form:

If we were to drop the only if, this would be just a another way of stating the law for lemmas, and we know that Γ ⊨ φ only if Γ, ψ ⊨ φ by monotonicity.

There might seem to be little point in regarding this as a case of a lemma at all. If a statement is entailed by the resources, why not just have a rule that allows us to add it to our active resources? Indeed, as far as soundness and safety are concerned, this would come to the same thing. But this second use of lemmas is motivated (as well as constrained) by considerations of decisiveness. That is, our system is decisive in part because active resources are added only to reduce the complexity of proximate arguments, and it may be useful to reach our goal by way of a lemma that is entailed by our resources but is more complex than they are. Adding such a sentence as an active resource would open the door to going around in circles in which we add complexity only to simplify and then add complexity again, and so on.

When discussing the soundness of QED in 2.3.4, 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—if the goal was entailed by available resources. We will not use such a sweeping rule but we will introduce a few rules in special cases that 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. However, 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 once been an active resource that has since been exploited (and it would already be part of the available resources if it had been), it has a status similar to such resources.

One example of the use of Adj is provided by the example in 2.4.3 (though we are thinking of the lemma differently now: there we thought of it as something entailed by the goal while here we think of it as something entailed by the resources).

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

This example also exhibits the sort of foresight or insight that is required to Adj and similar rules. At stage 2, after simplifying our resources as far as possible, we look ahead to the analysis of the goal (before we have built that analysis into our derivation at stages 3 and 5), and we see that we will need to establish B ∧ A twice to reach it. Noticing that we already have the makings of this sentence among our resources, we then assemble it using Adj to have it available for later use.

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. This means that safety and soundness (even strictness) hold as they would for a gap that is completely unchanged. A rule like this must be considered when arguing for the soundness of rules like QED that use merely available resources, but the required argument was already considered in 2.3.4: an counterexample that lurks in a gap and all its ancestors will already make true not only all the available resources but also any sentence φ that is entailed by them, so we do nothing to change the situation by adding such a sentence φ to the available resources.

Of course, a rule like Adj does raise 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. We will not state the sort restriction on the use of attachment rules that would enable us to prove decisiveness; and, for practical purposes, the most valuable constraint on their use is simple good sense. But, as a rule of thumb, it is natural to limit the use of such rules to cases where the lemma is a component of a goal or active resource since such cases will represent the principal grounds for using these rules in any case. But it is important 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.