Системы аксиом и теоремы о полноте

Мотивация: совпадают ли «истинно» и «доказуемо»?

В пропозициональной логике мы имеем два независимых понятия: семантика (что истинно при каждой оценке) и синтаксис (что выводится из аксиом по правилам). Теорема полноты утверждает их совпадение: всё семантически истинное доказуемо. Теорема корректности — обратное: всё доказуемое истинно. Вместе они гарантируют адекватность формальной системы.

Исчисление высказываний (стиль Гильберта)

Аксиомы:

(A1) φ → (ψ → φ) — «слабление»
(A2) (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)) — «распределение»
(A3) (¬ψ → ¬φ) → (φ → ψ) — «контрапозиция»

Единственное правило вывода: Modus Ponens (MP): из φ и φ → ψ выводится ψ.

Вывод из Γ: последовательность φ₁, ..., φₙ, где каждая φᵢ — аксиома, либо принадлежит Γ, либо получена из предыдущих по MP. Γ ⊢ φ — φ выводима из Γ.

Теоремы корректности и полноты

Теорема корректности (Soundness): Γ ⊢ φ ⟹ Γ ⊨ φ. Доказательство: индукция по длине вывода. Аксиомы — тавтологии; MP сохраняет истинность.

Теорема полноты (Completeness, Пост 1921): Γ ⊨ φ ⟹ Γ ⊢ φ. Любое семантическое следствие — синтаксически доказуемо. Это означает: система аксиом «достаточна» для всей классической логики.

Теорема дедукции: Γ ∪ {φ} ⊢ ψ ⟺ Γ ⊢ φ → ψ. Гипотезу можно «убирать» в антецедент импликации.

Теорема компактности: Γ ⊨ φ ⟺ существует конечное Γ₀ ⊂ Γ: Γ₀ ⊨ φ. Эквивалентно: Γ выполнимо ⟺ каждое конечное подмножество выполнимо.

Функциональная полнота

Базис связок: набор, через который выражаются все остальные.

{¬, ∧} — базис: p∨q ≡ ¬(¬p∧¬q).
{NAND} — однэлементный: p NAND q ≡ ¬(p∧q); ¬p ≡ p NAND p.
{NOR} — однэлементный: p NOR q ≡ ¬(p∨q).

Критерий функциональной полноты (Пост): Набор F функционально полон ⟺ он не содержится ни в одном из пяти классов Поста (монотонные, само-двойственные, T-сохраняющие, F-сохраняющие, линейные).

Численный пример

Задача: Вывести p → p в системе Гильберта.

Шаг 1. Запишем A2 при φ = p, ψ = (p→p), χ = p: (p→((p→p)→p)) → ((p→(p→p)) → (p→p)). — (1)

Шаг 2. A1 при φ = p, ψ = (p→p): p→((p→p)→p). — (2)

Шаг 3. A1 при φ = p, ψ = p: p→(p→p). — (3)

Шаг 4. MP из (1) и (2) — устраняем первый антецедент (1): (p→(p→p)) → (p→p). — (4)

Шаг 5. MP из (4) и (3): p→p. ■

Итоговая запись вывода:

p→((p→p)→p) [A1]
(p→((p→p)→p))→((p→(p→p))→(p→p)) [A2]
(p→(p→p))→(p→p) [MP из 2,1]
p→(p→p) [A1]
p→p [MP из 3,4]

Проверка: p→p — тавтология (при p=0: 0→0=1; при p=1: 1→1=1) ✓.

Реальное приложение

Автоматическое доказательство теорем (ATP): системы типа Prover9, E-prover используют полноту логики для автоматического поиска доказательств. Теорема дедукции — ключевой инструмент для перевода задачи «доказать A ⊨ B» в задачу «выполнима ли ¬(A→B)?» (через отрицание).

Дополнительные аспекты

Системы аксиом — это не только Гильбертовское исчисление с modus ponens, но и системы натурального вывода (Генцен, Пратт), секвенциальные исчисления и табличные методы. Теоремы корректности (всё доказуемое истинно) и полноты (всё истинное доказуемо) для пропозициональной логики были полностью установлены к 1920-м гг. Полнота для логики предикатов первого порядка (теорема Гёделя 1929 г.) — гораздо глубже: она утверждает, что синтаксический вывод улавливает все семантические следствия, и используется в любом современном автоматическом доказателе теорем. Для интуиционистской и модальной логик существуют свои теоремы полноты относительно крипкевских моделей.

Связь с другими разделами математики

Теоремы о полноте и компактности естественно выходят за пределы чистой логики и входят в арсенал современных математиков. В теории моделей они используются для переноса результатов между алгебраическими структурами. Классический пример — аксиоматизация полей: полнота логики первого порядка позволяет формализовать доказательство теоремы Тарского о том, что теория вещественно замкнутых полей является модельно полной и допускает устранение кванторов; отсюда вытекает элементарная эквивалентность всех вещественно замкнутых полей данной характеристики. Это напрямую связано с действительным анализом и дифференциальными уравнениями, где такие поля служат «обобщенными» континуумами.

В абстрактной алгебре теорема Левенхейма–Сколема и компактность дают нетривиальные следствия: например, существование несчетных моделей счетных теорий групп, колец, тел. Результат Малцева о локально конечных группах опирается на модельно-теоретические методы, где полнота логики обеспечивает переход от «все конечные подструктуры удовлетворяют...» к существованию модели всего набора аксиом.

В топологии логические методы проявляются через конструкцию стоуновского пространства для булевой алгебры высказываний. Представление Стоуна (1936) связывает булевы алгебры с компактными тотально несвязными пространствами; полнота классической логики выражается здесь в том, что каждое согласованное множество формул реализуется ультрафильтром, то есть точкой такого пространства.

В теории вероятностей аксиоматический подход Колмогорова (1933) формулируется в языке логики множеств: корректность и полнота систем типа ZFC задают границы того, что можно формально обосновать о вероятностных моделях. В численных методах и вычислительной математике полнота пропозициональной логики лежит в основе корректности SAT-решателей: алгоритм поиска модели фактически реализует семантическую сторону, а получаемые резолюционные доказательства интерпретируются как синтаксические выводы (полнота резолюции для пропозициональной логики доказана Робинсоном в 1965 году).

Историческая справка и развитие идеи

Семантическая полнота классической логики была постепенно осознана в начале XX века. Для исчисления высказываний первые строгие доказательства приписывают Эмилю Посту (1921) и связанной с ним традиции аксиоматик типа Гильберта. Полнота логики первого порядка была установлена Куртом Гёделем в 1929 году в статье в Monatshefte für Mathematik und Physik: он показал, что если формула истинна во всех моделях, то существует вывод в стандартной аксиоматике. Это стало фундаментом нового направления — теории доказательств и теории моделей. Мотивирующие задачи исходили от программы Гильберта: формализовать всю математику и обосновать её непротиворечивость чисто синтаксическими средствами. Логические системы Фреге и послекардановские разработки Пеано и Вайля создавали почву для постановки вопроса о совпадении «логической истины» и «выводимости». Параллельно Пост и Щенон (Sheffer) исследовали функциональную полноту связок, подготавливая алгебраическое видение логики. В середине XX века, после работ Гёделя, Тарского, Хенкина, Лёвенхейма, Сколема, теория моделей оформилась в самостоятельную область.