Is this natural deduction proof of $\exists x Fx \to G \vdash \forall x [Fx \to G]$ in predicate logic correct?

Question

Like the title says, is this correct?

Edit I left out a big detail: G is a closed formula (meaning it does not contain x as a free variable).

Answer 1

Your proof is incorrect. For one, notice the difference between the scopes of the quantifiers in your conclusion $\forall x [Fx] \to G$ and the one you need to derive $\forall x [Fx \to G]$. The former includes only the antecedent of the conditional while the latter includes the entire conditional. This difference stems from an incorrect application of universal introduction on line $6$. Whenever the rule is applied to a formula, it should be applied to the entire formula and not a mere component. So, instead of inferring $\forall x [Fx] \to G$ on line $6$, you should have inferred $\forall x [Fx \to G]$. Making this correction will get you closer to the conclusion you need to derive, however, I'm afraid it's still not enough. You cannot apply existential elimination twice over on lines $7$ and $8$. After applying it the first time to infer $\forall x [Fx \to G]$ on line $7$, the best you can do is infer the conditional $\exists x [Fx] \to \forall x [Fx \to G]$ on line $8$ via the inference rule known as conditional proof, also known as arrow introduction.

Instead of assuming $\exists x [Fx]$ on line $2$, begin by assuming $Fa$ and then apply existential introduction to obtain $\exists x [Fx]$. Then, after applying modus ponens to infer $G$, you can infer $Fa \to G$ via conditional proof and end your proof with universal introduction. I sketch out such a proof below that includes dependency numbers (appearing in curly brackets) to emphasize that the conclusion of the proof rests solely on its single premise.

$ \begin{array}{llll} \{1\} & 1. & \exists x [Fx] \to G & \text{premise} \\ \{2\} & 2. & Fa & \text{Assumption} \\ \{2\} & 3. & \exists x [Fx] & \text{2 $\exists$ Intro} \\ \{1,2\} & 4. & G & \text{1,3 Modus Ponens} \\ \{1\} & 5. & Fa \to G & \text{2,4 $\to$ Intro} \\ \{1\} & 6. & \forall x [Fx \to G] & \text{5 $\forall$ Intro} & \square \\ \end{array} $