TheInfoList

OR:

In mathematics, an existence theorem is a
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
which asserts the existence of a certain object. It might be a statement which begins with the phrase " there exist(s)", or it might be a universal statement whose last quantifier is
existential Existentialism ( ) is a form of philosophical inquiry that explores the problem of human existence and centers on human thinking, feeling, and acting. Existentialist thinkers frequently explore issues related to the meaning, purpose, and valu ...
(e.g., "for all , , ... there exist(s) ..."). In the formal terms of symbolic logic, an existence theorem is a theorem with a
prenex normal form A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in prop ...
involving the
existential quantifier In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
, even though in practice, such theorems are usually stated in standard mathematical language. For example, the statement that the sine function is
continuous Continuity or continuous may refer to: Mathematics * Continuity (mathematics), the opposing concept to discreteness; common examples include ** Continuous probability distribution or random variable in probability and statistics ** Continuous ...
everywhere, or any theorem written in big O notation, can be considered as theorems which are existential by nature—since 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 purely theoretic existence theorems, that is, theorems which depend on non-constructive foundational material such as 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 ...
, 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 ...
or 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 ...
. Such theorems provide no indication as to how to construct (or exhibit) the object whose existence is being claimed. From a constructivist viewpoint, such approaches are not viable as it lends to mathematics losing its concrete applicability, while the opposing viewpoint is that abstract methods are far-reaching, in a way that
numerical analysis Numerical analysis is the study of algorithms that use numerical approximation (as opposed to symbolic manipulations) for the problems of mathematical analysis (as distinguished from discrete mathematics). It is the study of numerical methods ...
cannot be.

# 'Pure' existence results

In mathematics, an existence theorem is purely theoretical if the proof given for it does not indicate a construction of the object whose existence is asserted. Such a proof is non-constructive, since the whole approach may not lend itself to construction. In terms of
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
s, purely theoretical existence theorems bypass all algorithms for finding what is asserted to exist. These are to be contrasted with the so-called "constructive" existence theorems, which many constructivist mathematicians working in extended logics (such as
intuitionistic 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 ...
) believe to be intrinsically stronger than their non-constructive counterparts. Despite that, the purely theoretical existence results are nevertheless ubiquitous in contemporary mathematics. For example, John Nash's original proof of the existence of a Nash equilibrium in 1951 was such an existence theorem. An approach which is constructive was also later found in 1962.

# Constructivist ideas

From the other direction, there has been considerable clarification of what
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 ...
is—without the emergence of a 'master theory'. For example, according to
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 ...
's definitions, the continuity of a function such as should be proved as a constructive bound on the
modulus of continuity In mathematical analysis, a modulus of continuity is a function ω : , ∞→ , ∞used to measure quantitatively the uniform continuity of functions. So, a function ''f'' : ''I'' → R admits ω as a modulus of continuity if and only if :, f(x)-f ...
, meaning that the existential content of the assertion of continuity is a promise that can always be kept. Accordingly, Bishop rejects the standard idea of pointwise continuity, and proposed that continuity should be defined in terms of "local uniform continuity". One could get another explanation of existence theorem from
type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
, in which a proof of an existential statement can come only from a ''term'' (which one can see as the computational content).