# Using existential instantiation (logic)

Am I using EI right on line 6? (Actually, I'm pretty sure the answer is 'no', and there's a few sketchy lines after that, too. So maybe you could also give a hint about how to do this).

Prove:

1. (∃x)(∀y)(Gxy → Hxy) (Premise)

2. (∀x)(∃y)￢Hxy (Premise)

    ∴ ￢(∀x)(∀y)Gxy

3. (∀y)(Gay → Hay) (1, Existential Instantiation)

4. Gab → Hab (3, Universal Instantiation)

5. (∃y)￢Hay (2, Universal Instantiation)

6. ￢Hab (5, Existential Instantiation)

7. ￢Gab (4, 6, Modus Tolens)

8. (∃y)￢Gay (7, Existential Generalization)

9. ￢(∀y)Gay (8, Quantifier Negation)

10. (∃x)￢(∀y)Gxy (9, Existential Generalization)

11. ￢(∀x)(∀y)Gxy (10, Quantifier Negation)

-
(6) is no good, because you introduced $b$ in (4). But you have essentially the right idea: just put (4) after (6)! – Zhen Lin Jul 27 '12 at 8:51
It would be very helpful if you tell explicitly in your question which system of logic you're working with, rather than leaving it to the reader to reconstruct it from abbreviated names of rules. – Henning Makholm Jul 28 '12 at 4:08