Using $\exists$ Elimination rule to prove an argument (Fitch-style)

first-order-logiclogicnatural-deduction

Trying to prove an exercise of P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 287, exercise C Ferio Argument), I came up with an error on application of $\exists$ Elimination:

enter image description here

On the book appears rule definition:

enter image description here

$c$ does not occur in any undischarged assumption in my proof, so what would be the problem with its application ?

Best Answer

$a$ does not occur in any undischarged assumption, but in $\mathcal{B} : Ha \land \neg Fa$, which is also not allowed according to the $\exists E$ rule specification.
So at the point where you leave the subproof and do an existential elimination, $a$ must already have been converted into a bound variable.

The solution is to prepone the $\exists I$ on line 10 to inside the subproof to get a conclusion in which $a$ no longer occurs, and then apply $\exists E$ on that existential conclusion as the very last step: 

...
 8 | | Ha ^ Fa       ^I, 4,7
 9 | | ∃x(Hx ^ Fx)   ∃I, 8
10 | ∃x(Hx ^ Fx)     ∃E, 2,3-9

As a rule of thumb, it often is the case that $\exists E$ is (or can be made) the last step in a natural deduction proof.

Related Question