Утверждение 2.В ИПΣ выполнимы все эквивалентности ИВ из теоремы 3.
Утверждение 3. Пусть φ, ψ – формулы ИПΣ переменная x не является свободной переменной формулы ψ, переменная у не является свободной переменной формулы φ. Тогда
1) ¬ xφ≡ x¬φ, 1΄) ¬ xφ≡ x¬φ,
2) x(φ∧ψ)≡ xφ∧ψ, 2΄) x(φ∨ψ)≡ xφ∨ψ,
3) x(φ∨ψ)≡ xφ∨ψ, 3΄) x(φ∧ψ)≡ xφ∧ψ,
4) xφ≡ x(φ) 4΄) xφ≡ x(φ)
Доказательство.Докажем эквивалентность 1). Построим квазивывод формулы ¬ xφ→ x¬φ из Ø:
1) φ→ xφ (схема аксиом 12);
2) ¬ xφ→¬φ (к п.1 применили свойство контрапозиции);
3) ¬ xφ→ x¬φ (к п.2 применили правило вывода 2).
Построим квазивывод формулы x¬φ→¬ xφ из Ø:
1) x¬φ→¬φ (схема аксиом 11);
2) ¬¬φ→¬ x¬φ ( к п.1 применили свойство контрапозиции);
3) φ→¬¬φ (тавтология);
4) φ→¬ x¬φ (к пп.3 и 2 применили свойство транзитивности);
5) xφ→¬ x¬φ (к п. 4 применили правило вывода 3);
6) ¬¬ x¬φ→¬ xφ ( к п.5 применили свойство контрапозиции);
7) x¬φ→¬¬ x¬φ (тавтология);
8) x¬φ→¬ xφ (к пп.7 и 6 применили свойство транзитивности).
Докажем эквивалентность 3΄). Построим квазивывод формулы
x(φ∧ψ)→ xφ∧ψ из Ø:
1) x(φ∧ψ)→φ∧ψ (схема аксиом 11);
2) φ∧ψ→φ (схема аксиом 3);
3) x(φ∧ψ)→φ (к пп.1 и 2 применили свойство транзитивности);
4) x(φ∧ψ)→ xφ (к п.3 применили правило вывода 2);
5) φ∧ψ→ψ (схема аксиом 4);
6) x(φ∧ψ)→ψ (к пп.1 и 5 применили свойство транзитивности);
7) ( x(φ∧ψ)→ xφ)→(( x(φ∧ψ)→ψ)→( x(φ∧ψ)→ xφ∧ψ)) (схема аксиом 5);
8) ( x(φ∧ψ)→ψ)→( x(φ∧ψ)→ xφ∧ψ) (к пп. 4 и 7 применили правило вывода 1);
9) x(φ∧ψ)→xφ∧ψ (к пп. 6 и 8 применили правило вывода 1).
Построим квазивывод формулы xφ∧ψ→ x(φ∧ψ) из Ø:
1. xφ∧ψ→ xφ (схема аксиом 3);
2. xφ→φ (схема аксиом 11);
3. xφ∧ψ→φ (к пп. 1 и 2 применили свойство транзитивности);
4. xφ∧ψ→ψ (схема аксиом 4);
5. ( xφ∧ψ→φ)→(( xφ∧ψ→ψ)→( xφ∧ψ→φ∧ψ)) (схема аксиом 5);
6. ( xφ∧ψ→ψ)→( xφ∧ψ→φ∧ψ) (к пп. 3 и 5 применили правило вывода 1);
7. xφ∧ψ→φ∧ψ (к пп. 4 и 5 применили правило вывода 1);
8. xφ∧ψ→ x(φ∧ψ) (к п. 6 применили правило вывода 2).
Теорема 2(о замене). Пусть φ ‑ формула ИПΣ, ψ ‑ ее подформула, φ' получается из φ заменой некоторого вхождения ψ на формулу ψ' ИПΣ и ψ≡ψ'. Тогда φ≡φ'.
Теорема 3. Для любой формулы φ ИПΣ существует ПНФ ψ, эквивалентная в ИПΣ формуле φ.