# Natural deduction moving quantifiers I have difficulties proving with natural deduction the following:

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

Thanks for the help!

• I added a picture of what I've tried. I think somewhere i have to use the existential quantor elimination. I know how the rule works but i don't know how to apply it in this case. That's what I'm having problems with Jun 28 at 9:54
• I would suggest using LEM: $Ga \lor \lnot Ga$. Jun 30 at 7:20

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}