Программа Гильберта

В математике программа Гильберта , сформулированная немецким математиком Давидом Гильбертом в начале 1920-х годов, ^[1] была предложенным решением фундаментального кризиса математики , когда было обнаружено, что ранние попытки прояснить основы математики страдают от парадоксов и противоречий. В качестве решения Гильберт предложил обосновать все существующие теории конечным полным набором аксиом и предоставить доказательство того, что эти аксиомы непротиворечивы . Гильберт предположил, что непротиворечивость более сложных систем, таких как вещественный анализ , может быть доказана в терминах более простых систем. В конечном итоге непротиворечивость всей математики может быть сведена к базовой арифметике .

Теоремы Гёделя о неполноте , опубликованные в 1931 году, показали, что программа Гильберта была недостижима для ключевых областей математики. В своей первой теореме Гёдель показал, что любая непротиворечивая система с вычислимым набором аксиом, которая способна выражать арифметику, никогда не может быть полной: можно построить утверждение, истинность которого можно показать, но которое нельзя вывести из формальных правил системы. Во второй теореме он показал, что такая система не может доказать свою собственную непротиворечивость, поэтому ее определенно нельзя использовать для доказательства непротиворечивости чего-либо более сильного с уверенностью. Это опровергло предположение Гильберта о том, что финитная система может быть использована для доказательства непротиворечивости самой себя, и, следовательно, не может доказать все остальное.

Изложение программы Гильберта

Главной целью программы Гильберта было обеспечить надежные основы для всей математики. В частности, это должно включать:

Формулировка всей математики; другими словами, все математические утверждения должны быть записаны на точном формальном языке и обрабатываться в соответствии с четко определенными правилами.
Полнота: доказательство того, что все истинные математические утверждения могут быть доказаны в рамках формализма.
Согласованность: доказательство того, что в формализме математики не может быть получено противоречие. Это доказательство согласованности должно предпочтительно использовать только «финитистские» рассуждения о конечных математических объектах.
Сохранение: доказательство того, что любой результат о «реальных объектах», полученный с помощью рассуждений об «идеальных объектах» (таких как несчетные множества), может быть доказан без использования идеальных объектов.
Разрешимость : должен существовать алгоритм для определения истинности или ложности любого математического утверждения.

Теоремы Гёделя о неполноте

Курт Гёдель показал, что большинство целей программы Гильберта было невозможно достичь, по крайней мере, если интерпретировать их наиболее очевидным образом. Вторая теорема Гёделя о неполноте показывает, что любая последовательная теория, достаточно мощная для кодирования сложения и умножения целых чисел, не может доказать свою собственную последовательность. Это представляет собой вызов программе Гильберта:

Невозможно формализовать все математические истинные утверждения в рамках формальной системы, поскольку любая попытка такого формализма упустит некоторые истинные математические утверждения. Не существует полного, последовательного расширения даже арифметики Пеано, основанного на вычислимо перечислимом наборе аксиом.
Такая теория, как арифметика Пеано, не может доказать даже свою собственную непротиворечивость, поэтому ее ограниченное «финитистское» подмножество, безусловно, не может доказать непротиворечивость более мощных теорий, таких как теория множеств.
Не существует алгоритма для определения истинности (или доказуемости) утверждений в любом последовательном расширении арифметики Пеано. Строго говоря, это отрицательное решение Entscheidungsproblem появилось через несколько лет после теоремы Гёделя, поскольку в то время понятие алгоритма не было точно определено.

Программа Гильберта по Гёделю

Многие текущие направления исследований в математической логике , такие как теория доказательств и обратная математика , можно рассматривать как естественные продолжения исходной программы Гильберта. Многое из этого можно спасти, слегка изменив цели (Zach 2005), и со следующими изменениями некоторые из них были успешно завершены:

Хотя невозможно формализовать всю математику, возможно формализовать по существу всю математику, которую кто-либо использует. В частности, теория множеств Цермело–Френкеля в сочетании с логикой первого порядка дает удовлетворительный и общепринятый формализм почти для всей современной математики.
Хотя невозможно доказать полноту для систем, которые могут выражать по крайней мере арифметику Пеано (или, в более общем смысле, которые имеют вычислимый набор аксиом), можно доказать формы полноты для многих других интересных систем. Примером нетривиальной теории, для которой была доказана полнота , является теория алгебраически замкнутых полей заданной характеристики .
На вопрос о том, существуют ли доказательства финитной непротиворечивости сильных теорий, ответить сложно, в основном потому, что не существует общепринятого определения «финитного доказательства». Большинство математиков в теории доказательств, по-видимому, считают, что финитная математика содержится в арифметике Пеано, и в этом случае невозможно дать финитные доказательства достаточно сильных теорий. С другой стороны, сам Гёдель предположил возможность дать доказательства финитной непротиворечивости с использованием финитных методов, которые не могут быть формализованы в арифметике Пеано, поэтому он, по-видимому, имел более либеральный взгляд на то, какие финитные методы могут быть разрешены. Несколько лет спустя Генцен дал доказательство непротиворечивости для арифметики Пеано. Единственной частью этого доказательства, которая не была явно финитной, была определенная трансфинитная индукция до ординала ε 0 . Если эта трансфинитная индукция принимается как финитный метод, то можно утверждать, что существует финитное доказательство непротиворечивости арифметики Пеано. Более мощные подмножества арифметики второго порядка получили доказательства непротиворечивости от Гаиси Такеути и других, и снова можно спорить о том, насколько точны или конструктивны эти доказательства. (Теории, непротиворечивость которых была доказана этими методами, довольно сильны и включают в себя большую часть «обычной» математики.)
Хотя в арифметике Пеано нет алгоритма для определения истинности утверждений, существует много интересных и нетривиальных теорий, для которых такие алгоритмы были найдены. Например, Тарский нашел алгоритм, который может определить истинность любого утверждения в аналитической геометрии (точнее, он доказал, что теория вещественных замкнутых полей разрешима). Учитывая аксиому Кантора–Дедекинда , этот алгоритм можно рассматривать как алгоритм для определения истинности любого утверждения в евклидовой геометрии . Это существенно, поскольку мало кто посчитает евклидову геометрию тривиальной теорией.

Смотрите также

Ссылки

^ Зак, Ричард (2023), Залта, Эдвард Н.; Нодельман, Ури (ред.), «Программа Гильберта», Стэнфордская энциклопедия философии (весеннее издание 2023 г.), Исследовательская лаборатория метафизики, Стэнфордский университет , дата обращения 05.07.2023

Г. Генцен, 1936/1969 г.р. Die Widerspruchfreiheit der Reinen Zahlentheorie. Математические Анналы 112: 493–565. Переведено как «Непротиворечивость арифметики» в Сборнике статей Герхарда Генцена , М. Е. Сабо (редактор), 1969.
D. Hilbert. «Die Grundlegung der elementaren Zahlenlehre». Mathematische Annalen 104:485–94. Перевод В. Эвальда как «The Grounding of Elementary Number Theory», стр. 266–273 в Mancosu (ред., 1998) От Брауэра до Гильберта: дебаты об основаниях математики в 1920-х годах , Oxford University Press. Нью-Йорк.
SG Simpson , 1988. Частичные реализации программы Гильберта (pdf). Журнал символической логики 53:349–363.
Р. Зак , 2006. Программа Гильберта тогда и сейчас. Философия логики 5:411–447, arXiv:math/0508572 [math.LO].

Внешние ссылки

Ричард Зак. «Программа Гильберта». В Zalta, Edward N. (ред.). Стэнфордская энциклопедия философии .