Lloyd Humberstone [Variations on a theme of Curry, Notre Dame Journal of Formal Logic, vol. 47 (2006),  pp. 101-131]  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. 167-169.]           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. 541-544. 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:              BCI*-2.  CCpCqrCCCCsstqCtCpr / (p→(q→r)) →((((s→s)→t)→q)→(t→(p→r))   I note, in passing, that CCpqCCCCrrCssCqtCpt / (p→q)→((((r→r)→(s→s))→(q→t))→(p→t)) is a single axiom for BC011I*, where C011 = CCpCCqtCruCCqtCpCru / (p→((q→t)→(r→u)))→((q→t)→(p→(r→u))) © 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 |