Trying to prove (A → -A) → -A with the following axioms:
A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
(-A → -B) → (B → A)
Not an axiom, but you can also use A → (-A → B), which I've already managed to prove it.
Intuitively the proposition makes sense, but I'm not sure how to prove it
Hint
With Ax.1 and Ax.2 you have to derive some preliminary useful results :
and eventually the Deduction Theorem.
Then, Ax.3 is crucial in deriving double negation laws:
Double negation, in turn, give us : $\vdash (A \to B) \to (\lnot B \to \lnot A)$.
Two further Lemma :
1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- Ax.1
2) $\vdash (\lnot B \to \lnot A) \to (A \to B)$ --- Ax.3
1) $\vdash \lnot A \to (A \to \lnot B)$ --- Lemma (A)
2) $\vdash (\lnot A \to (A \to \lnot B)) \to ((\lnot A \to A) \to (\lnot A \to B))$ --- Ax.2
3) $\vdash (\lnot A \to A) \to (\lnot A \to B)$ --- from 1) and 2) by MP
4) $\vdash (\lnot A \to \lnot B) \to (B \to A)$ --- Ax.3
1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- Lemma (B)
2) $\vdash ((\lnot A \to A) \to ((\lnot A \to A) \to A)) \to (((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A))$ --- Ax.2
3) $\vdash ((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A)$ --- from 1) and 2) by MP
4) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from $\vdash A \to A$ above
Now the proof :
1) $\vdash (\lnot \lnot A \to \lnot A) \to \lnot A$ --- Lemma (C)
2) $A \to \lnot A$ --- assumed [a]
3) $\lnot \lnot A \to \lnot A$ --- from 2)
4) $\lnot A$ --- from 1) and 3) by MP