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 |