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

Определение 29.4. Формальная теория называется семантически непротиворечивой, если ни одна из ее теорем (формул) не является противоречивой, т. е. ложной при любой ее интерпретации. Аналогично, множество  формул называется семантически непротиворечивым, если ни одна формула, выводимая из  , не является противоречивой.
В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см. следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво. Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории этих классов составными частями, что вполне соответствует общенаучному принципу универсальности законов логики (Лейбниц формулировал его как выполнимость логических законов "во всех мыслимых мирах").
Произвольная формальная теория  есть теория множества  всех своих моделей, а значит, теория  семантически непротиворечива, если и только если  , т.е. для теории  существует модель. Если отождествить пригодность математической теории, ее целесообразность с ее семантической непротиворечивостью, то можно сказать, что сформулированный критерий пригодности теории известен уже давно. Отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства "законности" теории. Математическая логика выработала аналог этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие синтаксической непротиворечивости теории.
Определение 29.5. Формальная теория  называется синтаксически (или дедуктивно, или формально) непротиворечивой, если не существует такой формулы  , что  и  являются теоремами теории  , т.е. в  невыводимыми являются одновременно формула и ее отрицание. Аналогичное определение можно сформулировать и для произвольного множества  формул:  называется синтаксически непротиворечивым, если из  невыводимы одновременно формула и ее отрицание.
В теореме 16.9 доказана синтаксическая непротиворечивость формализованного исчисления высказываний. Аналогично доказывается следующая теорема.