Natural deduction moving quantifiers

Question

I have difficulties proving with natural deduction the following:

$$Ga\rightarrow\exists xFx \vdash \exists x(Ga\rightarrow Fx)$$

Thanks for the help!

Answer 1

The idea is to first isolate $\exists x Fx$ from the hypothesis $Ga \to \exists x Fx$ to get rid of the existential quantifier in $\exists xFx$, and then reintroduce the existential quantifier outside of $Ga \to Fx$. Formally, the derivation in natural deduction has the form below.

\begin{align} \dfrac{ \dfrac{ Ga \to \exists x Fx \qquad Ga }{ \exists xFx }\to_\text{elim} \qquad \dfrac{\dfrac{[Fx]^*}{Ga \to Fx}\to_\text{intro} }{ \exists x (Ga \to Fx)}\exists_\text{intro}}{\exists x (Ga \to Fx) } \exists_\text{elim}^* \end{align}

But there is a problem! We added an hypothesis $Ga$ which we have not discharged. Thus, the derivation above actually proves that $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$.

The next step to answer your question is then to plug the derivation above into another derivation, so that we can discharge the further hypothesis $Ga$. The way to do that is quite technical, see below (the vertical dots stand for the derivation $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$ above).

\begin{align} \small \dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \dfrac{\dfrac{\dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \genfrac{}{}{0pt}{0}{\genfrac{}{}{0pt}{0}{Ga \to \exists x Fx, \ [Ga]^\circ}{\vdots}}{\exists x (Ga \to Fx)}}{\bot}\lnot_\text{elim}}{Fx}\text{efq}}{Ga \to Fx}\to_\text{intro}^\circ }{\exists x (Ga \to Fx)}\exists_\text{intro}}{\bot}\lnot_\text{elim} }{\exists x (Ga \to Fx)}\text{raa}^\bullet \end{align}