1. Аксиомы исчисления предикатов - общезначимые формулы.
2. Формула, получающаяся из общезначимых формулы по любому из правил вывода 1-4, является общезначимой.
3. Любая доказуемая в исчислении предикатов формула общезначима.
Доказательство.
1. Для аксиом А1-А3 утверждение следует из леммы 5.5, для аксиом А4-А5 это следует из теорем 4.1 и 4.2.
2. Для правила modus ponens утверждение следует из свойств импликации. Справедливость утверждения для правил вывода 2 и 3 следует из лемм 5.6 и 5.7. Справедливость утверждения для четвертого правила вывода легко доказывается.
3. Эта часть теоремы следует из утверждений 1 и 2.
Доказательство обратной теоремы значительно сложней.
Теорема 5.6 (теорема Геделя о полноте исчисления предикатов, 1930). Всякая общезначимая формула выводима в исчислении предикатов.
В отличие от случая исчисления высказываний в исчислении предикатов первого порядка у нас нет эффективного способа для распознавания общезначимости.
Теорема 5.7 (теорема Черча о неразрешимости исчисления предикатов, 1936). Не существует алгоритма, который для любой формулы исчисления предикатов первого порядка устанавливает, общезначима она или нет.