3.3.2. Using lemmas to complete reductios

Now that we have IP, we are in a position to provide a proof for any argument whose validity depends only on the properties of ⊤, ⊥, conjunction, and negation. However, to do this using only the rules we have so far, we would often need to use LFR—or, in simpler cases, Adj—to make use of negative resources. This poses no problems when we construct derivations for valid arguments, but it makes it difficult to show that an argument is not valid. LFR does not itself exploit resources, so negated compounds remain as active resources until a gap is closed. In order to count an open gap as having reached a dead end, we would need some description of the conditions under which LFR had been used often enough. Such a description could certainly be given; and, in the last two chapters, we will need to take an analogous approach in the case of one of the rules for quantifiers. But, in the case of negation, it is possible to keep track of the use of resources by way of a genuine exploitation rule, which will eliminate the need to use LFR and Adj.

The basis for this approach is one of the lessons drawn from the law of negation as a premise: if a reductio that has ¬ φ as a premise is valid, then φ must be a valid conclusion from the premises other than ¬ φ. That is, Γ, ¬ φ ⊨ ⊥ only if Γ ⊨ φ. Now φ is just the lemma we need in order to use the premise ¬ φ to reach the goal ⊥ and complete the reductio. The fact that our goal is ⊥ tells us that it is safe to set φ as a goal, and the law for negation as a premise tells us that it is safe to drop ¬ φ from the active resources of the gap in which we establish the lemma φ. That is, we can use a negation ¬ φ to complete any reductio argument, so we can exploit a negated compound whenever our goal is ⊥.

This is illustrated by a segment of an argument tree and a schematic indication of the corresponding two steps in completing a conclusion tree.

¬ φ ? ⊥

¬ φ ? φ ⊥

On the left we have ¬ φ among the resources we hope to use to complete a reductio by reaching the conclusion ⊥. On the right, we have decided to use ¬ φ as one of two premises from which we conclude ⊥, and we seek a way of using other resources to conclude the second premise. The argument on the right is really Nc but our use of that pattern here is different from its use to close a gap when we already have not only ¬ φ but also φ among our resources.

We will call the rule that implements these ideas Completing a Reductio (CR).

Notice that the use of CR is limited to cases where ¬ φ is the negation of a non-atomic sentence. CR is sound and safe when it is applied to negations of atomic sentences, but it would not be progressive in that case because it would allow us to go around in circles. Both IP and CR carry us between gaps whose proximate arguments have the forms Γ, ¬ φ / ⊥ and Γ / φ; but they carry us in opposite directions, so, if there is any overlap in the sentences φ to which they apply, a derivation could move back and forth between the two arguments forever. We block such circles by limiting IP to cases where φ is atomic and limiting CR to cases where φ is non-atomic.

One way of understanding the role of CR is to compare it with a use of LFR, where the recourse to lemma is more explicit. Below are two derivations for the argument that was used as an illustration in the last subsection. The one on the left uses CR and the one on the right uses LFR:

Notice that the gap resulting from CR on the left is identical to, and filled in the same way as, the first of the two gaps introduced by LFR on the right. We know in advance that the second of these gaps will close because the denial of its supposition is one or our active resources. Indeed the point of choosing (A ∧ B) ∧ ¬ C as the lemma in LFA is to combine it with the resource ¬ ((A ∧ B) ∧ ¬ C) to reach ⊥ and complete the reductio. That is, LFA on the right is part of a plan to use the first premise. What is new in CR is the claim that this resource need not be used further in developing the derivation and may be dropped from its active resources. And this makes CR clearly progressive in a way that LFR is not.