Математическая логика
Теоремы Гёделя о неполноте
Программа Гильберта (1920): аксиоматизировать всю математику полно и непротиворечиво. Гёдель (1931): невозможно. Одно из самых глубоких математических открытий XX века - граница того, что формальные системы могут знать о себе.
- Проблема остановки Тьюринга: неразрешимость HALT - прямое следствие диагонального аргумента Гёделя, применённого к программам
- Независимость CH от ZFC: Гёдель и Коэн доказали, что гипотеза континуума не решается стандартными аксиомами теории множеств
- Верификация программ: полная автоматическая верификация произвольных программ невозможна - это следствие теорем о неразрешимости
- Proof assistants (Lean, Coq): работают в системах с аксиомой выбора и унивалентности, выходящих за рамки PA, - каждая такая система порождает новые независимые утверждения
Гёделевская нумерация и диагонализация
В 1931 году 25-летний Курт Гёдель доказал: в любой достаточно богатой непротиворечивой формальной системе, включающей арифметику Пеано, существует истинное утверждение, недоказуемое внутри системы. Программа Гильберта - аксиоматизировать всю математику полно и непротиворечиво - оказалась невыполнимой.
Теорема применима к любой рекурсивно аксиоматизированной системе, содержащей достаточную арифметику: PA, ZFC, ZF, теория типов. Чем сильнее система, тем больше новых независимых предложений она порождает - добавление G как аксиомы создаёт новые G' по той же схеме.
Что утверждает первая теорема Гёделя о неполноте?
Первая теорема Гёделя: в любой непротиворечивой формальной системе S, содержащей арифметику натуральных чисел, существует предложение G такое, что ни G, ни neg G не доказуемы в S.
Следствия для оснований математики
Теоремы Гёделя имеют конкретные математические следствия. Непрерывность гипотезы (CH) независима от ZFC - Гёдель (1940) доказал её совместность, Коэн (1963) доказал независимость отрицания. Аксиома выбора независима от ZF. Существование больших кардиналов не доказуемо и не опровержимо в ZFC.
Связь с вычислимостью: теорема Гёделя и неразрешимость проблемы остановки Тьюринга - одно семейство диагональных аргументов. Гёдель кодирует синтаксис в арифметике; Тьюринг кодирует программы в числах. Обе конструкции создают самореференциальный объект, опровергающий полноту.
Что утверждает вторая теорема Гёделя?
Вторая теорема Гёделя: если S рекурсивно аксиоматизирована, содержит достаточную арифметику и непротиворечива, то S не доказывает Con(S). Это убивает программу Гильберта: невозможно финитарно обосновать непротиворечивость математики.
Итоги
- Гёделевская нумерация: формулы отображаются в числа через простые множители, что позволяет арифметике говорить о собственном синтаксисе
- Лемма о диагонализации: для любого предиката P существует G такое, что G эквивалентно P(ulcorner G urcorner)
- 1-я теорема: в непротиворечивой S, содержащей PA, существует G: S не доказывает G и S не доказывает neg G
- 2-я теорема: S не доказывает Con(S) - программа Гильберта неосуществима
- CH независима от ZFC: два из самых фундаментальных результатов математики XX века следуют из техники Гёделя
- Связь с Тьюрингом: проблема остановки и теоремы Гёделя - один класс диагональных аргументов о самоприменении