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.
Hint
For Mendelson's system, see :
We need :
Lemma 1.8 [ page 27 ] : $\vdash \varphi \to \varphi$.
With it, (Ax.1) and (Ax.2), we can prove Prop.1.9 (Deduction Th) [ page 28 ] and some useful results [ page 29 ]:
Corollary 1.10(a) : $\varphi \to \psi, \psi \to \tau \vdash \varphi \to \tau$
and :
Lemma 1.11(b) : $\vdash \lnot \lnot \varphi \to \varphi$.
First, we can prove the "easy" version :
a) if $\Gamma \cup \{ \lnot \gamma \}$ is inconsistent, then $\Gamma ⊢ \gamma$.
Proof
1) $\Gamma \cup \{ \lnot \gamma \}$ is inconsistent, i.e. $\Gamma \cup \{ \lnot \gamma \} \vdash \varphi$ and $\Gamma \cup \{ \lnot \gamma \} \vdash \lnot \varphi$, for some formula $\varphi$
Thus :
2) $\Gamma \vdash \lnot \gamma \to \varphi$ --- from 1) by Ded.Th
3) $\Gamma \vdash \lnot \gamma \to \lnot \varphi$ --- from 1) by Ded.Th
4) $\vdash (\lnot \gamma \to \lnot \varphi) \to ((\lnot \gamma \to \varphi) \to \gamma)$ --- (Ax.3)
5) $\Gamma \vdash \gamma$ --- from 2), 3) and 4) by modus ponens twice.
Finally, for the sought result :
b) if $\Gamma \cup \{ \gamma \}$ is inconsistent, then $\Gamma ⊢ \lnot \gamma$,
we have to apply Noah's suggestion.
As in case a) above, we have :
1) $\Gamma \vdash \gamma \to \varphi$
2) $\Gamma \vdash \gamma \to \lnot \varphi$
3) $\vdash \lnot \lnot \gamma \to \gamma$ --- by Lemma 1.11(a)
4) $\Gamma \vdash \lnot \lnot \gamma \to \lnot \varphi$ --- from 2), 3) and Corollary 1.10(a)
5) $\Gamma \vdash \lnot \lnot \gamma \to \varphi$ --- from 1), 3) and Corollary 1.10
6) $\vdash (\lnot \lnot \gamma \to \lnot \varphi) \to ((\lnot \lnot \gamma \to \varphi) \to \lnot \gamma)$ --- (Ax.3)
7) $\Gamma \vdash \lnot \gamma$ --- from 4), 5) and 6) by modus ponens twice.
Best Answer
IMO the "trick" in similar cases of long derivations in Hilbert-style, is to use some intermediate result as Lemma.
Having Ax.3 and the Doble Negation laws, you can prove all Contraposition laws (various combinations).
In addition, it is useful to have an intermediate result: call it
Poof:
$(A \to (\lnot A \to \lnot B))$ --- easily proved using Ax.1, Contraposition and Transitivity
$(A \to (\lnot A \to \lnot B)) \to ((A \to \lnot A) \to (A \to \lnot B))$ --- Ax.2
$((A \to \lnot A) \to (A \to \lnot B))$ --- from 1) and 2) by MP
$(A \to \lnot B) \to (B \to \lnot A)$ --- Contraposition
$(A \to \lnot A) \to (B \to \lnot A)$ --- from 3) and 4) by Transitivity.
Now for the main result:
$(A \to \lnot A) \to ((A \to \lnot A) \to \lnot A)$ --- Lemma 1
$[(A \to \lnot A) \to ((A \to \lnot A) \to \lnot A)] \to [((A \to \lnot A) \to (A \to \lnot A)) \to ((A \to \lnot A) \to \lnot A)]$ --- Ax.2
$[((A \to \lnot A) \to (A \to \lnot A)) \to ((A \to \lnot A) \to \lnot A) ]$ --- from 1) and 2) by MP
$((A \to \lnot A) \to (A \to \lnot A))$ --- from $(\alpha \to \alpha)$