Теорема 1(о дедукции). Пусть φ1,…,φm,φ,ψ – формулы ИВ. Тогда φ1,…,φm,φ⊢ψ φ1,…,φm,⊢φ→ψ.
Пример 4. Покажем, что φ→ψ⊢¬ψ→¬φ;
Решение.По теореме о дедукции
φ→ψ⊢¬ψ→¬φ φ→ψ, ¬ψ⊢¬φ.
Строим вывод формулы ¬φ из формул φ→ψ,¬ψ:
1) φ→ψ (гипотеза);
2) ¬ψ (гипотеза);
3) (φ→ψ)→((φ→¬ψ)→¬ψ) (схема аксиом 9);
4) (φ→¬ψ)→¬φ (к пп. 1 и 3 применили правило вывода);
5) ¬ψ→(φ→¬ψ) (схема аксиом 1);
6) φ→¬ψ (к пп. 2 и 5 применили правило вывода);
7) ¬φ (к пп. 6 и 4 применили правило вывода).
Пример 5.Покажем, что φ→(ψ→χ)⊢ψ→(φ→χ)
Решение. По теореме о дедукции
φ→(ψ→χ)⊢ψ→(φ→χ) φ→(ψ→χ),ψ⊢(φ→χ) φ→(ψ→χ),ψ,φ⊢χ.
Строим вывод формулы χ из формул φ→(ψ→χ),ψ,φ:
1) φ→(ψ→χ) (гипотеза);
2) φ (гипотеза);
3) ψ (гипотеза);
4) ψ→χ (к пп. 2 и 1 применили правило вывода);
5) χ (к пп. 3 и 4 применили правило вывода).