Can u help show that this is a theorem? $ (∀x_1 (∃x_2 (p(x_1, x_2) ⇒ (∀x_2 p(x_1, x_2)))));$

I was trying to use the deduction theorem but i hit a wall. Can u help me out using derivatives and Hilbert Calculus?

  • $\begingroup$ It is good that you used parenthesis to disambiguate the expression, but they way you placed them, your second $x_2$ is over writing the first $x_2$, I think that is might be a typographical error. $\endgroup$ – DanielV Mar 23 '19 at 18:12
  • $\begingroup$ @DanielV: No, that's how it's supposed to go. The body of the $\forall x_1$ is an instance of the Drinker paradox. $\endgroup$ – hmakholm left over Monica Mar 23 '19 at 18:14
  • 1
    $\begingroup$ @HenningMakholm It still should be $\forall x_3(p(x_1,\,x_3))$ (say), though. $\endgroup$ – J.G. Mar 23 '19 at 18:18
  • 1
    $\begingroup$ See the post Proof of Drinker paradox as well as the post Why is this true? (∃x)(P(x)⇒(∀y)P(y)) $\endgroup$ – Mauro ALLEGRANZA Mar 23 '19 at 18:29
  • 1
    $\begingroup$ @J.G.: You could also write that. But most formalizations of first-order logic do allow a quantifier to re-bind a variable that is already bound by an enclosing quantifier -- for reasons discussed in this question. $\endgroup$ – hmakholm left over Monica Mar 23 '19 at 18:30


In this post you can find an Hilbert-style proof of :

$⊢(∀xβ → α) ↔ ∃x(β → α)$, provided that $x$ is not free in $\alpha$.

We have to consider :

$∀x_2p(x_1,x_2) \to ∀x_2p(x_1,x_2)$;

it is an instance of the propositional tautology : $\vdash A \to A$, and thus is a theorem.

Now we apply the equivalence above to it, due to the fact that $x_2$ is not free in $∀x_2p(x_1,x_2)$ to get :

$\vdash ∃x_2 \ (p(x_1,x_2) \to ∀x_2p(x_1,x_2))$.

The last step is obtained with Generalization:

$\vdash ∀x_1 \ ∃x_2 \ (p(x_1,x_2) \to ∀x_2p(x_1,x_2))$.


"English" answer:

Fix any $x_1,\,x_2$. If $p(x_1,\,x_2)$ is false, the required implication is vacuously true. If $x_2$ cannot be chosen so that $p(x_1,\,x_2)$ is false, our choice of $x_1$ has obtained $\forall x_2 (p(x_1,\,x_2))$, so again the implication succeeds.

HC answer:

$$\exists x_2(\neg p(x_1,\,x_2))\implies(p(x_1,\,x_2)\implies \forall x_3 (p(x_1,\,x_3)))$$ $$\not\exists x_2(\neg p(x_1,\,x_2))\implies\forall x_3(p(x_1,\,x_3)),\,\implies(p(x_1,\,x_2)\implies\forall x_3(p(x_1,\,x_3)))$$ Then use $(q\implies r)\land (\neg q\implies r)\implies r$.

  • $\begingroup$ Yeah Thanks , but i was trying to do it using a sequece of derivatives with hilbert calculus. $\endgroup$ – Something Mar 23 '19 at 18:18
  • $\begingroup$ @PedroSantos I hope my edit is a little bit more useful. $\endgroup$ – J.G. Mar 23 '19 at 18:42

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.