# 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.

• Have you ever done any kind of detailed proof in this system? – DanielV Sep 1 '18 at 18:39
• @DanielV Yes, I have proved things like $\alpha \rightarrow \alpha$ and $\lnot\lnot\alpha \rightarrow \alpha$ – Rab Sep 1 '18 at 18:47
• There was a related question posted---perhaps it will give you some ideas: math.stackexchange.com/questions/2038747/… – prime4567 Sep 2 '18 at 12:44
• @Bram28 Why did you add the (natural-deduction) tag? – Git Gud Sep 2 '18 at 20:36
• Please state your question in the body of the text and not just in the title. Also please expand the abbreviation HPC. – Rob Arthan Sep 2 '18 at 22:44

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

$$\neg (\alpha \rightarrow \neg \beta) \vdash \neg (\beta \rightarrow \neg \alpha)$$