In
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, a constructive proof is a method of
proof that demonstrates the existence of a
mathematical object
A mathematical object is an abstract concept arising in mathematics.
In the usual language of mathematics, an ''object'' is anything that has been (or could be) formally defined, and with which one may do deductive reasoning and mathematical p ...
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.
A constructive proof may also refer to the stronger concept of a proof that is valid in
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
.
Constructivism
Constructivism may refer to:
Art and architecture
* Constructivism (art), an early 20th-century artistic movement that extols art as a practice for social purposes
* Constructivist architecture, an architectural movement in Russia in the 1920s a ...
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
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, Exclusive or, either this proposition or its negation is Truth value, true. It is one of the so-called Law of thought#The three tradit ...
, the
axiom of infinity
In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing th ...
, and the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
, and induces a different meaning for some terminology (for example, the term "or" has a stronger meaning in constructive mathematics than in classical).
Some non-constructive proofs show that if a certain proposition is false, a contradiction ensues; consequently the proposition must be true (
proof by contradiction
In logic and mathematics, 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. Proof by contradiction is also known ...
). However, the
principle of explosion
In classical logic, intuitionistic logic and similar logical systems, the principle of explosion (, 'from falsehood, anything ollows; or ), or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a ...
(''ex falso quodlibet'') has been accepted in some varieties of constructive mathematics, including
intuitionism
In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
.
Constructive proofs can be seen as defining certified mathematical
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
s: this idea is explored in the
Brouwer–Heyting–Kolmogorov interpretation In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the rea ...
of
constructive logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
, the
Curry–Howard correspondence between proofs and programs, and such logical systems as
Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer scie ...
's
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and ph ...
, and
Thierry Coquand
Thierry Coquand (; born 18 April 1961 in Jallieu, Isère, France) is a professor in computer science at the University of Gothenburg, known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. u ...
and
Gérard Huet
Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and ...
's
calculus of constructions
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, ...
.
A historical example
Until the end of 19th century, all mathematical proofs were essentially constructive. The first non-constructive constructions appeared with
Georg Cantor
Georg Ferdinand Ludwig Philipp Cantor ( , ; – January 6, 1918) was a German mathematician. He played a pivotal role in the creation of set theory, which has become a fundamental theory in mathematics. Cantor established the importance of ...
’s theory of
infinite set
In set theory, an infinite set is a set that is not a finite set. Infinite sets may be countable or uncountable.
Properties
The set of natural numbers (whose existence is postulated by the axiom of infinity) is infinite. It is the only set th ...
s, and the formal definition of
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every real ...
s.
The first use of non-constructive proofs for solving previously considered problems seems to be
Hilbert's Nullstellensatz
In mathematics, Hilbert's Nullstellensatz (German for "theorem of zeros," or more literally, "zero-locus-theorem") is a theorem that establishes a fundamental relationship between geometry and algebra. This relationship is the basis of algebraic ...
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
polynomial
In mathematics, a polynomial is an expression consisting of indeterminates (also called variables) and coefficients, that involves only the operations of addition, subtraction, multiplication, and positive-integer powers of variables. An exa ...
s in indeterminates with
complex
Complex commonly refers to:
* Complexity, the behaviour of a system whose components interact in multiple ways so possible interactions are difficult to describe
** Complex system, a system composed of many components which may interact with each ...
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
__NOTOC__
Paul Albert Gordan (27 April 1837 – 21 December 1912) was a Jewish-German mathematician, a student of Carl Jacobi at the University of Königsberg before obtaining his PhD at the University of Breslau (1862),. and a professor ...
, wrote: ''"this is not mathematics, it is theology''".
Twenty five years later,
Grete Hermann
Grete Hermann (2 March 1901 – 15 April 1984) was a German mathematician and philosopher noted for her work in mathematics, physics, philosophy and education. She is noted for her early philosophical work on the foundations of quantum mechanics, ...
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
.
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 number
A prime number (or a prime) is a natural number greater than 1 that is not a product of two smaller natural numbers. A natural number greater than 1 that is not prime is called a composite number. For example, 5 is prime because the only ways ...
s.
Euclid
Euclid (; grc-gre, Wikt:Εὐκλείδης, Εὐκλείδης; BC) was an ancient Greek mathematician active as a geometer and logician. Considered the "father of geometry", he is chiefly known for the ''Euclid's Elements, Elements'' trea ...
'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 number
In mathematics, the irrational numbers (from in- prefix assimilated to ir- (negative prefix, privative) + rational) are all the real numbers that are not rational numbers. That is, irrational numbers cannot be expressed as the ratio of two integ ...
s
and
such that
is
rational
Rationality is the quality of being guided by or based on reasons. In this regard, a person acts rationally if they have a good reason for what they do or a belief is rational if it is based on strong evidence. This quality can apply to an abi ...
." 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:
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:
*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
:
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
In logic, the law of excluded middle (or the principle 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 noncontradi ...
, 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.
As it turns out,
is irrational because of the
Gelfond–Schneider theorem
In mathematics, the Gelfond–Schneider theorem establishes the transcendence of a large class of numbers.
History
It was originally proved independently in 1934 by Aleksandr Gelfond and Theodor Schneider.
Statement
: If ''a'' and ''b'' are ...
, but this fact is irrelevant to the correctness of the non-constructive proof.
Constructive proofs
A ''constructive'' proof of the above theorem on irrational powers of irrationals would give an actual example, such as:
:
The
square root of 2
The square root of 2 (approximately 1.4142) is a positive real number that, when multiplied by itself, equals the number 2. It may be written in mathematics as \sqrt or 2^, and is an algebraic number. Technically, it should be called the princip ...
is irrational, and 3 is rational.
is also irrational: if it were equal to
, then, by the properties of
logarithms
In mathematics, the logarithm is the inverse function to exponentiation. That means the logarithm of a number to the base is the exponent to which must be raised, to produce . For example, since , the ''logarithm base'' 10 of ...
, 9
''n'' 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
Graph may refer to:
Mathematics
*Graph (discrete mathematics), a structure made of vertices and edges
**Graph theory, the study of such graphs and their properties
* Graph (topology), a topological space resembling a graph in the sense of discr ...
. A consequence of this theorem is that a
graph
Graph may refer to:
Mathematics
*Graph (discrete mathematics), a structure made of vertices and edges
**Graph theory, the study of such graphs and their properties
*Graph (topology), a topological space resembling a graph in the sense of discre ...
can be drawn on the
torus
In geometry, a torus (plural tori, colloquially donut or doughnut) is a surface of revolution generated by revolving a circle in three-dimensional space about an axis that is coplanar with the circle.
If the axis of revolution does not tou ...
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
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
, a statement may be disproved by giving a
counterexample
A counterexample is any exception to a generalization. In logic a counterexample disproves the generalization, and does so rigorously in the fields of mathematics and philosophy. For example, the fact that "John Smith is not a lazy student" is a ...
, 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, if 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 In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 19 ...
, which shows that the full
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
is non-constructive in systems of
constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a con ...
, since the axiom of choice implies the law of excluded middle in such systems. The field of
constructive reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
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. 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
Goldbach's conjecture is one of the oldest and best-known unsolved problems in number theory and all of mathematics. It states that every even natural number greater than 2 is the sum of two prime numbers.
The conjecture has been shown to hold ...
, 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:
[Mark van Atten, 2015,]
Weak Counterexamples
, Stanford Encyclopedia of Mathematics
:
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
In mathematics, a Cauchy sequence (; ), named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses. More precisely, given any small positive distance, all but a finite numbe ...
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
*
Constructivism (philosophy of mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove t ...
*
Errett Bishop
Errett Albert Bishop (July 14, 1928 – April 14, 1983) was an Americans, American mathematician known for his work on analysis. He expanded constructive analysis in his 1967 ''Foundations of Constructive Analysis'', where he Mathematical proof, p ...
- author of the book "Foundations of Constructive Analysis".
*
*
Non-constructive algorithm existence proofs
*
Probabilistic method
The probabilistic method is a nonconstructive method, primarily used in combinatorics and pioneered by Paul Erdős, for proving the existence of a prescribed kind of mathematical object. It works by showing that if one randomly chooses objects fr ...
References
Further reading
*
J. Franklin and A. Daoud (2011)
Proof in Mathematics: An Introduction'. Kew Books, , ch. 4
*
Hardy, G. H. &
Wright, E. M. (1979) ''An Introduction to the Theory of Numbers'' (Fifth Edition). Oxford University Press.
*
Anne Sjerp Troelstra
Anne Sjerp Troelstra (10 August 1939 – 7 March 2019) was a professor of pure mathematics and foundations of mathematics at the Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam.
He was a constructivist logi ...
and
Dirk van Dalen
Dirk van Dalen (born 20 December 1932, Amsterdam) is a Dutch mathematician and historian of science.
Van Dalen studied mathematics and physics and astronomy at the University of Amsterdam. Inspired by the work of Brouwer and Heyting, he receive ...
(1988) "Constructivism in Mathematics: Volume 1" Elsevier Science.
{{Refend
External links
*
Weak counterexamples' by Mark van Atten, Stanford Encyclopedia of Philosophy
Mathematical proofs
Constructivism (mathematics)