|
|
|
Fig. 2.4.1-1. Developing a derivation by introducing a lemma at stage n (a rule that will be part of our systems of derivations only in more restricted forms).
A fully general rule for introducing lemmas was cited in 2.3.2 as an example of an unsafe rule because argument from our resources to the lemma might fail even though the proximate argument of the gap was valid. Such 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 that they can also be progressive. In this section we will look at the problems posed by lemmas more closely before consider a couple of special cases where they do not arise.
The law for lemmas of 1.4.2 can be stated as follows:
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 holds only as an if claim; the corresponding only if does not hold in all cases. 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 that φ ⇒ ψ, we would know Γ ⇒ ψ because of the chain law and there are other cases where would know Γ ⇒ ψ because of special connections between Γ and ψ. These are the two sorts of cases in which we will use lemmas 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 this rule would take the following form:
| ψ | ||||
| ψ | φ | |||
| Lem | ||||
| φ | ||||
Here the proof of φ divides into two branches. The first is a proof of the lemma ψ and the second is a proof φ using ψ in addition to the already available assumptions and the exploitation chains that grow from them. The box around the right-hand branch is intended to indicate that the use of ψ is limited to that part of the proof and ψ’s presence at the upper left is intended to indicate that it is available for this branch as a further assumption from which we may begin exploitation chains.
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.
|
|
|
Fig. 2.4.1-1. Developing a derivation by introducing a lemma at stage n (a rule that will be part of our systems of derivations only in more restricted forms).
The assumption ψ is available only as long as the second of the two short scope lines continues, so it is effectively boxed off in derivations just as it is in the rule above for tree-form proofs.
The second of the two new gaps 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 can be 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.
Even in cases where we can sure backtracking is not necessary the introduction of lemmas can interfere with decisiveness because there may be enough safe lemmas to keep introducing them forever. So our restrictions of the rule Lem will be more severe than would be required merely to insure that the lemma it introduces is safe.