3
$\begingroup$

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!

$\endgroup$
0

1 Answer 1

Reset to default
1
$\begingroup$

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}

$\endgroup$
7
  • $\begingroup$ @PédeLeão You're welcome! I've seen other answers from you and I can tell you're really good at logic. Keep up the good work! :) $\endgroup$
    – Bram28
    Jul 15, 2017 at 15:00
  • $\begingroup$ Can you prove you need to use EE (which has indeed not been introduced yet at that point)? $\endgroup$
    – Henno Brandsma
    Jul 16, 2017 at 9:13
  • $\begingroup$ Why are 6 and 7 repeated? why not save one step? $\endgroup$
    – Henno Brandsma
    Jul 16, 2017 at 9:14
  • $\begingroup$ @HennoBrandsma 6 and 7 ate different actually. 6 says rhat the statement is a consequence of sratements 1 and 3, while 7 says that the statement is a consequence of 1 and 2. IN a Fitch proof one would be inside a subproof while the other one would be outside that subproof $\endgroup$
    – Bram28
    Jul 16, 2017 at 11:29
  • $\begingroup$ @Bram28 Thanks for another answer! I was worried I was missing a possible proof without existential elimination, but it seems not. I've marked this as the answer, but let me know if you do see some way of doing it without EE. I'm interested in Henno Brandsma's first question too: can we be totally certain that EE is required? Do we know it is required just because we can't find any proof that doesn't use it, or is there some way of seeing why any proof of the sequent must go via EE? Thanks :) $\endgroup$
    – Dlogic
    Jul 16, 2017 at 20:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .