The axioms, if p and q are two sentences
p$\Rightarrow$(q$\Rightarrow$p)
(p$\Rightarrow$(q$\Rightarrow$r))$\Rightarrow$((p$\Rightarrow$q)$\Rightarrow$(p$\Rightarrow$r))
(~q$\Rightarrow$~p)$\Rightarrow$(p$\Rightarrow$q)
using these axioms and Modus Ponens how to prove
~a$\Rightarrow$(a$\Rightarrow$b)
When i start with axiom two,
p as ~a ,
q as ~a$\Rightarrow$(a$\Rightarrow$b) and
r as ~a
end up with no solution.
How to approach these kind of proofs?
We can use the Deduction Theorem : with it, we can easily get the "derived rule" of Syllogism :
$A \to B, B \to C \vdash A \to C$.
Now for the main proof :
1) $\lnot A \to (\lnot B \to \lnot A)$ --- Ax.1
2) $(\lnot B \to \lnot A) \to (A \to B)$ --- Ax.3
3) $\lnot A \to (A \to B)$ --- from 1) and 2) by Syllogism.
We can get rid of the Deduction Th with the following derivation of Syllogism :
1) $A \to B$ --- premise
2) $B \to C$ --- premise
3) $(B \to C) \to (A \to (B \to C))$ --- Ax.1
4) $A \to (B \to C)$ --- from 2) and 3) by modus ponens
5) $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$ --- Ax.2
6) $(A \to B) \to (A \to C)$ --- from 4) and 5) by modus ponens
7) $A \to C$ --- from 1) and 6) by modus ponens.
I use Polish notation and condensed detachment.
axiom 1 CpCqp
axiom 2 CCpCqrCCpqCpr
axiom 3 CCNpNqCqp
D1.3 4 CpCCNqNrCrq
D2.4 5 CCpCNqNrCpCrq
D5.1 6 CNpCpq
