Аксиоматическая система исчисления предикатов

Теорема 29.14 (теорема Гёделя о полноте ФИП). Класс доказуемых замкнутых формул совпадает с классом общезначимых (или тождественно истинных) формул:  .
Доказательство. Эта теорема непосредственно вытекает из предыдущей при  .
Справедлива она и для открытых формул. В самом деле, если  , где  — свободные предметные переменные в формуле  , то в силу определения квантора общности это будет равносильно тому, что  . По теореме 29.14 это равносильно тому, что  . В силу свойств выводимости последнее утверждение равносильно тому, что  .

Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах
В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14 может быть истолкована как некая внешняя полнота формализованного исчисления предикатов, его полнота относительно логики предикатов: в этой теории могут быть формально доказаны все общезначимые формулы логики предикатов. Рассмотрим вопросы внутренней полноты формализованного исчисления предикатов, т.е. выясним, будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и 27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного исчисления предикатов совпадает с множеством тавтологий (общезначимых формул) логики предикатов, а в логике предикатов существуют выполнимые, но не общезначимые формулы, формализованное исчисление предикатов не является абсолютно полной теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном исчислении высказываний. Что же касается полноты формализованного исчисления предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства приведем пример формулы, не являющейся теоремой формализованного исчисления предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением правил вывода) приводит к непротиворечивой формальной аксиоматической теории.
Пример 29.15. Рассмотрим формулу  . Нетрудно убедиться в том, что она не является общезначимой (приведите пример конкретного одноместного предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании теоремы К. Гёделя о полноте она не доказуема в формализованном исчислении предикатов. С другой стороны, добавив к аксиомам формализованного исчисления предикатов рассматриваемую формулу, получим непротиворечивую формальную теорию  . Ее непротиворечивость можно доказать следующим образом.
Рассмотрим модель этой теории на одноэлементном множестве  . Ясно, что данная формула тождественно истинна на  . Далее, учитывая, что на  можно определить для каждого натурального  лишь два n-местных предиката  и  , причем  и  , нетрудно доказать, что все аксиомы новой теории  тождественно истинны на этой модели и правила вывода от тождественно истинных на  формул приводят к тождественно истинным на  формулам. Таким образом, доказывается утверждение: всякая теорема теории  тождественно истинна на одноэлементном множестве  .
Следовательно, если бы для некоторой формулы  обе формулы  и  были теоремами теории  , то они были бы тождественно истинны на одноэлементном множестве  , что невозможно. Поэтому расширенная теория  непротиворечива, что и доказывает неполноту в узком смысле формализованного исчисления предикатов.