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

Теорема 29.10 (теорема Гёделя о существовании модели). Любое синтаксически непротиворечивое множество  замкнутых формул узкого исчисления предикатов сигнатуры  имеет модель.

▼ Доказательство

Теоремы о непротиворечивости формул предикатов
Теорема Гёделя о существовании модели позволяет доказать теорему, обратную к теореме 29.8, и они вместе образуют следующую важную метатеорему.
Теорема 29.11 (о непротиворечивости). Множество формул узкого исчисления предикатов семантически непротиворечиво тогда и только тогда, когда оно синтаксически непротиворечиво.
Доказательство. Необходимость есть теорема 29.8. Обратно, если множество формул синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме 29.7 оно семантически непротиворечиво.
Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10. Получим следующее.
Теорема 29.12 (о непротиворечивости). Множество формул узкого исчисления предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда, когда оно имеет модель.
Приведем интересный комментарий, который дает теореме о непротиворечивости известный логик Р. Линдон, по мнению которого доказательства (дедуктивной) непротиворечивости какой-либо теории посредством указания ее модели широко распространены в абстрактной математике. Менее очевидное из утверждений теоремы о непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой теории — используется далеко не так часто. Возможно, это объясняется тем, что математики не слишком-то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное выражение довольно-таки расплывчатого мнения, что существование в математике — это не что иное, как непротиворечивость.
Возможности применения теоремы о непротиворечивости к проблемам установления непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение модели обычно требует принятия в метаязыке допущений, значительно более сильных, нежели те, которые выражаются предметной теорией. Другой путь установления непротиворечивости какой-нибудь аксиоматической теории состоит в том, чтобы с помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако, также невелика. Теорема Гёделя не позволяет надеяться на получение доказательства непротиворечивости теории, если не допускать в теории, предназначенной для такого доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно сложных математических теорий базируется в конечном счете на интуиции и опыте.