Proof about Clavius's Law

Question

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:

1. $\neg A \rightarrow (A \rightarrow \neg A)$ by L1
2. $(\neg A \rightarrow (A \rightarrow \neg A)) \rightarrow (\neg A \rightarrow A) \rightarrow (\neg A \rightarrow \neg A)$ by L2
3. $(\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

Answer 1

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

Answer 2

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)].

Answer 3

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