Constructive proof

Last updated

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. For avoiding confusion with the stronger concept that follows, such a constructive proof is sometimes called an effective proof.

Contents

A constructive proof may also refer to the stronger concept of a proof that is valid in constructive mathematics. 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). [1]

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.

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.

A historical example

Until the end of 19th century, all mathematical proofs were essentially constructive. The first non-constructive constructions appeared with Georg Cantor’s theory of infinite sets, and the formal definition of real numbers.

The first use of non-constructive proofs for solving previously considered problems seems to be Hilbert's Nullstellensatz and Hilbert's basis theorem. From a philosophical point of view, the former is especially interesting, as implying the existence of a well specified object.

The Nullstellensatz may be stated as follows: If are polynomials in n indeterminates with complex coefficients, which have no common complex zeros, then there are polynomials 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. She proved that, if exist, they can be found with degrees less than . [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

Examples

Non-constructive proofs

First consider the theorem that there are an infinitude of prime numbers. Euclid's proof is constructive. 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! + 1 (1 + the product of the first n numbers). Either this number is prime, or all of its prime factors are greater than n. Without establishing a specific prime number, this proves that one exists that is greater than n, contrary to the original postulate.

Now consider the theorem "there exist irrational numbers and such that is rational." This theorem can be proven by using both a constructive proof, and a non-constructive proof.

The following 1953 proof by Dov Jarden has been widely used as an example of a non-constructive proof since at least 1970: [4] [5]

CURIOSA
339.A Simple Proof That a Power of an Irrational Number to an Irrational Exponent May Be Rational.
is either rational or irrational. If it is rational, our statement is proved. If it is irrational, proves our statement.
     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. 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 thembut does not show which onemust yield the desired example.

As it turns out, is irrational because of the Gelfond–Schneider theorem, but this fact is irrelevant to the correctness of the non-constructive proof.

Constructive proofs

A constructive proof of the theorem that a power of an irrational number to an irrational exponent may be rational gives 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. [6] 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. [7] 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 the 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. [8] 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, which asks whether every even natural number larger than 4 is the sum of two primes. Define a sequence a(n) of rational numbers as follows: [9]

For each n, the value of a(n) can be determined by exhaustive search, and so a is a well defined sequence, constructively. 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.

Several facts about the real number α can be proved constructively. However, based on the different meaning of the words in constructive mathematics, if there is a constructive proof that "α = 0 or α 0" 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.

See also

Related Research Articles

In logic, the law of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradiction, and the law of identity. However, no system of logic is built on just these laws, and none of these laws provides inference rules, such as modus ponens or De Morgan's laws.

In the philosophy of mathematics, constructivism asserts that it is necessary to find a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. Such a proof by contradiction might be called non-constructive, and a constructivist might reject it. The constructive viewpoint involves a verificational interpretation of the existential quantifier, which is at odds with its classical interpretation.

In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid.

In mathematics, a transcendental number is a real or complex number that is not algebraic – that is, not the root of a non-zero polynomial of finite degree with rational coefficients. The best-known transcendental numbers are π and e.

The fundamental theorem of algebra, also called d'Alembert's theorem or the d'Alembert–Gauss theorem, states that every non-constant single-variable polynomial with complex coefficients has at least one complex root. This includes polynomials with real coefficients, since every real number is a complex number with its imaginary part equal to zero.

<span class="mw-page-title-main">Mathematical proof</span> Reasoning for mathematical statements

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. A proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm that, for any given Diophantine equation, can decide whether the equation has a solution with all unknowns taking integer values.

In mathematics, Hilbert's Nullstellensatz is a theorem that establishes a fundamental relationship between geometry and algebra. This relationship is the basis of algebraic geometry. It relates algebraic sets to ideals in polynomial rings over algebraically closed fields. This relationship was discovered by David Hilbert, who proved the Nullstellensatz in his second major paper on invariant theory in 1893.

The Riemann hypothesis is one of the most important conjectures in mathematics. It is a statement about the zeros of the Riemann zeta function. Various geometrical and arithmetical objects can be described by so-called global L-functions, which are formally similar to the Riemann zeta-function. One can then ask the same question about the zeros of these L-functions, yielding various generalizations of the Riemann hypothesis. Many mathematicians believe these generalizations of the Riemann hypothesis to be true. The only cases of these conjectures which have been proven occur in the algebraic function field case.

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

<span class="mw-page-title-main">Diophantine approximation</span> Rational-number approximation of a real number

In number theory, the study of Diophantine approximation deals with the approximation of real numbers by rational numbers. It is named after Diophantus of Alexandria.

In mathematics, a quadratic irrational number is an irrational number that is the solution to some quadratic equation with rational coefficients which is irreducible over the rational numbers. Since fractions in the coefficients of a quadratic equation can be cleared by multiplying both sides by their least common denominator, a quadratic irrational is an irrational root of some quadratic equation with integer coefficients. The quadratic irrational numbers, a subset of the complex numbers, are algebraic numbers of degree 2, and can therefore be expressed as

<span class="mw-page-title-main">Square root of 2</span> Unique positive real number which when multiplied by itself gives 2

The square root of 2 (1.4142...) is a positive real number that, when multiplied by itself or squared, equals the number 2. It may be written in mathematics as or . It is an algebraic number, and therefore not a transcendental number. Technically, it should be called the principal square root of 2, to distinguish it from the negative number with the same property.

In mathematics, a proof by infinite descent, also known as Fermat's method of descent, is a particular kind of proof by contradiction used to show that a statement cannot possibly hold for any number, by showing that if the statement were to hold for a number, then the same would be true for a smaller number, leading to an infinite descent and ultimately a contradiction. It is a method which relies on the well-ordering principle, and is often used to show that a given equation, such as a Diophantine equation, has no solutions.

In mathematics, the Gelfond–Schneider theorem establishes the transcendence of a large class of numbers.

The Gelfond–Schneider constant or Hilbert number is two to the power of the square root of two:

In mathematics, a proof of impossibility is a proof that demonstrates that a particular problem cannot be solved as described in the claim, or that a particular set of problems cannot be solved in general. Such a case is also known as a negative proof, proof of an impossibility theorem, or negative result. Proofs of impossibility often are the resolutions to decades or centuries of work attempting to find a solution, eventually proving that there is no solution. Proving that something is impossible is usually much harder than the opposite task, as it is often necessary to develop a proof that works in general, rather than to just show a particular example. Impossibility theorems are usually expressible as negative existential propositions or universal propositions in logic.

In number theory, Vinogradov's theorem is a result which implies that any sufficiently large odd integer can be written as a sum of three prime numbers. It is a weaker form of Goldbach's weak conjecture, which would imply the existence of such a representation for all odd integers greater than five. It is named after Ivan Matveyevich Vinogradov, who proved it in the 1930s. Hardy and Littlewood had shown earlier that this result followed from the generalized Riemann hypothesis, and Vinogradov was able to remove this assumption. The full statement of Vinogradov's theorem gives asymptotic bounds on the number of representations of an odd integer as a sum of three primes. The notion of "sufficiently large" was ill-defined in Vinogradov's original work, but in 2002 it was shown that 101346 is sufficiently large. Additionally numbers up to 1020 had been checked via brute force methods, thus only a finite number of cases to check remained before the odd Goldbach conjecture would be proven or disproven. In 2013, Harald Helfgott proved Goldbach's weak conjecture for all cases.

<span class="mw-page-title-main">Irrational number</span> Number that is not a ratio of integers

In mathematics, the irrational numbers are all the real numbers that are not rational numbers. That is, irrational numbers cannot be expressed as the ratio of two integers. When the ratio of lengths of two line segments is an irrational number, the line segments are also described as being incommensurable, meaning that they share no "measure" in common, that is, there is no length, no matter how short, that could be used to express the lengths of both of the two given segments as integer multiples of itself.

In algebraic number theory, the Grunwald–Wang theorem is a local-global principle stating that—except in some precisely defined cases—an element x in a number field K is an nth power in K if it is an nth power in the completion for all but finitely many primes of K. For example, a rational number is a square of a rational number if it is a square of a p-adic number for almost all primes p. The Grunwald–Wang theorem is an example of a local-global principle.

References

  1. Bridges, Douglas; Palmgren, Erik (2018), "Constructive Mathematics", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Summer 2018 ed.), Metaphysics Research Lab, Stanford University, retrieved 2019-10-25
  2. McLarty, Colin (April 15, 2008). Circles disturbed: the interplay of mathematics and narrative — Chapter 4. Hilbert on Theology and Its Discontents The Origin Myth of Modern Mathematics. Doxiadēs, Apostolos K., 1953-, Mazur, Barry. Princeton: Princeton University Press. doi:10.1515/9781400842681.105. ISBN   9781400842681. OCLC   775873004. S2CID   170826113.
  3. Hermann, Grete (1926). "Die Frage der endlich vielen Schritte in der Theorie der Polynomideale: Unter Benutzung nachgelassener Sätze von K. Hentzelt". Mathematische Annalen (in German). 95 (1): 736–788. doi:10.1007/BF01206635. ISSN   0025-5831. S2CID   115897210.
  4. J. Roger Hindley, "The Root-2 Proof as an Example of Non-constructivity", unpublished paper, September 2014, full text Archived 2014-10-23 at the Wayback Machine
  5. Dov Jarden, "A simple proof that a power of an irrational number to an irrational exponent may be rational", Curiosa No. 339 in Scripta Mathematica 19:229 (1953)
  6. Fellows, Michael R.; Langston, Michael A. (1988-06-01). "Nonconstructive tools for proving polynomial-time decidability" (PDF). Journal of the ACM. 35 (3): 727–739. doi:10.1145/44483.44491. S2CID   16587284.
  7. Mandelkern, Mark (1989). "Brouwerian Counterexamples". Mathematics Magazine. 62 (1): 3–27. doi:10.2307/2689939. ISSN   0025-570X. JSTOR   2689939.
  8. A. S. Troelstra, Principles of Intuitionism , Lecture Notes in Mathematics 95, 1969, p. 102
  9. Mark van Atten, 2015, "Weak Counterexamples", Stanford Encyclopedia of Mathematics

Further reading