Deducing $(\lnot B) \to A$ from $\lnot A \to B$ using Hilbert deductive system

Question

As the title says, I've been trying to prove this:

$(\lnot A \to B) \vdash (\lnot B) \to A)$

but unfortunately keep winding up with crazy long steps and then I have no idea where to go. The only axioms I can use are: \begin{gather} A \to (B \to A), \tag{Ax1} \\[0.1in] \big(A \to (B \to C)\big) \to \big((A \to B) \to (A \to C)\big), \tag{Ax2} \\[0.1in] (\neg B \to \neg A) \to (A \to B), \tag{Ax3} \\[0.1in] A \to \neg (\neg A). \tag{Ax4} \end{gather} Any help would be greatly appreciated. I thought about doing $(\mathrm{Ax2})$ first to get the $B$ and $A$ rearranged, followed by $(\mathrm{Ax3})$, but then I got lost there.

Answer 1

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:

1. $(\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):

2. $(\neg A \rightarrow (B \rightarrow \neg\neg B)) \rightarrow ((\neg A \rightarrow B) \rightarrow (\neg A \rightarrow \neg \neg B))$, Ax2
3. $(B \rightarrow \neg\neg B) \rightarrow ( \neg A \rightarrow (B \rightarrow \neg\neg B)) $, Ax1
4. $B \rightarrow \neg\neg B$, Ax4
5. $\neg A \rightarrow (B \rightarrow \neg\neg B)) $, 2,3, MP
6. $(\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?)

Answer 2

First, Ax4 is provable from the first three axioms.

Second, I'll suggest that you prove this handy formula: {(A→B)→[(C→A)→(C→B)]}. You can prove it from axioms 1 and 2 only, and you only need to use modus ponens/detachment three times to prove it.

Now you can hopefully solve this yourself. If note, the following information may prove useful. But, to encourage you to do a little thinking, I've made it a bit harder to read.

Now since you have detachment, that formula tells you that if you have, in Polish/Lukasiewicz notation, Cab and Cca, you can infer Ccb. Thus, if you have CaNNb and CNaa, you can infer CNaNNb. Then make CNaNNb into the antecedent of axiom 3 and you can detach CNba.