C. A. Meredith introduced the C-pure substitution/detachment system BCK 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].
 
           With substitution and detachment/modus ponens as rules,
Meredith's origjnal axioms were:
        
 B
.  CCpqCCrpCrq  /   (pq)[(rp)(rq)]     [B / Syl* / Weak Syl]
           C.  CCpCqrCqCpr  /    [p(qr)][q(pr)]      [C / Com]
           K.   CpCqp                /    p(qp)                               [K / Simp]

Shorter bases exist.  For an example that I have not found in the literature, one can replace B with B' = CCpqCCqrCpr / (pq)((qr)(pr)) [also known as Syl] and then collapse C and K into CCCpCqprr / ((p(qp))r)r giving us a 2-base containing in all just 20 occurrences of letters and the connective [proofs here].
          Meredith also found
[see section 8 of the paper cited above] the first single axiom for BCK. It is of type <17,5>, being 17 symbols in length with occurrences of 5 distinct sentence letters:
        
BCK-1
.  CCCpqrCCsCrtCqCst / [(pq)r]{[s(rt)][q(st)]}

     
   

NEW RESULTS
I've completed a proof that no shorter single axioms for BCK exist.  However,
I have found seven additional type <17,5> single axioms for it:

       
 
BCK-2.  CCpCqrCCCstqCtCpr   /  (p(qr)){[(pt)q][t(sr)]}
         BCK-3.  CpCCqCrsCCCtprCqs   /  p[(q(rs)){[(tp)r](qs)}]
         BCK-4.  CCCpqrCqCCsCrtCst    /  [(pq)r][q{[s(rt)](st)]}]
         BCK-5.  CpCCCqprCCsCrtCst    /  p[[(qp)r]{[s(rt)](st)]}]
         BCK-6.  CpCCCqrsCCsCptCrt    /  p[[(qr)s]{[s(pt)](rt)]}]
         BCK-7.  CCCpqrCsCCrCstCqt    /  [(pq)r][s{[r(st)](qt)]}]
         BCK-8.  CCpCqrCsCCCtsqCpr   /  [p(qr)][s{[(ts)q](pr)}]
 

Next I and, independently, John Halleck, showed that BCK-Candidate 13 from the list of previously unresolved candidates displayed below is an additional single axiom for BCK.  Subsequently (April, 2009), Mark Stickel found proofs that four additional formulas from that list are single axioms.

          BCK-9.    CCpqCCqCCrstCsCpt / (pq)[{q[(rs)t]}[(s(pt)]]
                                (Also shown by John Halleck independently; formerly BCK-Candidate 13)
          BCK-10. CCpCCqrsCrCCtpCts / {p[(qr)s]}{r[(tp)(ts)]}
                                (Shown by Mark Stickel; formerly BCK-Candidate 3)
          BCK-11. CpCCqCCrpsCCtqCtsp{q[(rp)s]}[(tq)(ts)]
                               (Shown by Mark Stickel; formerly BCK-Candidate 7)
          BCK-12. CCpCqrCqCCCstpCtr / [p(qr)][q{[(st)p](tr)}]
                               (Shown by Mark Stickel; formerly BCK-Candidate 12)
          BCK-13CpCCqCprCCCstqCtr / p[[q(pr)]{[(st)q](tr)}]
                               (Shown by Mark Stickel; formerly BCK-Candidate 8)


OPEN QUESTIONS
John Halleck has shown, via a syntactic argument, that BCK-Candidate 29 is not a single axiom. So there remain twenty-seven theorems of BCK of length 17 (those not deleted with grey highlighting below) whose status has not yet been determined. Please e-mail me (dulrich at purdue dot edu) if you can settle the status of any of them.

          BCK-Candidate   1. CCCpqCrsCCtrCtCqs
          BCK-Candidate   2. CCCpqrCCCCrsstCqt
          BCK-Candidate   3. CCpCCqrsCrCCtpCts (a single axiom for BCK - Stickel)
          BCK-Candidate   4. CCpCqrCCCstpCqCtr
          BCK-Candidate   5. CCpqCCCrsCqtCpCst
          BCK-Candidate   6. CCCCCpqrrsCCstCqt
          BCK-Candidate   7. CpCCqCCrpsCCtqCts (a single axiom for BCK - Stickel)
          BCK-Candidate   8. CpCCqCprCCCstqCtr (a single axiom for BCK - Stickel)
          BCK-Candidate   9. CCCpqrCCCCrsCqstt
          BCK-Candidate 10. CCCpqrCCrCstCsCqt
          BCK-Candidate 11. CCCpqrCCrsCCCqstt
          BCK-Candidate 12. CCpCqrCqCCCstpCtr (a single axiom for BCK - Stickel)
          BCK-Candidate 13. CCpqCCqCCrstCsCpt (a single axiom for BCK-Ulrich/Halleck)
          BCK-Candidate 14. CCpqCpCCCrsCqtCst
          BCK-Candidate 15. CCCCCpqrCCrsCqstt
          BCK-Candidate 16. CpCCpqCCCrsCqtCst
          BCK-Candidate 17. CCCpqrCCpCrsCqCps
          BCK-Candidate 18. CCCpqrCCrCpsCpCqs
          BCK-Candidate 19. CCCpqCrsCCprCpCqs
          BCK-Candidate 20. CCCpqrCpCCrCpsCqs
          BCK-Candidate 21. CCCpqrCqCCpCrsCps
          BCK-Candidate 22. CCpCCqrsCrCCqpCqs
          BCK-Candidate 23. CCpCqrCCCpsqCsCpr
          BCK-Candidate 24. CCpCqrCqCCCqspCsr
          BCK-Candidate 25. CCpCqrCsCCCpsqCpr
          BCK-Candidate 26. CCpqCCCprCqsCpCrs
          BCK-Candidate 27. CCpqCCCqrCqsCpCrs
          BCK-Candidate 28. CCpqCCqCCprsCrCps
          BCK-Candidate 29. CCpqCCqCCqrsCrCps  (not a single axiom - Halleck)
          BCK-Candidate 30. CCpqCpCCCprCqsCrs
          BCK-Candidate 31. CpCCCpqrCCrCpsCqs
          BCK-Candidate 32. CpCCCqprCCqCrsCqs
          BCK-Candidate 33. CpCCpqCCCprCqsCrs


© 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 |