о Гёделе и Изабелле, take 1
Sep. 2nd, 2002 12:46 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaНашлась потерянная было запись о формализации док-ва Гёделя, поэтому кидаю её сюда под элжекат для тех, кому интересно.
subject: формализация V=L и консистенстности аксиомы выбора
(контекст: математика, теория множеств, аксиома выбора)
Немного контекста. В 1940-м году Гёдель доказал, что аксиома выбора (и обобщённая гипотеза континуума вместе с ней) консистентны с остальными аксиомами теории множеств, т.е. что невозможно при помощи остальных аксиом их опровергнуть (при условии, что остальные аксиомы непротиворечивы сами по себе). Это, во-первых, окончательно укрепило статус аксиомы выбора в глазах математиков; во-вторых, результат Гёделя вместе с доказательством Коэна 20 лет спустя (Коэн показал, что эти утверждения из остальных аксиом невозможно доказать) доказывают независимость аксиомы выбора от остальных аксиом -- первое и самое важное нетривиальное доказательство неполноты мощной формальной системы (в данном случае теории множеств без аксиомы выбора), не опирающееся на теоремы Гёделя о неполноте.
(иными словами, из знаменитых теорем Гёделя о неполноте мы знаем, что любая достаточно мощная формальная система -- в том числе теория множеств -- неполна, т.е. существуют утверждения, к-е она не может ни доказать, ни опровергнуть. Но конкретное такое утверждение, формулируемое в процессе док-ва неполноты, независимого математического интереса не представляет. Пример интересного такого утверждения - пятый постулат Евклида, независимый от остальных аксиом геометрии; но аксиомы геометрии намного слабее, чем аксиомы арифметики или теории множеств. Аксиома выбора -- пример такого интересного утверждения, независимого от теории множеств.)
Доказательство Гёделя основывалось на построении специального рода модели теории множеств, под названием конструктивная вселенная (её обычно обозначают буквой L, в отличие от "всей вселенной" вообще, обозначаемой буквой V). В конструктивной вселенной аксиому выбора можно доказать; затем можно показать, что любое док-во противоречия в L влечёт за собой док-во противоречия в обычной теории множеств. Поэтому если бы аксиому выбора можно было опровергнуть при помощи других аксиом, то такое опровержение существовало бы и "внутри" L, и тогда вместе с док-вом аксиомы выбора "внутри" L явило бы собой противоречие, к-е можно было бы вытащить "наружу" в V, и доказать, что остальные аксиомы теории множеств сами по себе противоречивы.
Larry Paulson (Кембридж) недавно закончил формализацию доказательства Гёделя в компьютерной системе Isabelle, существующей для строгой формализации и формальной верификации математических доказательств. Это интересный результат. Формальная верификация математических доказательств -- весьма сложное дело; простой и очевидно истинный для человека-математика шаг в математическом доказательстве может потребовать перевода в сотни и тысячи маленьких формальных шажков для того, чтобы компьютер мог потвердить его формальную строгость и истинность. По этой причине не так уж и много нетривиальных математических теорем (даже в очень слабом для профессионального математика смысле слова "нетривиальный") были формально верифицированы. Вот краткое описание того, что сделал Полсон; а этот файл (>200 страниц, автоматически сгенерированный) содержит нужные формальные определения и доказательства - его любопытно полистать в качестве примера длинного нетривиального формального доказательства.
Я хотел также разобраться в системе Isabelle, но быстро понял, что мне не хватает как адекватного знания лямбда-исчисления (lambda calculus), так и знания языка ML, на котором она написана. Особенно λ-calculus давно уже пора было как следует изучить.
subject: формализация V=L и консистенстности аксиомы выбора
(контекст: математика, теория множеств, аксиома выбора)
Немного контекста. В 1940-м году Гёдель доказал, что аксиома выбора (и обобщённая гипотеза континуума вместе с ней) консистентны с остальными аксиомами теории множеств, т.е. что невозможно при помощи остальных аксиом их опровергнуть (при условии, что остальные аксиомы непротиворечивы сами по себе). Это, во-первых, окончательно укрепило статус аксиомы выбора в глазах математиков; во-вторых, результат Гёделя вместе с доказательством Коэна 20 лет спустя (Коэн показал, что эти утверждения из остальных аксиом невозможно доказать) доказывают независимость аксиомы выбора от остальных аксиом -- первое и самое важное нетривиальное доказательство неполноты мощной формальной системы (в данном случае теории множеств без аксиомы выбора), не опирающееся на теоремы Гёделя о неполноте.
(иными словами, из знаменитых теорем Гёделя о неполноте мы знаем, что любая достаточно мощная формальная система -- в том числе теория множеств -- неполна, т.е. существуют утверждения, к-е она не может ни доказать, ни опровергнуть. Но конкретное такое утверждение, формулируемое в процессе док-ва неполноты, независимого математического интереса не представляет. Пример интересного такого утверждения - пятый постулат Евклида, независимый от остальных аксиом геометрии; но аксиомы геометрии намного слабее, чем аксиомы арифметики или теории множеств. Аксиома выбора -- пример такого интересного утверждения, независимого от теории множеств.)
Доказательство Гёделя основывалось на построении специального рода модели теории множеств, под названием конструктивная вселенная (её обычно обозначают буквой L, в отличие от "всей вселенной" вообще, обозначаемой буквой V). В конструктивной вселенной аксиому выбора можно доказать; затем можно показать, что любое док-во противоречия в L влечёт за собой док-во противоречия в обычной теории множеств. Поэтому если бы аксиому выбора можно было опровергнуть при помощи других аксиом, то такое опровержение существовало бы и "внутри" L, и тогда вместе с док-вом аксиомы выбора "внутри" L явило бы собой противоречие, к-е можно было бы вытащить "наружу" в V, и доказать, что остальные аксиомы теории множеств сами по себе противоречивы.
Larry Paulson (Кембридж) недавно закончил формализацию доказательства Гёделя в компьютерной системе Isabelle, существующей для строгой формализации и формальной верификации математических доказательств. Это интересный результат. Формальная верификация математических доказательств -- весьма сложное дело; простой и очевидно истинный для человека-математика шаг в математическом доказательстве может потребовать перевода в сотни и тысячи маленьких формальных шажков для того, чтобы компьютер мог потвердить его формальную строгость и истинность. По этой причине не так уж и много нетривиальных математических теорем (даже в очень слабом для профессионального математика смысле слова "нетривиальный") были формально верифицированы. Вот краткое описание того, что сделал Полсон; а этот файл (>200 страниц, автоматически сгенерированный) содержит нужные формальные определения и доказательства - его любопытно полистать в качестве примера длинного нетривиального формального доказательства.
Я хотел также разобраться в системе Isabelle, но быстро понял, что мне не хватает как адекватного знания лямбда-исчисления (lambda calculus), так и знания языка ML, на котором она написана. Особенно λ-calculus давно уже пора было как следует изучить.
