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 |