How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC I have the three axioms
$$\alpha \rightarrow (\beta \rightarrow \alpha)$$
$$\Big(\alpha \rightarrow (\beta \rightarrow\gamma)\Big)\rightarrow \Big((\alpha \rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma)\Big)$$
$$(\lnot \alpha \rightarrow\beta)\rightarrow\Big((\lnot \alpha \rightarrow\lnot\beta)\rightarrow\alpha\Big)$$
I can see that the r.h.s is $\alpha \land \beta$ while the l.h.s is $\beta\land\alpha$ however, I am unable to actually find a proof using the three axioms.
 A: Assuming you can use the Deduction Theorem, I would follow the following path:
First, prove:
$$\neg \alpha \rightarrow (\alpha \rightarrow \beta)$$
Combine this with the following instantiation of Axiom 3:
$$(\neg \alpha \rightarrow (\alpha \rightarrow \beta)) \rightarrow ((\neg \alpha \rightarrow \neg (\alpha \rightarrow \beta)) \rightarrow \alpha)$$
to show that:
$$\neg (\alpha \rightarrow \neg \beta) \vdash \alpha$$
Similarly, show:
$$\neg (\alpha \rightarrow \neg \beta) \vdash \beta$$
You can now easily show:
$$\neg (\alpha \rightarrow \neg \beta), \neg \neg (\beta \rightarrow \neg \alpha) \vdash \alpha, \neg \alpha$$
Finally, use this result with another instantiation of axiom 3:
$$(\neg \neg (\beta \rightarrow \neg \alpha) \rightarrow \alpha) \rightarrow ((\neg \neg (\beta \rightarrow \neg \alpha) \rightarrow \neg \alpha) \rightarrow \neg (\beta \rightarrow \neg \alpha)$$
to get your desired result:
$$\neg (\alpha \rightarrow \neg \beta) \vdash \neg (\beta \rightarrow \neg \alpha)$$
