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
RESULT
CCCCCpqCrpCCpqCrqCCssCtCuvCCwtCuCwv. |
||
© 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 | | D-complete axioms for (classical) equivalence | Exit page | |