Теорема о полноте

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

История

Предыстория

Проблема соотношения истинности и доказуемости восходит к античной философии и трудам Аристотеля, однако формальная постановка возникла лишь в конце XIX — начале XX века в связи с развитием аксиоматического метода. Создание исчисления высказываний и исчисления предикатов в работах Готлоба Фреге, Бертрана Рассела и Альфреда Норта Уайтхеда (в частности, в их трёхтомном труде «Principia Mathematica») поставило вопрос: охватывает ли синтаксическая выводимость все логически необходимые истины?

Доказательство Гёделя (1930)

Первое полное доказательство теоремы о полноте для логики первого порядка было представлено Куртом Гёделем в его докторской диссертации (1929) и опубликовано в 1930 году. Гёдель показал, что если формула общезначима, то существует её формальное доказательство в стандартном гильбертовом исчислении первого порядка. Доказательство использовало построение специальной (канонической) модели из синтаксических объектов — так называемый метод «от противного» с перечислением всех возможных непротиворечивых расширений теории.

Последующие формулировки и обобщения

В 1936 году Леон Хенкин независимо от Гёделя дал более простое и конструктивное доказательство теоремы для логики первого порядка с использованием так называемой «максимальной непротиворечивой последовательности» (теории Линденбаума). Этот подход стал стандартным в современных учебниках. В 1950-е годы теорема о полноте была распространена на ряд неклассических логик (интуиционистская, модальная, многозначная) в работах Соломона Крипке, Альфреда Тарского и других. Для логики высказываний теорема была доказана Постом (1921) и независимо Бернайсом (1926) путём построения таблиц истинности; её иногда называют теоремой о полноте для исчисления высказываний или семантической полнотой булевых формул.

Формулировка

Для формальной системы \( \mathcal{L} \) логики первого порядка теорема о полноте состоит из двух взаимно обратных утверждений:

Направление (корректность — soundness): Если формула \( \phi \) доказуема в исчислении (записывается как \( \vdash \phi \)), то она общезначима (записывается как \( \models \phi \)).
Направление (полнота — completeness): Если формула \( \phi \) общезначима, то она доказуема в исчислении (\( \models \phi \Rightarrow \vdash \phi \)).

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

Доказательство (основные этапы)

Для исчисления высказываний

В простейшем случае пропозициональной логики доказательство полноты опирается на понятие таблицы истинности. Поскольку любая формула содержит конечное число пропозициональных переменных, можно вычислить все возможные истинностные значения. Если формула оказывается истинной при всех комбинациях (тавтология), то существует алгоритм (например, метод семантических таблиц Бет-Хинтикки), строящий доказательство из аксиом и правил вывода, опираясь на эквивалентность между семантической и синтаксической выводимостью.

Для логики первого порядка

Основная идея доказательства (по Хенкину) состоит из трёх шагов:

Расширение теории до максимально непротиворечивой: Пусть \( T \) — непротиворечивое множество формул (например, искомое аксиоматическое описание). Используя лемму Цорна, его можно расширить до максимального непротиворечивого множества \( T^* \), которое для каждой формулы содержит либо её, либо её отрицание.
Построение канонической модели: Из синтаксических объектов — термов языка — строится структура (интерпретация). В этой структуре каждый терм интерпретируется как сам (с учётом эквивалентности по доказуемости), а предикаты задаются принадлежностью атомарных формул к \( T^* \). Полученная структура называется моделью языка.
Лемма о выполнимости: Показывается, что любая формула из \( T^* \) истинна в построенной канонической модели. Если же исходная формула \( \phi \) общезначима, то её отрицание невыполнимо — то есть множество \( \{\neg \phi\} \) противоречиво. Из противоречия выводится \( \phi \), что и доказывает существование формального вывода.

Следствия и значение

Теорема о компактности

Прямым следствием теоремы о полноте является теорема о компактности для логики первого порядка: множество формул имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель. Это важнейшее свойство используется в теории моделей и приложениях, например, в аксиоматизации алгебр и классов структур.

Критика и границы

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

Применение в информатике

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

Модификации и обобщения