3.3.1. Indirect proof

The last section pursued consequences of the law for negation as a conclusion. The rules of this section will implement the other basic law for negation, the law for it as a premise:

This says that a negation is ¬ φ inconsistent with a set Γ if and only if the sentence φ is entailed by that set.

There are two lessons we can learn from this law. First, the only-if-statement tells us that negative conclusions are not the only ones that can be established by way of reductio arguments. That is, an entailment Γ ⇒ φ can be supported by the reductio Γ, ¬ φ ⇒ ⊥. The if-statement tells us in part that such an approach is safe, that the reductio is valid whenever the argument we wish to support by it is valid. But if-statement tells us more. Notice that φ is just the sort of resource that would enable us to complete a reductio that has ¬ φ as a premise. The if-claim above tells us that, if a reductio with ¬ φ as a premise can be completed at all, we would be able to validly conclude φ as a lemma—and that concluding it would not depend on using ¬ φ itself as a premise. This further lesson will provide the basis for exploiting negative resources, but its full application depends on the broader use of reductio arguments supported by the other two lessons, and that is what we will consider first.

Here is an example of this broader use. If we take No one is home to be the negation ¬ someone is home, the law for negation as a premise says we can rest the validity of the left-hand argument below on the validity of the right-hand argument.

The right-hand argument depends in part on the logical properties of if; but, as far as negation is concerned, it depends on only the fact that a sentence and its negation are mutually exclusive.

The same basic fact gives us ¬ ¬ φ, ¬ φ ⇒ ⊥. If we apply the law for negation as a premise to this, we get the principle ¬ ¬ φ ⇒ φ. Moreover, the latter principle can be combined with the law for negation as a conclusion to establish the law for negation as a premise. So the further logical properties of negation that are captured by the law for negation as a premise can be summarized in the principle that a double negation entails the corresponding positive claim.

This principe is one that was rejected by Brouwer in his intuitionistic mathematics. And one of his chief reasons for rejecting it was that it would allow us to draw a conclusion of the form Something has the property P when the corresponding claim Nothing has the property P was inconsistent with our premises—that is, just the sort of thing done in the example above. His concern with this is that it would enable us to conclude Something has the property P in cases where we were unable, even in principle, to provide an actual example of a thing with that property P. Brouwer did not object to such an argument in ordinary reasoning about the physical world (like the example above); but he held that, in reasoning concerning infinite mathematical structures, we were not reasoning about an independently existing realm of objects but instead about procedures for constructing abstract objects and that we had no business claiming the existence of such objects without having procedures enabling us to construct them. Brouwer’s concerns may not lead you to question the law for negation as a premise; but they highlight the indirectness of basing a positive conclusion on the fact that its denial is inconsistent with our premises. This aspect of these arguments is reflected in a common term for them, indirect proofs.

Although we will employ indirect proofs, we will need them for only a limited range of conclusions. We have other ways of planning for a goal that is a conjunction or a negation. We can simply close a gap whose goal is ⊤. And we will not adopt any rule to plan for the goal ⊥ of a reductio argument. At the moment, that leaves only unanalyzed components; and, until the last chapter, those are the only goals for which we will use indirect proofs. We have often closed gaps whose goals are atomic so, even for them, we know that indirect proof is not always necessary. However, it will serve us as a last resort.

In chapter 6, we will begin to analyze sentences into components that are not sentences, and we will still use indirect proof for goals that are analyzed in that way. In anticipation of this, we will use the term atomic for the kind of goals to which we will apply indirect proof; and we will refer to other sentences as non-atomic. Until chapter 6, any sentence we analyze will be a compound formed by applying a connective to one or more sentences, so, for the time being, the atomic sentences will be the unanalyzed sentences. ⊤ and ⊥ count as non-atomic since identifying them as logical constants counts as an analysis of their logical form. As a result, for the time being, the atomic sentences will be simple letters, and all other sentences will be non-atomic.

The rule implementing indirect proofs in derivations will be called Indirect Proof (IP). It takes the following form:

Here is an example, which is related to the argument at the beginning of 3.2.2.

This example adds to the premise Ann and Bill were not both home without the car being in the driveway further premises telling us that each of Ann and Bill was home, and we conclude that the car was in the driveway. Although the initial premises and conclusion differ from those of the argument in 3.2.2, the reductio argument that is set up at stage 1 here has the same resources as the reductio set up at stage 3 in the derivation for the argument of 3.2.2 that was given at the end of 3.2.3.

The rule IP is not direct (in the sense used in 2.3.4) because it introduces a sentence more complex than the goal it plans for. It is, however, progressive. We will treat both atomic sentences and their negations as equally basic when they are resources: neither sort of resource will be exploited. And, as was noted above, we will treat ⊥ as the basic form of goal, the only one without a corresponding planning rule. Thus IP leaves us with a goal that requires no planning and introduces no resources that need to be exploited further. This is, of course, not to say that applying IP will eliminate the need for further exploitations; indeed, since negated compounds will be exploited only in reductio arguments, we will often be in a position to exploit such resources only after we have used IP. The rule we will use to do that is the one we will consider next.