Попытка формализовать всю математику на основе конечного набора аксиом.
В математике программа Гильберта , сформулированная немецким математиком Давидом Гильбертом в начале 1920-х годов, [1] была предложенным решением фундаментального кризиса математики , когда было обнаружено, что ранние попытки прояснить основы математики страдают от парадоксов и несоответствий. В качестве решения Гильберт предложил обосновать все существующие теории конечным полным набором аксиом и предоставить доказательство того, что эти аксиомы непротиворечивы . Гильберт предположил, что непротиворечивость более сложных систем, таких как реальный анализ , можно доказать на основе более простых систем. В конечном счете, последовательность всей математики можно свести к элементарной арифметике .
Теоремы Гёделя о неполноте , опубликованные в 1931 году, показали, что программа Гильберта недостижима для ключевых областей математики. В своей первой теореме Гёдель показал, что любая непротиворечивая система с вычислимым набором аксиом, способная выражать арифметику, никогда не может быть полной: можно построить утверждение, истинность которого можно доказать, но которое нельзя вывести из формальные правила системы. В своей второй теореме он показал, что такая система не может доказать свою собственную непротиворечивость, поэтому ее определенно нельзя использовать для достоверного доказательства непротиворечивости чего-либо более сильного. Это опровергло предположение Гильберта о том, что финитистская система может быть использована для доказательства непротиворечивости самой себя и, следовательно, не может доказать все остальное.
Формулировка программы Гильберта
Основная цель программы Гильберта заключалась в обеспечении надежных основ всей математики. В частности, это должно включать:
- Формулировка всей математики; другими словами, все математические утверждения должны быть написаны на точном формальном языке и обрабатываться в соответствии с четко определенными правилами.
- Полнота: доказательство того, что все истинные математические утверждения могут быть доказаны с помощью формализма.
- Непротиворечивость: доказательство того, что в математическом формализме не может быть получено никакого противоречия. Это доказательство непротиворечивости предпочтительно должно использовать только «финитистские» рассуждения о конечных математических объектах.
- Сохранение: доказательство того, что любой результат о «реальных объектах», полученный с помощью рассуждений об «идеальных объектах» (таких как несчетные множества), может быть доказан без использования идеальных объектов.
- Разрешимость: должен существовать алгоритм определения истинности или ложности любого математического утверждения.
Теоремы Гёделя о неполноте
Курт Гёдель показал, что большинство целей программы Гильберта невозможно достичь, по крайней мере, если интерпретировать их самым очевидным образом. Вторая теорема Гёделя о неполноте показывает, что любая непротиворечивая теория, достаточно мощная для кодирования сложения и умножения целых чисел, не может доказать свою собственную непротиворечивость. Это представляет собой проблему для программы Гильберта:
- Невозможно формализовать все математические истинные утверждения в рамках формальной системы, поскольку любая попытка такого формализма будет упускать некоторые истинные математические утверждения. Не существует полного и последовательного расширения даже арифметики Пеано, основанного на рекурсивно перечислимом наборе аксиом.
- Такая теория, как арифметика Пеано, не может доказать даже свою собственную непротиворечивость, поэтому ее ограниченное «финитистское» подмножество определенно не может доказать непротиворечивость более мощных теорий, таких как теория множеств.
- Не существует алгоритма для определения истинности (или доказуемости) утверждений в любом последовательном расширении арифметики Пеано. Строго говоря, это отрицательное решение проблемы Entscheidungs появилось через несколько лет после теоремы Гёделя, поскольку в то время понятие алгоритма не было точно определено.
Программа Гильберта после Гёделя
Многие современные направления исследований в области математической логики , такие как теория доказательств и обратная математика , можно рассматривать как естественное продолжение исходной программы Гильберта. Большую часть проекта можно спасти, слегка изменив его цели (Зак, 2005), и с помощью следующих модификаций некоторые из них были успешно завершены:
- Хотя невозможно формализовать всю математику, можно формализовать практически всю математику, которой кто-либо пользуется. В частности, теория множеств Цермело-Френкеля в сочетании с логикой первого порядка дает удовлетворительный и общепринятый формализм почти для всей современной математики.
- Хотя невозможно доказать полноту систем, которые могут выражать хотя бы арифметику Пеано (или, в более общем смысле, которые имеют вычислимый набор аксиом), можно доказать формы полноты для многих других интересных систем. Примером нетривиальной теории, для которой доказана полнота , является теория алгебраически замкнутых полей заданной характеристики .
- На вопрос о том, существуют ли финитарные доказательства непротиворечивости сильных теорий, ответить трудно, главным образом потому, что не существует общепринятого определения «финитарного доказательства». Большинство математиков, занимающихся теорией доказательств, похоже, считают, что финитная математика содержится в арифметике Пеано, и в этом случае невозможно дать финитарные доказательства достаточно сильных теорий. С другой стороны, сам Гёдель предлагал возможность предоставления доказательств финитной непротиворечивости с использованием финитарных методов, которые не могут быть формализованы в арифметике Пеано, поэтому он, похоже, имел более либеральный взгляд на то, какие финитарные методы могут быть разрешены. Несколько лет спустя Генцен дал доказательство непротиворечивости арифметики Пеано. Единственной частью этого доказательства, которая не была явно финитной, была некоторая трансфинитная индукция до порядкового ε 0 . Если эту трансфинитную индукцию принять как финитный метод, то можно утверждать, что существует финитное доказательство непротиворечивости арифметики Пеано. Гаиси Такеути и другие предоставили доказательства непротиворечивости более мощным подмножествам арифметики второго порядка , и снова можно спорить о том, насколько финитными или конструктивными являются эти доказательства. (Теории, непротиворечивость которых доказана этими методами, довольно сильны и включают большую часть «обычной» математики.)
- Хотя в арифметике Пеано не существует алгоритма определения истинности утверждений, существует множество интересных и нетривиальных теорий, для которых такие алгоритмы были найдены. Например, Тарский нашел алгоритм, который может определить истинность любого утверждения аналитической геометрии (точнее, он доказал, что теория действительных замкнутых полей разрешима). Учитывая аксиому Кантора-Дедекинда , этот алгоритм можно рассматривать как алгоритм определения истинности любого утверждения в евклидовой геометрии . Это существенно, поскольку мало кто считает евклидову геометрию тривиальной теорией.
Смотрите также
Рекомендации
- ^ Зак, Ричард (2023), Залта, Эдвард Н.; Нодельман, Ури (ред.), «Программа Гильберта», Стэнфордская энциклопедия философии (изд. весной 2023 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 5 июля 2023 г.
- Г. Генцен, 1936/1969 г.р. Die Widerspruchfreiheit der Reinen Zahlentheorie. Математические Анналы 112: 493–565. Переведено как «Непротиворечивость арифметики» в Сборнике статей Герхарда Генцена , М. Е. Сабо (редактор), 1969.
- Д. Гильберт. «Die Grundlegung der elementaren Zahlenlehre». Математические Аннален 104: 485–94. Переведено В. Эвальдом как «Обоснование элементарной теории чисел», стр. 266–273 в Манкосу (изд., 1998). От Брауэра до Гильберта: дебаты об основах математики в 1920-х годах , Oxford University Press. Нью-Йорк.
- С.Г. Симпсон, 1988. Частичные реализации программы Гильберта (pdf). Журнал символической логики 53:349–363.
- Р. Зак , 2006. Программа Гильберта тогда и сейчас. Философия логики 5:411–447, arXiv:math/0508572 [math.LO].
Внешние ссылки
