Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$ We're in first-order logic, using the Hilbert system (with inference rule of modus ponens), and the problem is to show $\vdash \exists x (Px \rightarrow \forall x Px)$.
We just learned about this stuff, so I'm really not sure where to begin. I believe we should create a sequence of deductions from $\exists x Px$ in order to arrive to the "proof of" $\forall x Px$. And we can use the following "axioms" along with modus ponens in order to arrive there:


*

*Tautologies

*$\forall x \alpha \rightarrow \alpha_t^x$, 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$
And if the language includes equality, 


*

*$x=x$

*$x=y \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.

 A: In this post you can find a proof of :

$\vdash (∀xβ→α)↔∃x(β→α)$, if $x$ is not free in $\alpha$.

The proof uses the axioms you have listed.
In the above theorem we replace $\beta$ with $Px$ and $\alpha$ with $\forall xPx$. Clearly, $x$ is not free in $\forall xPx$: thus, the proviso of the theorem applies :

$(∀xPx→∀xPx)↔∃x(Px→∀xPx)$.

The LHS is a tautology; thus, by modus ponens :


$\vdash ∃x(Px→∀xPx)$.



We can prove it directly with the above axioms and rules (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)) :
(1) $\lnot Px \vdash Px \rightarrow \forall x Px$ --- by $\vDash_{TAUT} \lnot \phi \rightarrow (\phi \rightarrow \psi)$
(2) $\lnot Px \vdash \exists x (Px \rightarrow \forall x Px)$ --- from (1) by the "derived rule" : $\varphi_t^x \rightarrow \exists x \varphi$ [provable from Ax.2] and modus ponens
(3) $\vdash \lnot Px \rightarrow \exists x (Px \rightarrow \forall x Px)$ --- from (2) by Deduction Theorem
(4) $\lnot \exists x (Px \rightarrow \forall x Px) \vdash \lnot Px \rightarrow \lnot \exists x (Px \rightarrow \forall x Px)$ --- by $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$
(5) $\lnot \exists x (Px \rightarrow \forall x Px) \vdash Px$ --- from (3) and (4) by $\vDash_{TAUT} (\lnot \phi \rightarrow \lnot \psi) \rightarrow ((\lnot \phi \rightarrow \psi) \rightarrow \phi)$ 
(6) $\lnot \exists x (Px \rightarrow \forall x Px) \vdash \forall x Px$ --- from (5) by GENERALIZATION THEOREM [page 117] : $x$ is not free in the assumption
(7) $\lnot \exists x (Px \rightarrow \forall x Px) \vdash Px \rightarrow \forall x Px$ --- from (6) by $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$
(8) $\lnot \exists x (Px \rightarrow \forall x Px) \vdash \exists x(Px \rightarrow \forall x Px)$ --- From (7) by the "derived rule" of (2) and modus ponens
(9) $\vdash \lnot \exists x (Px \rightarrow \forall x Px) \rightarrow \exists x(Px \rightarrow \forall x Px)$ --- from (9) by Deduction Theorem
(10) $\vdash \lnot \exists x (Px \rightarrow \forall x Px) \rightarrow \lnot \exists x(Px \rightarrow \forall x Px)$ --- by $\vDash_{TAUT} \phi \rightarrow \phi$

(11) $\vdash \exists x (Px \rightarrow \forall x Px)$ --- from (9) and (10) by $\vDash_{TAUT} (\lnot \phi \rightarrow \lnot \psi) \rightarrow ((\lnot \phi \rightarrow \psi) \rightarrow \phi)$ 

