I'm working through Paul Tomassi's Logic (here), and I'm attempting to prove the following sequent (Exercise 6.3, Question 10, p. 286):
∀y[Gy → Hy] : ∃x[Gx] → ∃y[Hy]
The catch is that the book hasn't yet given a rule for eliminating the existential quantifier. The approach I've been trying is to assume ∃x[Gx] for conditional proof and try to prove ∃y[Hy] from it, but I don't know how to make any progress if I can't eliminate the quantifier from ∃x[Gx].
The proof system is a Lemmon-style natural deduction system, with the rules:
- Conjunction introduction and elimination
- Disjunction introduction and elimination
- Modus ponens, modus tollens, conditional proof
- Biconditional introduction and elimination
- Double negation introduction and elimination
- Reductio ad absurdum
And:
- Universal quantifier introduction and elimination
- Existential quantifier introduction
Tomassi says the proof can be done in 7 lines, although I'm aware that that's very dependent on the specifics of the proof system. Any help appreciated!