Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Теорема, утверждающая существование объекта
Theorem which asserts the existence of an object
В математике теорема о существовании – это теорема, утверждающая существование некоторого объекта. Это может быть утверждение, начинающееся с фразы "существует", или универсальное утверждение, последний квантор которого является экзистенциальным (например, "для всех x, y, существует"). В формальных терминах символической логики, теорема о существовании – это теорема в пренексной нормальной форме, включающая экзистенциальный квантор, хотя на практике такие теоремы обычно формулируются на стандартном математическом языке. Например, утверждение о том, что функция синуса непрерывна везде, или любая теорема, записанная в нотации «большого О», можно рассматривать как теоремы, экзистенциальные по своей природе, поскольку квантификация содержится в определениях используемых понятий. Споры, восходящие к началу двадцатого века, касаются вопроса чисто теоретических теорем о существовании, то есть теорем, зависящих от неконструктивных основ, таких как аксиома бесконечности, аксиома выбора или закон исключённого третьего. Такие теоремы не предоставляют информации о том, как построить (или указать) объект, существование которого утверждается. С конструктивистской точки зрения, такие подходы нецелесообразны, поскольку приводят к потере математикой её конкретной применимости, в то время как противоположная точка зрения состоит в том, что абстрактные методы имеют далеко идущие последствия, в отличие от численного анализа.
In mathematics, an existence theorem is a theorem 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 (e. g., "for all x, 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 lends to mathematics losing its concrete applicability, while the opposing viewpoint is that abstract methods are far reaching, in a way that numerical analysis cannot be.
"Чистые" результаты существования
В математике теорема о существовании считается чисто теоретической, если приведённое для неё доказательство не указывает способ построения объекта, существование которого утверждается. Такое доказательство является неконструктивным, поскольку весь подход может оказаться непригодным для построения. С точки зрения алгоритмов, чисто теоретические теоремы о существовании обходят все алгоритмы для нахождения того, существование чего утверждается. Они противопоставляются так называемым "конструктивным" теоремам о существовании, которые многие конструктивистские математики, работающие в расширенных логиках (таких как интуиционистская логика), считают принципиально более сильными, чем их неконструктивные аналоги. Несмотря на это, чисто теоретические результаты о существовании всё же широко распространены в современной математике. Например, первоначальное доказательство Джоном Нэшем существования равновесия Нэша в 1951 году являлось такой теоремой о существовании. Конструктивный подход был найден позднее, в 1962 году.
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 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, 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.
Конструктивистские идеи
С другой стороны, произошло значительное прояснение того, что такое конструктивная математика, – без возникновения какой-либо "всеобъемлющей теории". Например, согласно определениям Эрретта Бишопа, непрерывность функции, такой как sin(x), должна быть доказана как конструктивная оценка модуля непрерывности, что означает, что экзистенциальное содержание утверждения о непрерывности представляет собой обещание, которое всегда можно выполнить. Соответственно, Бишоп отвергает стандартное представление о точечной непрерывности и предложил определять непрерывность в терминах "локальной равномерной непрерывности". Другое объяснение теорем о существовании можно получить из теории типов, где доказательство экзистенциального утверждения может исходить только из терма (который можно рассматривать как вычислимое содержание).
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 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". 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).