Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Основания математики II: Золотая Мечта Гильберта

В предыдущем посте мы разобрались с тем, что такое доказательства и как их объективным образом проверять. Выяснилось, что это очень просто. Я рекомендую вначале прочитать его.
http://akuklev.livejournal.com/604920.html

Теперь поговорим о золотой мечте Гильберта. Давиду Гильберту хотелось вначале взять и переложить все основы математики на тот солидный фундамент, который я выше описал. Избавиться от несовершенного человеческого языка, больного многозначностями и недосказанностями, и перейти к использованию формального, а затем записать доказательства всех теорем так, чтобы их можно было механически проверить. И это было to great extent действительно сделано двумя независимыми группами — трёхтомником Principia Mathematica Уайтхеда и Рассела (1910-1913гг) и многотомником Николя Бурбаки (псевдоним группы французских математиков, 1930ые).

К сожалению, и то и другое было написано до открытия соответствия Карри-Говарда, появления читабельных формальных языков и компьютеров, поэтому читать эти книжки практически невозможно. Но тем не менее, свои задачи они выполнили — поставили математику на солидную основу. Посмотреть на тысячи формализованных и компьютерно проверенных доказательств в их современном виде можно вот тут: http://au.metamath.org/index.html

Второй пункт программы Гильберта состоял в том, чтобы доказать полноту и непротиворечивость основ математики, из которых растёт всё остальное — теории множеств и арифметики.

С первым Гильберта ждал крупный облом. Полнота теории — это когда мы можем любое высказывание в рамках теории доказать или опровергнуть. Гильберт сам бы мог догадаться, что полных теорий не бывает.
Помните парадокс Лжеца? Там человек говорит «я сейчас лгу». Если он говорит правду, значит он лжет. Если лжет — значит говорит правду. Короче, это высказывание — вовсе не высказывание, оно не может быть ни истинно, ни ложно. Подобное высказывание можно сформулировать в рамках любой теории, и звучит оно «это высказывание невозможно доказать». Если его возможно доказать, значит оно ложное, если невозможно — истинное. Итого:
Всякая теория, способная к рефлексии (т.е. такая, что высказывание «это высказывание невозможно доказать» можно написать её языком) неполна. И в принципе нету в этом ничего страшного или удивительного. Нельзя зафиксировать конечным количеством аксиом ответы на все-все вопросы.
* Это, кстати, называется, первой теоремой Гёделя о неполноте.

Но есть ещё второй пункт. Там, где про непротиворечивость основ математики. Но как доказывать непротиворечивость, из чего исходить? Не можем же мы исходить из самих основ. Мы ещё не знаем, что они непротиворечивые. Гильберт предложил исходить из теории, содержащей очень-очень-очень простой набор аксиом, самый простой из возможных — чтобы каждый поверил, что уж тут точно не может быть противоречия. И в рамках этой теории нужно доказать две вещи:
1) Что она сама непротиворечива.
2) Что непротиворечива теория множеств и арифметика.

Народ ещё не успел заняться этим делом вплотную, как Гёдель доказал свою вторую теорему о неполноте. И её содержание было ужасно:
«В рамках теории, содержащей арифметику, нельзя доказать её собственную непротиворечивость»

Доказательство непротиворечивости теории её же методами просто было бы бесконечно длинным, а это уже не доказательство, а фигня какая-то.

После этой теоремы семь десятилетий считалось, что это Гильбертовский подход обречён, что нас всегда будет преследовать арифметическая иерархия и доказать непротиворечивость как-то нормально не получится. Оказалось, ничего подобного. В 2001 году Дан Виллард обнаружил, что можно придумать теорию, которая рефлексивна in appropriate sense, но не содержит арифметики. В рамках этой самой системы удалось доказать оба высказывания:
- и то, что эта система сама непротиворечива,
- и то, что непротиворечива теория множеств.*

http://en.wikipedia.org/wiki/Self-verifying_theories

Вот так разрешилась великая проблема математики, и золотая мечта Гильберта сияет над нашими головами. Только один мелкий облом омрачают триумф логики — не существует автоматического способа определить истинность высказывания автоматически, и он никогда не будет найден. В поиске доказательств мы можем полагаться только на творческие способности человеческого ума.

Следующая серия: http://akuklev.livejournal.com/605330.html
_____
* — тут есть тонкость, описываемая в следующей серии. На самом деле доказывается непротиворечивость арифметики Пеано на определимых внутри неё объектах. Это доказывает непротиворечивость NBG-теории множеств в рамках её constructable universe.
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments