Утверждение 3.Пусть φ,ψ, χ – формулы ИВ. Тогда
1) ⊢φ→φ;
2) φ∧ψ⊢φ;
3) φ∧ψ⊢ψ;
4) φ,ψ⊢φ ψ;
5) φ→ψ, ψ→χ⊢φ→χ (свойство транзитивности);
6) φ→(ψ→χ)≡ψ→(φ→χ) (свойство перестановочности посылок);
7) φ→(ψ→χ)≡φ∧ψ→χ (свойство соединения и разъединения посылок);
8) φ→ψ≡¬ψ→¬φ (свойство контрапозиции).
Доказательство. Пункты 1, 4, 6, 8 доказаны в примерах 13, 14, 16, 17.
Докажем пункт 7. Покажем, что φ→(ψ→χ)⊢φ ψ→χ. По теореме о дедукции
φ→(ψ→χ)⊢φ ψ→χ φ→(ψ→χ), φ ψ⊢χ.
Строим вывод формулы χ из формул φ→(ψ→χ), φ ψ:
1) φ→(ψ→χ) (гипотеза);
2) φ ψ (гипотеза);
3) φ ψ→φ (схема аксиом 3);
4) φ (к пп. 2 и 4 применили правило вывода);
5) φ ψ→ψ (схема аксиом 4);
6) ψ (к пп. 2 и 5 применили правило вывода);
7) ψ→χ (к пп. 4 и 1 применили правило вывода);
8) χ (к пп. 6 и 7 применили правило вывода).
Покажем, что φ ψ→χ⊢φ→(ψ→χ). По теореме о дедукции
φ ψ→χ⊢φ→(ψ→χ) φ ψ→χ, φ⊢φ→χ φ ψ→χ, φ, ψ⊢χ.
Строим квазивывод формулы χ из формул φ ψ→χ, φ, ψ:
1) φ ψ→χ (гипотеза);
2) φ (гипотеза);
3) ψ (гипотеза);
4) φ ψ (к п.п. 2 и 3 применили свойство 4);
5) χ (к пп. 4 и 1 применили правило вывода).