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.

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

to get your desired result:

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

  • $\begingroup$ This is actually good, I was able to prove it. A question though, how do we try to solve something like this? is there some sort of reverse-engineering way? $\endgroup$ – Rab Sep 4 '18 at 22:03
  • $\begingroup$ @Rab. Yes, you got it: reverse engineering! I start with a natural deduction proof (a much easier system to work with!), and then see how I can translate that into an axiomatic proof. Glad you were able to fill in the details :) $\endgroup$ – Bram28 Sep 4 '18 at 22:15
  • $\begingroup$ @Rab Figure out how to implement truth tables in your logic. If you can do that, you can prove or disprove any proposition. This is equivalent to showing propositional completeness, so any proof of the completeness of your logic will be doing that also. $\endgroup$ – DanielV Sep 5 '18 at 22:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.