3.2.2. Drawing negative conclusions

The law for negation as a conclusion

describes the conditions under which an entailment of the form Γ ⊨ ¬ φ holds. An example may help in thinking about this law. The argument

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. So the negative conclusion of this argument is valid because the conclusion denies something that is excluded by the premises.

This connection between validity and exclusion is just what the law for negation as a conclusion states. For a reductio entailment Γ, φ ⊨ ⊥ is the way we capture exclusion in terms of entailment: Γ excludes φ if adding φ to Γ would enable us to reach an absurd conclusion. And the law tells us that we can validly conclude a negation ¬ φ when we can reduce to absurdity the result of adding φ to the premises Γ. So we can say that the example above is valid because due to the inconsistency of the three sentences

We can reduce these claims to absurdity by noting that the second and third together imply Ann and Bill were both home without the car being in the driveway and that this is what the first denies.

Although this reduction to absurdity shows the inconsistency of the full set of sentences from which we draw the absurd conclusion, we focus attention on the last one of them to draw a negative conclusion from the first two. And in general, the entailment Γ, φ ⊨ ⊥ shows the inconsistency of the full set containing the members of Γ together with φ, but we focus attention on φ when we say it is excluded by, or is inconsistent with, Γ. We can focus attention on a single sentence when speaking of reduction to absurdity itself by saying that the argument Γ, φ / ⊥ reduces φ to absurdity given Γ. And this allows us to 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 Γ. In the example above, we reduced Bill was home to absurdity given the two premises of the original argument.

As a rule for argument trees, the principle for negation as a conclusion would lead us to grow the tree as shown here:

There is no branching, but a premise is added and the required conclusion is strengthened to ⊥. And if we state this rule for conclusion trees, it takes the following form:

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 clearly does not capture all that is going on here. The conclusion ¬ φ is, in general, weaker than ⊥. The premise ⊥ falls within the scope of a supposition of φ. After that supposition is discharged, our conclusion must be weaker than ⊥. The conclusion ¬ φ is in general weaker than ⊥, and it is weaker in a way that licenses us to drop φ from our assumptions: since ¬ φ rules out no case where φ is false, it need no longer depend on an assumption φ that rules out such cases.

This illustrates a use of suppositions that is different from that in the rules Lem and LFR of 2.4. In those rules, the supposition represents a lemma that we have on loan, a loan that is paid if we are also able to conclude the lemma without supposing it. When we suppose φ in order to prove ¬ φ, we make a different use of the supposition: we suppose it in order to refute it by reducing it to absurdity. That is, we make the supposition in order to describe a sort of possibility, and we go on to rule out this sort of possibility on the basis of other assumptions. We will encounter still other uses of suppositions in later chapters.

The rule that implements these ideas in derivations will be called Reductio Ad Absurdum or RAA. It is shown in Figure 3.2.2-1.

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.

As with other rules, the form of RAA in conclusion trees explains the numerical annotations for it in derivations. A stage number is placed to the right of ⊥, since it is the premise from which ¬ φ is concluded. The supposition φ is not a premise of the rule but plays a different role so no stage number is added to its right (though one might appear later if it is exploited inside the gap as it develops further). The fact that the supposition is discharged when we draw a conclusion from ⊥ is shown in the derivation simply by the fact that its scope line ends with ⊥.

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. This is sometimes referred to also as the law of contradiction when the focus is simply on the fact that it is a law for concluding something from a contradictory pair rather than the fact that what we conclude is that they cannot be both 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:

This pattern of argument will appear in derivations as a way of completing a reductio argument:

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 moot, as it was with QED and EFQ, since the gap closes. And, in a way, the possibility of using available but inactive resources 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.