Математическая логика
Теоремы Гёделя о неполноте
В 1931 году 25-летний Курт Гёдель уничтожил программу Гильберта одной теоремой. Любая достаточно богатая математическая теория содержит истинные утверждения, которые невозможно доказать в ней самой. Математика принципиально шире, чем любая её формализация.
- Теоретические ограничения верификации программ: нельзя доказать корректность всех программ
- Криптография: некоторые утверждения о сложности могут быть неразрешимы
- Философия разума: аргумент Лукаса о несводимости человеческого мышления к алгоритму
Первая теорема о неполноте
Первая теорема Гёделя о неполноте: любая непротиворечивая формальная система T, достаточно сильная для кодирования элементарной арифметики, является синтаксически неполной - существует формула G такая, что ни G, ни ¬G не выводимы из T.
Гёделево предложение G истинно (в стандартной модели ℕ), но недоказуемо в T. Это не значит, что математика «не знает» правды - мы знаем, что G истинна, рассуждая вне системы T. Система не может «увидеть» эту истину изнутри.
Что утверждает первая теорема Гёделя о неполноте?
Вторая теорема о неполноте
Вторая теорема Гёделя: непротиворечивая формальная система T, достаточно сильная для кодирования арифметики, не может доказать собственную непротиворечивость. Cons(T) - формула, выражающая «T непротиворечива» - не выводима из T.
Вторая теорема означает, что математика противоречива
Вторая теорема означает, что система не может сама подтвердить собственную непротиворечивость. Она может быть непротиворечивой - мы просто не можем доказать это изнутри системы.
Это похоже на то, что судья не может быть объективным свидетелем в собственном деле. Непротиворечивость системы можно доказать в более сильной метасистеме - но тогда непротиворечивость метасистемы становится вопросом.
Почему вторая теорема Гёделя разрушила программу Гильберта?
Гёделизация и нумерация
Гёделизация - технический приём: кодирование синтаксических объектов (формул, доказательств) натуральными числами. Это позволяет арифметике «говорить о себе» - выражать метаматематические утверждения внутри самой системы.
Современные доказательства используют лямбда-исчисление или рекурсивные функции вместо простых чисел, но принцип тот же. Важно, что кодирование примитивно рекурсивно: это гарантирует, что PA может работать с кодами и восстанавливать оригиналы.
Зачем нужна гёделизация в доказательстве теорем о неполноте?
Самореференция и диагональная лемма
Диагональная лемма (лемма о самореференции): для любой формулы F(x) существует предложение G такое, что T ⊢ G ↔ F(⌈G⌉). Это математически точный способ построить формулу, «говорящую о себе».
Теорема Тарского о невыразимости истины - близкий родственник теорем Гёделя: нельзя определить предикат Truth(x) «x - истинное предложение PA» внутри самой PA. Это строже, чем неполнота: не просто неразрешимые предложения, а принципиальная невыразимость понятия истины.
Самореференция и диагональная лемма?
Review the concept above.
Теоремы Гёделя о неполноте: ключевые идеи
- Первая теорема: в любой богатой непротиворечивой теории есть истинные недоказуемые предложения
- Вторая теорема: теория не может доказать собственную непротиворечивость
- Гёделизация: кодирование синтаксиса числами позволяет арифметике говорить о себе
- Диагональная лемма: для любого свойства можно построить формулу, говорящую о себе
- Теорема Тарского: понятие «истины» не определимо внутри достаточно богатой системы
От логики к теории вычислений
Идеи Гёделя напрямую связаны с неразрешимостью проблемы остановки Тьюринга. Недоказуемость ≈ невычислимость. Следующий урок рассматривает теорию моделей - другой инструмент для изучения формальных систем.
Вопросы для размышления
- Гёделево предложение G истинно, но недоказуемо в PA. Как мы вообще знаем, что G истинно?
- Означают ли теоремы о неполноте, что математика «незавершена»? Или что она богаче, чем любая её формализация?
- Если мы добавим G как новую аксиому к PA, получим более сильную систему. Но теорема применима и к ней. Что это означает?