Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

о Гёделе и Изабелле, take 1

Нашлась потерянная было запись о формализации док-ва Гёделя, поэтому кидаю её сюда под элжекат для тех, кому интересно.

subject: формализация V=L и консистенстности аксиомы выбора

(контекст: математика, теория множеств, аксиома выбора)

Немного контекста. В 1940-м году Гёдель доказал, что аксиома выбора (и обобщённая гипотеза континуума вместе с ней) консистентны с остальными аксиомами теории множеств, т.е. что невозможно при помощи остальных аксиом их опровергнуть (при условии, что остальные аксиомы непротиворечивы сами по себе). Это, во-первых, окончательно укрепило статус аксиомы выбора в глазах математиков; во-вторых, результат Гёделя вместе с доказательством Коэна 20 лет спустя (Коэн показал, что эти утверждения из остальных аксиом невозможно доказать) доказывают независимость аксиомы выбора от остальных аксиом -- первое и самое важное нетривиальное доказательство неполноты мощной формальной системы (в данном случае теории множеств без аксиомы выбора), не опирающееся на теоремы Гёделя о неполноте.

(иными словами, из знаменитых теорем Гёделя о неполноте мы знаем, что любая достаточно мощная формальная система -- в том числе теория множеств -- неполна, т.е. существуют утверждения, к-е она не может ни доказать, ни опровергнуть. Но конкретное такое утверждение, формулируемое в процессе док-ва неполноты, независимого математического интереса не представляет. Пример интересного такого утверждения - пятый постулат Евклида, независимый от остальных аксиом геометрии; но аксиомы геометрии намного слабее, чем аксиомы арифметики или теории множеств. Аксиома выбора -- пример такого интересного утверждения, независимого от теории множеств.)

Доказательство Гёделя основывалось на построении специального рода модели теории множеств, под названием конструктивная вселенная (её обычно обозначают буквой L, в отличие от "всей вселенной" вообще, обозначаемой буквой V). В конструктивной вселенной аксиому выбора можно доказать; затем можно показать, что любое док-во противоречия в L влечёт за собой док-во противоречия в обычной теории множеств. Поэтому если бы аксиому выбора можно было опровергнуть при помощи других аксиом, то такое опровержение существовало бы и "внутри" L, и тогда вместе с док-вом аксиомы выбора "внутри" L явило бы собой противоречие, к-е можно было бы вытащить "наружу" в V, и доказать, что остальные аксиомы теории множеств сами по себе противоречивы.


Larry Paulson (Кембридж) недавно закончил формализацию доказательства Гёделя в компьютерной системе Isabelle, существующей для строгой формализации и формальной верификации математических доказательств. Это интересный результат. Формальная верификация математических доказательств -- весьма сложное дело; простой и очевидно истинный для человека-математика шаг в математическом доказательстве может потребовать перевода в сотни и тысячи маленьких формальных шажков для того, чтобы компьютер мог потвердить его формальную строгость и истинность. По этой причине не так уж и много нетривиальных математических теорем (даже в очень слабом для профессионального математика смысле слова "нетривиальный") были формально верифицированы. Вот краткое описание того, что сделал Полсон; а этот файл (>200 страниц, автоматически сгенерированный) содержит нужные формальные определения и доказательства - его любопытно полистать в качестве примера длинного нетривиального формального доказательства.

Я хотел также разобраться в системе Isabelle, но быстро понял, что мне не хватает как адекватного знания лямбда-исчисления (lambda calculus), так и знания языка ML, на котором она написана. Особенно λ-calculus давно уже пора было как следует изучить.
Subscribe
  • Post a new comment

    Error

    default userpic

    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.
  • 8 comments