How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC

Question

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.

Answer 1

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