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$.
  • $\begingroup$ Do you mean $\exists x(Px\rightarrow \forall yPy)$? $\endgroup$ – Arthur Nov 9 '14 at 19:34
  • $\begingroup$ No, it is written with just $x$ in my book problem. $\endgroup$ – Bobby Lee Nov 9 '14 at 19:43
  • $\begingroup$ I just think it's strange to quantify twice over $x$ is all. $\endgroup$ – Arthur Nov 9 '14 at 19:54
  • $\begingroup$ Anyway, an intuitive "proof" goes like this: either $\forall xPx$, in which case the sentence $Px\rightarrow \forall xPx$ is a tautology. Otherwise, there is at least one $x$ such that $\lnot Px$. If you chose such an $x$ from the $\exists x$-part, the sentence is of the form "false $\to$ false", which is also a tautology. $\endgroup$ – Arthur Nov 9 '14 at 20:00

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 :


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

  • $\begingroup$ Wait you showed $\neg Px \vdash \exists x (Px \rightarrow \forall x Px)$ in line 3. Then you showed $\neg Px$ in line 4. Isn't this enough to show $\vdash \exists x (Px \rightarrow \forall x Px)$? $\endgroup$ – Bobby Lee Nov 10 '14 at 19:50
  • $\begingroup$ @Bobby Lee - NO - In line (3) we have $¬Px \vdash ∃x(Px→∀Px)$ but in line (4) we have $¬∃x(Px→∀Px)⊢¬Px→¬∃x(Px→∀Px)$ ... $\endgroup$ – Mauro ALLEGRANZA Nov 11 '14 at 7:18
  • $\begingroup$ How does line 2 follow from modus ponens? We would need $Pt \rightarrow \forall x Px$. $\endgroup$ – CuriousKid7 Mar 10 '17 at 5:00
  • $\begingroup$ Could you please explain how the derived rule is being used? I don't see how it's applicable here. $\endgroup$ – CuriousKid7 Mar 10 '17 at 17:11
  • 1
    $\begingroup$ NO; $t$ is a term and not a constant and $x$ is a term; thus $\varphi^x_x$ is $\varphi$. $\endgroup$ – Mauro ALLEGRANZA Mar 10 '17 at 19:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.