            The implicational fragment RI of the relevance logic R can be axiomatized, with substitution and detachment as rules, by the following four axioms:          CCpqCCqrCpr / (p→q)→((q→r)→(p→r))            B' / Syl          CCpCqrCqCpr / (p→(q→r))→(q→(p→r))            C / Com          Cpp                      /  p→p                                                 I  / Id          CCpCpqCpq     / (p→(p→q))→(p→q)                    W/ Hilbert  The more standard axiomatization of RI uses B / Syl* = CCpqCCrpCrq / (p→q)→((r→p)→(r→q)) in place of B' / Syl (whence the common alternate name "BCIW" for RI).   Of course B' and B are interdeducible in the presence of C, but in my experience B' has seemed to be more generally useful in obtaining proofs of other results than B in a variety of settings.           Anderson and Belnap ask [Entailment: the logic of relevance and necessity, Princeton University Press, Princeton, 1975] if there exists a single axiom for RI, and the question was answered affirmatively by Rezus [On a theorem of Tarski, Libertas mathematica, vol. 2 (1982), pp. 63-9], who showed how to construct (but did not actually display) such an axiom.  Written out in full, the Rezus axiom developed from the base shown above is of type <93, 23>, that is, is 93 symbols in length and contains occurrences of 23 distinct sentence letters: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCdeCCefCdfgghhCCiCCCjjCCkkCCllCCmmCinnoo. NEW RESULTThe following theorem [proof here] of RI of type <35, 8> gives B', C, I, and W [proof here] and, so, is a single axiom for RI:                     CCCCCpqCrpCCpqCrqCCssCtCuvCCwtCuCwv. OPEN QUESTIONIs there a shorter single axiom?  (The author expects that the answer is "yes".) © 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 |