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"
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
/ 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.
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:
| D-complete axioms for (classical) equivalence | Exit page |