2.4.3. Теорема Геделя о полноте. Непротиворечивость исчисления предикатов

Теорема 4. Все доказуемые в ИП^Σ формулы являются тождественно истинными.

Доказательство проводим индукцией по длине вывода формулы. Очевидно, что аксиомы ИП^Σ являются тождественно истинными. Проверку того, что правила вывода 1-3 сохраняют тождественную истинность, мы оставляем читателю в качестве упражнения.

Следствие 3. ИП^Σ непротиворечиво, т.е. не все формулы ИП^Σ доказуемы в ИП^Σ.

В ИП^Σ справедлив аналог теоремы о полноте в исчислении высказываний.

Теорема 5 (Геделя о полноте). Формула φ исчисления ИП^Σ доказуема тогда и только тогда, когда φ тождественно истинна.

Таким образом, проверка доказуемости формулы φ сводится к проверке ее тождественной истинности. Однако в отличие от ИВ, в общем случае не существует алгоритма распознавания доказуемости формул ИП^Σ, т. е. ИП^Σ неразрешимо. Тем не менее, если в формуле φ "записать", что каждая переменная может принимать конечное число значений, то перебором всех возможных систем можно установить, является ли формула тождественно истинной или нет.