Lloyd Humberstone [Variations on a theme of Curry, Notre Dame
Journal of Formal Logic,
vol. 47 (2006), pp. 101131]
has stimulated interest in
the smallest extension of Meredith's system BCI in which each
theorem provably implies every theorem. He conjectures that the set
of theorems of that system, which he calls "monothetic BCI"
("mBCI"
for short)
are exactly the formulas provable in the system BCI* consisting
of the axioms B, C, and I* = CCppCqq / (p→p)→(q→q) together with the standard rules of substitution and
detachment
/ modus ponens. [The latter system had
been introduced earlier by M. W. Bunder in his paper The answer to a
problem of Iséki on BCI algebras, Mathematics
Seminar Notes, Kobe University, vol. 11 (1983), pp. 167169.] Humberstone himself goes a considerable way towards proving his conjecture, and, to complete the proof, needs only a demonstration that at least one formula of the form CCCpqCCqrCprCαα / ((p→q)→((q→r)→(p→r)))→(α→α) is provable in BCI*. My own demonstration that such a formula is, indeed, provable in BCI* runs thirteen steps in length. As it happens, a different proof (albeit somewhat longer) had been found earlier, before I had even heard of the problem, by two of Humberstone's colleagues: see T. Kowalski and S. Butchart, A note on monothetic BCI, Notre Dame Journal of Formal Logic, vol. 47, Number 4, 2006, pp. 541544.


NEW RESULTS Humberstone's three axioms can be reduced to two: I* plus the amazing formula CCCCpqqrCCrsCps / (((p→q)→q)→r)→((r→s)→(p→s)) does the job, and with a total of just 22 occurrences of sentence letters and connectives. More surprising is the fact that there is a single axiom involving just 19 such symbols that works, as well [proofs here]: BCI*1. CCCCppqrCCsCrtCqCst / (((p→p)→q)→r)→((s→(r→t))→(q→(s→t)))
No shorter single axiom exists,
but I have also found another of the same length:


Entrance page  Home page  Twentysix open questions  Single axioms for:

BCI 
4 subsystems of BCI 
monothetic BCI 
Cpure R 
Cpure RMingle 
Cpure
LNo   Dcomplete axioms for (classical) equivalence  Exit page  