Symbolic Logic, Irving M.Copi, Prentice Hall, 5th edition, 1973, p. 150, problem 9

The argument is set as follows:

There is exactly one penny in my right hand. There is exactly one penny in my left hand. Nothing is in both my hands. Therefore, there are exactly two pennies in my hands.

To prove it is not a challenge, to translate it into logical notation is.

1. (∃x){Px • Rx • (y)[(Py • Ry) ⊃y = x]}
2. (∃x){Px • Lx • (y)[(Py • Ly) ⊃y = x]}
3. ¬ (∃x)(Lx • Rx)
4. ∴(∃x)(∃y){Px • Py • Rx • Ly • ¬ (x = y) • (z){[Pz • (Rz ∨Lz)] ⊃z = x ∨z = y}}
5. * ¬ (∃x)(∃y){Px • Py • Rx • Ly • ¬ (x = y) • (z){[Pz • (Rz ∨Lz)] ⊃z = x ∨z = y}} ......... AIP
6. * (x)(y){[Px • Py • Rx • Ly • ¬ (x = y)] ⊃(∃z)[Pz • (Rz ∨Lz) • ¬ (z = x) • ¬ (z = y)]} ......... 5CQ
7. * Pa • Ra • (y)[(Py • Ry) ⊃y = a] ......... 1EI x/a
8. * Pm • Lm • (y)[(Py • Ly) ⊃y = m] ......... 2EI x/m
9. * (x)(Lx ⊃¬ Rx) ......... 3CQ
10. * Lm ⊃¬ Rm ......... 9UI x/m
11. * Lm ......... 8Simp.
12. * ¬ Rm ......... 11,10MP
13. * Ra ......... 7Simp.
14. * ¬ (a = m) ......... 12,13Id.
15. * Pa ......... 7Simp.
16. * Pm ......... 8Simp.
17. * Pa • Pm • Ra • Lm • ¬ (a = m) ......... 15,16,13,11Conj.
18. * (y){[Pa • Py • Ra • Ly • ¬ (a = y)] ⊃(∃z)[Pz • (Rz ∨Lz) • ¬ (z = a) • ¬ (z = y)] ......... 6UI x/a
19. * [Pa • Pm • Ra • Lm • ¬ (a = m)] ⊃(∃z)[Pz • (Rz ∨Lz) • ¬ (z = a) • ¬ (z = m)] ......... 18UI y/m
20. * (∃z)[Pz • (Rz ∨Lz) • ¬ (z = a) • ¬ (z = m)] ......... 17,19MP
21. * Pr • (Rr ∨Lr) • ¬ (r = a) • ¬ (r = m) ......... 20EI z/r
22. * (y)[(Py • Ry) ⊃y = a] ......... 7Simp.
23. * (Pr • Rr) ⊃r = a ......... 22UI y/r
24. * ¬ (r = a) ......... 21Simp.
25. * ¬ (Pr • Rr) ......... 23,24MT
26. * ¬ Pr ∨¬ Rr ......... 25DeM
27. * Pr ......... 21Simp.
28. * ¬ Rr ......... 27,26DS
29. * Rr ∨Lr ......... 21Simp.
30. * Lr ......... 28,29DS
31. * (y)[(Py • Ly) ⊃y = m] ......... 8Simp.
32. * (Pr • Lr) ⊃r = m ......... 31UI y/r
33. * Pr • Lr ......... 27,30Conj.
34. * r = m ......... 33,32MP
35. * ¬ (r = m) ......... 21Simp.
36. * r = m • ¬ (r = m) ......... 34,35Conj.
37. ¬ ¬ (∃x)(∃y){Px • Py • Rx • Ly • ¬ (x = y) • (z){[Pz • (Rz ∨Lz)] ⊃z = x ∨z = y}} ......... 5-36IP
38. (∃x)(∃y){Px • Py • Rx • Ly • ¬ (x = y) • (z){[Pz • (Rz ∨Lz)] ⊃z = x ∨z = y}} ......... 37DN