C. A. Meredith introduced the C-pure substitution/detachment system BCI in 1956 [cf. C. A. Meredith and A. N. Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, vol. IV (1963), pp. 171-187].
           As formulated originally by Meredith, BCI's well-formed formulas ('wffs', for short) are built from  denumerably many sentence letters p, q, r, ... and just one binary connective ('C' in Polish notation, '
' in standard infix notation). Its only rules of inference are (uniform) substitution of wffs for letters and detachment (i.e., modus ponens), the rule that permits inference of the wff β from any two wffs Cαβ and α, and Meredith's axioms were: 

  B.  CCpqCCrpCrq   /   (pq)((rp)(rq))     [B is also known as Syl* and as Weak Syl]
  C.  CCpCqrCqCpr   /    (p
(qr))(q(pr))      [C is also known as Com and as Exchange]
  I.   Cpp                        /    p
p                                        [I is also known as Id]



Many other axiom sets produce, with substitution and detachment, equivalent systems with the same theorems and the same derived rules of inference.  Most obviously, B can, in the presence of C, be replaced by its commuted variant B' = CCpqCCqrCpr / (pq)((qr)(pr)) [also known as Syl].
          Smaller axiom sets will do the job as well.  A simple two-base is given by B' together with the wff K1 = CpCCCqqCprr / p
(((qq)(pr))r) of A. Rezus's On a theorem of Tarski, Libertas Mathematica, vol 2 (1982), pp. 63-97.  An even shorter base (containing just 18 symbols in all, and apparently previously unknown) is given by {CCCCpqqrCCrsCps, Cpp}, which develops quite quickly.
          And Meredith himself found [see section 7 of the paper cited above] two examples of single axioms for this system, each 19 symbols in length (counting occurrences of letters and of the binary connective):   

  BCI-1.  CCpCqrCCCssCtqCtCpr   /   (p(qr))(((ss)(tq))(t(pr)))
  BCI-2.  CCCppCqrCCsCrtCqCst   /   ((p

I have completed a proof that these are shortest possible single axioms, that is, no theorem of BCI containing fewer than 19 symbols gives B, C, and I with the rules in question.  They are, however, not unique. I've found that each of the following twenty-six formulas is also a single axiom for BCI:

  BCI-3.   CCpqCCCrrCCCqsstCpt   /   (pq)(((rr)(((qs)s)t))(pt))
  BCI-4.   CCpqCCqCCrrCstCsCpt   /   (p
  BCI-5.   CCCCCppCqrrsCCstCqt   /   ((((p
.   CCCCpqqrCCCssCrtCpt   /   (((p
  BCI-7.   CCpCqrCCCCCssprtCqt   /   (p
  BCI-8.   CCpCqrCCCssCrtCqCpt   /   (p
  BCI-9.   CCCppCCCqrrsCCstCqt   /   ((p
  BCI-10. CCCppCqrCsCCrCstCqt   /   ((p
  BCI-11. CCCppCqrCCCCrsstCqt    /   ((p
  BCI-12. CCCppCqrCCrCstCsCqt   /   ((p
  BCI-13. CCpCCqqCrsCCstCrCpt   /   (p
  BCI-14. CCpCCqqrCsCCrCstCpt   /   (p
  BCI-15. CCpqCCCrrCqCstCsCpt   /   (p
  BCI-16. CCpCqrCqCCCssCrtCpt   /   (p
  BCI-17. CpCCCqqCrsCCsCptCrt   /    p
  BCI-18. CpCCqCprCCCssCrtCqt   /   p
  BCI-19. CCpqCrCCCssCqCrtCpt   /   (p
  BCI-20. CCCppCqrCCCCsttqCsr  /   ((p
  BCI-21. CpCCCqqCrCpsCCtrCts   /   p
  BCI-22. CCCppCqCrsCCtqCrCts   /   ((p
  BCI-23. CCpqCCCrrCCCspqtCst   /   (p
  BCI-24. CCpCCqqCrsCCtpCrCts   /   (p
  BCI-25. CCCppCqrCCCCsqrtCst   /   ((p
  BCI-26. CCCppCqrCCsCtqCtCsr   /   ((p
  BCI-27. CCpCCqqrCCrCstCsCpt   /   (p
  BCI-28. CCpCqrCCCssCtpCqCtr   /   (p

I and others next found fifty-two additional single axioms of this length for BCI BCI-29 below was discovered by John Halleck and Larry Wos. Working shortly thereafter  from a preliminary list of candidates I had circulated privately, Halleck also showed that the formulas shown below as BCI-73 and BCI-74  are single axioms, and Wos showed that BCI-75, BCI-76, and BCI-77 are as well.  BCI-78, BCI-79, and BCI-80 were shown to be single axioms by Mark Stickel.

  BCI-29. CCCppCqCrsCCstCrCqt / ((pp)(q(rs)))((st)(r(qt))) Halleck and Wos
  BCI-30. CCCppCqCrsCCtrCtCqs / ((pp)(q(rs)))((tr)(t(qs)))
  BCI-31. CCCppCqCrsCrCCstCqt / ((pp)(q(rs)))(r((st)(qt)))
  BCI-32. CCCppCqCrsCrCCtqCts / ((pp)(q(rs)))(r((tq)(ts)))
  BCI-33. CCCppCqrCqCCsCrtCst / ((pp)(qr))(q((s(rt))(st)))
  BCI-34. CCpCCqqCrsCCtrCtCps / (p((qq)(rs)))((tr)(t(ps)))
  BCI-35. CCpCqrCCsCCttpCqCsr / (p(qr))((s((tt)p))(q(sr)))
  BCI-36. CCpCqrCqCCCssCtpCtr / (p(qr))(q(((ss)(tp))(tr)))
  BCI-37. CCpqCCCCCrrCsttpCsq / (pq)(((((rr)(st))t)p)(sq))
  BCI-38. CCpqCCCrrCsCqtCpCst / (pq)(((rr)(s(qt)))(p(st)))
  BCI-39. CCpqCCCrrCsCtpCtCsq / (pq)(((rr)(s(tp)))(t(sq)))
  BCI-40. CCpqCCrCCssCqtCpCrt / (pq)((r((ss)(qt)))(p(rt)))
  BCI-41. CCpqCrCCCssCtCrpCtq / (pq)(r(((ss)(t(rp)))(tq)))
  BCI-42. CpCCqCCrrCpsCCstCqt / p((q((rr)(ps)))((st)(qt)))
  BCI-43. CpCCCqqCrsCCtCprCts / p(((qq)(rs))((t(pr))(ts)))
  BCI-44. CpCCqCCrrCpsCCtqCts / p((q((rr)(ps)))((tq)(ts)))
  BCI-45. CpCCqCCrrsCCsCptCqt / p((q((rr)s))((s(pt))(qt)))
  BCI-46. CCpCqrCsCCCttCsqCpr / (p(qr))(s(((tt)(sq))(pr)))
  BCI-47. CCpqCCrCCssCtpCtCrq / (pq)((r((ss)(tp)))(t(rq)))
  BCI-48. CpCCqCrsCCCttCprCqs / p((q(rs))(((tt)(pr))(qs)))
  BCI-49. CpCCqrCCCssCrCptCqt / p((qr)(((ss)(r(pt)))(qt)))
  BCI-50. CCCCCppqrsCCqCtrCts / ((((pq)q)r)s)((q(tr))(ts))
  BCI-51. CCCCpqqrCCCssCtpCtr / (((pq)q)r)(((ss)(tp))(tr))
  BCI-52. CCCCpqrsCCCttCqrCps / (((pq)r)s)(((tt)(qr))(ps))
  BCI-53. CCCppCCCqrrsCCtqCts / ((pp)(((qr)r)s))((tq)(ts))
  BCI-54. CCCppCCCqrstCCrsCqt / ((pp)(((qr)s)t))((rs)(qt))
  BCI-55. CCpqCpCCCrrCsCqtCst / (pq)(p(((rr)(s(qt)))(st)))
  BCI-56. CpCCqCprCCCssCtqCtr / p((q(pr))(((ss)(tq))(tr)))
  BCI-57. CpCCpqCCCrrCsCqtCst / p((pq)(((rr)(s(qt)))(st)))
  BCI-58. CpCCqrCCrCCssCptCqt / p((qr)((r((ss)(pt)))(qt)))
  BCI-59. CCCCCppCqrrsCCtqCts / ((((pp)(qr))r)s)((tq)(ts))
  BCI-60. CCCCpCqrrsCCCttpCqs / (((p(qr))r)s)(((tt)p)(qs))
  BCI-61. CCCppqCCCCqCrsstCrt / ((pp)q)((((q(rs))s)t)(rt))
  BCI-62. CCpCqrCqCCsCCttpCsr / (p(qr))(q((s((tt)p))(sr)))
  BCI-63. CCCppCqCrsCtCCtrCqs / ((pp)(q(rs)))(t((tr)(qs)))
  BCI-64. CCCppCCCqrCCsqrtCst / ((pp)(((qr)((sq)r))t))(st)
  BCI-65. CCpqCCCCqrrCCsstCpt / (pq)((((qr)r)((ss)t))(pt))
  BCI-66. CCpqCCCCrpqCCsstCrt / (pq)((((rp)q)((ss)t))(rt))
  BCI-67. CpCCCqqCrCpsCCstCrt / p(((qq)(r(ps)))((st)(rt)))
  BCI-68. CpCCCqqCrCstCCpsCrt / p(((qq)(r(st)))((ps)(rt)))
  BCI-69. CpCCqCCrrCstCCpsCqt / p((q((rr)(st)))((ps)(qt)))
  BCI-70. CpCCqCprCCsCCttqCsr / p((q(pr))((s((tt)q))(sr)))
  BCI-71. CpCCqrCCsCCttCpqCsr / p((qr)((s((tt)(pq)))(sr)))
  BCI-72. CpCCpqCCrCCssCqtCrt / p((pq)((r((ss)(qt)))(rt)))
  BCI-73. CCCppCqrCsCCtCsqCtr / ((pp)(qr))(s((t(sq))(tr))) Halleck
  BCI-74. CCpqCCCCCrrCqsstCpt / (pq)(((((rr)(qs))s)t)(pt)) Halleck
  BCI-75. CCpqCCCCrssCCttpCrq / (pq)((((rs)s)((tt)p))(rq)) Wos
  BCI-76. CCCCpqCCrpqCCsstCrt / (((pq)((rp)q))((ss)t))(rt) Wos
  BCI-77. CCCCCppCqrCCsqrtCst / ((((pp)(qr))((sq)r))t)(st) Wos
  BCI-78. CpCCqrCCCssCtCpqCtr / p((qr)(((ss)(t(pq)))(tr))) Stickel
  BCI-79. CCCCCppCqrstCCrsCqt / ((((pp)(qr))s)t)((rs)(qt)) Stickel
  BCI-80. CCpqCCCCCrrCspqtCst / (pq)(((((rr)(sp))q)t)(st)) Stickel


The only BCI theorems of length 19 whose status as single axioms for that system remain open are the following. If you can resolve the status of any of these, please e-mail me (dulrich at purdue dot edu). Those that have now been shown not to be single axioms are "deleted" by being highlighted in grey.

  BCI-Candidate   1 . CCpCCqqrCCCCsttpCsr / (p((qq)r))((((st)t)p)(sr))
  BCI-Candidate   2 . CCCCpqqCCrrsCCstCpt / (((pq)q)((rr)s))((st)(pt))
  BCI-Candidate   3 . CCCCpqqCCrrsCCtpCts / (((pq)q)((rr)s))((tp)(ts))
  BCI-Candidate   4 . CCCCpqrCCsstCCqrCpt / (((pq)r)((ss)t))((qr)(pt))
  BCI-Candidate   5 . CCCCpqqrCCrCCsstCpt / (((pq)q)r)((r((ss)t))(pt)) 

  BCI-Candidate   6. CCCCpqqrCCrCCsssCps / (((pq)q))r)((r((ss)s))(ps)
  BCI-Candidate   7. CCpCCqqCqrCCspCqCsr / (p((qq)(qr)))((sp)(q(sr)))
  BCI-Candidate   8. CCpCCqqr CCrCqsCqCps / (p((qq)r))((r(qs))(q(ps)))
  BCI-Candidate   9. CCpCqrCCCssCrsCqCps / (p(qr))(((ss)(rs))(q(ps)))
  BCI-Candidate 10. CCpCqrCCCssCspCqCsr / (p(qr))(((ss)(sp))(q(sr)))
  BCI-Candidate 11. CCpCqrCqCCCssCrsCps / (p(qr))(q(((ss)(rs))(ps)))
  BCI-Candidate 12. CCpCqrCsCCCrrCsqCpr / (p(qr))(s(((rr)(sq))(pr)))
  BCI-Candidate 13. CCpqCCCCrpqCCsssCrs / (pq)((((rp)q)((ss)s))(rs))
  BCI-Candidate 14. CCpqCCCCrssCCsspCrq / (pq)((((rs)s)((ss)p))(rq))
UP-DATE: John Halleck has found a syntactic proof that BCI-candidate 
                                               14 is not a single axiom for BCI.

  BCI-Candidate 15. CCpqCCCrrCCCspqrCsr / (pq)(((rr)(((sp)q)r))(sr))
  BCI-Candidate 16. CpCCCqqCqrCCrCpsCqs / p(((qq)(qr))((r(ps))(qs)))
  BCI-Candidate 17. CpCCCqqCrqCCsCprCsq / p(((qq)(rq))((s(pr))(sq)))
  BCI-Candidate 18. CpCCqCCppCprCCsqCsr / p((q((pp)(pr)))((sq)(sr)))
  BCI-Candidate 19. CpCCqCprCCCssCsqCsr / p((q(pr))(((ss)(sq))(sr)))
  BCI-Candidate 20. CpCCqrCCrCCppCpsCqs / p((qr)((r((pp)(ps)))(qs)))

Dolph Ulrich, 2007, 2009            

 Entrance page | Home page | Twenty-six open questions |

Single axioms for:  | BCI | 4 subsystems of BCI | monothetic BCI | C-pure R | C-pure R-Mingle | C-pure LNo |
| BCK | C-pure intuitionism | Classical equivalence | A few more systems |

| D-complete axioms for (classical) equivalence | Exit page |