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

редактировать

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

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

СОДЕРЖАНИЕ
  • 1 Утверждение программы Гильберта
  • 2 теоремы Гёделя о неполноте
  • 3 программа Гильберта после Гёделя
  • 4 См. Также
  • 5 ссылки
  • 6 Внешние ссылки
Утверждение программы Гильберта

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

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

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

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

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

  • Хотя невозможно формализовать всю математику, можно формализовать практически всю математику, которую кто-либо использует. В частности, теория множеств Цермело – Френкеля в сочетании с логикой первого порядка дает удовлетворительный и общепринятый формализм почти для всей современной математики.
  • Хотя невозможно доказать полноту систем, которые могут выражать по крайней мере арифметику Пеано (или, в более общем плане, которые имеют вычислимый набор аксиом), возможно доказать формы полноты для многих других интересных систем. Примером нетривиальной теории, полнота которой доказана, является теория алгебраически замкнутых полей заданной характеристики.
  • На вопрос, существуют ли доказательства финитарной непротиворечивости сильных теорий, трудно ответить, главным образом потому, что нет общепринятого определения «финитарного доказательства». Большинство математиков в теории доказательств, кажется, считают, что конечная математика содержится в арифметике Пеано, и в этом случае невозможно дать конечные доказательства достаточно сильных теорий. С другой стороны, сам Гёдель предположил возможность предоставления доказательств финитарной непротиворечивости с использованием финитарных методов, которые не могут быть формализованы в арифметике Пеано, поэтому он, похоже, имел более либеральное представление о том, какие финитные методы могут быть разрешены. Несколько лет спустя Генцен дал доказательство непротиворечивости арифметики Пеано. Единственная часть этого доказательства, которая не была явно финитной, - это некоторая трансфинитная индукция до порядкового числа ε 0. Если эту трансфинитную индукцию принять как конечный метод, то можно утверждать, что существует конечное доказательство непротиворечивости арифметики Пеано. Более мощные подмножества арифметики второго порядка получили доказательства непротиворечивости Гайси Такеути и другими, и снова можно спорить о том, насколько точны или конструктивны эти доказательства. (Теории, непротиворечивость которых была доказана этими методами, довольно сильны и включают большую часть "обычной" математики.)
  • Хотя в арифметике Пеано нет алгоритма для определения истинности утверждений, существует множество интересных и нетривиальных теорий, для которых такие алгоритмы были найдены. Например, Тарский нашел алгоритм, который может определить истинность любого утверждения в аналитической геометрии (точнее, он доказал, что теория вещественных замкнутых полей разрешима). Учитывая аксиому Кантора – Дедекинда, этот алгоритм можно рассматривать как алгоритм для определения истинности любого утверждения в евклидовой геометрии. Это существенно, поскольку мало кто считает евклидову геометрию тривиальной теорией.
Смотрите также
Рекомендации
  • Г. Генцен, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen 112: 493–565. Переведено как «Непротиворечивость арифметики» в Сборнике статей Герхарда Гентцена, М. Е. Сабо (ред.), 1969.
  • Д. Гильберт. «Die Grundlegung der elementaren Zahlenlehre». Mathematische Annalen 104: 485–94. Переведено У. Эвальдом как «Основание элементарной теории чисел», стр. 266–273 в Mancosu (изд., 1998). От Брауэра до Гильберта: дебаты об основах математики в 1920-е годы, Oxford University Press. Нью-Йорк.
  • С.Г. Симпсон, 1988. Частичные реализации программы Гильберта. Журнал символической логики 53: 349–363.
  • Р. Зак, 2006. Программа Гильберта тогда и сейчас. Философия логики 5: 411–447, arXiv: math / 0508572 [math.LO].
внешняя ссылка
Последняя правка сделана 2024-01-10 02:44:31
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте