2.4.s. Summary

The introduction of a lemma is one way of dividing up the work of a proof. We can implement this idea in derivations by dividing a gap into two, one with the lemma as a goal and the other with it as a further assumption to use in reaching the goal of the parent gap. The rule Lemma (Lem) that does this is not safe in general nor is it always progressive, and we will use only special instances of it.

A lemma is always safe when it is entailed by the goal it is designed to help us reach. The principal use of this idea will come in arguments whose goal is ⊥—that is, in reductio arguments. Since ⊥ entails any sentence a rule Lemma for Reductio (LFR) which allows free use of lemmas in reductio arguments will be safe (though some restriction on its use is needed to insure it is progressive).

A lemma is also safe if we know we can reach it. Rules applying this idea will be designed for particular sorts of entailment and, since the lemma is known to follow from our resources, there is no need to divide the gap or even introduce a new scope line. Indeed, we will use this sort of lemma only in attachment rules that add the lemma as an available but inactive resource. The first example of this sort of rule is Adjunction (Adj) which adds a conjunction when both conjuncts are already available. Although attachment rules can help us to close gaps sooner, the rules themselves are not direct so some care is needed in their use if they are to be progressive.

The derivation rules we have so far are summarized in the table below. The names of the rules are links to the point in the text where they were initially described; look there to see the actual form taken by the rule.