A Concise Introduction to Logic, Patrick J. Hurley, Wadsworth, 2006, 9th ed,. 8.7, III, 11 p. 448

There are at least two philosophers in the library. Robert is the only French philosopher in the library. Therefore, there is a philosopher in the library who is not French. (Px: x is a philosopher; Lx: x is in the library; Fx: x is French; r: r is Robert)

1.     (∃x)(∃y)(Px • Lx • Py • Ly • x ≠ y) 2.     Pr • Fr • Lr • (x)[(Px • Fx • Lx) ⊃ x = r] ∴ (∃x)(Px • Lx • ~ Fx) 3.     ~ (∃x)(Px • Lx • ~ Fx) 4.     (x)~ (Px • Lx • ~ Fx) 5.     (x)[~ (Px • Lx) v Fx] 6.     (x)[( Px • Lx) ⊃ Fx] 7.     (∃y)(Pm • Lm • Py • Ly • m ≠ y) 8.     Pm • Lm • Pq • Lq • m ≠ q 9.     (Pm • Lm) ⊃ Fm 10. Pm • Lm 11. Fm 12. (x)[(Px • Fx • Lx) ⊃ x = r] • Pr • Fr • Lr 13. (x)[(Px • Fx • Lx) ⊃ x = r] 14. (Pm • Fm • Lm) ⊃ m = r 15. Pm • Lm • Fm 16. Pm • Fm • Lm 17. m = r 18. (Pq • Fq • Lq) ⊃ q = r 19. (Pq • Lq) ⊃ Fq 20. Pq • Lq • Pm • Lm • m ≠ q 21. Pq • Lq 22. Fq 23. Pq • Lq • Fq 24. Pq • Fq • Lq 25. q = r 26. r = q 27. m = q 28. m ≠ q • Pq • Lq • Pm • Lm 29. m ≠ q 30. m ≠ q • m = q 31. ~ ~ (∃x)(Px • Lx • ~ Fx) 32. (∃x)(Px • Lx • ~ Fx)

AIP 3 QC 4 DM 5 Impl 1 EI 7 EI 6 UI 8 Simp 9,10 MP 2 Com 12 Simp 13 UI 10,11 Conj 15 Com 14,16 MP 13 UI 6 UI 8 Com 20 Simp 19,21 MP 21,22 Conj 23 Com 18,24 MP 25 Com 17,26 Id 20 Com 28 Simp 27, 29 Conj 3-30 IP 31 DN