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 ⊥.

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

The motivation for CR lies in its use to exploit the negations of non-atomic sentences, since we can arrange things so that the negations of atomic sentences remain active forever. In fact, we must limit the use of CR to the negations of non-atomic sentences. It is sound and safe in the case of 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.