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)((qr)(pr))            B' / Syl
          CCpCqrCqCpr / (p
(qr))(q(pr))            C / Com
          Cpp                      p
p                                                 I  / Id
          CCpCpqCpq     / (p
(pq))(pq)                    W/ Hilbert

The more standard axiomatization of RI uses B / Syl* = CCpqCCrpCrq / (pq)((rp)(rq)) 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:




e 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:


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