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

We are to show that the following formula is a tautology. A useful hint here is that before we instantiate line 2 by universal instantiation, we should first instantiate our assumption by egistential instantiation on line 3, into the constant 'a', or any other. This ensures that the procedure is valid. We assume on line 1 a non-negated disjunct in anticipation of the fact that once we discharge the assumption we will be easily able to turn a conditional into a disjunct by conditional exchange (or material implication) on the last line of the proof.

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

1. * (x)(Fx ≡ Gx) / ACP
2. * (x)[(Fx ⊃Gx) • (Gx ⊃Fx)] / 1BE
3. * * (∃x)Fx / ACP
4. * * Fa / 3EI
5. * * (Fa ⊃Ga) • (Ga ⊃Fa) / 2UI
6. * * Fa ⊃Ga / 5Simp.
7. * * Ga / 4,6MP
8. * * (∃x)Gx / 7EG
9. * (∃x)Fx ⊃(∃x)Gx / 3-8CP
10. * * (∃x)Gx / ACP
11. * * Gm / 10EI
12. * * (Fm ⊃Gm) • (Gm ⊃Fm) / 2UI
13. * * Gm ⊃Fm / 12Simp.
14. * * Fm / 11,13MP
15. * * (∃x)Fx / 14EG
16. * (∃x)Gx ⊃(∃x)Fx / 10-15CP
17. * [(∃x)Fx ⊃(∃x)Gx] • [(∃x)Gx ⊃(∃x)Fx] / 9,16Conj.
18. * (∃x)Fx ≡ (∃x)Gx / 17BE
19. (x)(Fx ≡ Gx) ⊃[(∃x)Fx ≡ (∃x)Gx ] / 1-18CP
20. ¬ (x)(Fx ≡ Gx) ∨[(∃x)Fx ≡ (∃x)Gx] / 19CE