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

Полнота и адекватность формализованного исчисления предикатов
Доказав теорему Гёделя о существовании модели (теорема 29.10), можно доказать теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е. утверждение о том, что из семантической выводимости следует синтаксическая выводимость. В самом деле, пусть  . Покажем, что тогда множество формул  противоречиво. Допустим на время, что это не так. Тогда по теореме 29.10 это множество имеет модель  , т.е. на  выполняется формула  и все формулы из  . Из последнего, ввиду условия  , следует, что на  выполняется и формула  . Получаем противоречие. Итак, множество  противоречиво. Значит, из него выводима любая формула, в частности  . Тогда по теореме о дедукции имеем  . Учитывая, что, кроме того, формула  является теоремой ФИВ, по правилу MP заключаем, что  .
Итак, мы доказали, что если  , то  . Объединив это утверждение со следствием 29.1 из теоремы 29.2, приходим к следующей важной метатеореме.
Теорема 29.13 (теорема адекватности). Формула  синтаксически выводима из множества формул  тогда и только тогда, когда она семантически выводима из  .
Если теорема оправданности означала, что при выборе аксиом и правил вывода мы не были слишком щедры (настолько, что сможем доказать лишь общезначимые формулы), то обратная теорема — теорема адекватности — означает, что при этом выборе мы не были и излишне скупы (ровно настолько, что сможем доказать всякую общезначимую формулу).
Заметим, что нетрудно показать, что теорема о существовании модели вытекает из теоремы адекватности. В самом деле, предположим, что  — непротиворечивое множество формул, не имеющее модели. Тогда ясно, что для любой формулы  справедливо семантическое следование  . В силу теоремы адекватности отсюда следует, что  для любой  , что означает противоречивость множества  , в противоречие с условием.