Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$

Question

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$.

Answer 1

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)$