Proof about Clavius's Law Clavius's Law claimed:

$(\neg A \rightarrow A) \rightarrow A$

What it is the proof about it in Deductive System $L$?

Deductive System $L$ is:
L1: $A \rightarrow (B \rightarrow  A)$
L2: $(A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C)$
L3: $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$ or $(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$
And only it allows us to use Modus Ponens

I was trying this:

*

*$\neg A \rightarrow (A \rightarrow \neg A)$ by L1

*$(\neg A \rightarrow (A \rightarrow \neg A)) \rightarrow (\neg A \rightarrow A) \rightarrow (\neg A \rightarrow \neg A)$ by L2

*$(\neg A \rightarrow A) \rightarrow (\neg A)$ by Modus Ponens (1,2)

Then I was thinking in show that
$\neg A \rightarrow A$
But don't get success and I'm not sure if that will help me
 A: We need $\vdash A \to A$, easily provable from Ax.1 and Ax.2.
We need also some "auxiliary" results :
Lemma 1 (Syllogism) :
1) $A \to B$ --- premise
2) $B \to C$ --- premise
3) $\vdash (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) $\vdash (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.


Lemma 2 :
1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- Ax.1
2) $\vdash (\lnot B \to \lnot A) \to (A \to B)$ --- Ax.3

3) $\vdash \lnot A \to (A \to B)$ --- from 1) and 2) by Syllogism.


Lemma 3 :
1) $\vdash \lnot A \to (A \to \lnot B)$ --- Lemma 2
2) $\vdash \lnot A \to (A \to \lnot B) \to ((\lnot A \to A) \to (\lnot A \to \lnot B))$ --- Ax.2
3) $\vdash (\lnot A \to A) \to (\lnot A \to \lnot B)$ --- from 1) and 2) by mp
4) $\vdash (\lnot A \to \lnot B) \to (B \to A)$ --- Ax.3

5) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and 4) by Syll.


Now for the main proof :
1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- Lemma 3
2) $\vdash ((\lnot A \to A) \to ((\lnot A \to A) \to A)) \to (((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A))$ --- Ax.2
3) $\vdash ((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A)$ --- from 1) and 2) by mp
4) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from $\vdash A \to A$


5) $\vdash (\lnot A \to A) \to A$ - from 3) and 4) by mp


A: Sequent calculus seems to do it quite shortly.
But this take uses Dyckhoff Rule (L->->):
------------------ Ax-c  ------- Ax
bot->p,p --> bot,p       p --> p
-------------------------------- L->->(4)
       (p->bot)->p --> p
       ----------------- L~def
          ~p->p --> p
          --------------- R->
           --> (~p->p)->p
          ------------------ Ltop
          top --> (~p->p)->p

Credits:
http://vidal-rosset.net/g4i_prover.html
