How to prove (P→¬P)→¬P when ¬ is primitive

Question

The logical connectives are → and ¬. Usable logical axioms, theorems and rules are

• A→(B→A)
• (A→(B→C))→((A→B)→(A→C))
• (¬A→¬B)→(B→A)
• ¬¬A→A
• A→¬¬A
• modus ponens.

Deduction theorem is also available.

I know how to do this if there were a falsum constant ⊥ and ¬P were defined as P→⊥. Assuming P and P→¬P I get ¬P:=P→⊥, then ⊥ is deduced from P→⊥ and the added premise P and finally P→⊥ results from the deduction theorem, cancelling P.

Now with ¬ being primitive, all I can get now is P,P→¬P⊢¬P and P,¬P⊢anything. I can't find a way to cancel the additional premise P. (P→¬P)→¬P should be provable because this system is complete relative to the usual truth value semantics.

Thanks.

Answer 1

The proof is quite tedious...

We have to prove :

$\vdash (A \to B) \to ((\lnot A \to B) \to B)$ --- (*).

With it, and the additional result : $\vdash A \to A$ --- (§), we have :

1) $\vdash \lnot P \to \lnot P$ --- from (§)

2) $P \to \lnot P$ --- assumed [a]

3) $\vdash (P \to \lnot P) \to ((\lnot P \to \lnot P) \to \lnot P)$ --- from (*)

4) $\lnot P$ --- from 1), 2) and 3) by modus ponens twice

5) $(P \to \lnot P) \to \lnot P$ --- from 2) and 4) by Deduction Th, discharging [a].

---

Now for the proof of (*) above :

(A) 1) $A \to B$

2) $\lnot \lnot A$ --- assumed [a]

3) $\vdash \lnot \lnot A \to A$

4) $A$ --- by mp

5) $B$ --- by mp

6) $\vdash B \to \lnot \lnot B$

7) $\lnot \lnot B$ --- by mp

8) $A \to B \vdash \lnot \lnot A \to \lnot \lnot B$ --- by DT, discharging [a].

---

(B) 1) $A \to B$ --- premise

2) $\lnot \lnot A \to \lnot \lnot B$ --- from (A)

3) $A \to B \vdash \lnot B \to \lnot A$ --- from 2) and Ax.3 by mp.

---

(C) 1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- Ax.1

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

---

(D) 1) $\vdash \lnot A \to (A \to \lnot B)$ --- from (C)

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 mp and DT.

---

(E) 1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- from (D)

2) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from $\vdash P \to P$

3) $\vdash (\lnot A \to A) \to A$ --- from 1), 2) and Ax.2 by mp.

---

(F) 1) $A \to B$ --- premise

2) $\lnot A \to B$ --- premise

3) $\lnot B \to \lnot A$ --- from 1) and (B) by mp

4) $\lnot B \to B$ --- from 3) and 2) by mp and DT

5) $\vdash (\lnot B \to B) \to B$ --- from (E)

6) $A \to B, \lnot A \to B \vdash B$ --- from 4) and 5) by mp.

Now, (*) follows from (F) by DT.

---

---

Added

1) $A$ --- premise

2) $\lnot B$ --- premise

3) $A \to B$ --- assumed [a]

4) $B$ --- from 1) and 3) by mp

5) $(A \to B) \to B$ --- from 3) and 4) by DT, discharging [a]

6) $\lnot B \to \lnot (A \to B)$ --- from 5) by (B) above

$A , \lnot B \vdash \lnot (A \to B)$ --- from 1), 2) and 5) by mp.

Answer 2

The easiest way that i consider here is that $A \rightarrow B$ is true when A is false (or) B is true.

So, $p \rightarrow ¬p$ is equivalent to $¬p \lor ¬p \Leftrightarrow ¬p$

Answer 3

Suppose we rewrite the definition of a formula such that we use Polish notation. We might then consider the axioms as:

1 CxCyx (A$\rightarrow$(B$\rightarrow$A))

2 CCxCyzCCxyCxz ((A$\rightarrow$(B$\rightarrow$C))$\rightarrow$((A$\rightarrow$B)$\rightarrow$(A$\rightarrow$C)))

3 CCNxNyCyx (($\lnot$A$\rightarrow$$\lnot$B)$\rightarrow$(B$\rightarrow$A))

The goal of the exercise lies in proving:

CCxNxNx ((P$\rightarrow$$\lnot$P)$\rightarrow$$\lnot$P)

