Hilbert's style proof (FO logic) I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic.
\begin{align}
\exists x(\alpha \rightarrow \beta) \rightarrow (\exists x \alpha \rightarrow \exists x \beta) , x \notin FV(\beta)  
\end{align}
\begin{align}
(\alpha \rightarrow \beta) \rightarrow (\exists x \alpha \rightarrow \exists x \beta) , x \notin FV(\beta)  
\end{align}
 The relevant axioms are:


*

*$\alpha \rightarrow (\beta \rightarrow \alpha)$

*$(\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta)\rightarrow(\alpha \rightarrow\gamma))$

*$\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$

*$\alpha \rightarrow \forall x \alpha, x \notin FV(\alpha)$ 

*$\forall x (\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$



I am not really sure if any other axioms will be required or if all the above listed ones will be required. Any hints will be appreciated.
 A: You can't prove it.
Consider the field of rationals. Take $\alpha(x)$ as $x=0$ and take $\beta$ as $\exists y(y\cdot 0=1)$. Then $\exists x (\alpha(x)\to\beta)$ holds (just take $x=1$) and $\exists x\alpha(x)$ also holds, but $\exists x\beta$ is false.
A: Neither : $(α→β) → (∃xα→∃xβ), x \notin FV(β)$ is valid.
In order to manufacture a counter-example, we can "re-cycle" that of Tetori's answer.
We refer to Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 88 for the definition of :

Logical Implication : Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \vDash \varphi$, iff for every structure $\mathfrak A$ for the language and every function $s : Var \to |\mathfrak A|$ such that $\mathfrak A$ satisfies every member of $\Gamma$ with $s, \mathfrak A$ also satisfies $\varphi$ with $s$ [in symbols : $\vDash_{ \mathfrak A} \varphi[s]$ ].

We apply the definition to the example above, with $\Gamma = \{ α→β \}$ and $\varphi := (∃xα→∃xβ)$.
Consider the domain of natural numbers $\mathbb N$ and let $\alpha := x = 0$ and $\beta := \exists y (y < 0)$.
$\exists y (y < 0)$ is false in $\mathbb N$; thus, also : $\exists x (x = 0) \rightarrow \exists x \exists y (y < 0)$ is false in it, i.e. : $\nvDash_{ \mathbb N} (\exists x(x = 0) \rightarrow \exists x \exists y (y < 0))$.
Consider now a variable assignment fuction $s$ such that $s(x)=1$.
We have that $(x = 0)[s]$ is false is $\mathbb N$, and thus : $\vDash_{ \mathbb N} ((x = 0) \rightarrow \exists y (y < 0))[s]$.
In conclusion, we have found a structure $\mathfrak A$ and a variable assignment function $s$ such that $\mathfrak A$ satisfies $(x = 0) \rightarrow \exists y (y < 0)$ with $s$, but $\mathfrak A$ does not satisfy $(\exists x(x = 0) \rightarrow \exists x \exists y (y < 0))$ with $s$, i.e. :


$(α→β) \nvDash (∃xα→∃xβ)$.


Thus $(α→β) \rightarrow (∃xα→∃xβ)$ is not valid.

A different approach is that of Dirk van Dalen, Logic and Structure (5th ed - 2013), page 67 :

Definition 3.4.4 : $\mathfrak A \vDash \varphi$ iff $\mathfrak A \vDash Cl(\varphi)$,
where : let $FV(\varphi) = \{ z_1, \ldots,z_k \}$, then $Cl(\varphi) := ∀z_1 \ldots z_k \varphi$ is the universal closure of $\varphi$.

The same counterexample above may be used to show that :

$\forall x[(α→β) → (∃xα→∃xβ)]$

is not valid.


Note
The axioms for quantifiers used in Enederton [see page 112] are the same of your post. But  in your post a third propositional axiom is missing : the two that you are listed are not enough for a complete system of axioms for the propositional part.
