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)}]   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 / (p→q)→[{q→[(r→s)→t]}→[(s→(p→t)]]                                 (Also shown by John Halleck independently; formerly BCK-Candidate 13)           BCK-10. CCpCCqrsCrCCtpCts / {p→[(q→r)→s]}→{r→[(t→p)→(t→s)]}                                 (Shown by Mark Stickel; formerly BCK-Candidate 3)           BCK-11. CpCCqCCrpsCCtqCts /  p→{q→[(r→p)→s]}→[(t→q)→(t→s)]                                (Shown by Mark Stickel; formerly BCK-Candidate 7)           BCK-12. CCpCqrCqCCCstpCtr / [p→(q→r)]→[q→{[(s→t)→p]→(t→r)}]                                (Shown by Mark Stickel; formerly BCK-Candidate 12)           BCK-13.  CpCCqCprCCCstqCtr / p→[[q→(p→r)]→{[(s→t)→q]→(t→r)}]                                (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 |