2.4.2. The dangers of lemmas

A fully general rule for introducing lemmas was cited in 2.3.4 as an example of an unsafe rule because the resources of a gap might not entail the lemma even when the proximate argument of the gap is valid. Such a rule would also prevent a system from being decisive because it would always be possible to develop a gap further by introducing a lemma. However, as was noted earlier, more limited rules for introducing lemmas can be safe, and we will see later that they can also be progressive. In this section we will look at the problems posed by lemmas more closely before going on, in 2.4.3 and 2.4.4, to consider a couple of special cases where these problems do not arise.

The law for lemmas of 1.4.7 can be stated as follows:

Let us recall why this is true: any possible world that is a counterexample to the first entailment will be a counterexample to one of the two on the right—the first of them if it makes ψ false and the second if it makes it true. So if both entailments on the right hold (that is, neither has a counterexample), then the one on the left will hold, too.

But this principle is stated only as an if claim, and the corresponding only if statement is not always true. When Γ ⊨ φ, we know that Γ, ψ ⊨ φ by the monotonicity of ⊨; but, since φ and ψ need have no connection with one another, knowing that Γ ⊨ φ would by itself give us no reason to suppose that Γ ⊨ ψ. Of course, in a case where we know that φ ⊨ ψ, we would know Γ ⊨ ψ because of the chain law, and there are other cases where would know Γ ⊨ ψ because of special connections between Γ and ψ. We will use lemmas in special cases like these; but, before turning to them, let’s look at what a fully general rule for lemmas would be like.

If used in conclusion trees a rule for lemmas would take the following form:

Before applying this rule to reach the conclusion φ, two things must be done. The first is to prove the lemma ψ, and the second is to prove φ, having available the lemma ψ in addition to the already available assumptions. The supposition ψ is offered for use as a branch tip only in the part of the tree above φ. Below φ, it has been discharged.

The value of using Lem rather than proving ψ on the right to begin with lies first in allowing us to consider the two components of the argument separately. But we could also save some work in cases where the assumption ψ appears more than once in the tree on the right since we would not need put the proof of ψ above each of these. Both of these functions lie behind the use of lemmas in mathematical proofs. In the next section, we will see a simple example of the second sort of use.

The appearance of a corresponding step in an argument tree is shown below. Notice that the assumption ψ is dropped between the second of the arguments to which the rule is applies and the result of applying it.

That is, to prove φ we first try on the one hand to prove ψ and, on the other, to use the supposition that φ is true to prove φ. Here the price we pay for the use of ψ as a premise in the second argument on the right is need to reach it as a conclusion in the argument above it. And that is what makes lemmas dangerous. Although the validity of the two arguments on the right will insure the validity of the argument on the left. The fact that we can validly conclude φ from certain premises certainly does not insure that we can conclude a sentence ψ (which, so far as the statement of the rule goes, might be anything) from the same premises.

Finally, here is the derivation rule for lemmas.

Remember that the assumption ψ is available only to the right of its scope line and that, after that scope line ends, it is said to have been discharged. The part of the proof in which this assumption is available corresponds to the right side of the tree in the conclusion trees and the lower branch in the argument trees we have been looking at.

Again, we gain something from proceeding in this way—but at a price. The second of the two new gaps in a derivation developed using Lem should be, if anything, easier to close than the original gap because it has a further resource. This increased ease is the point of introducing a lemma. The price we pay for this is the need to close the first new gap also. If the lemma is properly chosen, that may also be easier than closing the original gap; but, because this rule is unsafe, we cannot be sure in general that the first new gap can be closed at all even if the original one could be closed eventually in other ways. Because of this, when lemmas are introduced in ordinary deductive reasoning we must be prepared to backtrack, to abandon the attempt to work by way of the lemma and look for another approach to the proof. The notation of derivations is not designed to incorporate backtracking, so we will use lemmas only in cases where we can be sure there will be no need to do that.

Indeed, we will not incorporate the rule Lem in the general form given here into our system of derivations. Instead, we will employ more specific rules that are based on the idea behind it. Even in cases where we can sure backtracking is not necessary, the introduction of lemmas could interfere with decisiveness if there were enough safe lemmas to keep introducing them forever. So our restrictions on the use of alternatives to Lem will be more severe than would be required merely to insure their safety.