Existence theorem
{{short description|Theorem which asserts the existence of an object}}
In mathematics, an existence theorem is a theorem which asserts the existence of a certain object.{{Cite web|url=https://www.dictionary.com/browse/existence-theorem|title=Definition of existence theorem {{!}} Dictionary.com|website=www.dictionary.com|language=en|access-date=2019-11-29}} 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 (e.g., "for all {{math|x}}, {{math|y}}, ... there exist(s) ..."). In the formal terms of symbolic logic, an existence theorem is a theorem with a prenex normal form involving the existential quantifier, even though in practice, such theorems are usually stated in standard mathematical language. For example, the statement that the sine function is 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, the axiom of choice or the law of excluded middle. 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 leads to mathematics losing its concrete applicability,See the section on nonconstructive proofs of the entry "Constructive proof". while the opposing viewpoint is that abstract methods are far-reaching,{{explain|date=March 2021}} in a way that numerical analysis 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,{{Cite web|url=http://mathworld.wolfram.com/ExistenceTheorem.html|title=Existence Theorem|last=Weisstein|first=Eric W.|website=mathworld.wolfram.com|language=en|access-date=2019-11-29}} since the whole approach may not lend itself to construction.{{cite book|author=Dennis E. Hesseling|title=Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s|url=https://books.google.com/books?id=6CXyBwAAQBAJ&pg=PA376|date=6 December 2012|publisher=Birkhäuser|isbn=978-3-0348-7989-7|page=376}} In terms of algorithms, 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,{{cite book|author1=Isaak Rubinstein|author2=Lev Rubinstein|title=Partial Differential Equations in Classical Mathematical Physics|url=https://books.google.com/books?id=pLjLf0_yvqsC&pg=PA246|date=28 April 1998|publisher=Cambridge University Press|isbn=978-0-521-55846-4|page=246}} which many constructivist mathematicians working in extended logics (such as intuitionistic logic) 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.{{cite book|author=Schaefer, Uwe|title=From Sperner's Lemma to Differential Equations in Banach Spaces : An Introduction to Fixed Point Theorems and their Applications|url=https://books.google.com/books?id=1B2yBQAAQBAJ&pg=PA31|date=3 December 2014|publisher=KIT Scientific Publishing|isbn=978-3-7315-0260-9|page=31}}
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 Bishop's definitions, the continuity of a function such as {{math|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. Accordingly, Bishop rejects the standard idea of pointwise continuity, and proposed that continuity should be defined in terms of "local uniform continuity".{{Cite web|url=https://ncatlab.org/nlab/show/Bishop's+constructive+mathematics|title=Bishop's constructive mathematics in nLab|website=ncatlab.org|access-date=2019-11-29}} One could get another explanation of existence theorem from type theory, in which a proof of an existential statement can come only from a term (which one can see as the computational content).