2.4.1. 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.2 and 2.4.3, to consider a couple of special cases where these problems do not arise.

The law for lemmas of 1.4.6 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 tree-form proofs a rule for lemmas would take the following form:

This rule divides the proof of φ into two branches, and represents a division of the task of proving φ into two components. The first is to prove the lemma ψ, and the second is to prove φ using the lemma ψ in addition to the already available assumptions and conclusions derived from them. The occurrence of ψ above φ at the right is intended to indicate that ψ is an assumption from which conclusions can be drawn in this branch, and the slash through it indicates that is not an assumption of the proof after the use of Lem. Such an assumption is said to be discharged, and we will use the same term when an assumption is no longer available in a derivation.

The assumption ψ may occur at the tips of several branches on the right, and it is legitimate to discharge some or all of them. The effect of Lem is understood to be the same as replacing the discharged assumptions ψ in the right branch with conclusions proved in the way shown by the left branch, so the effect of the rule is to erase the discharged assumptions as assumptions.

The value of using Lem rather than proving ψ on the right to begin with lies in allowing us to consider the two components of the argument separately and to save some work in cases where the assumption ψ appears more than once in the tree on the right. 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 a sequent proof is shown below. Notice that the assumption ψ is dropped between the second of the premise sequents and the conclusion sequent.

Sequent proofs with such a rule would work in only one direction. The law for lemmas does justify the conclusion sequent if we are able to establish the premise sequents, but we cannot go in the other direction. That is, since the conclusion sequent may hold even if the first of the premise sequents does not hold, we cannot investigate the requirements for an entailment to hold by moving up from the root.

In the notation of derivations, we use scope lines to mark the scope of added assumptions, which are marked off from other resources along a scope line by the sort of horizontal line we use to indicate the premises of the ultimate argument. In the diagram below, notice that the proximate arguments of the gaps before and after the rule is applied follow the pattern shown in the sequent proof step above.

The assumption ψ is available only to the right of its scope line. 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 tree-form and sequent proofs we have been looking at.

The effect of this rule on an argument tree is the following pattern of branching:

Again notice that ψ is added to the premises in the right-hand child, and it is no longer among the assumptions when we move from this child back down the tree to its parent. (Nothing rules out the possibility that ψ already appears in Γ; this would be equivalent to having a tree-form proof in which the use of Lem discharges only some of the occurrences of the assumption ψ.)

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.