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

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.

• Aren't these statements related by being contrapositives of each other? – ncmathsadist Oct 12 '14 at 21:37
• Ax. 4 is provable from the first three (assuming uniform substitution and detachment). – Doug Spoonwood Oct 13 '14 at 5:52

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):

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

• Well I'm a little confused because you have the desired result to be $(\lnot A \to B) \to (\lnot A \to \lnot \lnot B)$. But I needed something like $(\lnot A \to B) \vdash (\lnot B \to A)$ (the original proposition) so should I not have ended up with $(\lnot B \to A)$ as the final line in this proof? So maybe I'm just not understanding correctly but that seems different from your final result – VakarianWrex Oct 13 '14 at 14:40
• @bloodruns4ever - you can find here the needed proof of Syllogism. With iy you can simplify a little bit the above proof of $(¬A→B) \vdash (\lnot B \rightarrow A)$. (i) assume $(¬A→B)$ and apply Syll with $(B→¬¬B)$ to get: $(¬A→¬¬B)$; (ii) use Ax3 to derive : $(¬B→A)$. – Mauro ALLEGRANZA Oct 13 '14 at 14:41
• Oh ok that makes sense now, thanks for your help! – VakarianWrex Oct 13 '14 at 14:50
• @bloodruns4ever Don't need to be confused: $\vdash (\neg A \rightarrow B) \rightarrow (\neg A \rightarrow \neg \neg B)$ and $(\neg A \rightarrow B) \vdash (\neg A \rightarrow \neg \neg B)$ are actually equivalent statements (see deduction theorem). – Bruno Bentzen Oct 13 '14 at 14:51
• @bloodruns4ever The idea of the proof is exactly the one Mauro described above in his useful comment. Good work. – Bruno Bentzen Oct 13 '14 at 14:54

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.