Proof of a theorem in Hilbert's system I have been trying to prove that the propositional formula $ \big( \alpha \rightarrow \lnot \beta \big) \rightarrow \big((\alpha \rightarrow \beta) \rightarrow \lnot \alpha \big)$ is a theorem in Hilbert's system, i.e., to prove $\vdash \big( \alpha \rightarrow \lnot \beta \big) \rightarrow \big((\alpha \rightarrow \beta) \rightarrow \lnot \alpha \big)$using the following three axioms and Modus Ponens.


*

*$\alpha \rightarrow \big(\beta \rightarrow\alpha \big)$

*$ \big({\alpha \rightarrow \big(\beta \rightarrow\gamma \big)}\big) \rightarrow  \big({\big(\alpha \rightarrow\beta \big) \rightarrow \big(\alpha \rightarrow\gamma \big)} \big)$

*$\big( \lnot \beta \rightarrow \lnot \alpha \big) \rightarrow \big( (\lnot \beta \rightarrow\alpha) \rightarrow \beta \big)$ 
Deduction theorem can be used as well. I am getting into long winded derivations which don't lead anywhere. Hints will be highly appreciated.
 A: This is just a re-labelling of $3$. It's 3s $\beta = \neg\alpha$ in theorem and $\alpha$ in 3. is $\beta$ in your theorem.
$$(\neg(\neg\alpha) \Rightarrow \neg\beta) \Rightarrow ((\neg(\neg\alpha) \Rightarrow \beta) \Rightarrow \neg\alpha)$$
For a proof of $\neg\neg\alpha \leftrightarrow\alpha$, you can refer to Thm. 6 on this site, to reduce to the proof of $(\neg\beta\Rightarrow\neg\alpha)\Rightarrow(\alpha\Rightarrow\beta)$ (Wich is their axiom 3)
A: I'm able to "manufacture" a quite long proof, with ref to :


*

*Elliott Mendelson, Introduction to mathematical logic (4th ed - 1997); see page 35 for the axioms [those that you are requested to use] and the only rule of inference : Modus Ponens.



With Ax 1 and Ax 2 we can prove [see Mendelson, Lemma 1.8, page 36] : $\vdash \alpha \rightarrow \alpha$.
(1) $\alpha → ((\alpha \rightarrow \alpha) → \alpha)$ --- from Ax 1
(2) $(\alpha → ((\alpha \rightarrow \alpha) → \alpha)) → ((\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha))$ --- from Ax 2
(3) $(\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha)$ --- from (1) and (2) by MP
(4) $\alpha → (\alpha \rightarrow \alpha)$ --- from Ax 1

(5) $\alpha \rightarrow \alpha$ --- from (3) and (4) by MP

With it, Ax 1 and Ax 2, we can prove the Deduction Theorem [see Mendelson, page 37].
In addition, with Ax 1 and Ax 2, we can prove Hypothetical Syllogism : $\alpha \rightarrow \beta, \beta \rightarrow \gamma \vdash \alpha \rightarrow \gamma$; in this post we can find a proof of it.

We need two additional Lemmas :
Lemma 1 [see Mendelson, Lemma 1.11(a), page 38] : $\vdash \lnot \lnot \beta \rightarrow \beta$
(1) $\vdash (\lnot \beta \rightarrow \lnot \lnot \beta) \rightarrow ((\lnot \beta \rightarrow \lnot \beta) \rightarrow \beta)$ from Ax 3 with $\lnot \beta$ in place of $\alpha$
(2) $\lnot \beta \rightarrow \lnot \lnot \beta$ --- assumed [a]
(3) $\vdash \lnot \beta \rightarrow \lnot \beta$ --- from $\vdash \alpha \rightarrow \alpha$ : see above
(4) $\beta$ --- from (1), (2) and (3) by MP twice
(5) $\vdash (\lnot \beta \rightarrow \lnot \lnot \beta) \rightarrow \beta$ --- from (2) and (4) by Deduction Th, discharging [a]
(6) $\vdash \lnot \lnot \beta \rightarrow (\lnot \beta \rightarrow \lnot \lnot \beta)$ --- Ax 1

(7) $\vdash \lnot \lnot \beta \rightarrow \beta$ --- from (5) and (6) by HS


Lemma 2 [see Mendelson, Lemma 1.11(e), page 38] : $\alpha \rightarrow \beta \vdash \lnot \beta \rightarrow \lnot \alpha$
(1) $\alpha \rightarrow \beta$ --- assumed [a]
(2) $\lnot \beta$ --- assumed [b]
(3) $\vdash \lnot \beta \rightarrow (\lnot \lnot \alpha \rightarrow \lnot \beta)$ --- Ax 1
(4) $\lnot \lnot \alpha \rightarrow \lnot \beta$ --- from (2) and (3) by MP
(5) $\vdash \lnot \lnot \alpha \rightarrow \alpha$ --- Lemma 1
(6) $\lnot \lnot \alpha \rightarrow \beta$ --- from (1) and (5) by HS
(7) $\vdash (\lnot \lnot \alpha \rightarrow \lnot \beta) \rightarrow ((\lnot \lnot \alpha \rightarrow \beta) \rightarrow \lnot \alpha)$ from Ax 3 with $\lnot \alpha$ in place of $\beta$
(8) $\lnot \alpha$ --- from (4), (6) and (7) by MP twice

(9) $\lnot \beta \rightarrow \lnot \alpha$ --- from (2) and (8) by DT, discharging [b]


Now for the proof of : $\vdash (\alpha \rightarrow \lnot \beta) \rightarrow ((\alpha \rightarrow \beta) \rightarrow \lnot \alpha)$
(1) $\alpha \rightarrow \lnot \beta$ --- assumed [a]
(2) $\alpha \rightarrow \beta$ --- assumed [b]
(3) $\lnot \beta \rightarrow \lnot \alpha$ --- from (2) by Lemma 2
(4) $\alpha \rightarrow \lnot \alpha$ --- from (1) and (3) by HS
(5) $\lnot \lnot \alpha \rightarrow \lnot \alpha$ --- from (4) by Lemma 2
(6) $ \vdash (\lnot \lnot \alpha → \lnot \lnot \alpha) → ((\lnot \lnot \alpha \rightarrow \lnot \alpha) → \lnot \alpha)$ --- from Ax 3
(7) $\vdash \lnot \lnot \alpha \rightarrow \lnot \lnot \alpha$ --- from $\vdash \alpha \rightarrow \alpha$
(8) $\lnot \alpha$ --- from (5), (6) and (7) by MP twice

(9) $\vdash (\alpha \rightarrow \lnot \beta) \rightarrow ((\alpha \rightarrow \beta) \rightarrow \lnot \alpha)$ --- from (1), (2) and (8), by two applications of DT, discharging assumptions [a] and [b].


Comment
It can be "istructive" to compare the above proof (I hope it can be simplified) with the Natural Deduction 9-lines proof.
