Deductive Logic, Warren Goldfarb, Hackett, 2003, Part IV, Ex. 13(a-b)

Russell's way of expressing definite descriptions was: (∃x)[Fx • (y)(Fy ⊃y = x)]; Quine preferred (∃x)(y)(Fy ≡ x = y). They are equivalent. We show this by first working one way and then the other (line 26). The equivalence is expressed as a conjunction of two conditionals (line2), then each conditional is proved separately. There are other ways of proving this equivalence - for one we could have condensed lines 28-34 using pre-nex rules rather than my cumbersome instantiation, then generalization, then instantiation again, but I have done it to show that it is possible. We can generalize within an assumption as long as the variable we generalize from is not free on the first line of the assumption.

1. (∃x)[Fx • (y)(Fy ⊃y = x)] ≡ (∃x)(y)(Fy ≡ x = y)
2. {(∃x)[Fx • (y)(Fy ⊃y = x)] ⊃(∃x)(y)(Fy ≡ x = y)} • {(∃x)(y)(Fy ≡ x = y) ⊃ (∃x)[Fx • (y)(Fy ⊃y = x)]} / 1BE
3. (∃x)[Fx • (y)(Fy ⊃y = x)] ⊃ (∃x)(y)(Fy ≡ x = y) / 2Simp.
4. * (∃x)[Fx • (y)(Fy ⊃y = x)] / ACP
5. * * ¬ (∃x)(y)(Fy ≡ x = y) / AIP
6. * * (x)(∃y) ¬ (Fy ≡ x = y) / 5CQ
7. * * (x)(∃y) ¬ [(Fy ⊃x = y) • (x = y ⊃Fy)] / 6BE
8. * * Fa • (y)(Fy ⊃y = a) / 4EI x/a
9. * * Fa / 8Simp.
10. * * (y)(Fy ⊃y = a) / 8Simp.
11. * * (∃y) ¬ [(Fy ⊃a = y) • (a = y ⊃Fy)] / 7UI x/a
12. * * ¬ [(Fm ⊃a = m) • (a = m ⊃Fm)] / 11EI y/m
13. * * ¬ (Fm ⊃a = m) ∨¬ (a = m ⊃Fm)] / 12DeM
14. * * Fm ⊃m = a / 10UI y/m
15. * * Fm ⊃a = m / 14Id
16. * * ¬ (a = m ⊃Fm) / 15,14DS
17. * * ¬ [¬ (a = m) ∨Fm] / 16MI
18. * * a = m • ¬ Fm / 17DeM
19. * * ¬ Fm / 18Simp.
20. * * ¬ (a = m) / 9,19Id
21. * * a = m / 18 Simp.
22. * * a = m • ¬ (a = m) / 20,21Conj.
23. * ¬ ¬ (∃x)(y)(Fy ≡ x = y) / 5 - 22IP
24. * (∃x)(y)(Fy ≡ x = y) / 23DN
25. (∃x)[Fx • (y)(Fy ⊃y = x)] ⊃ (∃x)(y)(Fy ≡ x = y) / 4 - 24CP
26. (∃x)(y)(Fy ≡ x = y) ⊃ (∃x)[Fx • (y)(Fy ⊃y = x)] / 2Simp.
27. * (∃x)(y)(Fy ≡ x = y) / ACP
28. * (y)(Fy ≡ a = y) / 27EI x/a
29. * Fy ≡ a = y / 28UI y/y
30. * (Fy ⊃ a = y) • (a = y ⊃Fy) / 29BE
31. * Fy ⊃ a = y / 30Simp.
32. * (y)(Fy ⊃ a = y) / 31UG
33. * a = y ⊃Fy / 30Simp.
34. * (y)(a = y ⊃Fy) / 33UG
35. * a = a ⊃Fa / 34UI y/a
36. * a = a / Id
37. * Fa / 36,35MP
38. * Fa • (y)(Fy ⊃a = y) / 37,32Conj.
39. * (∃x)[Fx • (y)(Fy ⊃x = y)] / 36EG
40. (∃x)(y)(Fy ≡ x = y) ⊃ (∃x)[Fx • (y)(Fy ⊃y = x)] / 27 - 39CP
41. {(∃x)[Fx • (y)(Fy ⊃y = x)] ⊃(∃x)(y)(Fy ≡ x = y)} • {(∃x)(y)(Fy ≡ x = y) ⊃ (∃x)[Fx • (y)(Fy ⊃y = x)]} / 25,40Conj.
42. (∃x)[Fx • (y)(Fy ⊃y = x)] ≡ (∃x)(y)(Fy ≡ x = y) / 41BE