Need Hints Prove "$((\neg \alpha \to \alpha) \to \alpha) $" Using Axiom 1,2,3 and MP and deduction theorem $((\neg \alpha \to \alpha) \to \alpha) $
Hi, I am trying to prove this.
Can someone gives me some hints to start the question...
My friend told me I might need to use deduction theorem here, but I have no clue to approach it..
Axiom 1: A→(B→A).
Axiom 2: (A→(B→C))→((A→B)→(A→C)).
Axiom 3: (¬B→¬A)→((¬B→A)→B).
To clarify: A, B, C, α, and β are propositions (i.e. assigned True or False). → and ¬ have the standard logical meanings.
 A: here's a proof without using the deduction theorem. I will use the Mendelson Axioms, which I think are the basic ones (or at least they are taught on a first course of logic). Hope it helps.
$1.- ¬a \implies ((¬a \implies ¬a) \implies ¬a )$   (Ax1)
$2.- (¬a \implies ((¬a \implies ¬a) \implies ¬a )) \implies ((¬a \implies (¬a \implies ¬a)) \implies (¬a \implies ¬a ))$  (Ax2)
$3.- (¬a \implies (¬a \implies ¬a)) \implies (¬a \implies ¬a ) $  (MP (1,2))
$4.- ¬a \implies (¬a \implies ¬a )$   (Ax1)
$5.-  ¬a \implies ¬a $   (MP(3,4))
$6.- ( ¬a \implies ¬a) \implies (( ¬a \implies  a) \implies a)$ (Ax3)
$7.-  (¬a \implies a) \implies a $ (MP(5,6))
A: I don't know what Axioms 1, 2, and 3 are. They are not standardized to that extent. But the following may help:


*

*Suppose $\neg\alpha \implies \alpha$.

*Suppose to the contrary that $\neg\alpha$.

*$\alpha$ (from 1 and 2).

*$\alpha \land \neg\alpha$ (from 3 and 2)

*$\neg\neg\alpha$ (from 2 and 4)

*$\alpha$ (from 5)

*$[\neg\alpha \implies \alpha]\implies \alpha$ (from 1 and 6)
A: Since I don't know your basis, I'll pick a three-axiom basis that I sometimes like which Elliot Mendelsohn uses (there is a suggestion that in some sense the basis can at least get said to have hinted at by Jaskowski in his original paper on Natural Deduction, "On the Rules Of Supposition in Formal Logic", if not earlier).  I use Polish/Lukasiewicz notation, and condensed detachment.
axiom 1 C p Cqp.
axiom 2 C CpCqr C Cpq Cpr.
axiom 3 C CNpNq C CNpq p.
D2.1  4 C Cpq Cpp.
D4.1  5 Cpp.
D3.5  6 CCNppp.

A: We can start with the "standard" proof of : 


$\vdash \alpha \rightarrow \alpha$.


(1) $\alpha → ((\alpha \rightarrow \alpha) → \alpha)$ --- from Ax 1
(2) $(\alpha → ((\alpha \rightarrow \alpha) → \alpha)) → ((\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha))$ --- from Ax 2
(3) $(\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha)$ --- from (1) and (2) by MP
(4) $\alpha → (\alpha \rightarrow \alpha)$ --- from Ax 1

(5) $\alpha \rightarrow \alpha$ --- from (3) and (4) by MP

With it, Ax 1 and Ax 2, we can prove the Deduction Theorem.

Now for the proof of :


$\vdash (¬α→α)→α$


(1) $\vdash \lnot \alpha \rightarrow \lnot \alpha$ --- see above
(2) $\lnot \alpha \rightarrow \alpha$ --- assumed [a]
(3) $\vdash (\lnot \alpha \rightarrow \lnot \alpha) \rightarrow ((\lnot \alpha \rightarrow \alpha) \rightarrow \alpha)$ --- from Ax 3
(4) $\alpha$ --- from (1), (2) and (3) by MP twice

(5) $(\lnot \alpha \rightarrow \alpha) \rightarrow \alpha$ --- from (1) and (4) by Deduction Theorem

