C. A. Meredith's C-pure logic BCI
(which has a page of its own elsewhere
within this site) has, as axioms, the formulas B = CCpqCCrpCrq
/
(p→q)→((r→p)→(r→q)),
C = CCpCqrCqCpr /
(p→(q→r))→(q→(p→r)),
and I = Cpp /
p→p. R. Kashima and N. Kamide [Substructural
implicational logics including the relevant logic E, Studia Logica,
vol. 63 (1999), pp. 181–212] have studied C alongside the seven
variants of it in which one or more of its sentential variables is replaced with a new formula of the form Cxy:
C000. CCpCqrCqCpr
/
((p→(q→r))→(q→(p→r))
C100. CCCpsCqrCqCCpsr
/ ((p→s)→(q→r))→(q→((p→s)→r))
C001. CCpCqCruCqCpCru
/ (p→(q→(r→u)))→(q→(p→(r→u)))
C101. CCCpsCqCruCqCCpsCru
/ ((p→s)→(q→(r→u)))→(q→((p→s)→(r→u)))
C010. CCpCCqtrCCqtCpr
/ (p→((q→t)→r))→((q→t)→(p→r))
C110. CCCpsCCqtrCCqtCCpsr
/ ((p→s)→((q→t)→r))→((q→t)→((p→s)→r))
C011. CCpCCqtCruCCqtCpCru
/ (p→((q→t)→(r→u)))→((q→t)→(p→(r→u)))
C111. CCCpsCCqtCruCCqtCCpsCru /
((p→s)→((q→t)→(r→u)))→((q→t)→((p→s)→(r→u)))
There are 255 axiom sets obtainable
by adding to B and I one or more of these formulas, but it
turns out that only five nonequivalent logics result: BC011I,
it’s two proper extensions BC001I and BC010I,
their common proper extension BC001C010I,
and its proper extension, BCI itself. And just as f0r BCI, each of these four
subsystems can be axiomatized using a single-axiom.
|
|
|
A SINGLE AXIOM
FOR BC011I
I've got a single axiom for BC011I
of type <15, 4>, that is, containing 15 symbols (not counting parentheses)
and occurrences of 4 distinct sentential variables:
CCpqCCCrrCqsCps
/
(p→q)→(((r→r)→(q→s))→(p→q))
It is shortest possible,
and it is unique: no other theorem of
BC011I
containing 15 or fewer symbols is a single axiom.
SINGLE AXIOMS FOR BC001I
I have found three single axioms for BC001I,
each of type <19, 5>:
CpCCqrCCpCCssCrtCqt /
p→((q→r)→((p→((s→s)→(r→t)))→(q→t)))
CpCCpCqrCCCssCrtCqt / p→((p→(q→r))→(((s→s)→(r→t))→(q→t)))
CCCppCqrCsCCsCrtCqt / ((p→p)→(q→r))→(s→((s→(r→t))→(q→t)))
No
shorter theorems of
BC001I
are single axioms for it, so these are shortest possible. Moreover, no other
theorems of type <19,5> are single axioms. I have not yet
checked the other theorems of length 19 (only those of types <19, 3> and
<19, 4> need be considered) but conjecture that none of them are
single axioms either.
SINGLE AXIOMS FOR BC010I
Each of the following five formulas is a type <19, 5> single axiom for
BC010I:
CCpqCCCCCrrssCqtCpt
/
(p→q)→(((((r→r)→s)→s)→(q→t))→(p→t))
CCCppCqrCCrsCCCqstt / ((p→p)→(q→r))→((r→s)→(((q→s)→t)→t))
CCCCpqCCCrrCqsCpstt / (((p→q)→((r→r)→(q→s))→(p→s))→t)→t
CCpqCCCrrCqsCCCpstt / (p→q)→(((r→r)→(q→s))→((p→s)→t)→t))
CCpqCCCCCrrCqsCpstt / (p→q)→(((((r→r)→(q→s))→(p→s))→t)→t)
No shorter theorems of BC010I
are single axioms for it, nor are any
other theorems of type <19,5> (though the length-19 theorems containing
occurrences of just 3 or just 4 distinct sentential letters have not yet
been checked).
The first of these axioms should be attributed to
Meredith, who presents it as a single axiom for the system with axioms B
and Specialized Assertion = CCCppqq / (((p→p)→q)→q), which he certainly would
have known is an alternate axiomatization of
BC010I.
SINGLE AXIOMS FOR BC001C010I
My first single axiom for BC001C010I
was the type <27, 7> CCCCpqCCrCCssCqtCptCCuuvCrv, but I have
since discovered seven shorter ones, each of type <23, 6>:
CCCCpqCCrCqsCpsCCttuCru
/
(((p→q)→((r→(q→s))→(p→s)))→((t→t)→u))→(r→u)
CCCpCCpCqrCsrCCttuCCsqu
/ ((p→((p→(q→r))→(s→r)))→((t→t)→u)))→((s→q)→u)
CCCCpCqrCCsqCsrCCttuCpu
/
(((p→(q→r))→((s→q)→(s→r)))→((t→t)→u))→(p→u)
CCCCpCqrCsrCCttuCCsqCpu
/ (((p→(q→r))→(s→r))→((t→t)→u))→((s→q)→(p→u))
CCCppCqrCsCCCCsCrtCqtuu
/ ((p→p)→(q→r))→(s→((((s→(r→t))→(q→t))→u)→u))
CCpqCCCCrCqsCpsCCttuCru
/ (p→q)→((((r→(q→s))→(p→s))→((t→t)→u))→(r→u))
CpCCCCpCqrCsrCCttuCCsqu
/ p→((((p→(q→r))→(s→r))→((t→t)→u))→((s→q)→u))
No theorems
of BC001C010I
of type <19,5> are single axioms for it, nor are any of its theorems
containing fewer than 19 symbols.
Of the other BC001C010I
theorems of length 19, only those of types <19, 3> and <19, 4> remain
to be checked.
It seems very likely that
there are additional single axioms of length 23, but I have not yet looked for
them.
|