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 here, 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, of course, safe when we know we can prove them. We will use such lemmas to add to the available resources. The sentences added will generally be more complex than those already present, so this use of lemmas can interfere with decisiveness.