Математическая логика
Теорема Гёделя о полноте
Гёдель доказал ДВЕ теоремы с похожими названиями. Теорема о ПОЛНОТЕ (1929): FOL полна - всё истинное доказуемо. Теорема о НЕполноте (1931): арифметика неполна - есть истинное, что недоказуемо. Одно имя, противоположный смысл. Путаница между ними убивает понимание. SAT-решатели (MiniSat, Glucose), Z3 SMT, Prolog, TLA+ - все реализуют теорему о полноте на практике.
- **SAT-решатели (CDCL):** полные для пропозициональной логики. MiniSat решает задачи с миллионами переменных - верификация аппаратуры Intel, AMD
- **Z3 SMT (Microsoft):** полный для линейной арифметики, массивов, битовых векторов. Используется в Dafny, F* для доказательства корректности кода
- **TLA+ (Lamport):** model checking конечных состояний - полная проверка. Amazon использует для верификации Dynamo, S3
Предварительные знания
- Формальные системы и понятие вывода (⊢)
- Семантика: модели, истинность формулы в интерпретации (⊨)
Корректность и полнота: два разных вопроса
Гёдель доказал две теоремы с похожими названиями, но противоположным смыслом. Теорема о ПОЛНОТЕ (1929, 23 года): логика первого порядка полна - всё истинное доказуемо. Теорема о НЕполноте (1931, 25 лет): арифметика Пеано неполна - есть истинное, что недоказуемо. Одно имя, два года, две теоремы. Путаница между ними - самая частая ошибка при чтении логики.
**Корректность (soundness):** если доказуемо, то истинно ⊢ φ ⟹ ⊨ φ **Полнота (completeness):** если истинно (во всех моделях), то доказуемо ⊨ φ ⟹ ⊢ φ Теорема Гёделя о полноте (1929): для логики первого порядка оба направления выполнены: ⊢ φ ⟺ ⊨ φ
SAT-решатель (CDCL) - полный алгоритм для пропозициональной логики: если формула выполнима, найдёт решение; если невыполнима - докажет это. Prolog (SLD-resolution) - полный для Horn-клауз, но не для всей логики первого порядка. Z3 SMT - полный для многих теорий (линейная арифметика, массивы, битовые векторы). Все они - практические реализации теоремы Гёделя о полноте в конкретных фрагментах.
**Чтобы не путаться:** корректность смотрит налево (из синтаксиса в семантику), полнота - направо. Звучит одинаково, стрелки разные. Большинство систем корректны по построению. Полнота - редкость и обычно дорогостояща (undecidable для богатых теорий).
Что означает «корректность» (soundness) исчисления предикатов?
Теорема Гёделя о полноте: формулировка и следствия
1929 год. Курт Гёдель. 23 года. Диссертация в Вене: первопорядковая логика полна - если формула истинна во всех моделях, она доказуема из аксиом. Через два года - теорема о неполноте. Один человек, два года, два результата, которые изменили математику и информатику навсегда. И не путайте их.
**Теорема Гёделя о полноте (1929):** Формула φ в логике первого порядка: ⊢ φ тогда и только тогда, когда ⊨ φ **Эквивалентная формулировка через непротиворечивость:** Теория T непротиворечива ⟺ у T есть модель **Следствие для автоматического доказательства:** Если φ логически следует из аксиом T (T ⊨ φ), то существует конечный вывод T ⊢ φ. Алгоритм resolution его найдёт - за конечное время.
Полнота - не то же самое, что разрешимость. Логика первого порядка полна (любая тавтология доказуема), но полуразрешима: алгоритм остановится и скажет «да» для любой истинной формулы, но для ложной может работать бесконечно. Именно поэтому automated theorem provers (Lean, Coq, Isabelle) требуют помощи человека: полнота гарантирует существование доказательства, но не его нахождение за разумное время.
«Логика первого порядка полна - значит, любую теорему можно доказать автоматически»
FOL полна, но полуразрешима: алгоритм найдёт доказательство если оно есть, но может не остановиться если формула ложна
Полнота говорит о существовании вывода, не о времени его поиска. Для богатых теорий (арифметика) время поиска может быть неограниченным - что физически эквивалентно недостижимости.
Как опровергнуть логическую формулу φ (показать, что ⊭ φ)?
Полнота в пропозициональной логике: SAT-решатели
Для пропозициональной логики полнота - не абстракция, а работающее программное обеспечение. DPLL-алгоритм (1960) и его потомок CDCL (Conflict-Driven Clause Learning, 1990-е) - полные алгоритмы: для любой пропозициональной формулы они дают ответ SAT (+ свидетель) или UNSAT (+ доказательство невыполнимости). MiniSat в 2003 году показал: это практично даже для миллионов переменных.
| Система | Охват | Полная? | Применение |
|---|---|---|---|
| DPLL/CDCL SAT | Пропозициональная логика | Да | Верификация схем, планирование |
| SLD-resolution (Prolog) | Horn-клаузы (FOL) | Да для Horn | Логическое программирование |
| Z3 SMT | LIA, NIA, BV, Arrays | Да для этих теорий | Верификация кода (Dafny, F*) |
| TLA+ model checker | Конечные состояния | Да для конечных | Распределённые алгоритмы |
| Общее FOL | Все формулы | Полуразрешима | Математические доказательства |
Теорема о компактности - следствие полноты. Бесконечное множество формул выполнимо тогда и только тогда, когда каждое его конечное подмножество выполнимо. На практике это позволяет строить нестандартные модели арифметики: добавить константу c и бесконечно много аксиом c > 0, c > 1, c > 2, ... - каждое конечное подмножество выполнимо (берём стандартную модель, интерпретируем c как достаточно большое). По компактности - всё множество выполнимо. Так рождается элемент, больший любого натурального числа.
Что гарантирует теорема о компактности для бесконечного множества формул Г?
Полнота (1929) vs Неполнота (1931): чёткое разграничение
Логика первого порядка полна. Арифметика Пеано неполна. Это не противоречие - это два разных объекта. Теорема о полноте говорит про логику как механизм вывода. Теорема о неполноте говорит про конкретную теорию (PA) как набор аксиом. Понять разницу - значит понять структуру математики.
| Свойство | Теорема о полноте (1929) | Теорема о неполноте (1931) |
|---|---|---|
| Объект | Логика первого порядка (механизм вывода) | Арифметика Пеано (конкретная теория) |
| Утверждение | ⊢ φ ⟺ ⊨ φ для FOL | Существует φ: PA ⊭ φ, PA ⊭ ¬φ |
| Знак результата | Позитивный: синтаксис = семантика | Негативный: есть недостижимые истины |
| Следствие | Автоматическое доказательство возможно | Нельзя аксиоматизировать всю математику |
| Год | 1929, диссертация Гёделя | 1931, Monatshefte für Mathematik |
Теорема Лёвенхейма-Сколема добавляет ещё одну грань. Если счётная теория первого порядка имеет бесконечную модель - она имеет счётную модель. ZFC (теория множеств) доказывает существование несчётных множеств. Но у ZFC есть счётная модель - модель Сколема. В ней «несчётное» множество (например, R) счётно снаружи - просто биекция с натуральными числами не определена внутри модели. Понятия «счётный» и «несчётный» зависят от того, из какой модели смотреть.
«Логика первого порядка полна - значит, можно аксиоматически задать натуральные числа как единственную модель»
Любая FOL-аксиоматика с моделью N также имеет нестандартные модели любой бесконечной мощности
Это следствие теоремы Лёвенхейма-Сколема. Натуральные числа ускользают от FOL. Логика второго порядка может аксиоматизировать N, но теорема о полноте для неё не верна: семантика и синтаксис расходятся.
Теория Т в логике первого порядка непротиворечива. Что гарантирует теорема Гёделя о полноте?
Ключевые идеи
- **Корректность (soundness):** ⊢ φ ⟹ ⊨ φ. Доказуемое - истинно. Проверяется индукцией по выводу
- **Полнота (completeness):** ⊨ φ ⟹ ⊢ φ. Истинное во всех моделях - доказуемо. Теорема Гёделя 1929
- **Эквивалент через модели:** T непротиворечива ⟺ у T есть модель. Ключевое следствие для SAT-решателей
- **Практика:** CDCL SAT - полный для PL; SLD-resolution - полный для Horn-клауз; Z3 SMT - полный для своих теорий
- **Полнота ≠ Неполнота:** FOL полна как механизм вывода; PA неполна как теория. Разные объекты, разные утверждения
- **Лёвенхейм-Сколем:** натуральные числа ускользают от FOL - любая аксиоматика имеет нестандартные модели
К теоремам о неполноте
Теорема о полноте - позитивный результат для FOL. Для конкретных теорий Гёдель доказал принципиально иное:
- Первая теорема о неполноте — Существует формула φ: PA ⊭ φ, PA ⊭ ¬φ - истинная, но недоказуемая
- Вторая теорема о неполноте — PA не доказывает собственную непротиворечивость (если она непротиворечива)
Вопросы для размышления
- Если логика первого порядка полна, почему автоматические доказатели теорем (Lean, Coq) требуют помощи человека?
- В чём смысл «парадокса Сколема»? Почему он не является настоящим противоречием?
- TypeScript не имеет полной системы типов: есть программы, которые не упадут, но не проходят type-check. Какой термин из этого урока описывает это свойство?
Связанные уроки
- ml-04 — Формальные системы и понятие вывода - без этого теорема о полноте не формулируется
- ml-06 — Первая теорема о неполноте - главный контраст: completeness (1929) vs incompleteness (1931)
- dm-05 — Комбинаторика пространства моделей: счётные vs несчётные, birthday problem для логических структур
- prob-04-bayes — Байесовский апдейт как семантическое следование: prior + evidence = posterior; аксиомы + вывод = теорема
- fl-22-decidability