C. A. Meredith's C-pure logic BCI (which has a page of its own elsewhere within this site) has, as axioms, the formulas B = CCpqCCrpCrq / (p→q)→((r→p)→(r→q)), C = CCpCqrCqCpr / (p→(q→r))→(q→(p→r)), and I = Cpp / p→p.  R. Kashima and N. Kamide [Substructural implicational logics including the relevant logic E, Studia Logica, vol. 63 (1999), pp. 181–212] have studied C alongside the seven variants of it in which one or more of its sentential variables is replaced with a new formula of the form Cxy:      C000.  CCpCqrCqCpr                                /  ((p→(q→r))→(q→(p→r))      C100.  CCCpsCqrCqCCpsr                       /  ((p→s)→(q→r))→(q→((p→s)→r))      C001.  CCpCqCruCqCpCru                      /  (p→(q→(r→u)))→(q→(p→(r→u)))      C101.  CCCpsCqCruCqCCpsCru            /  ((p→s)→(q→(r→u)))→(q→((p→s)→(r→u)))      C010.  CCpCCqtrCCqtCpr                        /  (p→((q→t)→r))→((q→t)→(p→r))      C110.  CCCpsCCqtrCCqtCCpsr              /  ((p→s)→((q→t)→r))→((q→t)→((p→s)→r))      C011.  CCpCCqtCruCCqtCpCru             /  (p→((q→t)→(r→u)))→((q→t)→(p→(r→u)))      C111.  CCCpsCCqtCruCCqtCCpsCru   /  ((p→s)→((q→t)→(r→u)))→((q→t)→((p→s)→(r→u))) There are 255 axiom sets obtainable by adding to B and I one or more of these formulas, but it turns out that only five nonequivalent logics result: BC011I, it’s two proper extensions BC001I and BC010I, their common proper  extension BC001C010I, and its proper extension, BCI itself.  And just as f0r BCI, each of these four subsystems can be axiomatized using a single-axiom. A SINGLE AXIOM FOR BC011I I've got a single axiom for BC011I of type <15, 4>, that is, containing 15 symbols (not counting parentheses) and occurrences of 4 distinct sentential variables: CCpqCCCrrCqsCps  /  (p→q)→(((r→r)→(q→s))→(p→q)) It is shortest possible, and it is unique: no other theorem of BC011I containing 15 or fewer symbols is a single axiom.   SINGLE AXIOMS FOR BC001I I have found three single axioms for BC001I, each of type <19, 5>: CpCCqrCCpCCssCrtCqt  /  p→((q→r)→((p→((s→s)→(r→t)))→(q→t))) CpCCpCqrCCCssCrtCqt  /  p→((p→(q→r))→(((s→s)→(r→t))→(q→t))) CCCppCqrCsCCsCrtCqt  /  ((p→p)→(q→r))→(s→((s→(r→t))→(q→t))) No shorter theorems of BC001I are single axioms for it, so these are shortest possible. Moreover, no other theorems of type <19,5> are single axioms.  I have not yet checked the other theorems of length 19 (only those of types <19, 3> and <19, 4> need be considered) but conjecture that none of them are single axioms either.   SINGLE AXIOMS FOR BC010I Each of the following five formulas is a type <19, 5> single axiom for BC010I: CCpqCCCCCrrssCqtCpt  /  (p→q)→(((((r→r)→s)→s)→(q→t))→(p→t)) CCCppCqrCCrsCCCqstt  /  ((p→p)→(q→r))→((r→s)→(((q→s)→t)→t)) CCCCpqCCCrrCqsCpstt  /  (((p→q)→((r→r)→(q→s))→(p→s))→t)→t CCpqCCCrrCqsCCCpstt  /  (p→q)→(((r→r)→(q→s))→((p→s)→t)→t)) CCpqCCCCCrrCqsCpstt  /  (p→q)→(((((r→r)→(q→s))→(p→s))→t)→t) No shorter theorems of BC010I are single axioms for it, nor are any other theorems of type <19,5> (though the length-19 theorems containing occurrences of just 3 or just 4 distinct sentential letters have not yet been checked).           The first of these axioms should be attributed to Meredith, who presents it as a single axiom for the system with axioms B and Specialized Assertion = CCCppqq / (((p→p)→q)→q), which he certainly would have known is an alternate axiomatization of BC010I.   SINGLE AXIOMS FOR BC001C010I My first single axiom for BC001C010I was the type <27, 7>  CCCCpqCCrCCssCqtCptCCuuvCrv, but I have since discovered seven shorter ones, each of type <23, 6>: CCCCpqCCrCqsCpsCCttuCru  /  (((p→q)→((r→(q→s))→(p→s)))→((t→t)→u))→(r→u) CCCpCCpCqrCsrCCttuCCsqu  /  ((p→((p→(q→r))→(s→r)))→((t→t)→u)))→((s→q)→u) CCCCpCqrCCsqCsrCCttuCpu  /  (((p→(q→r))→((s→q)→(s→r)))→((t→t)→u))→(p→u) CCCCpCqrCsrCCttuCCsqCpu  /  (((p→(q→r))→(s→r))→((t→t)→u))→((s→q)→(p→u)) CCCppCqrCsCCCCsCrtCqtuu  /  ((p→p)→(q→r))→(s→((((s→(r→t))→(q→t))→u)→u)) CCpqCCCCrCqsCpsCCttuCru  /  (p→q)→((((r→(q→s))→(p→s))→((t→t)→u))→(r→u)) CpCCCCpCqrCsrCCttuCCsqu  /   p→((((p→(q→r))→(s→r))→((t→t)→u))→((s→q)→u)) No theorems of BC001C010I of type <19,5> are single axioms for it, nor are any of its theorems containing fewer than 19 symbols.  Of the other BC001C010I theorems of length 19, only those of types <19, 3> and <19, 4> remain to be checked.             It seems very likely that there are additional single axioms of length 23, but I have not yet looked for them. © Dolph Ulrich, 2007        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 |