Пусть Φ, Ψ — формулы исчисления предикатов. Построить вывод формулы исчисления предикатов из данного множества гипотез.
∃x(Φ(x)→Ψ(x))⊢∀ Φ(x)→∃yΨ(y).
Решение
Придерживаемся следующей аксиоматики (Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. — 5-е изд., исправл., — М.: ФИЗМАТЛИТ, 2004. — 256 с., стр. 91):
Ψ(x)→∃yΨ(y) — аксиома 12,
∀xΨ(x)→Ψ(x) — аксиома 11,
∀xΨ(x)→∃yΨ(y) — из (1) и (2) по правилу modus ponens,
Φ(x,y)→∃zΦ(z,y) — аксиома 12 (с учётом оговоренных условий),
∃zΦ(z,y)→∃x∃zΦ(z,x) — аксиома 12 (с учётом оговоренных условий),
Φ(x,y)→∃x∃zΦ(z,x) — из (4) и(5) по правилу силлогизма,
∃x∃zΦ(z,x)→ ∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 6,
Φ(x,y)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (6) и(7) по правилу силлогизма,
Ψ(x)→∃xΨ(x) — аксиома 12 (с учётом оговоренных условий),
∃xΨ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 7,
Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (9) и(10) по правилу силлогизма,
Φ(x,y)→∃x∃zΦ(z,x)∨∃xΨ(x)→Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x)→Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 8,
Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x)→Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (12) и (8) по правилу modus ponens,
Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (13) и (11) по правилу modus ponens,
∃x∃zΦ(z,x)∨∃xΨ(x) — из (14) и (3) по правилу modus ponens.