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!
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}