Общезначимость выводимых в исчислении предикатов формул

Теорема: аксиомы ИП – общезначимые формулы. Пусть A – тавтология логики высказываний и x1, …, xn – список её переменных. Подставив вместо каждой переменной формулы ИП (и логики предикатов) B1, …, Bn (так, чтобы не нарушались определения формулы), получим общезначимую формулу ИП (и логики предикатов). Из этого следует, что все схемы аксиом ИВ, применяемые в ИП, являются общезначимыми формулами.

Теорема: формула, получающаяся из общезначимой по любому из правил вывода 1 – 4, является общезначимой. Для правила вывода 1 это следует из свойств импликации.

Теорема: любая выводимая в исчислении предикатов формула общезначима. Это следует из двух предыдущих теорем.

Теорема: ИП непротиворечиво. Это следует из того, что невозможно одновременно A и A.

Теорема Геделя (о полноте ИП). Всякая общезначимая формула выводима в ИП. Без доказательства.