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  /   (p→q)→((r→p)→(r→q))     [B / Syl* / Weak Syl]
            C.  CCpCqrCqCpr  /    p→(q→r))→(q→(p→r))      [C / Com]
            K.   CpCqp                /    p→(q→p)                               [K / Simp]

Shorter bases exist.  For an example that I have not found in the literature, one can replace B with B' = CCpqCCqrCpr / (p→q)→((q→r)→(p→r)) [also known as Syl] and then collapse C and K into CCCpCqprr / ((p→(q→p))→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 / [(p→q)→r]→{[s→(r→t)]→[q→(s→t)]}
     
   

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→(q→r))→{[(p→t)→q]→[t→(s→r)]}
           BCK-3.  CpCCqCrsCCCtprCqs   /  p→[(q→(r→s))→{[(t→p)→r]→(q→s)}]
           BCK-4.  CCCpqrCqCCsCrtCst    /  [(p→q)→r]→[q→{[s→(r→t)]→(s→t)]}]
           BCK-5.  CpCCCqprCCsCrtCst    /  p→[[(q→p)→r]→{[s→(r→t)]→(s→t)]}]
           BCK-6.  CpCCCqrsCCsCptCrt    /  p→[[(q→r)→s]→{[s→(p→t)]→(r→t)]}]
           BCK-7.  CCCpqrCsCCrCstCqt    /  [(p→q)→r]→[s→{[r→(s→t)]→(q→t)]}]
           BCK-8.  CCpCqrCsCCCtsqCpr   /  [p→(q→r)]→[s→{[(t→s)→q]→(p→r)}]
 


 OPEN QUESTIONS
There are thirty-three theorems of BCK of length 17 whose status I have not yet been able to determine. 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
          BCK-Candidate   4. CCpCqrCCCstpCqCtr
          BCK-Candidate   5. CCpqCCCrsCqtCpCst
          BCK-Candidate   6. CCCCCpqrrsCCstCqt
          BCK-Candidate   7. CpCCqCCrpsCCtqCts
          BCK-Candidate   8. CpCCqCprCCCstqCtr
          BCK-Candidate   9. CCCpqrCCCCrsCqstt
          BCK-Candidate 10. CCCpqrCCrCstCsCqt
          BCK-Candidate 11. CCCpqrCCrsCCCqstt
          BCK-Candidate 12. CCpCqrCqCCCstpCtr
          BCK-Candidate 13. CCpqCCqCCrstCsCpt
          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
          BCK-Candidate 30. CCpqCpCCCprCqsCrs
          BCK-Candidate 31. CpCCCpqrCCrCpsCqs
          BCK-Candidate 32. CpCCCqprCCqCrsCqs
          BCK-Candidate 33. CpCCpqCCCprCqsCrs


© Dolph Ulrich, 2007

 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 |