Deduction, D.Bonevac, Blackwell, 2nd edition, 2003; 8.3 problem 11

The task is to show that the given sequence (line 2) is a consequence of a formula. The formula is a translation of the English sentence: There is one and only one God. The conclusion (the given sequence) reads: Something that is a God has property 'F' if and only if anything that is a God has property 'F'. Perhaps the most valuable hints here are that: a) the universal quantifier on line 6 can be instantiated again, to a constant (here 'a') on line 11, and b) that the universal quantifier can be instantiated to the same constant (here 'a' on line 24 and 25) as the existential quantifier. Then it is just a matter of assuming a = a, without any justification. There is no reason to worry about using the same constant again after line 22 because all previous assumptions have been discharged.

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