Deduction, Daniel Bonevac, Blackwell Publishing, 2003, 8.3, Problem 14

As in earlier problems in this section (11, 12, 13), we show that the implication holds. The overall strategy is to show that the biconditional in the conclusion holds both ways, so we prove each implication separately and conjoin them on line 48. After making the first assumption on line 3 we might be tempted to carry on and assume Fa on line 4 in order to bring us faster to the conclusion. However, we have already introduced Fa on line 3 and repeating it would be a violation. Instead, it is better to assume the negation of (∃x)(Gx • Hx) and then show that we can obtain the negation of Fa. Since it is an implication, we swap round the sides by contraposition and arrive at the desired conclusion on line 20. Likewise, in the second set of assumptions further down, the conclusion has been negated - this time to obtain a contradiction.

1. (∃x)(y)(y = x ≡ Gy)
2. ∴ (∃x)[Gx • (Fa ⊃Hx)] ≡ [Fa ⊃(∃x)(Gx • Hx)]
3. * (∃x)[Gx • (Fa ⊃Hx)] / ACP
4. * * ¬ (∃x)(Gx • Hx) / ACP
5. * * (x)(Gx ⊃¬ Hx) / 4QC
6. * * Gr • (Fa ⊃Hr) / 3EI x/r
7. * * (y)(y = m ≡ Gy) / 1EI x/m
8. * * r = m ≡ Gr / 7UI y/r
9. * * (r = m ⊃ Gr) • (Gr ⊃r = m) / 8BE
10. * * Gr ⊃r = m / 9Simp.
11. * * Gr / 6Simp.
12. * * r = m / 11,10MP
13. * * Gm ⊃¬ Hm / 5UI x/m
14. * * Gm / 12,11Id
15. * * ¬ Hm / 14,13MP
16. * * ¬ Hr / 12,15Id
17. * * Fa ⊃Hr / 6Simp.
18. * * ¬ Fa / 16,17MT
19. * ¬ (∃x)(Gx • Hx) ⊃¬ Fa / 4-18ACP
20. * Fa ⊃(∃x)(Gx • Hx) / 19Contrap.
21. (∃x)[Gx • (Fa ⊃Hx)] ⊃[Fa ⊃(∃x)(Gx • Hx)] / 3-20CP
22. * Fa ⊃(∃x)(Gx • Hx) / ACP
23. * * ¬ (∃x)[Gx • (Fa ⊃Hx)] / AIP
24. * * (x)[Gx ⊃(Fa • ¬ Hx)] / 23QC
25. * * (y)(y = m ≡ Gy) / 1EI x/m
26. * * m = m ≡ Gm / 25UI y/m
27. * * (m = m ⊃Gm) • (Gm ⊃m = m) / 26BE
28. * * m = m ⊃Gm / 27Simp.
29. * * m = m / Id
30. * * Gm / 29,28MP
31. * * Gm ⊃(Fa • ¬ Hm) / 24UI x/m
32. * * Fa • ¬ Hm / 30,31MP
33. * * Fa / 32Simp.
34. * * (∃x)(Gx • Hx) / 22,33MP
35. * * Gr • Hr / 34EI x/r
36. * * r = m ≡ Gr / 25UI y/r
37. * * (r = m ⊃Gr) • (Gr ⊃r = m) / 36BE
38. * * Gr ⊃r = m / 37Simp.
39. * * Gr / 35Simp.
40. * * r = m / 38,39MP
41. * * Hr / 35Simp.
42. * * Hm / 40, 41Id
43. * * ¬ Hm / 32Simp.
44. * * Hm • ¬ Hm / 42,43Conj.
45. * ¬ ¬ (∃x)[Gx • (Fa ⊃Hx)] / 23-44IP
46. * (∃x)[Gx • (Fa ⊃Hx)] / 45DN
47. [Fa ⊃(∃x)(Gx • Hx)] ⊃(∃x)[Gx • (Fa ⊃Hx)] / 23-46CP
48. {(∃x)[Gx • (Fa ⊃Hx)] ⊃[Fa ⊃(∃x)(Gx • Hx)]} • {[Fa ⊃(∃x)(Gx • Hx)] ⊃(∃x)[Gx • (Fa ⊃Hx)]} / 21,47Conj.
49. (∃x)[Gx • (Fa ⊃Hx)] ≡ [Fa ⊃(∃x)(Gx • Hx)] / 48BE