Here is a derivation of the RI 4-base B', C,
I, and W from the axiom in
question: |
||

1.
CCCCCpqCrpCCpqCrqCCssCtCuvCCwtCuCwvD1.1 =
2. CCpqCCqqCpq
D1.2 =
3. CCpCCqrCsqCCqrCpCsrD1.3 =
4. CCpCCqqCrqCrCpqD1.4 =
5. CCpCCCqrCqrCCssCqrCqCprD4.2 =
6. CpCCpqqD5.2 =
7. CpCCCqqCprrD2.6 =
8. CCCCpqqCCpqqCpCCpqqD6.6 =
9. CCCpCCpqqrrD7.7 = 10.
CCCppCCqCCCrrCqssttD6.8 = 11.
CCCCCCpqqCCpqqCpCCpqqrrD7.9 = 12.
CCCppCCCCqCCqrrssttD9.10 = 13.
CCCppCCqqrrD10.7 = 14.
Cpp
[I]D1.13 = 15.
CCpCqrCqCpr
[C ]D15.12 = 16.
CpCCCqqCCCCrCCrssttCpuuD1.11 = 17.
[CCpqCCqrCprB']D1.16 = 18.
CCpCqrCCCqrqCprD17.17 = 19.
CCCCpqCrqsCCrpsD9.18 = 20.
CCCCpqqCpqCpqD19.20 = 21.
[CCpCpqCpqW]I remark that the
subformula
[Line CCCpsCCqtCruCCqtCCpsCru) and the
proof will still go through. So line 7 is, for
example, provable also in EI,
which has C = ^{010}CCpCCqtrCCqtCpr in place of RI's
C. Unfortunately, though, its addition to B', C, and
I does not axiomatize EI.]The formula in question, CCCpqCrpCCpqCrq, is of interest because it, in
turn, gives W
in the presence of B', C, and I: W]Consequently { B', C, I, CCCpqCrpCCpqCrq} is a new
4-base for RI, one which has the interesting feature of being
3-solvable in the sense of Rezus [On
a theorem of Tarski, Libertas Mathematica, vol. 2 (1982), pp.
63-97]. Briefly, a formula α
is
m-solvable
(m any positive integer)
just in case the result of using
α
as major premise and detaching Cpp as minor, then using that
result as major and detaching Cpp as minor again, etc., produces
Cpp itself after m iterations; and a base for a logic is m-solvable just in case each member of the base is
itself k-solvable for some positive integer k less than or
equal to m. Rezus originally conjectured that no theorem of RI not provable in BCI is m-solvable for
any m.
He abandoned that conjecture in the face of a
counter-example provided by David Meredith (our
CCCpqCrpCCpqCrq
is another), and subsequently speculated that a solvable basis for RI
might exist. That latter speculation thus proves to be correct.
Incidentally, if we replace C with Pon = CpCCpqq /
p→((p→q)→q) in our new 4-base, we get a
2-solvable base for RI. |
||

© Dolph Ulrich, 2007 |