Ernst, Fitelson, Harris, and Wos [A concise axiomatization of RM→, Bulletin of the Section of Logic (University of Lódź), vol. 30 (2001), pp. 191-194]  discovered two three-bases for the implicational fragment of Dunn's system R-Mingle, {CCpqCCqrCpr, CpCCpqq, CCCCCpqrCqprr} and {CCpqCCqrCpr, CpCCpqq, CCCpCCCqprqrr}. Each of their bases has a total length of 31 (counting occurrences of sentential variables and of the connective).
                 Wos later asks [as Open Question OQ29.RM in L. Wos and G. Pieper, Automated Reasoning and the Discovery of Missing and Elegant Proofs, Rinton Press, Paramus, 2003] if there exists an equivalent two-base, and [as Open Question OQ30.RM] if there exists a single axiom for this system.
 
     
   

ANSWER TO OQ29.RM
Here are two two-bases, each of total length 28:

                CCCCpqqrCCrsCps
                 CCCCCpqrCqprr
                 CCCCpqqrCCrsCps
                CCCpCCCqprqrr


ANSWER TO OQ30.RM
My first single axioms for implicational R-Mingle were embarrassingly long (85 symbols in 21 distinct sentence letters, and 77 symbols in 19 letters). Here is a single axiom, 37 symbols in length and containing occurrences of nine distinct sentential variables:
                CCCCCCCpqrCqpCsrCsrCCttCuCvwCCxuCvCxw
For those who can open a Microsoft Word 2000 file, a document reviewing the long history (starting in 1952) of the problem of axiomatizing this logic, and displaying proofs for the bases listed above, is available by clicking here.

 

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