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

We are to show by deduction, using the laws of identity, that the following formula: (∃x)Fxy • (x) ¬ Fxz implies: ¬ (z = y). If we first assume z = y by indirect proof, then drop the quantifiers in the premise, we will obtain Fay and ¬ Faz. Substituting 'y' for 'z', or the other way round, we will obtain a contradiction, which will prove that ¬ (z = y) does indeed follow from the original premise. However, if we choose not to use the laws of identity (below), we must be careful to generalize by UG the free variables 'y' and 'z' first before we use indirect proof. Doing things in reverse order will mean we have to generalize them within the assumption, which will violate the rule which says that we can't generalize within the scope of an assumption if the instantiating variable occurs free in the first line of the sequence.

1. (∃x)Fxy • (x) ¬ Fxz
2. ∴¬ (z = y)
3. (∃x)Fxy / 1Simp.
4. (y)(∃x)Fxy / 3UG y/y
5. (x) ¬ Fxz / 1Simp.
6. (z)(x) ¬ Fxz / 5UG z/z
7. * z = y / AIP
8. * (∃x)Fxm / 4UI y/m
9. * (x) ¬ Fxm / 6UI z/m
10. * Fam / 8EI x/a
11. * ¬ Fam / 9EI x/a
12. * Fam • ¬ Fam / 10,11Conj.
13. ¬ (z = y) / 7 - 12IP