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

Prove the theorem. There is more than one way of doing it. If we go past the contradiction on line 16, we can bring in just about any statement, including (x)Fxx, because anything follows from a contradiction.

(x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] ⊃(x)Fxx

1. * (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] / ACP
2. * * ¬ (x)Fxx / AIP
3. * * (∃x) ¬ Fxx / 2QC
4. * * ¬ Faa / 3EI x/a
5. * * (y)[Fay ≡ (z)(Gaz ≡ Gyz)] / 1UI x/a
6. * * Faa ≡ (z)(Gaz ≡ Gaz) / 5UI y/a
7. * * [Faa ⊃(z)(Gaz ≡ Gaz)] • [(z)(Gaz ≡ Gaz) ⊃Faa] / 6BE
8. * * (z)(Gaz ≡ Gaz) ⊃Faa / 7Simp.
9. * * ¬ (z)(Gaz ≡ Gaz) / 4,8MT
10. * * (∃z) ¬ (Gaz ≡ Gaz) / 9QC
11. * * (∃z) ¬ [(Gaz ⊃ Gaz) • [(Gaz ⊃ Gaz)] / 10BE
12. * * ¬ [(Gam ⊃ Gam) • [(Gam ⊃ Gam)] / 11EI z/m
13. * * ¬ (Gam ⊃ Gam) ∨ ¬ [(Gam ⊃ Gam)] / 12DeM
14. * * ¬ (Gam ⊃ Gam) / 13Tuatology
15. * * ¬ (¬ Gam ∨ Gam) / 14MI
16. * * Gam • ¬ Gam / 15DeM
17. * * Gam / 16Simp.
18. * * Gam ∨¬ (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] / 17Add.
19. * * ¬ Gam / 16Simp.
20. * * ¬ (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] / 19,18DS
21. * ¬ (x)Fxx ⊃¬ (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] / 2-20IP
22. * (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] ⊃(x)Fxx / 21Contrap.
23. * (x)Fxx / 1,22MP
24. (x)(y)[Fxy ≡ (z)(Gxz ≡ Gyz)] ⊃(x)Fxx / 1-23CP