8.5.2. Constructive and non-constructive proof

Let us now turn to the task of establishing an existential conclusion. As the title suggests, we will consider two ways of doing this. 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. We are led to do things in this way by entailment’s focus on a single sentence as the conclusion. Were we to consider relative exhaustiveness rather than entailment, a law for ∃ that makes no reference to ∀ would be easier to state because the consideration of multiple alternatives makes it possible to formulate a principle dual to the principle for the universal as a premise; see appendix B for the form this principle takes.

The second rule for existential conclusions takes a more direct approach. 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, some 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 a different sort of 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.

Before considering the implementation of these principles of entailment in derivations, let us look a little more closely 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. In one of its forms it is this: Γ ⊨ φ ∨ ψ if and only if Γ, ¬^± φ ⊨ ψ. We could have avoided the asymmetric treatment of the two components in this principle 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. 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. So, instead of adding the denials of all instances of the existential, we add the corresponding generalization ∀x ¬^± θx.

Any approach to existential conclusions that is more analogous to the principle for disjunctions as a conclusion would force us to consider repeated partial planning for existential goals as we consider we consider repeated partial exploitation of universal premises. And that would involve a far greater modification of the system of derivations than the rules we will now go on to consider.