Constructive proof

From Wikipedia, the free encyclopedia

In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem) which proves the existence of a particular kind of object without providing an example.

Some non-constructive proofs show that if a certain proposition is false, a contradiction ensues; consequently the proposition must be true (proof by contradiction). However, the principle of explosion (ex falso quodlibet) has been accepted in some varieties of constructive mathematics, including intuitionism.

Constructivism is a mathematical philosophy that rejects all but constructive proofs in mathematics. This leads to a restriction on the proof methods allowed (prototypically, the law of the excluded middle is not accepted) and a different meaning of terminology (for example, the term "or" has a stronger meaning in constructive mathematics than in classical).

Constructive proofs can be seen as defining certified mathematical algorithms: this idea is explored in the Brouwer–Heyting–Kolmogorov interpretation of constructive logic, the Curry–Howard correspondence between proofs and programs, and such logical systems as Per Martin-Löf's Intuitionistic Type Theory, and Thierry Coquand and Gérard Huet's Calculus of Constructions.

Example

Consider the theorem "There exist irrational numbers $a$ and $b$ such that $a^{b}$ 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,^[1] proceeds as follows:^[2]

Recall that ${\sqrt {2}}$ is irrational, and 2 is rational. Consider the number $q={\sqrt {2}}^{{{\sqrt 2}}}$ . 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}}^{{{\sqrt 2}}}$ and $b$ being ${\sqrt {2}}$ , since

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

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 ${\sqrt {2}}^{{{\sqrt 2}}}$ 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:

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

The square root of 2 is irrational, and 3 is rational. $\log _{2}9$ is also irrational: if it were equal to ${m \over n}$ , then, by the properties of logarithms, 9ⁿ would be equal to 2^m, 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.

Brouwerian counterexamples

In constructive mathematics, a statement may be disproved by giving a counterexample, as in classical mathematics. However, it is also possible to give a Brouwerian counterexample to show that the statement is non-constructive. This sort of counterexample shows that the statement implies some principle that is known to be non-constructive. If it can be proved constructively that a statement implies some principle that is not constructively provable, then the statement itself cannot be constructively provable. For example, a particular statement may be shown to imply the law of the excluded middle. An example of a Brouwerian counterexample of this type is Diaconescu's theorem, which shows that the full axiom of choice is non-constructive in systems of constructive set theory, since the axiom of choice implies the law of excluded middle in such systems. The field of constructive reverse mathematics develops this idea further by classifying various principles in terms of "how nonconstructive" they are, by showing they are equivalent to various fragments of the law of the excluded middle.

Brouwer also provided "weak" counterexamples.^[3] Such counterexamples do not disprove a statement, however; they only show that, at present, no constructive proof of the statement is known. One weak counterexample begins by taking some unsolved problem of mathematics, such as Goldbach's conjecture. Define a function f of a natural number x as follows:

$f(x)={\begin{cases}0&{\mbox{if Goldbach's conjecture is false}}\\1&{\mbox{if Goldbach's conjecture is true}}\end{cases}}$

Although this is a definition by cases, it is still an admissible definition in constructive mathematics. Several facts about f can be proved constructively. However, based on the different meaning of the words in constructive mathematics, if there is a constructive proof that "f(0) = 1 or f(0) ≠ 1" then this would mean that there is a constructive proof of Goldbach's conjecture (in the former case) or a constructive proof that Goldbach's conjecture is false (in the latter case). Because no such proof is known, the quoted statement must also not have a known constructive proof. However, it is entirely possible that Goldbach's conjecture may have a constructive proof (as we do not know at present whether it does), in which case the quoted statement would have a constructive proof as well, albeit one that is unknown at present. The main practical use of weak counterexamples is to identify the "hardness" of a problem. For example, the counterexample just shown shows that the quoted statement is "at least as hard to prove" as Goldbach's conjecture. Weak counterexamples of this sort are often related to the limited principle of omniscience.

References

↑ Dummett, Michael (1977 (first edition), 2000 (second edition)). Elements of Intuitionism. Oxford Science Publications. p. 6. Check date values in: |date= (help)
↑ George, Alexander; Velleman, Daniel J. (2002). Philosophies of mathematics. Blackwell. pp. 3–4. ISBN 0-631-19544-0.
↑ A. S. Troelstra, Principles of Intuitionism, Lecture Notes in Mathematics 95, 1969, p. 102

External links

Weak counterexamples by Mark van Atten, Stanford Encyclopedia of Philosophy

This article is issued from Wikipedia. The text is available under the Creative Commons Attribution/Share Alike; additional terms may apply for the media files.

Constructive proof

Example

Brouwerian counterexamples

See also

References

Further reading

External links