# Hilbert Calculus Derivation

Im tryng to prove that this is a theorem using Hilbert calculus $$(∀x_1 (∀x_2 (p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(x_2)))))))$$

The problem is getting this part $$(p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(x_2)))))))$$ because then we just have to do some generalizations but i cant seem to prove this i get stuck, I tried using this theorems

$$(α ⇒ (β ⇒ (α ∧ β)))$$

$$((α ∧ β) ⇒ α)$$

but i cant seem to find a way to get that expression. Thanks.

• Obviously, for an "Hilbert's proof", you have to state the axioms and rules of the system you are using... – Mauro ALLEGRANZA Mar 24 '19 at 12:24

1) $$p(x_1)$$ --- premise

2) $$\lnot p(x_2)$$ --- premise

3) $$(p(x_1) \to p(x_2))$$ --- premise

4) $$p(x_2)$$ --- from 1) and 3) by MP

Up to now we have : $$\{ p(x_1), \lnot p(x_2), (p(x_1) \to p(x_2)) \} \vdash p(x_2)$$, and thus, by DT :

6) $$\{ p(x_1), \lnot p(x_2) \} \vdash (p(x_1) \to p(x_2)) \to p(x_2)$$.

Obviously : $$\{ p(x_1), \lnot p(x_2), (p(x_1) \to p(x_2)) \} \vdash \lnot p(x_2)$$, and thus, by DT :

7) $$\{ p(x_1), \lnot p(x_2) \} \vdash (p(x_1) \to p(x_2)) \to \lnot p(x_2)$$.

We use the propositional tautology :

8) $$\vdash (A \to B) \to ((A \to \lnot B) \to \lnot A)$$

to get :

9) $$\{ p(x_1), \lnot p(x_2) \} \vdash \lnot (p(x_1) \to p(x_2))$$.

Now we conclude with two application of DT

10) $$\vdash p(x_1) \to (\lnot p(x_2) \to \lnot (p(x_1) \to p(x_2)))$$

followed by two Generalization :

11) $$\forall x_1 \forall x_3 (p(x_1) \to (\lnot p(x_2) \to \lnot (p(x_1) \to p(x_2)))).$$

• Ah , i dont think i was aware of the existence of that axiom , guess it simplies it a bit – Something Mar 24 '19 at 12:42
• @PedroSantos - as said above, there are many axiom system; the one that I suggest allows every propositional tautology as axiom, plus quantifier axioms and modus ponens. – Mauro ALLEGRANZA Mar 24 '19 at 12:45
• Yeah in my logic class we just gave the 5 axioms and the use of MP and Generalizations. Then we constructed theorems that we could use whenever we wanted. – Something Mar 24 '19 at 12:46
• Just a questin since we have $p(x_2)$ and its negative cant we aplly the contradiction theorem to get ${p(x1),¬p(x2)⊢ ¬(p(x1)→p(x2))$ and then get the others from the deduction theorem and then do the generalizations ? @MauroALLEGRANZA – Something Mar 24 '19 at 17:51
• @PedroSantos - perfect. You can use it in place of step 8) above. – Mauro ALLEGRANZA Mar 24 '19 at 18:01