0
$\begingroup$

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 $\vdash$C$\alpha$$\beta$, from $\vdash$$\alpha$ also, we may infer $\vdash$$\beta$.

Can CNCxyx get proven in around 50 steps?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Doug Spoonwood Aug 28 '16 at 18:06
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.