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.
Constructivism is a mathematical philosophy that rejects all proof methods that involve the existence of objects that are not explicitly built.
This excludes, in particular, the use of the law of the excluded middle, the axiom of infinity, and the axiom of choice, and induces a different meaning for some terminology (for example, the term "or" has a stronger meaning in constructive mathematics than in classical).
However, the principle of explosion (ex falso quodlibet) has been accepted in some varieties of constructive mathematics, including intuitionism.
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.
The first non-constructive constructions appeared with Georg Cantor’s theory of infinite sets, and the formal definition of real numbers.
From a philosophical point of view, the former is especially interesting, as implying the existence of a well specified object.
such that Such a non-constructive existence theorem was such a surprise for mathematicians of that time that one of them, Paul Gordan, wrote: "this is not mathematics, it is theology".
[2] Twenty five years later, Grete Hermann provided an algorithm for computing
which is not a constructive proof in the strong sense, as she used Hilbert's result.
[3] This provides an algorithm, as the problem is reduced to solving a system of linear equations, by considering as unknowns the finite number of coefficients of the
But a common way of simplifying Euclid's proof postulates that, contrary to the assertion in the theorem, there are only a finite number of them, in which case there is a largest one, denoted n. Then consider the number n!
Dov Jarden Jerusalem In a bit more detail: At its core, 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.
is irrational because of the Gelfond–Schneider theorem, but this fact is irrelevant to the correctness of the non-constructive proof.
However, the proof of the existence of this finite set is not constructive, and the forbidden minors are not actually specified.
However, it is also possible to give a Brouwerian counterexample to show that the statement is non-constructive.
[7] This sort of counterexample shows that the statement implies some principle that is known to be non-constructive.
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.
One weak counterexample begins by taking some unsolved problem of mathematics, such as Goldbach's conjecture, which asks whether every even natural number larger than 4 is the sum of two primes.
Moreover, because a is a Cauchy sequence with a fixed rate of convergence, a converges to some real number α, according to the usual treatment of real numbers in constructive mathematics.
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.