Deductive Logic, Warren Goldfarb, Hackett, 2003, Part IV, Ex. 5(b)

We set out to show that the following schema is valid using the laws of identity. Once an assumption has been made for indirect proof, we set up Modus Tollens to derive the identity 'a = m' on line 13. Next we continue instantiating line 5, which we stopped on line 7. Since the Convention says that the instantiating variable must be free or the instantiating constant must occur in the instantiating statement in at least all those places where the variable is free in the 'decapitated' general statement (see Suber, Copi), we are allowed to instantiate (z)(Gaz ⊃¬ Gzm) into Gaa ⊃¬ Gam. Then it is just a matter of replacing 'm' with 'a' on line 16 based on the previously derived identity.

1. (x)Gxx
2. (x)(y)[¬(x = y) ⊃(∃z)(Gxz • Gzy)
3. ∴(x)(y)(∃z)(Gxz • Gzy)
4. * ¬(x)(y)(∃z)(Gxz • Gzy) / AIP
5. * (∃x)(∃y)(z)(Gxz ⊃¬ Gzy) / 4CQ
6. * (∃y)(z)(Gaz ⊃¬ Gzy) / 5EI x/a
7. * (z)(Gaz ⊃¬ Gzm) / 6EI y/m
8. * (z)(¬Gaz ∨¬ Gzm) / 7MI
9. * (z) ¬ (Gaz • Gzm) / 8DeM
10. * ¬ (∃z)(Gaz • Gzm) / 9CQ
11. * (y)[¬(a = y) ⊃(∃z)(Gaz • Gzy) / 2UI x/a
12. * ¬ (a = m) ⊃(∃z)(Gaz • Gzm) / 11UI y/m
13. * a = m / 10,12MT
14. * Gaa / 1UI x/a
15. * Gaa ⊃¬ Gam / 7UI z/a
16. * ¬ Gam / 14,15MP
17. * ¬ Gaa / 13,16Id
18. * Gaa • ¬ Gaa / 14,17Conj.
19. ¬ ¬ (x)(y)(∃z)(Gxz • Gzy) / 4 - 18IP
20. (x)(y)(∃z)(Gxz • Gzy) / 19DN