Constructive Proof - Example

Example

Consider the theorem "There exist irrational numbers and such that is rational." This theorem can be proven via a constructive proof, or via a non-constructive proof.

Dov Jarden's non-constructive proof, also attributed to Peter Rogosinski and Roger Hindley, proceeds as follows:

• Recall that is irrational, and 2 is rational. Consider the number . Either it is rational or it is irrational.

• If is rational, then the theorem is true, with and both being .

• If is irrational, then the theorem is true, with being and being, since

This proof is non-constructive because it relies on the statement "Either q is rational or it is irrational"—an instance of the law of excluded middle, which is not valid within a constructive proof. The non-constructive proof does not construct an example a and b; it merely gives a number of possibilities (in this case, two mutually exclusive possibilities) and shows that one of them—but does not show which one—must yield the desired example.

(It turns out that is irrational because of the Gelfond–Schneider theorem, but this fact is irrelevant to the correctness of the non-constructive proof.)

A constructive proof of the theorem would give an actual example, such as:

The square root of 2 is irrational, and 3 is rational. is also irrational: if it were equal to, then, by the properties of logarithms, 9n would be equal to 2m, but the former is odd, and the latter is even.

A more substantial example is the graph minor theorem. A consequence of this theorem is that a graph can be drawn on the torus if, and only if, none of its minors belong to a certain finite set of "forbidden minors". However, the proof of the existence of this finite set is not constructive, and the forbidden minors are not actually specified. They are still unknown.