Deducing $((\neg a \to \neg b) \to ((\neg a \to b) \to b)))$ from axioms I have seen many questions here, using a different set of axioms than mine.
Here is mine :
$$1) (a \to (b \to a))$$
$$2) ((a \to (b \to c)) \to ((a \to b) \to (a \to c)))$$
$$3) ((\neg b \to \neg a) \to (a \to b))$$
Is it possible to deduce the following from these: $((a \to b) \to ((\neg a \to b) \to b))$.
I couldn't find a proof myself or online.
Thank you very much!!!
 A: I have a fairly simple proof which when fully expanded is likely to be longer than the proofs found by Prover9 and Otter.
Beyond making use of the deduction theorem, it requires the following three lemmas (I give the lengths of the proofs found by my own amateurish theorem prover):


*

*33 lines: $(\lnot x \to y) \to (\lnot y \to x)$

*7 lines: $(y \to z) \to (x \to y) \to (x \to z)$

*23 lines: $(\lnot x \to x) \to x$


Proof: assume $(\lnot a \to b)$ and $(a \to b)$. By $(\lnot a \to b)$ and lemma 1 $[a/x, b/y]$ conclude $(\lnot b \to a)$. By this and the assumption $(a \to b)$ plus lemma 2, conclude $(\lnot b \to b)$. By lemma 3, conclude $b$.
Convert this to an assumption-free proof of $(\lnot a \to b) \to (a \to b) \to b$ by applying the deduction theorem unwinding algorithm.
Proof, now with more symbols and fewer words:


*

*$(\lnot a \to b), (a \to b) \vdash \lnot a \to b \quad$ [assumption]

*$(\lnot a \to b), (a \to b) \vdash (\lnot a \to b) \to (\lnot b \to a) \quad$ [lemma 1]

*$(\lnot a \to b), (a \to b) \vdash \lnot b \to a \quad$ [modus ponens, $2 \sim (1 \to 3)$]

*$(\lnot a \to b), (a \to b) \vdash (a \to b) \to (\lnot b \to a) \to (\lnot b \to b) \quad$ [lemma 2]

*$(\lnot a \to b), (a \to b) \vdash (a \to b) \quad$ [assumption]

*$(\lnot a \to b), (a \to b) \vdash (\lnot b \to a) \to (\lnot b \to b) \quad$ [modus ponens, $4 \sim (5 \to 6)$]

*$(\lnot a \to b), (a \to b) \vdash (\lnot b \to b) \quad$ [modus ponens, $6 \sim (3 \to 7)$]

*$(\lnot a \to b), (a \to b) \vdash (\lnot b \to b) \to b \quad$ [lemma 3]

*$(\lnot a \to b), (a \to b) \vdash b \quad$ [modus ponens, $8 \sim (7 \to 9)$]


Proofs of the lemmas are available on request.
A: It helps to know:


*

*Two logical expressions are equivalent iff they have the same truth table

*$(a \rightarrow b) \leftrightarrow (\neg a \vee b) $ (One can proof that using the truth table)

*$(a \rightarrow b) \leftrightarrow (\neg b \rightarrow \neg a) $ (One can proof that using the truth table)

*$(a \vee \neg a) =1$ (Tautology)

*$\neg \neg a = a$ (Double negation)

*$1$ is the neutral element of the logical conjuction: $1\wedge a = a$



Here is my approach to deduce the given expression from elementary propositions:
Let $a$ and $b$ be two propositions, with 
$$a \rightarrow b$$
$$ \leftrightarrow \neg a \vee b$$ 
$$\leftrightarrow (\neg a \wedge b)\vee(\neg a \vee b)$$
$$\leftrightarrow (\neg (a \vee \neg b))\vee(\neg a \vee b)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (\neg a \vee b)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge 1 $$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge (b \vee \neg b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee( \neg a \wedge \neg b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(a \vee b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(\neg \neg a \vee b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg( \neg a \rightarrow b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow \neg( \neg a \rightarrow b) \vee b $$
$$\leftrightarrow (a \vee \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (\neg b \vee a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (b \rightarrow a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (\neg a \rightarrow \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b)$$
