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. 639], 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
RESULT
CCCCCpqCrpCCpqCrqCCssCtCuvCCwtCuCwv. 

© Dolph Ulrich, 2007 Entrance page  Home page  Twentysix open questions  Single axioms for:

BCI 
4 subsystems of BCI 
monothetic BCI 
Cpure R 
Cpure RMingle 
Cpure
LNo   Dcomplete axioms for (classical) equivalence  Exit page  