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

Следствие 29.2 (теорема оправданности). Из синтаксической выводимости следует семантическая выводимость, т. е. если  , то  .
Доказательство. Пусть  и пусть  — любая алгебраическая система, в которой выполняются все формулы из  , то есть  . Тогда по доказанной теореме  . По определению семантического следствия это и означает, что  .
Следствие 29.3. Всякая доказуемая формула является общезначимой (т.е. любая теорема истинна): если  , то  .
Доказательство получается из предыдущего следствия при  .

Непротиворечивость формализованного исчисления предикатов
Важнейшим компонентом критерия оправданности всякой математической теории является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого утверждения и его отрицания одновременно. Трудности, связанные с доказательством этого свойства математических теорий (а одной из причин этих трудностей, несомненно, было отсутствие в содержательных математических теориях точного понятия доказательства), привели к тому, что в математике более естественным стал другой признак непротиворечивости теории, основанный на возможностях реализации этой теории, ее моделируемости. Но в то же время этот подход и привел к возникновению парадоксов в математике, которые, в свою очередь, привели к возникновению науки об основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории. Одной из задач этого подхода была выработка такого формального понятия доказательства, при котором для конкретной математической теории понятие ее формальной непротиворечивости совпало бы с понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу точности определения доказательства, становится математической теоремой (точнее, метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух понятий непротиворечивости было непростым. В частности, неприятие современниками неевклидовых геометрий Лобачевского–Бояи объясняется также и тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, совпадающим по существу с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их содержательную непротиворечивость, были найдены позднее.
Наша задача состоит в том, чтобы в рамках формализованного (узкого) исчисления предикатов дать точные определения двух понятий непротиворечивости и установить их эквивалентность.
Напомним, что формула логики предикатов называется общезначимой, если она истинна в любой интерпретации, и противоречивой, если она ложна в любой интерпретации, т.е. если ее отрицание общезначимо. Эти семантические понятия, связывающие непротиворечивость с истинностью, позволяют сформулировать понятие семантически непротиворечивой теории.