Symbolic Logic, Dale Jacquette, Wadsworth, 2001, Chapter 8, Ex. III, problem 9

Show that the following disjunction is a tautology. A disjunction is often easiest to prove by assuming the negation of one of the disjuncts. In this case it is also sensible to write the other disjunct at the bottom of the page and work backwards by simplifying, until we can see what it is that we are aiming to get. Then we make further assumptions: (x)Gx on line 8 and (x)Fx on line 17.

(∃x)(Fx ≡ ¬ Gx) ∨[(∃x) ¬ Fx ≡ (∃x) ¬ Gx]

1. * ¬ (∃x)(Fx ≡ ¬ Gx) / ACP
2. * (x) ¬ (Fx ≡ ¬ Gx) / 1QC
3. * (x) ¬ [(Fx ⊃¬ Gx) • (¬ Gx ⊃Fx)] / 2BE
4. * ¬ [(Fx ⊃¬ Gx) • (¬ Gx ⊃Fx)] / 3UI x/x
5. * ¬ (Fx ⊃¬ Gx) ∨¬ (¬ Gx ⊃Fx) / 4DeM
6. * (Fx ⊃¬ Gx) ⊃(¬ Gx • ¬ x) / 5MI
7. * (Fx ⊃¬ Gx) ⊃¬ (Gx ∨Fx) / 6DeM
8. * * (x)Gx / ACP
9. * * Gx / 8UI x/x
10. * * Gx ∨Fx / 9Add.
11. * * ¬ (Fx ⊃¬ Gx) / 10,7MT
12. * * ¬ (¬ Fx ∨¬ Gx) / 11MI
13. * * Fx • Gx / 12DeM
14. * * Fx / 13 Simp.
15. * * (x)Fx / 14UG
16. * (x)Gx ⊃(x)Fx / 8-15CP
17. * * (x)Fx /ACP
18. * * Fx / 17UI x/x
19. * * Fx ∨Gx / 18Add.
20. * * Gx ∨Fx / 19Comm.
21. * * ¬ (Fx ⊃¬ Gx) / 20,7MT
22. * * ¬ (¬ Fx ∨¬ Gx) / 21MI
23. * * Fx • Gx / 22DeM
24. * * Gx / 23Simp.
25. * * (x)Gx / 24UG
26. * (x)Fx ⊃(x)Gx / 17-25CP
27. * ¬ (x)Fx ⊃¬ (x)Gx / 16Contrap.
28. * (∃) ¬ Fx ⊃(∃x) ¬ Gx / 27QC
29. * ¬ (x)Gx ⊃¬ (x)Fx / 26 Contrap.
30. * (∃) ¬ Gx ⊃(∃x) ¬ Fx / 29QC
31. * [(∃) ¬ Fx ⊃(∃x) ¬ Gx] • [ (∃) ¬ Gx ⊃(∃x) ¬ Fx] / 28,30Contrap.
32. * (∃x) ¬ Fx ≡ (∃x) ¬ Gx / 31BE
33. ¬ (∃x)(Fx ≡ ¬ Gx) ⊃[(∃x) ¬ Fx ≡ (∃x) ¬ Gx] / 1-32CP
34. ¬ ¬ (∃x)(Fx ≡ ¬ Gx) ∨[(∃x) ¬ Fx ≡ (∃x) ¬ Gx] / 33MI
35. (∃x)(Fx ≡ ¬ Gx) ∨[(∃x) ¬ Fx ≡ (∃x) ¬ Gx] / 34DN