I'm trying to derive the following rule :
from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$
in the system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).
The axioms are [see page 112] :
The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs:
Tautologies;
$\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;
$\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;
$\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.
If the language includes equality, the usual axiom for it are added.
Modus ponens is the sole rule of inference.
What we can prove in Enderton's system is the following meta-theorem :
if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\beta$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \exists x \alpha \rightarrow \beta$.
Proof :
We have to start from :
(1) $\Gamma \vdash \alpha \rightarrow \beta$
(2) $\Gamma \vdash \lnot \beta \rightarrow \lnot \alpha$ --- from (1) and Taut, by mp
(3) $\lnot \beta$ --- assumed
(4) $\Gamma, \lnot \beta \vdash \lnot \alpha$.
Now, due to the proviso, we can apply the Gen Th to have :
(5) $\Gamma, \lnot \beta \vdash \forall x \lnot \alpha$
(6) $\Gamma \vdash \lnot \beta \rightarrow \forall x \lnot \alpha$ --- from (3) and (5), by Deduction Theorem
(7) $\Gamma \vdash \lnot \forall x \lnot \alpha \rightarrow \beta$ --- from (6) and Taut, by mp
(8) $\Gamma \vdash \exists x \alpha \rightarrow \beta$ --- abbreviation.
From this theorem, under the same proviso, with $\Gamma = \emptyset$ we have :
(A) if $\vdash \alpha \rightarrow \beta$, then $\vdash \exists x \alpha \rightarrow \beta$.
Note : these rules are not stated in Enderton's book, but we can easily derive the last one from the theorem in Example (Q3B) [page 122] :
$\vdash (\exists x \alpha \rightarrow \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\beta$.
Proof :
(1) $\vdash \alpha \rightarrow \beta$
(2) $\vdash \forall x(\alpha \rightarrow \beta)$ --- by Generalization Theorem [page 117] : if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$, with $\Gamma = \emptyset$.
(3) $\vdash \exists x \alpha \rightarrow \beta$ --- by (Q3B).
In the same way, from the theorem of Example (Q2A) [page 121] :
$\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\alpha$,
we can prove the meta-theorem :
(B) if $\vdash \alpha \rightarrow \beta$, then $\vdash \alpha \rightarrow \forall x \beta$,
with the same proviso.
Of course, we can deduce it from the "more general" meta-theorem :
if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\alpha$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \alpha \rightarrow \forall x \beta$
which can easily be proved as the other one.
The rules (A) and (B) are the Rules for the Universal and Existential Quantifiers used by David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (2nd ed - 1937; see english translation, page 70) and due to Paul Bernays (see footnote); they are used also by S.C.Kleene in his textbooks.