# Help with Hilbert Calculus

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?

• 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. – DanielV Mar 23 at 18:12
• @DanielV: No, that's how it's supposed to go. The body of the $\forall x_1$ is an instance of the Drinker paradox. – Henning Makholm Mar 23 at 18:14
• @HenningMakholm It still should be $\forall x_3(p(x_1,\,x_3))$ (say), though. – J.G. Mar 23 at 18:18
• See the post Proof of Drinker paradox as well as the post Why is this true? (∃x)(P(x)⇒(∀y)P(y)) – Mauro ALLEGRANZA Mar 23 at 18:29
• @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. – Henning Makholm Mar 23 at 18:30

Hint

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

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