How can I prove (┐p→p)→p using ONLY (L1, L2, L3, MP) by 19 steps? Sorry for not declaring the Axiom. Here is my Axiom, which is different from the one below:
L1: p→(q→p)
L2: (p→(q→r))→((p→q)→(p→r))
L3: (┐p→┐q)→(q→p)
Thanks a lot for answering me again.
We have to start with the proof of :
(A) $ \ \vdash \alpha \rightarrow \alpha$.
(1) $\alpha → ((\alpha \rightarrow \alpha) → \alpha)$ --- from Ax1
(2) $(\alpha → ((\alpha \rightarrow \alpha) → \alpha)) → ((\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha))$ --- from Ax2
(3) $(\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha)$ --- from 1) and 2) by modus ponens
(4) $\alpha → (\alpha \rightarrow \alpha)$ --- from Ax1
(5) $\alpha \rightarrow \alpha$ --- from 3) and 4) by modus ponens.
We need :
(B) $ \ \vdash \alpha \to \beta, \beta \to \gamma \vdash \alpha \to \gamma$.
(1) $\alpha \to \beta$
(2) $\beta \to \gamma$
(3) $(\beta \to \gamma) \to (\alpha \to (\beta \to \gamma))$ --- by Ax1
(4) $\alpha \to (\beta \to \gamma)$ --- from 2) and 3) by modus ponens
(5) $(\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma))$ --- by Ax2
(6) $(\alpha \to \beta) \to (\alpha \to \gamma)$ --- from 4) and 5) by modus ponens
(7) $\alpha \to \gamma$ --- from 1) and 6) by modus ponens.
We need :
(C) $ \ \vdash \lnot \alpha \to (\alpha \to \beta)$.
(1) $\lnot \alpha \to (\lnot \beta \to \lnot \alpha)$ --- by Ax1
(2) $(\lnot \beta \to \lnot \alpha) \to (\alpha \to \beta)$ --- by Ax3
(3) $\lnot \alpha \to (\alpha \to \beta)$ --- from 1) and 2) by (B).
We need :
(D) $ \ \vdash (\lnot \alpha \to \alpha) \to (\beta \to \alpha)$.
(1) $\lnot \alpha \to (\alpha \to \lnot \beta)$ --- by (C)
(2) $(\lnot \alpha \to (\alpha \to \lnot \beta)) \to ((\lnot \alpha \to \alpha) \to (\lnot \alpha \to \lnot \beta))$ --- by Ax2
(3) $(\lnot \alpha \to \alpha) \to (\lnot \alpha \to \lnot \beta)$ --- from 1) and 2) by mp
(4) $(\lnot \alpha \to \lnot \beta) \to (\beta \to \alpha)$ --- by Ax3
(5) $(\lnot \alpha \to \alpha) \to (\beta \to \alpha)$ --- from 3) and 4) by (B).
Finally :
(E) $ \ \vdash (\lnot \alpha \to \alpha) \to \alpha)$.
(1) $(\lnot \alpha \to \alpha) \to ((\lnot \alpha \to \alpha) \to \alpha)$ --- by (D)
(2) $((\lnot \alpha \to \alpha) \to ((\lnot \alpha \to \alpha) \to \alpha)) \to (((\lnot \alpha \to \alpha) \to (\lnot \alpha \to \alpha)) \to ((\lnot \alpha \to \alpha) \to \alpha))$ --- by Ax2
(3) $((\lnot \alpha \to \alpha) \to (\lnot \alpha \to \alpha)) \to ((\lnot \alpha \to \alpha) \to \alpha)$ --- from 1) and 2) by mp
(4) $(\lnot \alpha \to \alpha) \to (\lnot \alpha \to \alpha)$ --- by (A)
(5) $(\lnot \alpha \to \alpha) \to \alpha$ --- from 3) and 4) by mp.
