# Can the Negation of a Conditional Implying the First Atomic Proposition Get Proven in Around 50 Steps?

The following uses Polish notation with the following definition for meaningful expressions.

1. All lower case letters are meaningful expressions.
2. If $\alpha$ is a meaningful expression, then so is N$\alpha$.
3. If $\alpha$ is a meaningful expression, if $\beta$ is a meaningful expression also, then C$\alpha$$\beta is a meaningful expression. The axioms are Ax1 CxCyx Ax2 CCxCyzCCxyCxz Ax3 CCNxNyCyx The rules of inference are uniform substitution for any thesis of the system and C-detachment, from \vdashC\alpha$$\beta$, from $\vdash$$\alpha also, we may infer \vdash$$\beta$.

Can CNCxyx get proven in around 50 steps?

• My assistant OTTER has found some decent candidates to write shortish proofs, possibly near 50 lines of the theorem schema CNCxyx. In OTTER's system what I have, have length 23, level 11; length 21, level 12; and one of length 20, level 13, all of which might help. I'll see. – Doug Spoonwood Aug 28 '16 at 18:06

Counting the axioms as steps in the proof, the following consists of a less than 50 step which indicates an answer of yes.

                                                     Expansion Number

1 CxCyx

2 CCxCyzCCxyCxz

3 CCNxNyCyx

1/CxCyx, y/z           4 CCxCyxCzCxCyx

4 * C1-5               5 CzCxCyx                            2

1 x/CCNxNyCyx, y/z     6 CCCNxNyCyxCzCCNxNyCyx

6 * C3-7               7 CzCCNxNyCyx                        2

2 x/z, y/x, z/Cyx      8 CCzCxCyxCCzxCzCyx

8 * C5-9               9 CCzxCzCyx                          2

2 x/z, y/CNxNy, z/Cyx  10 CCzCCNxNyCyxCCzCNxNyCzCyx

10 * C7-11             11 CCzCNxNyCzCyx                      2

11 z/Ny                12 CCNyCNxNyCNyCyx

1 x/Ny, y/Nx           13 CNyCNxNy

12 * C13-14            14 CNyCyx                             3

9 z/Ny, x/Cyx, y/z     15 CCNyCyxCNyCzCyx

15 * C14-16            16 CNyCzCyx                           2

2 x/Ny, z/x            17 CCNyCyxCCNyyCNyx

17 * C14-18            18 CCNyyCNyx                          2

11 z/CNyy, x/y, y/x    19 CCCNyyCNyNxCCNyyCxy

18 x/Nx                20 CCNyyCNyNx

19 * C20-21            21 CCNyyCxy                           3

1 x/CCNyyCNyx, y/z     22 CCCNyyCNyxCzCCNyyCNyx

22 * C18-23            23 CzCCNyyCNyx                        2

2 x/CNyy, y/x, z/y     24 CCCNyyCxyCCCNyyxCCNyyy

24 * C21               25 CCCNyyxCCNyyy                      2

2 x/z, y/CNyy, z/CNyx  26 CCzCCNyyCNyxCCzCNyyCzCNyx

26 * 23-27             27 CCzCNyyCzCNyx                      2

25 x/Cxy               28 CCCNyyCxyCCNyyy

28 * C21-29            29 CCNyyy                             2

27 z/Ny, y/Cyx, x/z    30 CCNyCNCyxCyxCNyCNCyxz

16 z/NCyx              31 CNyCNCyxCyx

30 * C31-32            32 CNyCNCyxz                          3

1 x/CCNyyy, y/x        33 CCCNyyyCxCCNyyy

33 * C29-34            34 CxCCNyyy                           2

2 x/Ny, y/NCyx         35 CCNyCNCyxzCCNyNCyxCNyz

35 * C32-36            36 CCNyNCyxCNyz                       2

2 y/CNyy, z/y          37 CCxCCNyyyCCxCNyyCxy

37 * C34-38            38 CCxCNyyCxy                         2

9 z/CxCNyy, x/Cxy, y/z 39 CCCxCNyyCxyCCxCNyyCzCxy

39 * C38-40            40 CCxCNyyCzCxy                       2

40 x/CNyNCyx           41 CCCNyNCyxCNyyCzCCNyNCyxy

36 z/y                 42 CCNyNCyxCNyy

41 * C42-43            43 CzCCNyNCyxy                        3

2 x/z, y/CNyNCyx, z/y  44 CCzCCNyNCyxyCCzCNyNCyxCzy

44 * C43-45            45 CCzCNyNCyxCzy                      2

45 z/NCxy, y/x, x/y    46 CCNCxyCNxNCxyCNCxyx

1 x/NCxy, y/NCxy       47 CNCxyCNxNCxy

46 * C47-48            48 CNCxyx                             3


I constructed the above proof with the help of this first-order, hyperresolution proof I found with OTTER as my assistant.

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

2 [] -P(C(N(C(p,N(q))),p)).

3 [] P(C(x,C(y,x))).

4 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

5 [] P(C(C(N(x),N(y)),C(y,x))).

6 [hyper,1,3,3] P(C(x,C(y,C(z,y)))).

8 [hyper,1,3,5] P(C(x,C(C(N(y),N(z)),C(z,y)))).

9 [hyper,1,4,6] P(C(C(x,y),C(x,C(z,y)))).

15 [hyper,1,4,8] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).

30 [hyper,1,15,3] P(C(N(x),C(x,y))).

67 [hyper,1,9,30] P(C(N(x),C(y,C(x,z)))).

68 [hyper,1,4,30] P(C(C(N(x),x),C(N(x),y))).

136 [hyper,1,15,68] P(C(C(N(x),x),C(y,x))).

138 [hyper,1,3,68] P(C(x,C(C(N(y),y),C(N(y),z)))).

220 [hyper,1,4,136] P(C(C(C(N(x),x),y),C(C(N(x),x),x))).

240 [hyper,1,4,138] P(C(C(x,C(N(y),y)),C(x,C(N(y),z)))).

326 [hyper,1,220,136] P(C(C(N(x),x),x)).

353 [hyper,1,240,67] P(C(N(x),C(N(C(x,y)),z))).

459 [hyper,1,3,326] P(C(x,C(C(N(y),y),y))).

503 [hyper,1,4,353] P(C(C(N(x),N(C(x,y))),C(N(x),z))).

659 [hyper,1,4,459] P(C(C(x,C(N(y),y)),C(x,y))).

902 [hyper,1,9,659] P(C(C(x,C(N(y),y)),C(z,C(x,y)))).

1343 [hyper,1,902,503] P(C(x,C(C(N(y),N(C(y,z))),y))).

1859 [hyper,1,4,1343] P(C(C(x,C(N(y),N(C(y,z)))),C(x,y))).

2803 [hyper,1,1859,3] P(C(N(C(x,y)),x)).

4153 [hyper,2,2803] \$F.