Введение
Попытка формализовать всю математику, основанная на конечном наборе аксиом. В математике программа Гильберта, сформулированная немецким математиком Давидом Гильбертом в начале 1920-х годов, представляла собой предложенное решение фундаментального кризиса математики, возникшего, когда ранние попытки прояснить основания математики оказались подвержены парадоксам и противоречиям. В качестве решения Гильберт предложил обосновать все существующие теории на конечном, полном наборе аксиом и предоставить доказательство их непротиворечивости. Гильберт предполагал, что непротиворечивость более сложных систем, таких как математический анализ, можно доказать на основе более простых систем. В конечном итоге, непротиворечивость всей математики могла быть сведена к базовой арифметике. Теоремы о неполноте Гёделя, опубликованные в 1931 году, показали, что программа Гильберта оказалась недостижимой для ключевых областей математики. В своей первой теореме Гёдель показал, что любая непротиворечивая система с вычислимым набором аксиом, способная выражать арифметику, не может быть полной: всегда можно построить утверждение, которое истинно, но не выводится из формальных правил системы. Во второй теореме он показал, что такая система не может доказать собственную непротиворечивость и, следовательно, не может быть использована для доказательства непротиворечивости более сложных систем с уверенностью. Это опровергло предположение Гильберта о том, что финитистская система может быть использована для доказательства собственной непротиворечивости и, следовательно, не может доказать все остальное.
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early 1920s, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic. Gödel's incompleteness theorems, published in 1931, showed that Hilbert's program was unattainable for key areas of mathematics. In his first theorem, Gödel showed that any consistent system with a computable set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger with certainty. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of itself, and therefore could not prove everything else.
Изложение программы Гильберта
Главной целью программы Гильберта было создание надёжных основ для всей математики. В частности, это предполагало:
Формализацию всей математики; иными словами, все математические утверждения должны быть записаны на точном формальном языке и оперироваться в соответствии с чётко определёнными правилами. Полноту: доказательство того, что все истинные математические утверждения могут быть доказаны в рамках этой формальной системы. Состоятельность: доказательство того, что в формальной системе математики нельзя получить противоречие. Это доказательство состоятельности желательно проводить, используя только "финитистские" рассуждения о конечных математических объектах. Сохранение: доказательство того, что любой результат о "реальных объектах", полученный с помощью рассуждений об "идеальных объектах" (таких как несчётные множества), можно доказать без использования идеальных объектов. Решимость: должен существовать алгоритм для определения истинности или ложности любого математического утверждения.
A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules. Completeness: a proof that all true mathematical statements can be proved in the formalism. Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects. Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects. Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.
Теоремы неполноты Гёделя
Курт Гёдель показал, что большинство целей программы Гильберта невозможно достичь, по крайней мере, если их интерпретировать наиболее очевидным образом. Вторая теорема о неполноте Гёделя демонстрирует, что любая непротиворечивая теория, достаточно мощная для кодирования сложения и умножения целых чисел, не может доказать собственную непротиворечивость. Это создает проблему для программы Гильберта:
Невозможно формализовать все истинные математические утверждения в рамках формальной системы, поскольку любая попытка такого формализма неизбежно исключит некоторые истинные математические утверждения. Не существует полного и непротиворечивого расширения даже арифметики Пеано, основанного на рекурсивно перечислимом множестве аксиом. Теория, такая как арифметика Пеано, не может даже доказать собственную непротиворечивость, следовательно, ограниченное "финитистическое" подмножество этой теории тем более не может доказать непротиворечивость более мощных теорий, таких как теория множеств. Не существует алгоритма, позволяющего определить истинность (или доказуемость) утверждений в любом непротиворечивом расширении арифметики Пеано. Строго говоря, отрицательное решение проблемы Entscheidungsproblem было получено спустя несколько лет после теоремы Гёделя, поскольку в то время понятие алгоритма ещё не было определено достаточно точно.
Программа Гильберта после Гёделя
Многие современные направления исследований в математической логике, такие как теория доказательств и обратная математика, можно рассматривать как естественное продолжение оригинальной программы Гильберта. Значительную часть из них можно спасти, слегка изменив цели (Zach 2005), и при следующих модификациях некоторые из них были успешно завершены: хотя формализовать всю математику невозможно, возможно формализовать, по существу, всю математику, которую кто-либо использует. В частности, теория множеств Цермело — Френкеля в сочетании с логикой первого порядка дает удовлетворительный и общепринятый формализм для почти всей современной математики. Хотя невозможно доказать полноту для систем, способных выразить, по крайней мере, арифметику Пеано (или, в более общем случае, обладающих вычислимым набором аксиом), возможно доказать формы полноты для многих других интересных систем. Примером нетривиальной теории, для которой доказана полнота, является теория алгебраически замкнутых полей заданной характеристики. На вопрос о существовании доказательств конечной непротиворечивости сильных теорий ответить трудно, главным образом из-за отсутствия общепринятого определения "конечного доказательства". Большинство математиков, работающих в теории доказательств, похоже, считают, что конечная математика содержится в арифметике Пеано, и в этом случае невозможно предоставить конечные доказательства для достаточно сильных теорий. С другой стороны, сам Гёдель предположил возможность получения доказательств конечной непротиворечивости с использованием конечных методов, которые нельзя формализовать в арифметике Пеано, и, следовательно, придерживался более либерального взгляда на то, какие методы можно считать конечными. Спустя несколько лет Гентцен представил доказательство непротиворечивости арифметики Пеано. Единственной частью этого доказательства, которая не была явно конечной, была определенная трансфинитная индукция до ординала ε0. Если эту трансфинитную индукцию принять как конечный метод, то можно утверждать, что существует конечное доказательство непротиворечивости арифметики Пеано. Более мощные подмножества арифметики второго порядка получили доказательства непротиворечивости от Гайси Такеути и других, и вновь можно спорить о том, насколько точно эти доказательства являются конечными или конструктивными. (Теории, непротиворечивость которых была доказана этими методами, достаточно сильны и включают в себя большую часть "обычной" математики.) Хотя алгоритма для определения истинности утверждений в арифметике Пеано не существует, существует множество интересных и нетривиальных теорий, для которых такие алгоритмы были найдены. Например, Тарский обнаружил алгоритм, способный определять истинность любого утверждения в аналитической геометрии (точнее, он доказал, что теория вещественно замкнутых полей является разрешимой). Учитывая аксиому Кантора — Дедекинда, этот алгоритм можно рассматривать как алгоритм для определения истинности любого утверждения в евклидовой геометрии. Это существенно, поскольку мало кто считает евклидову геометрию тривиальной теорией.
Although it is not possible to formalize all mathematics, it is possible to formalize essentially all the mathematics that anyone uses. In particular Zermelo–Fraenkel set theory, combined with first order logic, gives a satisfactory and generally accepted formalism for almost all current mathematics. Although it is not possible to prove completeness for systems that can express at least the Peano arithmetic (or, more generally, that have a computable set of axioms), it is possible to prove forms of completeness for many other interesting systems. An example of a non trivial theory for which completeness has been proved is the theory of algebraically closed fields of given characteristic. The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand, Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, Gentzen gave a consistency proof for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite induction up to the ordinal ε0. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of second order arithmetic have been given consistency proofs by Gaisi Takeuti and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.) Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non trivial theories for which such algorithms have been found. For example, Tarski found an algorithm that can decide the truth of any statement in analytic geometry (more precisely, he proved that the theory of real closed fields is decidable). Given the Cantor–Dedekind axiom, this algorithm can be regarded as an algorithm to decide the truth of any statement in Euclidean geometry. This is substantial as few people would consider Euclidean geometry a trivial theory.