2.4.3. Lemmas for reductio arguments

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

which tells us that, when φ ⊨ ψ, it is not only sound but also safe to introduce a lemma ψ in a derivation whose goal is φ. It is the only if part of this principle—and, more specifically, the part that says Γ ⊨ φ only if Γ ⊨ ψ—that requires the assumption that φ ⊨ ψ.

In order to apply the idea of this principle in derivations, we can look for convenient ways of insuring that φ ⊨ ψ. The obvious valid arguments of this form 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 extraction 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 basic idea here—isolating a component of an argument to avoid repeating it—is an important one. However, the actual simplification in this case is limited, and we would have few opportunities to use lemmas whose safety was assured by Ext. So we will not build this use of lemmas into our system of derivations, it will serve us only as an initial example.

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:

The principle associated with this rule is the following:

Although this follows from the principle stated at the beginning of the section and the validity of EFQ, it is instructive to look at its justification more directly. The if part again is just an instance of the law for lemmas. The only if part tells us that any counterexample lurking in one of the child gaps will also lurk in the parent. But this must be so, for any counterexample lurking in a child will make the active resources of the parent true (since they all remain active in each of the children) and because every interpretation makes ⊥ false.

Unfortunately, we are not yet in a position to illustrate this rule because 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 member or as a component of one. Such a set a can be shown to entail ⊥ with use of nothing but Ext and QED, so introducing LFR would merely complicate that argument.

In the next chapter, the rule LFR will serve us as a temporary expedient, but we will eventually introduce other special rules that are designed to cover the case where LFR would be most useful, and LFR itself will be ignored. One reason is that the free use of LFR would undermine decisiveness since the form of the rule places no constraints on the number of different lemmas that might be introduced. Something like a limitation to sentences that already appear as components of active resources and goals would be sufficient to insure decisiveness and would still permit the more important uses of the rule, but we will not attempt to formulate the sort of restriction that would enable us to prove decisiveness for a system with LFR. It is simply not important enough to bother. Apart from its role as a temporary expedient, it will serve us mainly as a way of displaying the connection between the special rules to be introduced later and the idea of a lemma.