Hilbert Calculus Derivation

Question

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.

Answer 1

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