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
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
Below a proof using Prover9 developed by William McCune (with the help of others) at Argonne National Laboratory.  It corresponds to a condensed detachment proof.  But first you might find this useful:

% -------- Comments from original proof --------

% Proof 1 at 0.22 (+ 0.06) seconds.

% Length of proof is 22.

% Level of proof is 8.

% Maximum clause weight is 20.

% Given clauses 175.

1 P((-x -> x) -> x) # label(non_clause) # label(goal).  [goal].

2 -P(x -> y) | -P(x) | P(y).  [assumption].

3 P(x -> (y -> x)).  [assumption].

4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))).  [assumption].

5 P((-x -> -y) -> (y -> x)).  [assumption].

6 -P((-c1 -> c1) -> c1).  [deny(1)].

7 P(x -> (y -> (z -> y))).  [hyper(2,a,3,a,b,3,a)].

8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))).  [hyper(2,a,4,a,b,4,a)].

9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))).  [hyper(2,a,3,a,b,4,a)].

11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)).  [hyper(2,a,4,a,b,5,a)].

12 P(x -> ((-y -> -z) -> (z -> y))).  [hyper(2,a,3,a,b,5,a)].

14 P(x -> (y -> (z -> (u -> z)))).  [hyper(2,a,3,a,b,7,a)].

26 P((x -> ((y -> x) -> z)) -> (x -> z)).  [hyper(2,a,8,a,b,7,a)].

44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)).  [hyper(2,a,8,a,b,14,a)].

159 P(-x -> (x -> y)).  [hyper(2,a,26,a,b,12,a)].

160 P((x -> y) -> ((z -> x) -> (z -> y))).  [hyper(2,a,26,a,b,9,a)].

165 P((-x -> x) -> (-x -> y)).  [hyper(2,a,4,a,b,159,a)].

815 P(((x -> y) -> z) -> (y -> z)).  [hyper(2,a,44,a,b,160,a)].

842 P(x -> ((-y -> -x) -> y)).  [hyper(2,a,815,a,b,11,a)].

1299 P((x -> (-y -> -x)) -> (x -> y)).  [hyper(2,a,4,a,b,842,a)].

4612 P((-x -> x) -> x).  [hyper(2,a,1299,a,b,165,a)].

4613 $F.  [resolve(4612,a,6,a)].

Now, here's a proof in prefix notation.

% -------- Comments from original proof --------

% Proof 1 at 0.23 (+ 0.01) seconds.

% Length of proof is 22.

% Level of proof is 8.

% Maximum clause weight is 20.

% Given clauses 175.

1 P(C(C(N(x),x),x)) # label(non_clause) # label(goal).  [goal].

2 -P(C(x,y)) | -P(x) | P(y).  [assumption].

3 P(C(x,C(y,x))).  [assumption]. [this corresponds to L1]

4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption]. [this corresponds to L2]

5 P(C(C(N(x),N(y)),C(y,x))).  [assumption]. [this corresponds to L4]

6 -P(C(C(N(c1),c1),c1)).  [deny(1)].

7 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].

8 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].

9 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).  [hyper(2,a,3,a,b,4,a)].

11 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].

12 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].

14 P(C(x,C(y,C(z,C(u,z))))).  [hyper(2,a,3,a,b,7,a)].

26 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,8,a,b,7,a)].

44 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).  [hyper(2,a,8,a,b,14,a)].

159 P(C(N(x),C(x,y))).  [hyper(2,a,26,a,b,12,a)].

160 P(C(C(x,y),C(C(z,x),C(z,y)))).  [hyper(2,a,26,a,b,9,a)].

165 P(C(C(N(x),x),C(N(x),y))).  [hyper(2,a,4,a,b,159,a)].

815 P(C(C(C(x,y),z),C(y,z))).  [hyper(2,a,44,a,b,160,a)].

842 P(C(x,C(C(N(y),N(x)),y))).  [hyper(2,a,815,a,b,11,a)].

1299 P(C(C(x,C(N(y),N(x))),C(x,y))).  [hyper(2,a,4,a,b,842,a)].

4612 P(C(C(N(x),x),x)).  [hyper(2,a,1299,a,b,165,a)].

4613 $F.  [resolve(4612,a,6,a)].