TITLE: Predicate logic natural deduction - proving conditional without existential elimination
QUESTION [3 upvotes]: 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!

REPLY [1 votes]: Here is an 8 line proof using Tomassi's proof system ... maybe Tomassi meant 7 steps ...
And you're right, you need to use EE ...
\begin{array}{llll}
& \{1\} & 1. & \forall y \ [Gy \to Hy] & \text{ Premise }\\
& \{2\} & 2. & \exists x \ [Gx] & \text{ Assumption for CP }\\
& \{3\} & 3. & Ga & \text{ Assumption for EE }\\
& \{1\} & 4. & Ga \to Ha & \text{ 1 UE }\\
& \{1,3\} & 5. & Ha & \text{ 3,4 MP }\\
& \{1,3\} & 6. & \exists y \ [Hy] & \text{ 5 EI }\\
& \{1,2\} & 7. & \exists y \ [Hy] & \text{ 2,3,6 EE }\\
& \{1\} & 8. & \exists x\ [Gx] \to \exists y[Hy] & \text{ 2,7 CP }\\
\end{array}
{"set_name": "stack_exchange", "score": 3, "question_id": 2359123}