Suppose that the axioms consist of the following three meaningful expressions, or correspond to the following three axioms if the formation rules get written differently:

Axiom          Alternative                           Name
CxCyx          C(x, C(y, x))                         Recursive Letter Prefixing
CCxCyzCCxyCxz  C(C(x, C(y, z)), C(C(x, y), C(x, z))) Conditional Distribution
CCNxNyCyx      C(C(N(x), N(y)), C(y, x))             Transposed Negation Elimination

Suppose that the only rules of inference allow for consistent substitution for letters with meaningful expressions (substitution in a meaningful expression has to work out as uniform... if we substitute one letter with some meaningful expression in one spot in a meaningful expression, we have to substitute it with an equiform/"the same" meaningful expression in another spot), and detachment:

From $\vdash$C$\alpha$$\beta$ and $\vdash$$\alpha$ we may infer that $\vdash$$\beta$.

I will refer to CCxyCCNxyy or any correspondent meaningful expression as "Eliminated Excluded Middle" hereafter, since it can get obtained from the law of the excluded middle AxNx and CAxyCCxzCCyzz.

Eliminated Excluded Middle gets listed in A. N. Prior's appendix as an axiom in a system used by Hilbert in a 1922 text. Reading elsewhere suggests that the text is Hilbert and Ackermann's Grundzuge der theoretischen Logik (translated as "Principles of Mathematical Logic"). Mauro Allerganza used Eliminated Excluded Middle recently in an answer to another question. Eliminated Excluded Middle also got derived in Elliot Mendelson's Introduction to Mathematical Logic as the last part of Lemma 1.11 (g) on p. 38 and then used in the metalogical proof of the completeness theorem (did Kalmar also use Eliminated Excluded Middle?).

Can a proof of Eliminated Excluded Middle get proven from Recursive Letter Prefixing, Conditional Distribution, and Transposed Negation Elimination in less than or equal to 50 detachments?

Using an automated reasoning program it has suggested that it comes as possible to write a proof with 74 detachments, 73 detachments, 69 detachments, 113 detachments, 93 detachments, 75 detachments, 76 detachments, 124 detachments, 61 detachments, 60 detachments, 63 detachments, 68 detachments, 71 detachments, a distinct proof with 68 detachments, 72 detachments, a distinct proof with 61 detachments, a distinct proof with 74 detachments, 117 detachments, a distinct proof with 60 detachments, and to write a proof with 59 detachments of Eliminated Excluded Middle from the above 3 axioms.

Edit: The automated reasoning program has suggested some more proofs, including a proof with 58 detachments.

Edit 2: A 57 detachment proof also can get written.

  • $\begingroup$ Can you explain why this sort of question is of interest? $\endgroup$ – Mariano Suárez-Álvarez Nov 11 '16 at 3:26
  • $\begingroup$ I'm curious why you are using "automated reasoning" for simple propositional logic. Negate the formula, feed it to a SAT solver. Asymptotically, the sat solver is your shortest proof. $\endgroup$ – DanielV Nov 11 '16 at 4:27
  • $\begingroup$ @MarianoSuárez-Álvarez If you check the link where Mauro posted his answer (see above), you'll see that we both posted proofs. At the time I believed that if he had proved CCxyCCNxyy (or it's correlate in another notation scheme) using just substitution and detachment, he would need more detachments to construct a proof relying on CCxyCCNxyy. But, now I'm not so sure. Also, this isn't necessarily an all too easy problem for a theorem prover to even find a proof in that it may require some input from the user to find a solution a fair amount of time. Also, the formula seems to have importance. $\endgroup$ – Doug Spoonwood Nov 11 '16 at 4:41
  • $\begingroup$ @DanielV I'm not familiar with how SAT solvers work. But, do they output something where there exists a sequence of formulas such that every single step corresponds to a tautology in propositional logic, using only the axioms and the rule of detachment/condensed detachment? If they do, have you tried this problem with an SAT solver and has it produced a proof? Or does it run into problems because it has to keep track of ever so many formulas and gets lost exploring too much of the theory? $\endgroup$ – Doug Spoonwood Nov 11 '16 at 4:51

