Deduction, Daniel Bonevac, Blackwell Publishing, 2003, 8.3 problem 16, p. 238

We can say in symbolic terms - according to the instructions to this problem - that there is one and only one God: (∃x)(y)(y = x ≡ Gy). We can further show that the following is a consequence of this formula: (∃x)(Gx • ¬ Fx) ≡ (x)(Gx ⊃¬ Fx). Since the conclusion is an equivalence, we need to prove it for two cases. A conditional proof is required in each case (twice in the first case). The hardest part, as usual, is being able to spot that we have to instantiate the same proposition more than once.

1. (∃x)(y)(y = x ≡ Gy)
2. ∴(∃x)(Gx • ¬ Fx) ≡ (x)(Gx ⊃¬ Fx)
3. CASE 1: (∃x)(Gx • ¬ Fx) ⊃ (x)(Gx ⊃¬ Fx)
4. * (∃x)(Gx • ¬ Fx) ......... ACP
5. * Ga • ¬ Fa ......... 4EI x/a
6. * (y)(y = m ≡ Gy) ......... 1EI x/m
7. * * Gx ......... ACP
8. * * x = m ≡ Gx ......... 6UI y/x
9. * * (x = m ⊃ Gx) • (Gx ⊃x = m) ......... 8BE
10. * * a = m ≡ Ga ......... 6UI y/a
11. * * (a = m ⊃ Ga) • (Ga ⊃a = m) ......... 10BE
12. * * Gx ⊃x = m ......... 9Simp.
13. * * x = m ......... 7,12MP
14. * * Ga ⊃a = m ......... 11Simp.
15. * * Ga ......... 5Simp.
16. * * a = m ......... 15,14MP
17. * * m = a ......... 16Comm.
18. * * x = a ......... 13,17Id
19. * * ¬ Fa ......... 5Simp.
20. * * ¬ Fx ......... 18,19Id
21. * Gx ⊃¬ Fx ......... 7-20CP
22. * (x)(Gx ⊃¬ Fx) ......... 21UG
23. (∃x)(Gx • ¬ Fx) ⊃ (x)(Gx ⊃¬ Fx) ......... 4-22CP
24. CASE 2: (x)(Gx ⊃¬ Fx) ⊃(∃x)(Gx • ¬ Fx)
25. * (x)(Gx ⊃¬ Fx) ......... ACP
26. * (y)(y = a ≡ Gy) ......... 1EI x/a
27. * a = a ≡ Ga ......... 26UI y/a
28. * (a = a ⊃ Ga) • (Ga ⊃a = a) ......... 27BE
29. * a = a ......... Id
30. * a = a ⊃ Ga ......... 28Simp.
31. * Ga ......... 29,30MP
32. * Ga ⊃¬ Fa ......... 25UI x/a
33. * ¬ Fa ......... 31,32MP
34. * Ga • ¬ Fa ......... 31,33Conj.
35. * (∃x)(Gx • ¬ Fx) ......... 34EG
36. (x)(Gx ⊃¬ Fx) ⊃(∃x)(Gx • ¬ Fx) ......... 25-35CP
37. [(∃x)(Gx • ¬ Fx) ⊃ (x)(Gx ⊃¬ Fx)] • [(x)(Gx ⊃¬ Fx) ⊃(∃x)(Gx • ¬ Fx)] ......... 23,36Conj.
38. (∃x)(Gx • ¬ Fx) ≡ (x)(Gx ⊃¬ Fx) ......... 37BE