Understanding Symbolic Logic, V. Klenk, Prentice Hall 2008, Unit 18, Ex.1(o)

1. (x)[(Px • ¬ Rxx) ⊃(y)(Py ⊃¬ Ryx)]
2. (x){Px ⊃ (y)[(Py • ¬ Rxy) ⊃¬ Hxy]}
3. ∴(x){[Px • (y)(Py ⊃¬ Rxy)] ⊃¬ (∃z)(Pz • Hzx)}
4. * Px • (y)(Py ⊃¬ Rxy) / ACP
5. * Px / 4 Simp
6. * (y)(Py ⊃¬ Rxy) / 4 Simp
7. * Px ⊃¬ Rxx / 6 UI
8. * ¬ Rxx / 5, 7 MP
9. * Px • ¬ Rxx / 5, 8 Conj
10. * (Px • ¬ Rxx) ⊃(y)(Py ⊃¬ Ryx) / 1 UI
11. * (y)(Py ⊃¬ Ryx) / 9, 10 MP
12. * * Pz / ACP
13. * * Pz ⊃¬ Rzx / 11 UI
14. * * ¬ Rzx / 12, 13 MP
15. * * Pz ⊃(y)[(Py • ¬ Rzy) ⊃¬ Hzy] / 2 UI
16. * * (y)[(Py • ¬ Rzy) ⊃¬ Hzy] / 12, 15 MP
17. * * (Px • ¬ Rzx) ⊃¬ Hzx / 16 UI
18. * * Px • ¬ Rzx / 5, 14 Conj
19. * * ¬ Hzx / 17, 18 MP
20. * Pz ⊃¬ Hzx / 12 - 19 CP
21. * (z)(Pz ⊃¬ Hzx) / 20 UG
22. * ¬ (∃z)(Pz • Hzx) / CQ
23. [Px • (y)(Py ⊃¬ Rxy)] ⊃¬ (∃z)(Pz • Hzx) / 4 - 22 CP
24. (x){[Px • (y)(Py ⊃¬ Rxy)] ⊃¬ (∃z)(Pz • Hzx)} / 23 UG

Comment

This deduction calls for multiple variable rewrite, including on lines 7, 13, and 17.

This is the first in my series of worked solutions to deduction problems left unanswered in logic course books. The aim is strictly educational and the answers are meant to help those who study on their own.

I haven’t worked out yet how to use the blogger tools to show the scope of assumptions in the way I find most clear – by indentation, or how to show step descriptions to the right of my work. So until I do that, I mark the scope of each new assumption with a star (*) to the left of the assumption, and separate the step descriptions with a forward stroke. It looks messy but I'd rather explain what I am doing on the line I'm doing it than add the comments below or not at all. When an assumption is discharged, the star is taken off. Most other notation is pretty standard. CP stands for discharge of conditional proof, CQ - change of quantifier (justified by one of the four equivalences).