Пусть Φ, Ψ — формулы исчисления высказываний. Построить вывод формулы исчисления высказываний из данного множества гипотез:
Φ∧Ψ⊢Φ∧(¬Φ∨Ψ).
Решение
Придерживаемся следующей аксиоматики (Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. — 5-е изд., исправл., — М.: ФИЗМАТЛИТ, 2004. — 256 с., стр. 65):
Также потребуется дополнительное правило силлогизма: A→B, B→C⊢A→C.
A→B→A→B→C→A→C — аксиома 2,
A→B — гипотеза,
A→B→C→A→C — из (1) и (2) по правилу modus ponens,
B→C→A→B→C — аксиома 1,
B→C — гипотеза,
A→B→C — из (4) и (5) по правилу modus ponens,
A→C — из (3) и (6) по правилу modus ponens.
Теперь докажем требуемое.
Φ∧Ψ→Φ — аксиома 3,
Φ∧Ψ→Ψ — аксиома 4,
Ψ→¬Φ∨Ψ — аксиома 7,
Φ∧Ψ→¬Φ∨Ψ — из (2) и (3) по правилу силлогизма,
Φ∧Ψ→Φ→Φ∧Ψ→¬Φ∨Ψ→Φ∧Ψ→Φ∧(¬Φ∨Ψ) —аксиома 5,
Φ∧Ψ→¬Φ∨Ψ→Φ∧Ψ→Φ∧(¬Φ∨Ψ) — из (5) и (1) по правилу modus ponens,
Φ∧Ψ→Φ∧(¬Φ∨Ψ) — из (6) и (4) по правилу modus ponens,
Φ∧Ψ — гипотеза,
Φ∧(¬Φ∨Ψ) —из (7) и (8) по правилу modus ponens.