A SINGLE AXIOM FOR BCI'
Where I' is the formula CCpqCpq, the formula
    CCpqCCCrCCrssCqtCpt  /   (p→q)→(((r→((r→t)→t)→(q→t))→(p→t))
is a single axiom for BCI'.
 

THE STRICT-IMPLICATIONAL FRAGMENT OF THE MODAL LOGIC S3.
The formula
    CCCCpCpqCCrsCpqCCCtuCCvwCCCxxCwyCvyzz
is a theorem of C3, quickly giving the standard base consisting of Syl = CCpqCCqrCpr, Hilbert = CCpCpqCpq, and Weak Irrelevance = CCpqCrr.

 

BCK plus INVERSION
CCCpCqpCCCCrssCCsrrCtuCCuvCtv is a <29,7> single axiom for BCK + Inversion = CCCpqqCCqpp.

 

BCK plus LINEARITY    
CCCCCCpCqprrCCCstCCCutCtuCsuvCwv is a <31,7> single axiom for BCK+Linearity = CCCpqCqpCqp.

C-PURE LC
CCCpCqpCCCCCCrstCCCsrttCuCuvCwvxCCwux is a <37,9> single axiom  [proof here] for the implicational fragment of Dummett's LC, which is axiomatizable by adding Dummett = CCCpqrCCCqprr to a base for implicational intuitionism.

© 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 |