8.5.2. Constructive and non-constructive proof

As the title suggests, we will consider two ways of establishing an existential conclusion. In the first and most general of these, we establish a claim ∃x θx that a property θ is exemplified by reducing to absurdity the claim ∀x ¬^± θx that nothing has this property. This way of drawing an existential conclusion is called a non-constructive proof because it enables us to establish a claim of exemplification without ever describing a particular example. The use of the term construction here can be traced historically to geometry, where claims of exemplification are typically established by a geometric construction of the figure that is claimed to exist; but the term construction has come to be applied in mathematics to other techniques that specify particular examples.

We will adopt the idea of non-constructive proof as our basic principle for the existential as a conclusion.

This principle does not explain the role of the existential as a conclusion directly, but instead makes a connection with the role of the universal as a premise. A law for ∃ that makes no reference to ∀ is easier to state for relative exhaustiveness where the use of multiple alternatives makes it possible to principle dual to the principle for the universal as a premise; see appendix B for the form this principle takes.

On the other hand, a constructive proof of a claim of exemplification establishes the claim by first producing an example of the sort that is claimed to exist. The move from an example to a claim of exemplification appears formally as a step from an instance of an existential to the existential itself. The principle of entailment governing this step is commonly known as existential generalization:

The conclusion of this entailment is not a generalization in the sense in which we have been using the term. But it may be said of someone who is making heavy use of words like something and someone that he is speaking in generalities and is not being specific. The principle of existential generalization is a license to move from a specific claim to a generality of an existential sort. We cannot rely on this principle alone, but it does provide a useful supplement in the way the principle of weakening supplements the law for disjunction as a conclusion. And, like weakening, we will count existential generalization as an attachment principle. (What is attached? In form, we could say it is the existential quantifier; in what is said, it is the other instances of the conclusion, the other ways in which it could be true.)

Although non-constructive proofs of exemplification have been common in modern mathematics, many have questioned their value. The doubts about them have not usually been doubts about their validity (though Brouwer, who was mentioned in 3.1.3, could be said to have doubted that in spite of the fact that early in his career he produced some non-constructive proofs for which he is still famous). The feature of non-constructive proofs that lies behind these doubts is instead a weakness that is granted even by those who accept such proofs happily: because they do not produce an example, non-constructive proofs may provide little insight into the reasons why a claim of exemplification is true.

The deepest concerns about non-constructive proof are focused on arguments about abstract and, especially, infinite structures, and even Brouwer thought that non-constructive proofs were valid for reasoning about ordinary claims concerning the world of sense experience. Still, the indirection and uninformativeness of non-constructive arguments can be felt with ordinary reasoning and is often unnecessary, so it is worthwhile considering the alternative.

Finally, let us look further at the reasons why our general account of the existential as the conclusion has been made parasitic on our account of the universal as a premise. First, recall our account of the role of disjunction as conclusion: Γ ⇒ φ ∨ ψ if and only if Γ, ¬^± φ ⇒ ψ. We could have avoided the asymmetric treatment of the two components if we had resorted to an even heavier use of negation; applying the idea behind IP to the right side of the law, we get this: Γ ⇒ φ ∨ ψ if and only if Γ, ¬^± φ, ¬^± ψ ⇒ ⊥. That is, a disjunction is a valid conclusion if and only if we can reduce to absurdity the supposition that its components are both false. We are often able to avoid this use of reductio arguments in the case of disjunction, but it would be awkward to do so in the case of the existential.

A strict analogue for the existential of this rule for disjunction would say that we can conclude an existential ∃x θx from premises Γ if and only if we can reduce to absurdity the result of adding denials of all the instances of ∃x θx to Γ. But, since there is no definite set of instances, we cannot take this approach literally. We had an analogous problem in the case of the universal, where an attempt to follow the pattern of our treatment of conjunction as a premise would lead us to replace a universal premise by all of its instances. Our solution was the to add instances freely while retaining the universal. We cannot replicate that approach for existentials in principles for entailment since it would require multiple alternatives rather than a single conclusion, but we can make our treatment of existentials parasitic on the account for universals. Instead of adding the denials of all instances of the existential, we add the corresponding generalization ∀x ¬^± θx.