In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object. This is in contrast to a nonconstructive proof (also known as an existence proof or pure existence theorem) which proves the existence of a mathematical object with certain properties, but does not provide a means of constructing an example.

Many nonconstructive proofs assume the non-existence of the thing whose existence is required to be proven, and deduce a contradiction. The non-existence of the thing has therefore been shown to be logically impossible, and yet an actual example of the thing has not been found. Nearly every proof which invokes the axiom of choice is nonconstructive in nature because this axiom is fundamentally nonconstructive. The same can be said for proofs invoking König's lemma.

Constructivism is the philosophy that rejects all but constructive proofs in mathematics. Typically, supporters of this view deny that pure existence can be usefully characterized as "existence" at all: accordingly, a non-constructive proof is instead seen as "refuting the impossibility" of a mathematical object's existence, a strictly weaker statement.

Example

Consider the theorem "There exist irrational numbers $a$ and $b$ such that $a^b$ is rational." This theorem can be proved via a constructive proof, or via a non-constructive proof. One possible non-constructive proof proceeds as follows:

• Recall that $sqrt\{2\}$ is irrational, and 2 is rational. Consider the number $q\; =\; sqrt\{2\}^\{sqrt2\}$. Either it is rational or it is irrational.
• If $q$ is rational, then the theorem is true, with $a$ and $b$ both being $sqrt\{2\}$.
• If $q$ is irrational, then the theorem is true, with $a$ being $sqrt\{2\}^\{sqrt2\}$ and $b$ being $sqrt\{2\}$, since

$left\; (sqrt\{2\}^\{sqrt2\}right\; )^\{sqrt2\}\; =\; sqrt\{2\}^\{(sqrt\{2\}\; cdot\; sqrt\{2\})\}\; =\; sqrt\{2\}^2\; =\; 2.$

Actually, q is irrational because of Gelfond-Schneider theorem. 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.

On the other hand, a constructive proof of the same theorem would give an actual example, such as:

$a\; =\; sqrt\{2\},\; ,\; quad\; b\; =\; log\_2\; 9,\; ,\; quad\; a^b\; =\; 3,\; .$

Both $log\_2\; 9$ and $sqrt\{2\}$ are irrational numbers according to unique factorization, and 3 is of course rational.

See also

• Intuitionistic Type Theory

References

• Hardy, G.H. & Wright, E.M. (1979) An Introduction to the Theory of Numbers (Fifth Edition). Oxford University Press. ISBN 0-19-853171-0