How to use axioms to prove a derivation in propositional calculus?

Question

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?

Answer 1

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

Answer 2

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.