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

Теорема компактности
Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт, непосредственно вытекающий из определения понятия вывода, что  тогда и только тогда, когда  , где  — некоторое конечное подмножество множества  формул. Теорема адекватности, установленная на основании выдающейся теоремы Гёделя о существовании модели, позволяет получить из этого тривиального соображения аналогичную теорему семантического содержания, уже отнюдь не столь очевидную.
Теорема 29.16 (теорема К. Гёделя–А. И. Мальцева). Если  , то для некоторого конечного подмножества  имеет место  .
Доказательство. Если  , то по теореме 29.13 (теорема адекватности)  . В силу сделанного перед настоящей теоремой замечания найдется такое конечное подмножество  , что  . Отсюда по теореме оправданности (следствие 29.2 из теоремы 29.1) заключаем, что  .
Следствие 29.17(локальная теорема К. Гёделя—А. И. Мальцева). Множество  замкнутых формул узкого исчисления предикатов сигнатуры  имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель.
Доказательство. Необходимость очевидна. Обратно, пусть каждое конечное подмножество множества  имеет модель. Тогда  — синтаксически непротиворечиво. (Если бы это было не так, то для некоторой формулы  имелись бы выводимости  и  , а значит, нашлось бы такое конечное подмножество  , что и  , то есть  было бы синтаксически противоречиво, а значит, по теореме 29.12 не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о существовании модели множество  имеет модель. Следствие доказано.
В заключение приведем еще одну теорему о формулах узкого исчисления предикатов и их моделях.
Теорема 29.18 (Лёвенгейм–Сколем). Пусть  — счетная сигнатура и  — множество замкнутых формул узкого исчисления предикатов сигнатуры  . Если  имеет модель, то  имеет счетную модель.