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

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

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

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

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

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

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