Deducing $(\lnot B) \to A$ from $\lnot A \to B$ using Hilbert deductive system
Fact about axiomatic proofs: It's not just your problem, but Hilbert-style proofs tend to be much more puzzling and laborious then Gentzen-style ones. Presumably, a natural deduction experienced logician would have troubles to prove the same theorem he just proved in the latter system using the former (For instance, note that the shortest known proof in Mendelson's system $M$ of the (trivial?) '$A \wedge B \vdash A$' requires $-$ as far as I know $-$ over 50 lines! [§2.3]).
In a Hilbert-style proof is not difficult to "keep winding up with crazy long steps" until we get some insight of how should we proceed. But you started very well by trying to instantiate axiom schemas II and III and maybe you just get lost in the middle of the instantiation. Maybe you can try to proceed like this:
(1) We first observe that, by a simple instance of the axiom schema III we obtain:
- $(\neg A \rightarrow \neg\neg B) \rightarrow (\neg B \rightarrow A)$
Now we just need to figure out how to "eliminate" the inner double negations in B to get our result:
$\vdash (\neg A \rightarrow B) \rightarrow (\neg B \rightarrow A)$
(2) Continuing our strategy, we can try to prove the following
$\vdash (\neg A \rightarrow B) \rightarrow (\neg A \rightarrow \neg \neg B)$
so that we could just proceed by a simple hypothetical syllogism and get our result. This is what we will try to do in the following steps (we now continue the proof):
- $(\neg A \rightarrow (B \rightarrow \neg\neg B)) \rightarrow ((\neg A \rightarrow B) \rightarrow (\neg A \rightarrow \neg \neg B))$, Ax2
- $(B \rightarrow \neg\neg B) \rightarrow ( \neg A \rightarrow (B \rightarrow \neg\neg B)) $, Ax1
- $B \rightarrow \neg\neg B$, Ax4
- $\neg A \rightarrow (B \rightarrow \neg\neg B)) $, 2,3, MP
- $(\neg A \rightarrow B) \rightarrow (\neg A \rightarrow \neg \neg B)$, Ax3
Now by hypothetical syllogism, 1 and 6 we have our desired result:
$7. (\neg A \rightarrow B) \rightarrow (\neg B \rightarrow A)$, 1,6, Hypothetical syllogism
Work (almost) done: We have derived the result we wanted. We just need to add a proof the hypothetical syllogism. Now can you complete the work? (Which axioms schemas to instantiate?)