At the end of this answer is a hyperresolution proof, used with permission, which Larry Wos obtained with the help of O.T.T.E.R.

Before that, though, I will display a proof of only 23 detachments with appropriate substitutions. This should not got interpreted as meaning that necessarily no shorter proof exists. The numerals in what follows only correspond to the proof below when a detachment gets made. There is no correspondence when a substitution gets made. Perhaps it is objectionable to do so during a course of a proof, but some different prefix notations will get used in the course of this demonstration. When in doubt as to how a notation works, we drop all parentheses and remove all spaces to see a form which fits with a definition suitable for the axioms.

Axiom                              3 CxCyx
Axiom                              4 CCxCyzCCxyCxz
Axiom                              5 CCNxNyCyx
3 x/CxCyx, y/z * 6                 6 CCxCyxCzCxCyx
6 * C3-25                         25 (C z (C x (C y x)))
4 x/CxCyz, y/Cxy, z/Cxz           26 CCCxCyzCCxyCxzCCCxCyzCxyCCxCyzCxz
26 * C4-27                        27 C C C x C y z C x y C C x C y z C x z
27 y/Cyx * 28                     28 CCCxCCyxzCxCyxCCxCCyxzCxz
25 z/CxCCyxz * 29                 29 CCxCCyxzCxCyx
28 * C28-32                       32 C C x C C y x z C x z
3 x/CCxCCyxzCxz, y/u *33          33 CCCxCCyxzCxzCuCCxCCyxzCxz
33 * C32-41                       41 C u C C x C C y x z C x z
32 y/x, x/CCyxz, z/Cxz * 42       42 CCCCyxzCCxCCyxzCxzCCCyxzCxz
41 u/CCyxz * 43                   43 CCCyxzCCxCCyxzCxz
42 * C43-45                       45 C(C(C(y,x),z),C(x,z))
45 y/Nx, x/Ny, z/Cyx              46 CCCNxNyCyxCNyCyx
46 * C5-51                        51 C (N y) (C y x)
45 y/x, x/Cyz, z/CCxyCxz * 52     52 CCCxCyzCCxyCxzCCyzCCxyCxz
52 * C4-53                        53 C Cyz CCxyCxz
4 x/Ny, z/x * 54                  54 CCNyCyxCCNyyCNyx
54 * C51-60                       60 C (CNyy) C (Ny) (x)
53 y/CCyxz, z/Cxz, x/u * 61       61 CCCCyxzCxzCCuCCyxzCuCxz
61 * C45-62                       62 C CuCCyxz CuCxz
53 y/CNxNy, z/Cyx, x/z            63 CCCNxNyCyxCCzCNxNyCzCyx
63 * C5-64                        64 C CzCNxNy C z C y x
62 u/CxCyz, y/x, x/y, z/Cxz * 65  65 CCCxCyzCCxyCxzCCxCyzCyCxz
65 * C4-79                        79 C C x C y z C y C x z
64 z/CNyy, x/y, y/z * 80          80 CCCNyyCNyNzCCNyyCzy
60 x/Nz * 81                      81 CCNyyCNyNz
80 * C81-82                       82 (C (C (N y) y) (C z y))
79 x/Cyz, y/Cxy, z/Cxz * 83       83 CCCyzCCxyCxzCCxyCCyzCxz
83 * C53-96                       96 C Cxy C Cyz Cxz
82 z/Cyx * 97                     97 CCNyyCCyxy
32 x/CNyy, z/y                    98 CCCNyyCCyxzCCNyyy
98 * C97-104                     104 (C (C (N y) y) y)


