Cleaning up some odds and ends, here are single axioms for a few more systems:
 
     
   

A SINGLE AXIOM FOR BCI'
Where I' is the formula CCpqCpq, the formula
  
 CCpqCCCrCCrssCqtCpt  /   (pq)(((r((rt)t)(qt))(pt))
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 |