The following uses a diagrammatic technique to indicate a letter getting uniformly substituted with some other expression which satisfies the formation rules. Two slanted lines indicate a use of the rule of modus ponens (I would prefer to use arrows, but I don't have the knowledge at present to do that). Spacing gets used for purposes of display to make the substitutions clearer, but does not indicate part of the formulas. In other words, as an example, C $\alpha$ $\beta$ means exactly the same as C$\alpha$$\beta$.

2  CCx    CyzCCx    yCx    z
     |     ||  |    | |    |
     ----- ||  -----| -----| 
   CCCNxNyCyxCCCNxNyyCCNxNyx 3 CCNxNyCyx 
            \                  /
             6 CCCNxNyyCCNxNyx 

6 CCCNxNyyCCNxNyx

2 CCxCyzCCxyCxz
       |      |
  CCxCyxCCxyCxx  1 CxCyx 
           \       /
         7  CCxy  Cxx  
               |
               ---
            CCxCyxCxx 1 CxCyx 
                \      /
             11  Cx   x  2 CCx  CyzCCx  yCx  z  
                  |   |      |       |    |
                  --- ---    ---     ---  ---
                 CCyz Cyz  CCCyzCyzCCCyzyCCyzz
                      \           /
                       CCCyzyCCyzz
                          |||  |||
                    12 CCCxyxCCxyy 

12 CCCxyxCCxyy

                                 1 Cx        Cyx
                                    |         || 
                                    --------- |---------
                                   CCCNxNyCyxCzCCNxNyCyx 3 CCNxNyCyx 
                                                \          /
                                              8 CzCCNxNyCyx   
                 1 Cx          Cyx
                    |           ||
                    ----------- |-----------
                   CCzCCNxNyCyxCuCzCCNxNyCxyx 8 CzCCNxNyCyx            
                                 \             /
                                  CuCzCCNxNyCyx
                                   | |   | | ||
                             16   CxCyCCNzNuCuz

16 CxCyCCNzNuCuz

12 CCCx          yx          CCx          yy 16 Cx            CyCCNzNuCuz 
      |          ||            |          ||     | 
      -----------|-----------  -----------||     -------------
   CCCCyCCNzNuCuzaCyCCNzNuCuzCCCyCCNzNuCuzaa    CCCyCCNzNuCuzaCyCCNzNuCuz
                            \                  /
                             CCCyCCNzNuCuzaa
                                |   | | ||||
                       30    CCCxCCNyNzCzyuu

30 CCCxCCNyNzCzyuu

                               1 Cx          Cyx
                                  |           ||       
                                  ----------- |-----------
                                 CCCCxyxCCxyyCzCCCxyxCCxyy 12 CCCxyxCCxyy
                                             \            /
                             18               CzCCCxyxCCxyy
2 CCxCy     z    CCxy    Cxz      
    | |     |      ||     ||
    | ----- -----  |----- |----- 
  CCzCCCxyx CCxyyCCzCCxyxCzCCxyy              CzCCCxyxCCxyy 
                             \                /   1 CxCy  x     
                              CCzCCxyxCzCCxyx          |          
                                |      |               ---
                          33  CCxCCxyxCxCCxyx       CxCCxyx
                                      \             /
                                    93 CxCCxyx            

93 CxCCxyx

                          1 Cx      Cyx    93 CxCCxyx 
                             |       ||        |  |||
                             ------- |-------  |  |||  
                            CCyCCyzzCxCyCCyzz CyCCyzz
                                   \         /
                               95   CxCyCCyzz        
2 CCxCyz    CCxyCxz
       |          |
       -----      -----                        
  CCxCyCCyzzCCxyCxCCyzz             CxCyCCyzz
           \                        /
             119    CCxy  CxCCy  zz    
                       |      |
                       ---    ---
                    CCxCyxCxCCCyxzz   1 CxCyx
                            \          /
                        160  CxCCCyxzz    
2 CCxCy    zCCxy    Cxz
      |        |
      -----    -----
  CCxCCCyxzzCCxCCyxzCxz      CxCCCyxzz
            \               /
         164  CCxCCyxzCxz

119 CCxyCxCCyzz

164 CCxCCyxzCxz

30 CCCx CCNyNzCzyu      u   164 CCx CCy  x  z  Cx  z
      |      | | |      |         |   |  |  |   |  |  
      --     | | ------ ------    --  -- -- --- -- ---
   CCCNxCCNyNxCxyCNxCxy CNxCxy  CCNxCCNy Nx CxyCNx Cxy
                       \        /
                   270   CNxCxy

270 CNxCxy

                 1 Cx          Cyx      
                    |           ||
                    ----------- |-----------
                    CCCxCCyxzCxzCuCCxCCyxzCxz 164 CCxCCyxzCxz
                                \                  /
                                  272 Cu    CCxCCyxzCxz
164 CCx    CCy x     z  Cx     z       |
      |      | |     |   |     |       |
      -----  | ----- --- ----- ---     -----
    CCCCyxzCCx CCyxz CxzCCCyxz Cxz    CCCyxzCCxCCyxzCxz
                        \            /
                         CCCyxzCxz
                            ||  |
                    4685 CCCxyzCyz

4685 CCCxyzCyz

                  4685 CCCx    yz      Cyz         
                          |    ||       ||
                          -----|------- |-------
                       CCCCNyNxxCCNyNxyCxCCNyNxy 6 CCCNyNxxCCNyNxy
2 CCxCy    zCCxy    Cxz         \                 /
      |    |   |      | 4730     CxCCNyNxy
      -----|   -----  |
  CCxCCNyNxyCCxCNyNxCxy          CxCCNyNxy
            \                   /
              4822 CCxCNyNxCxy

4822 CCxCNyNxCxy

              2 CCx CyzCCx yCx z
                  |  ||  | | | |
                  -- ||  --| --|
                CCNxCxyCCNxxCNxy  270 CNxCxy
                       \             /
                     279  CCNxxCNxy  
4822 CCx   CNyNx   Cx   y         |
       |     | |    |   |         |
       ----  | ---- ----|         -----
     CCCNxxCNxNCNxxCCNxxx CCNxxCNxNCNxx
                   \      /
               6579 CCNxxx

6579 CCNxxx

4685 CCCxy   z      Cy   z     2 CCxCyzCCxyCxz
        ||   |       |   |         | ||  || ||
        |--- ------- --- -------   | ||  || ||
     CCCzCxy CCzxCzyCCxy CCzxCzy CCzCxyCCzxCzy
                        \        /
                    4731 CCxyCCzxCzy

4731 CCxyCCzxCzy

4731 CCx   yCCzx   Czy
       |   |   |     |
       ----|   ----  |
     CCCNxxxCCzCNxxCzx 6579 CCNxxx
            \               /
     6614     CCz     CNxxCz     x       4685 CCCxy zCy z
                |       || |     |                | | | 
                ------  || ------|                --| --| 
              CCCCxNyyCNyyCCCxNyyy            CCCxNyyCNyy
                          \                   /
                      7112  CCCxNyyy

7112 CCCxNyyy

4731 CCx     yCCzx     Czy
       |         |
       ------    ------
     CCCCxNyyyCCzCCxNyyCzy  7112 CCCxNyyy
              \                  /
                 CCzCCxNyyCzy
                   |  | || ||
            7188 CCxCCyNzzCxz

7188 CCxCCyNzzCxz

93 Cx     CCx     yy  
    |       |     ||
    ------  ------||
   CCNxCxyCCCNxCxyzz  270 CNxCxy
          \              /
         278 CCCNx   Cx   yz      z       7188 CCx    CCyNzzCx    z
                 |    |    |      |              |      | || |    |
                 ---- ---- ------ -------        -----  | || -----|
             CCCNCxNyCCxNyyCNCxNyyCNCxNyy      CCNCxNyCCxNyyCNCxNyy
                                 \            /
                              15176 CNCxNyy

15176 CNCxNyy

119 CCx    yCx    CCyzz
      |      |
      -----  -----
    CCNCxNyyCNCxNyCCyzz 15176 CNCxNyy
             \               /
        15320  CNCxNyCCyzz

15320 CNCxNyCCyzz

6579 CCNx       x       x      15320 CNCx   NyCCyz  z 
        |       |       |               |    |   |  |
        ------- ------  -------         ---- |   -- --
     CCNCCxNxNx CCxNxNx CCxNxNx      CNCCxNxNxCCxNx Nx
                      \              /
                    17238   CCxNxNx

17238 CCxNxNx

I do not recall seeing an instance of CCNxxx getting used as the major premiss (the longer one) when using the rule of modus ponens before in the axiomatic context. I feel rather surprised to see it happen at all in the axiomatic context, though perhaps this indicates something of the power of using an automated reasoning program as an assistant, since the above got obtained with the help of William McCune's program O.T.T.E.R. (originally developed at Argonne National Laboratory in the 1990s).

The above proof has 29 detachments (uses of the rule of detachment/the rule of modus ponens). I did find some other proofs (hyper-resolution proofs which correspond to condensed detachment proofs) when searching for this one, but so far at least, I do not know of a proof which indicates that this can get done with less than 29 detachments for this theorem. Though, perhaps a proof with fewer detachments can get found (using only the axioms that I used).