96 x/Cxy, y/CCyzCxz, z/u * 105   105 CCCxyCCyzCxzCCCCyzCxzuCCxyu
105 * C96-112                    112 C C C C y z C x z u C C x y u
53 y/CNyy, z/y, x/z * 113        113 CCCNyyyCCzCNyyCzy
113 * C104-118                   118 C C z C N y y C z y
118 z/Cyx, y/x                   119 CCCyxCNxxCCyxx
112 z/x, x/Nx, u/CCyxx           120 CCCCyxCNxxCCyxxCCNxyCCyxx
120 * C119-134                   134 C CNxy C Cyx x
96 x/CNxy, y/CCyxx * 135         135 CCCNxyCCyxxCCCCyxxzCCNxyz
135 * C134-144                   144 C C C C y x x z C C N x y z
134 x/y, y/Cyx * 145             145 CCNyCyxCCCyxyy
145 * C51-146                    146 C(C(C(y,x),y),y)
53 y/CCyxy, z/y, x/z * 147       147 CCCCyxyyCCzCCyxyCzy
147 * C146-158                   158 C C z C C y x y C z y
158 z/Cay * 159                  159 CCCayCCyxyCCayy
112 x/Cyx, z/y, u/CCayy, y/a    159' CCCCayCCyxyCCayyCCCyxaCCayy
159' * C159-160                  160 C (C C y x a) C (C a y) y
160 a/x * 161                    161 CCCyxxCCxyy
144 z/CCxyy                      162 CCCCyxxCCxyyCCNxyCCxyy
162 * C161-163                   163 C CNxy C Cxy y
79 x/CNxy, y/Cxy, z/y            164 CCCNxyCCxyyCCxyCCNxyy
164 * 163-174                    174 CCxyCCNxyy

----- Otter 3.3g-work, Jan 2005 ----- The process was started by wos on vanquish, Wed Nov 9 21:08:42 2016 The command was "otter". The

process ID is 17263.

----> UNIT CONFLICT at 0.02 sec ----> 175 [binary,174.1,11.1] $ANS(TAR).

Length of proof is 23. Level of proof is 15.

---------------- PROOF ----------------

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

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

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

5 [] P(i(i(n(x),n(y)),i(y,x))).

11 [] -P(i(i(a1,a2),i(i(n(a1),a2),a2)))|$ANS(TAR).

25 [hyper,1,3,3] P(i(x,i(y,i(z,y)))).

27 [hyper,1,4,4] P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).

32 [hyper,1,27,25] P(i(i(x,i(i(y,x),z)),i(x,z))).

41 [hyper,1,3,32] P(i(x,i(i(y,i(i(z,y),u)),i(y,u)))).

45 [hyper,1,32,41] P(i(i(i(x,y),z),i(y,z))).

51 [hyper,1,45,5] P(i(n(x),i(x,y))).

53 [hyper,1,45,4] P(i(i(x,y),i(i(z,x),i(z,y)))).

60 [hyper,1,4,51] P(i(i(n(x),x),i(n(x),y))).

62 [hyper,1,53,45] P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))).

64 [hyper,1,53,5] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).

79 [hyper,1,62,4] P(i(i(x,i(y,z)),i(y,i(x,z)))).

82 [hyper,1,64,60] P(i(i(n(x),x),i(y,x))).

96 [hyper,1,79,53] P(i(i(x,y),i(i(y,z),i(x,z)))).

104 [hyper,1,32,82] P(i(i(n(x),x),x)).

112 [hyper,1,96,96] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).

118 [hyper,1,53,104] P(i(i(x,i(n(y),y)),i(x,y))).

134 [hyper,1,112,118] P(i(i(n(x),y),i(i(y,x),x))).

144 [hyper,1,96,134] P(i(i(i(i(x,y),y),z),i(i(n(y),x),z))).

146 [hyper,1,134,51] P(i(i(i(x,y),x),x)).

158 [hyper,1,53,146] P(i(i(x,i(i(y,z),y)),i(x,y))).

160 [hyper,1,112,158] P(i(i(i(x,y),z),i(i(z,x),x))).

166 [hyper,1,144,160] P(i(i(n(x),y),i(i(x,y),y))).

174 [hyper,1,79,166] P(i(i(x,y),i(i(n(x),y),y))).

175 [binary,174.1,11.1] $ANS(TAR).


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.