Is my answer to the following question correct?
Discuss whether a rule of "partial generalization", i.e. $\frac{H(x)\rightarrow Gx}{\forall x H(x) \rightarrow \exists x Gx}$ is derivable as an inference rule in the Hilbert-calculus.
Answer: Assume that
(1) $\Sigma \vdash_H H(x) \rightarrow G(x)$, such that x does not occur free in $\Sigma$. Then, by universal generalization,
(2) $\Sigma \vdash_H \forall x( H(x) \rightarrow G(x))$. Now, by Axiom 4 and Modus Ponens, it follows that
(3) $\Sigma \vdash_H \forall x H(x) \rightarrow \forall x G(x)$. Application of the Deduction Theorem yields
(4) $\Sigma , \forall x H(x) \vdash_H \forall x G(x)$. But as
(5) $\forall x G(x) \vdash_H \exists x G(x)$ is a rule in $\vdash_H$,
(6) $\Sigma , \forall x H(x) \vdash_H \exists x G(x) $ follows by (4) and (5) via the Rule of Cut. Repeated application of the Deduction Theorem yields the desired result:
(7) $\Sigma \vdash_H \forall x H(x) \rightarrow \exists x G(x) $. ∎
Note: I made use of the following theorems, axioms and rules, which are all free to use for this exercise:
Universal Generalization in the Hilbert Calculus: $\frac {H}{\forall v H}$ (such that if H is deduced from $\Sigma$, then v must not occur free in $\Sigma$.
Axiom 4 of the Hilbert Calculus: $\forall v (H_1 \rightarrow H_2) \rightarrow (\forall v H_1 \rightarrow \forall v H_2)$
Deduction Theorem: $\Sigma , H \vdash G$ iff $\Sigma \vdash H \rightarrow G$
Rule of Cut: $\Sigma \vdash C, \Delta \cup {C} \vdash H \Rightarrow \Sigma, \Delta \vdash H$
I also presuppose (5) as an evident rule.