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 several 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, for it says that an entailment Γ ⊨ φ must hold if the reductio Γ, ¬ φ ⊨ ⊥ holds. Further, 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 we could do so without using ¬ φ itself as a premise. This further lesson will provide the basis for exploiting negative resources. However, 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 of reductios. 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 fact that they are mutually exclusive also supports the entailment ¬ ¬ φ, ¬ φ ⊨ ⊥. If we apply the law for negation as a premise to this entailment, 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 principle 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, and that is just the sort of thing that was 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 supporting a positive conclusion by an argument concerning its denial. 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, and we can simply close a gap whose goal is ⊤. 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 (where we consider the logical properties of something), those are the only goals for which we will use indirect proofs. We have often closed gaps whose goals are atomic, so we know that indirect proof is not always necessary even for such goals, but 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 Tautology and Absurdity 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.

In tree-form and sequent proofs, this new form of argument will look like RAA or negation as a conclusion except that the positions of φ and ¬ φ will be reversed. The same is true of the rule implementing indirect proofs in derivations, but we will choose a name that reflects its rather different role and call it 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 easily seen to be strict and safe, but we need to be more careful in assessing the decisiveness of a system using it. We will consider this question most fully in 3.4.1, but we can see the issue in outline now. Since IP introduces a sentence with one more connective than the goal it plans for, it does not reduce the quantity we have used to assess the progressiveness of other rules. But IP can be seen to be progressive nonetheless if we look progressiveness in a slightly different way. 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 it introduces no resources that need to be exploited further. This suggests a way of looking at the distance of a proximate argument from a dead end that would allow us to say that IP reduces this quantity. This way of looking at distance from a dead end is a departure from counting connectives but only a small departure. We may count connectives except for the case of those sentences that are never exploited or planned for—i.e., atomic and negated atomic sentences as resources and ⊥ as a goal—and these sentences will be given a lower degree than all other sentences, no matter how few connectives those sentences contain.

Although IP introduces a resource that needs no exploitation, this is 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 it can put us in the position to use is the one we will consider next.