Given a formal system called "$P0$" that has 1 rule (Modus Ponens) and 3 axioms:

$1.$ $\alpha$ $\rightarrow$$(\beta \rightarrow \alpha)$ --- (Ak)

$2.$ $(\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta ) \rightarrow (\alpha \rightarrow \gamma))$ --- (AS)

$3.$ $(\lnot \beta \rightarrow \lnot \alpha) \rightarrow ((\lnot \beta \rightarrow \alpha) \rightarrow \beta)$ --- (A$\lnot$)

How do I replace the wff of the axioms with real wff to prove a derivation like : $\vdash \alpha \rightarrow \alpha$.

What wff should I use to set up the derivation and use the axioms to prove it?

  • 1
    $\begingroup$ You can find many proofs of it on this site. Try with tags: propositional-calculus and hilbert-system $\endgroup$ – Mauro ALLEGRANZA Feb 2 '18 at 19:50

As I said in response to another of the OP's questions along the same lines: The axiom system you are being asked to use is a standard one -- famously used in the classic textbook Elliott Mendelson, Introduction to Mathematical Logic (many editions, there is bound to be one in the library).

Since you are evidently very unclear what the rules of the deduction game are, you badly need to pause and take a slow and careful look at e.g. Mendelson's text.


That one is well known, but hard to come up with by yourself from scratch, certainly when you just begin to study this system. Indeed, typically textbooks will just provide this one:

$1. \ (\alpha \rightarrow ((\alpha \rightarrow \alpha)) \rightarrow \alpha) \rightarrow ((\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha)) \quad (AS)$

$2. \ \alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha) \quad (Ak)$

$3. \ (\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha) \quad (MP \ 1,2)$

$4. \ \alpha \rightarrow (\alpha \rightarrow \alpha) \quad (Ak)$

$5. \ \alpha \rightarrow \alpha \quad (MP \ 3,4)$

  • $\begingroup$ Yes, my question is : how do I use the Axioms, what wff do I have , what stuff that I can replace with $\beta$? I don't need the proof, but the steps that I should follow to write those lines $\endgroup$ – Bleeeaa Feb 2 '18 at 20:10
  • $\begingroup$ @Bleeeaa So if you look at my line 1: I used $\alpha$ for $\alpha$, $\alpha \rightarrow \alpha$ for $\beta$, and $\alpha$ for $\gamma$. So the general idea is: you can use any expression for any variable, as long as you do it consistently. $\endgroup$ – Bram28 Feb 2 '18 at 20:13
  • $\begingroup$ So the only wff I can use are $\alpha$ and $\alpha \rightarrow \alpha$? How do I decide what wff can I use to prove something ? $\endgroup$ – Bleeeaa Feb 2 '18 at 20:22
  • $\begingroup$ @Bleeeaa No, it really can be anything. For example, $(\neg P \rightarrow Q) \rightarrow (\neg \neg R \rightarrow (\neg P \rightarrow Q))$ would be a perfectly good instance of axiom $(Ak)$. So it's not a matter of deciding which one you can use (you can use any), but which ones would actually be useful to use in getting towards your goal. $\endgroup$ – Bram28 Feb 2 '18 at 20:41
  • $\begingroup$ So if I want to prove $\lnot (\alpha \rightarrow \beta) \vdash \lnot \beta$ can I use $(\lnot \lnot \beta \rightarrow \lnot \beta) \rightarrow \lnot \beta$? Known that $\lnot \alpha \rightarrow \alpha \vdash \alpha$. And why can't I use $\alpha \rightarrow \alpha$ to prove $\lnot \alpha \rightarrow \alpha \vdash \alpha$? $\endgroup$ – Bleeeaa Feb 2 '18 at 21:48

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.