Семантическая полнота

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

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

Определение и формализация

Семантическая полнота формальной системы \( S \) с множеством аксиом \( A \) и правилами вывода \( R \) формулируется следующим образом: для любой формулы \( \phi \) языка системы, если \( \phi \) истинна во всех моделях системы \( S \) (обозначение \( \models_{S} \phi \)), то \( \phi \) выводима в системе \( S \) (обозначение \( \vdash_{S} \phi \)).

Здесь важны два ключевых понятия:

• Модель — это некоторая математическая структура (интерпретация), которая приписывает значения всем символам языка системы таким образом, что все аксиомы системы в этой структуре истинны.
• Истинность (в модели) — это определение согласно правилам семантики данной логики (обычно по Тарскому). Формула считается истинной в модели, если она выполняется при данной интерпретации.

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

История и ключевые теоремы

Вопрос о семантической полноте впервые был поставлен и решён в контексте исчисления высказываний.

Теорема о полноте для исчисления высказываний

Классическое исчисление высказываний является семантически полным относительно классической двузначной логики. Это было доказано Эмилем Постом в 1921 году. Теорема Поста утверждает, что любая тавтология (формула, истинная при всех истинностных значениях входящих в неё пропозициональных переменных) является доказуемой в стандартном гильбертовском исчислении высказываний.

Теорема Гёделя о полноте

Наиболее известный результат о семантической полноте касается логики первого порядка. Курт Гёдель в 1929 году (в своей докторской диссертации) доказал теорему о полноте: исчисление предикатов первого порядка (с правилами вывода) является семантически полным относительно стандартной семантики первого порядка. Эта теорема стала фундаментальным результатом современной логики.

Теорема Гёделя о полноте (не путать с его же теоремами о неполноте для арифметики Пеано) утверждает, что в логике первого порядка любая логически общезначимая формула (истинная во всех возможных моделях) может быть выведена синтаксически. Это означает, что синтаксический аппарат логики первого порядка полностью адекватен для выражения всех логических истин.

Теоремы Гёделя о неполноте и их связь

Теоремы Гёделя о неполноте (1931) часто ошибочно истолковываются как опровержение теоремы о полноте. На самом деле, они относятся к другому понятию полноты — синтаксической. Они показывают, что для достаточно богатых формальных систем (например, арифметики Пеано, содержащей аксиомы для натуральных чисел) существует истинное (в стандартной модели) утверждение, которое не может быть ни доказано, ни опровергнуто в рамках этой системы. Однако сама эта система (арифметика Пеано) не является семантически полной, так как существуют истинные в стандартной модели арифметики утверждения, которые не выводимы. Логика первого порядка, как язык, остаётся семантически полной; проблема в том, что система аксиом арифметики неполна — она не способна «захватить» все истины об арифметике.

Семантическая полнота в различных логиках

• Логика высказываний: Полностью семантически полна (теорема Поста).
• Логика первого порядка: Полностью семантически полна (теорема Гёделя о полноте).
• Логика второго порядка: Не является семантически полной (как показали Склем и Линдстрём). В ней фундаментальные понятия (например, понятие множества всех подмножеств) не поддаются полной аксиоматизации.
• Интуиционистская логика: Семантически полна относительно определённых классов моделей (например, семантики Крипке или алгебраической семантики алгебр Гейтинга).
• Модальные логики: Для большинства стандартных модальных логик (T, S4, S5) существуют теоремы о полноте относительно определённых классов моделей Крипке (например, рефлексивных, транзитивных, симметричных).

Значение и применение

Семантическая полнота является одним из краеугольных камней теории доказательств и теории моделей. Её значение многогранно:

1. Основание для доказательств: Теорема Гёделя о полноте позволяет использовать методы теории моделей для доказательства невыводимости: если формула \( \phi \) не выводима, то существует модель, в которой она ложна (от противного: если бы она была истинна во всех моделях, то была бы выводима).
2. Компактность: Следствием теоремы о полноте является теорема компактности (Мальцев, 1936): если любое конечное подмножество множества аксиом \( \Sigma \) имеет модель, то всё \( \Sigma \) имеет модель. Этот результат широко применяется в алгебре и теории чисел.
3. Искусственный интеллект и формальная верификация: Понимание полноты необходимо для построения систем доказательства теорем (автоматических доказателей). Если система не полна, она может пропускать истинные утверждения, что критично при верификации программ или алгоритмов.
4. Философия математики: Семантическая полнота логики первого порядка показывает, что дедуктивные методы адекватны для охвата всех логических истин, что укрепляет доверие к формальным методам.

Критика и ограничения

Сам термин «полнота» многозначен. Различают:

• Семантическую полноту (о которой идёт речь).
• Синтаксическую полноту (каждое утверждение или его отрицание доказуемо). Теоремы Гёделя о неполноте показали, что для достаточно мощных систем синтаксическая полнота невозможна.
• Выразительную полноту (способность языка выразить определённые понятия). Логика первого порядка не является выразительно полной (например, она не может определить понятие конечности модели без дополнительных аксиом).

Кроме того, теорема о полноте для логики первого порядка не гарантирует, что процесс поиска доказательства эффективен (есть алгоритм, всегда завершающийся и дающий ответ). Доказательство существования вывода не означает, что можно найти его за конечное время для любого утверждения. Логика первого порядка является полуразрешимой: если формула выводима, то найдётся алгоритм, который найдёт доказательство, но если формула невыводима, алгоритм может работать бесконечно.

Примеры

• Пример 1 (исчисление высказываний): Формула \( (\neg P \to \neg Q) \to (Q \to P) \) является тавтологией (истинна при любых \( P \) и \( Q \)). Теорема о полноте гарантирует, что существует её доказательство в исчислении высказываний. Действительно, её можно вывести из аксиом через modus ponens.
• Пример 2 (логика первого порядка): Утверждение «Если всякий человек смертен, и Сократ — человек, то Сократ смертен» является логически общезначимым (истинно во всех интерпретациях). Теорема Гёделя гарантирует, что его можно вывести в исчислении предикатов первого порядка.
• Пример 3 (отсутствие семантической полноты): Система арифметики Пеано (PA) не является семантически полной. Утверждение Геделя \( G_{PA} \), построенное в доказательстве теорем о неполноте, истинно в стандартной модели \( \mathbb{N} \) (натуральные числа), но не выводимо в \( PA \). Следовательно, существует истинная (в модели) формула, не имеющая доказательства.

Источники

1. Мендельсон, Э. (2008). Введение в математическую логику. 6-е изд. М.: Издательство ЛКИ / URSS.
2. Гёдель, К. (1929). О полноте исчисления предикатов (докторская диссертация).
3. Клини, С. К. (1952). Введение в метаматематику. М.: Иностранная литература.
4. Чёрч, А. (1956). Introduction to Mathematical Logic. Princeton University Press.
5. Эпштейн, Р., & Карниелли, У. (2008). Computability: Computable Functions, Logic, and the Foundations of Mathematics. Wadsworth Publishing.