2.4.2. Lemmas for reductio arguments

We have seen that a lemma is bound to be safe if it is entailed by the goal we seek. That is, we can state following principle:

which tells us that when φ ⇒ ψ, it is both sound and safe to introduce a lemma ψ in a derivation whose goal is φ.

In order to apply this idea, we can look for appropriate choices of φ and ψ in valid single-premised arguments. The obvious arguments among those we have identified so far are EFQ and the two forms of Ext. Although EFQ will prove to be the more important, Ext is a better source of examples at the moment and we will consider it first. Here is a derivation which uses the rule Lem to introduce a lemma that is the result of applying left Ext to the final goal.

Here the rule Lem is applied at stage 2 with the left component of the goal as the lemma. This yields a slight shortening of the derivation since we are able to use the lemma to conclude B ∧ A by QED at stages 7 and 9 rather than repeating the proof used at stages 3-5 twice.

The simplification here is slight and it occurs at all only because of a repetition in the goal that we would not expect to encounter often. While we would have more opportunities to use this sort of lemma in later chapters, there would not be enough to lead us to introduce a special rule and this will serve us only as an initial example. It is worth remembering, however, that it is legitimate pattern of deductive reasoning to conclude one of the two components of a conjunction and then use that component to conclude the other (as we here have used the lemma B ∧ A in concluding A ∧ (B ∧ A)).

The pattern Ex Falso Quodlibet provides the basis for a much more imporant use of lemmas. An argument whose conclusion is ⊥ is often called a reductio argument; reductio here is short for the Latin phrase reductio ad absurdum (‘reduction to absurdity’). We will often need to use a lemma to complete such an argument and, since EFQ tells us that ⊥ entails any sentence, we know that any lemma we choose is safe. We will call the rule implementing this idea Lemma for Reductio or LFR:

│... │ ││... ││ ││ ││ ││ ││ ││ ││ ││ ││ ││ ││ │├─ ││⊥ │...

│... │ ││... ││ │││ │││ ││├─ │││φ n ││ │││φ ││├─ │││ │││ ││├─ │││⊥ n │├─ n LFR ││⊥ │...

Fig. 2.4.2-1. Developing a derivation by introducing a lemma for a reductio at stage n.

We know this is safe from earlier arguments, but it is also easy to see that directly. Any interpretation that divided either of the new gaps would certainly have to make all active resources of the original gap true; but an interpretation that did that would divide the original gap since its goal ⊥ is bound to be false. So neither of the two new gaps divided unless their parent was.

While this rule is certainly important, we are not yet in a position to illustrate it because, as yet, we have no non-trivial examples of formally valid reductio arguments. A reductio is formally valid only if its premises constitute a formally inconsistent set (that is, one whose members cannot be all true on any extensional interpretation) and the only formally inconsistent sets available with our current analyses of sentences contain ⊥ either as a premise or as a component of one. And such set a can be shown to entail ⊥ with use of nothing but Ext and QED. This situation will change in the next chapter but, even there, our chief use of lemmas will be in a special modified version of this rule that is designed to actually exploit resources.

That rule will be direct but rules that introduce lemmas usually will not be and, in order to be sure a system employing them was decisive we would need to show that they could be considered progressive (on the right measure of distance from the end). The use of Lem to introduce a component of the goal can be regarded as progressive provided we require that the lemma is not already an active resource. But the free use of LFR would undermine decisiveness even if we forbid such repetition since the form of the rule places no constraints on the number of different lemmas that might be introduced. Something like a limitation to components of active resources and goals would be sufficient but more minimal restrictions would also work. In general, we will not attempt to formulate the sort of restriction that would enable us to prove decisiveness for a system with LFR. The value of the rule is a practical one and in practice the constraint of good sense in its use is restrictive enough.