Existence theorem
Encyclopedia
In mathematics
, an existence theorem is a theorem with a statement beginning 'there exist(s) ..', or more generally 'for all x, y, ... there exist(s) ...'. That is, in more formal terms of symbolic logic
, it is a theorem with a statement involving the existential quantifier. Many such theorems will not do so explicitly, as usually stated in standard mathematical language. For example, the statement that the sine
function is continuous
; or any theorem written in big O notation
. The quantification can be found in the definitions of the concepts used.
A controversy that goes back to the early twentieth century concerns the issue of pure existence theorems. Such theorems may depend on non-constructive foundational material such as the axiom of infinity, the axiom of choice, or the law of excluded middle. From a constructivist
viewpoint, by admitting them mathematics loses its concrete applicability (see nonconstructive proof
). The opposing viewpoint is that abstract methods are far-reaching, in a way that numerical analysis
cannot be.
From a more rigorous point of view, this is a problematic concept. This is because it is a tag applied to a theorem, but qualifying its proof; hence, pure is here defined in a way which violates the standard proof irrelevance of mathematical theorems. That is, theorems are statements for which the fact is that a proof exists, without any 'label' depending on the proof: they may be applied without knowledge of the proof, and indeed if that's not the case the statement is faulty. Thus, many constructivist mathematicians work in extended logics (such as intuitionistic logic
) where pure existence statements are intrinsically weaker than their constructivist counterparts.
Such pure existence results are in any case ubiquitous in contemporary mathematics. For example, for a linear problem the set of solutions will be a vector space
, and some a priori calculation of its dimension may be possible. In any case where the dimension is probably at least 1, an existence assertion has been made (that a non-zero solution exists.)
Theoretically, a proof could also proceed by way of a metatheorem
, stating that a proof of the original theorem exists (for example, that a proof by exhaustion
search for a proof would always succeed). Such theorems are relatively unproblematic when all of the proofs involved are constructive; however, the status of "pure existence metatheorems" is extremely unclear,
's definitions, the continuity of a function (such as sin x) should be proved as a constructive bound on the modulus of continuity
, meaning that the existential content of the assertion of continuity is a promise that can always be kept. One could get another explanation from type theory
, in which a proof of an existential statement can come only from a term (which we can see as the computational content).
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, an existence theorem is a theorem with a statement beginning 'there exist(s) ..', or more generally 'for all x, y, ... there exist(s) ...'. That is, in more formal terms of symbolic logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
, it is a theorem with a statement involving the existential quantifier. Many such theorems will not do so explicitly, as usually stated in standard mathematical language. For example, the statement that the sine
Sine
In mathematics, the sine function is a function of an angle. In a right triangle, sine gives the ratio of the length of the side opposite to an angle to the length of the hypotenuse.Sine is usually listed first amongst the trigonometric functions....
function is continuous
Continuous function
In mathematics, a continuous function is a function for which, intuitively, "small" changes in the input result in "small" changes in the output. Otherwise, a function is said to be "discontinuous". A continuous function with a continuous inverse function is called "bicontinuous".Continuity of...
; or any theorem written in big O notation
Big O notation
In mathematics, big O notation is used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, usually in terms of simpler functions. It is a member of a larger family of notations that is called Landau notation, Bachmann-Landau notation, or...
. The quantification can be found in the definitions of the concepts used.
A controversy that goes back to the early twentieth century concerns the issue of pure existence theorems. Such theorems may depend on non-constructive foundational material such as the axiom of infinity, the axiom of choice, or the law of excluded middle. From a constructivist
Constructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
viewpoint, by admitting them mathematics loses its concrete applicability (see nonconstructive proof
Constructive proof
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...
). The opposing viewpoint is that abstract methods are far-reaching, in a way that numerical analysis
Numerical analysis
Numerical analysis is the study of algorithms that use numerical approximation for the problems of mathematical analysis ....
cannot be.
'Pure' existence results
An existence theorem may be called pure if the proof given of it doesn't also indicate a construction of whatever kind of object the existence of which is asserted.From a more rigorous point of view, this is a problematic concept. This is because it is a tag applied to a theorem, but qualifying its proof; hence, pure is here defined in a way which violates the standard proof irrelevance of mathematical theorems. That is, theorems are statements for which the fact is that a proof exists, without any 'label' depending on the proof: they may be applied without knowledge of the proof, and indeed if that's not the case the statement is faulty. Thus, many constructivist mathematicians work in extended logics (such as intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
) where pure existence statements are intrinsically weaker than their constructivist counterparts.
Such pure existence results are in any case ubiquitous in contemporary mathematics. For example, for a linear problem the set of solutions will be a vector space
Vector space
A vector space is a mathematical structure formed by a collection of vectors: objects that may be added together and multiplied by numbers, called scalars in this context. Scalars are often taken to be real numbers, but one may also consider vector spaces with scalar multiplication by complex...
, and some a priori calculation of its dimension may be possible. In any case where the dimension is probably at least 1, an existence assertion has been made (that a non-zero solution exists.)
Theoretically, a proof could also proceed by way of a metatheorem
Metatheorem
In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory but not the object theory.- Discussion :A formal...
, stating that a proof of the original theorem exists (for example, that a proof by exhaustion
Proof by exhaustion
Proof by exhaustion, also known as proof by cases, perfect induction, or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases and each case is checked to see if the proposition in question holds...
search for a proof would always succeed). Such theorems are relatively unproblematic when all of the proofs involved are constructive; however, the status of "pure existence metatheorems" is extremely unclear,
Constructivist ideas
From the other direction there has been considerable clarification of what constructive mathematics is; without the emergence of a 'master theory'. For example according to Errett BishopErrett Bishop
Errett Albert Bishop was an American mathematician known for his work on analysis. He is the father of constructive analysis, because of his 1967 Foundations of Constructive Analysis, where he proved most of the important theorems in real analysis by constructive methods.-Life:Errett Bishop's...
's definitions, the continuity of a function (such as sin x) should be proved as a constructive bound on the modulus of continuity
Modulus of continuity
In mathematical analysis, a modulus of continuity is a function\omega:[0,\infty]\to[0,\infty]used to measure quantitatively the uniform continuity of functions. So, a function f:I\to\R admits \omega as a modulus of continuity if and only if|f-f|\leq\omega,for all x and y in the domain of f...
, meaning that the existential content of the assertion of continuity is a promise that can always be kept. One could get another explanation from type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, in which a proof of an existential statement can come only from a term (which we can see as the computational content).