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

Теорема 29.6. Формализованное исчисление предикатов синтаксически непротиворечиво.
Доказательство. Допустим противное, т.е. предположим, что ФИП синтаксически противоречиво. Значит, найдется такая формула  , что  и  будут теоремами ФИП. Тогда по следствию 29.3 из теоремы 29.1 формулы Fa -,Fбудут общезначимыми, что невозможно на основании определения общезначимости.
Теперь перейдем к установлению взаимосвязей между понятиями семантической и синтаксической непротиворечивости. Наша задача состоит в том, чтобы доказать их эквивалентность. Начнем с достаточно простой, но важной леммы.
Лемма 29.7. Если множество формул имеет модель, то это множество семантически непротиворечиво.
Доказательство. Если множество  формул имеет модель  , то ни одна формула, выводимая из  , не является противоречивой, т.е. ложной во всякой интерпретации, ибо в противном случае она была бы ложна и в  (что невозможно в силу теоремы 29.1). Это и означает, что  семантически непротиворечиво.
Теорема 29.8. Если множество формул семантически непротиворечиво, то оно синтаксически непротиворечиво.
Доказательство. Допустим, что некоторое множество  формул узкого исчисления предикатов семантически непротиворечиво, но противоречиво синтаксически. Следовательно, из него выводима некоторая формула  и ее отрицание  . Но тогда из  выводима и их конъюнкция (по правилу введения конъюнкции)  . Но эта формула ложна в любой интерпретации, что означает, что множество  семантически противоречиво. Получаем противоречие, доказывающее, что  синтаксически непротиворечиво.
Непосредственно из предыдущих леммы и теоремы вытекает такое следствие.
Следствие 29.9. Если множество формул имеет модель, то оно синтаксически непротиворечиво.

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