|
|
|
Fig. 3.2.2-1. Developing a derivation by planning for a negation at stage n.
The law for negation as a conclusion
Γ ⇒ ¬ φ if and only if Γ, φ ⇒ ⊥
describes the conditions under which an entailment of the form Γ ⇒ ¬ φ holds. An example may help in thinking about this law. The argument
|
Ann and Bill were not both home without the car being in the driveway Ann was home but the car was not in the driveway Bill was not home |
is valid and seeing that it is valid comes to the same thing as seeing that Bill could not have been home if the premises are true. But to see this is to see that the claim Bill was home is excluded by the premises of the argument. The negative conclusion of this argument is valid because the conclusion denies something that is excluded by the premises.
And the law for negation as a conclusion says that this holds in general since a reductio entailment Γ, φ ⇒ ⊥ is the way we capture exclusion in terms of entailment. That is, Γ excludes φ if adding φ to Γ would enable us to reach an absurd conclusion. In these terms, we can validly conclude a negation ¬ φ when we can reduce to absurdity the result of adding φ to the premises Γ.
Although the entailment Γ, φ ⇒ ⊥ shows the inconsistency of the full set containing the members of Γ together with φ, we focus attention on φ when we say it is excluded by, or is inconsistent with, Γ. Similarly, we can say that the argument Γ, φ / ⊥ reduces φ to absurdity given Γ. So we can restate the law for negation as a conclusion in another way: we can validly conclude a negation ¬ φ from premises Γ when we can reduce φ to absurdity given the premises Γ.
To implement this idea as a way of developing a gap whose goal is ¬ φ, we must add φ as a further resource in the child gap. Unlike resources added through Ext, this added resource will generally go beyond information contained in the premises. It is a genuine addition to the claims made by the premises, amounting to a further assumption for the purposes of the argument. Such further assumptions are often called suppositions and the verb suppose is used to introduce them when putting this sort of deductive reasoning into words. Suppositions can have a variety of roles in deductive reasoning. In the second gap introduced by the rules Lemma and LFR of §2.4, the lemma is introduced as a supposition. In those rules it represents a resource that we have on loan, a loan that is paid if we are able to close the first gap. When we suppose φ in order to prove ¬ φ, we make the supposition in order to refute it by reducing it to absurdity. That is, we make the supposition in order to consider a possibility, and we go on to rule out the possibility on the basis of the assumptions to which the supposition was added. We will encounter still other uses of suppositions in later chapters.
The rule that implements this idea in derivations will be called Reductio Ad Absurdum or RAA. It leads us to develop a gap by adding a supposition and, at the same time, changing our goal to ⊥. The part of the derivation these changes affect is marked by a scope line, and the added resource is marked off at the top by a horizontal line. That is, the rule by which we plan for negative goals will take the form shown in Figure 3.2.2-1.
|
|
|
Fig. 3.2.2-1. Developing a derivation by planning for a negation at stage n.
If we state this rule for tree-form proofs, it takes the following form (which you should compare to the analogous diagram for the rule Lem of §2.4.1):
| φ | ||
| ⊥ | ||
| RAA | ||
| ¬ φ | ||
This shows a pattern of argument in which we conclude ¬ φ from the premise ⊥. But that description would apply also to the rule EFQ, so it does not capture all that is going on here. The conclusion ¬ φ is, in general, weaker than ⊥. And the rule for negation as a conclusion tells us that the particular way it is weaker licenses us to drop φ from our assumption. The fact that ⊥ falls within the scope of a supposition φ in the tree-form argument, shows that it is itself the conclusion of a reductio argument. The rule RAA enables us to transform that argument by both weakening its conclusion and ending the scope of the assumption φ.
Once we have begun a reductio argument, we have ⊥ as our goal and we must look for ways of reaching it. The only way we have in our rules so far is QED, but that requires that we have ⊥ among our resources. While it is, of course, possible that our new supposition is ⊥ or that ⊥ was already among our resources, we would not expect this to happen in general. Usually, we will need to make use of both the supposition and the pre-existing resources and make use of some negative claims among them. Our full discussion of the use of negative resources will come only in §3.3, but the core principle for using such resources is one we can consider now.
One of the traditional laws of logic is the law of non-contradiction. Even though this is sometimes referred to as the law of contradiction
and its name is more consistent than the way it is stated, the basic idea is always the same: a statement and its denial cannot both be true. We know it as the principle that ¬ φ and φ are mutually exclusive—or, in the form most relevant at the moment, that ¬ φ, φ ⇒ ⊥. This idea lies behind a pattern of argument that we will call Non-contradiction or Nc:
| ¬ φ | φ | ||
| Nc | |||
| ⊥ | |||
This pattern of argument will appear in derivations as a way of completing a reductio argument:
|
|
|
Fig. 3.2.2-2. Closing the gap of a reductio argument one of whose resources negates another.
Notice that, as with other rules that close gaps, the resources required to apply this need only be available and they are marked with parenthesized stage numbers. The latter point is, of course, moot since the gap closes and, in a way, the first point is moot also. Once we have the further rules of §3.3, we will need this rule only when φ is an unanalyzed component (though it will be usable and useful in other cases, too). And we will never have rules for exploiting unanalyzed components or their negations so such resources will be active whenever they are available.