2.4. Using lemmas

2.4.0. Overview

Although our system of derivations as it stands is both sound and complete, we will add rules that reflect the use of lemmas, both because of the importance of lemmas in ordinary explicit deductive reasoning and because the sorts of organization and simplification they provde in that context are of value for our work, too.

2.4.1. The dangers of lemmas
Although the use of lemmas is valuable in general, not all individual lemmas are valuable: the uncontrolled use of lemmas can lead us into blind alleys or delay the progress of a derivation.

2.4.2. Lemmas for reductio arguments
A lemma that is entailed by our goal is safe (though not necessarily progressive); this means that any lemma is safe when the goal is ⊥.

2.4.3. Attachment rules
Lemmas are certainly safe when we know we can prove them. We will use such lemmas to add to the available resources. The sentences added in this way may be more complex than those already present, so this use of lemmas can interfere with decisiveness.