Many other axiom sets produce, with substitution and detachment,
equivalent systems with the same theorems and the same derived rules of
inference. Most obviously, B can, in the
presence of C, be replaced by its commuted variant B' =
CCpqCCqrCpr / (p→q)→((q→r)→(p→r)) [also known as Syl].
Smaller axiom sets will
do the job as well.
A simple two-base is given by B' together with the wff K1 =
CpCCCqqCprr / p→(((q→q)→(p→r))→r) of A. Rezus's On a theorem of Tarski,
Libertas Mathematica, vol 2 (1982), pp. 63-97. An even shorter base
(containing just 18 symbols in all, and apparently previously unknown) is given
by {CCCCpqqrCCrsCps, Cpp}, which
develops quite quickly.
And Meredith himself found [see
section 7 of the paper cited above] two examples of single axioms for this
system, each 19 symbols in length (counting occurrences of letters and of the
binary connective):
BCI-1.
CCpCqrCCCssCtqCtCpr / (p→(q→r))→(((s→s)→(t→q))→(t→(p→r)))
BCI-2. CCCppCqrCCsCrtCqCst /
((p→p)→(q→r))→((s→(r→t))→(q→(s→t)))
NEW RESULTS
I have completed a
proof that
these are
shortest possible single axioms, that is, no theorem of BCI
containing fewer than 19 symbols gives B, C, and I with the
rules in question. They are, however, not
unique. I've found that each of
the following twenty-six formulas is
also a single axiom for
BCI:
BCI-3.
CCpqCCCrrCCCqsstCpt /
(p→q)→(((r→r)→(((q→s)→s)→t))→(p→t))
BCI-4.
CCpqCCqCCrrCstCsCpt /
(p→q)→((q→((r→r)→(s→t)))→(s→(p→t)))
BCI-5.
CCCCCppCqrrsCCstCqt /
((((p→p)→(q→r))→r)→s)→((s→t)→(q→t))
BCI-6.
CCCCpqqrCCCssCrtCpt /
(((p→q)→q)→r)→(((s→s)→(r→t))→(p→t))
BCI-7.
CCpCqrCCCCCssprtCqt /
(p→(q→r))→(((((s→s)→p)→r)→t)→(q→t))
BCI-8.
CCpCqrCCCssCrtCqCpt /
(p→(q→r))→(((s→s)→(r→t))→(q→(p→t)))
BCI-9.
CCCppCCCqrrsCCstCqt /
((p→p)→(((q→r)→r)→s))→((s→t)→(q→t))
BCI-10.
CCCppCqrCsCCrCstCqt /
((p→p)→(q→r))→(s→((r→(s→t))→(q→t)))
BCI-11.
CCCppCqrCCCCrsstCqt /
((p→p)→(q→r))→((((r→s)→s)→t)→(q→t))
BCI-12.
CCCppCqrCCrCstCsCqt /
((p→p)→(q→r))→((r→(s→t))→(s→(q→t)))
BCI-13.
CCpCCqqCrsCCstCrCpt /
(p→((q→q)→(r→s)))→((s→t)→(r→(p→t)))
BCI-14.
CCpCCqqrCsCCrCstCpt /
(p→((q→q)→r))→(s→((r→(s→t))→(p→t)))
BCI-15.
CCpqCCCrrCqCstCsCpt /
(p→q)→(((r→r)→(q→(s→t)))→(s→(p→t)))
BCI-16.
CCpCqrCqCCCssCrtCpt /
(p→(q→r))→(q→(((s→s)→(r→t))→(p→t)))
BCI-17.
CpCCCqqCrsCCsCptCrt /
p→(((q→q)→(r→s))→((s→(p→t))→(r→t)))
BCI-18.
CpCCqCprCCCssCrtCqt /
p→((q→(p→r)]→(((s→s)→(r→t))→(q→t)))
BCI-19.
CCpqCrCCCssCqCrtCpt /
(p→q)→(r→(((s→s)→(q→(r→t)))→(p→t)))
BCI-20.
CCCppCqrCCCCsttqCsr /
((p→p)→(q→r))→((((s→t)→t]→q)→(s→r))
BCI-21.
CpCCCqqCrCpsCCtrCts /
p→(((q→q)→(r→(p→s)))→((t→r)→(t→s)))
BCI-22.
CCCppCqCrsCCtqCrCts /
((p→p)→(q→(r→s)))→((t→q)→(r→(t→s)))
BCI-23.
CCpqCCCrrCCCspqtCst /
(p→q)→(((r→r)→(((s→p)→q)→t))→(s→t))
BCI-24.
CCpCCqqCrsCCtpCrCts /
(p→(((q→q)→(r→s)))→((t→p)→(r→(t→s))
BCI-25.
CCCppCqrCCCCsqrtCst /
((p→p)→(q→r))→((((s→q)→r)→t)→(s→t))
BCI-26.
CCCppCqrCCsCtqCtCsr /
((p→p)→(q→r))→((s→(t→q))→(t→(s→r)))
BCI-27.
CCpCCqqrCCrCstCsCpt /
(p→((q→q)→r))→((r→(s→t))→(s→(p→t)))
BCI-28.
CCpCqrCCCssCtpCqCtr /
(p→(q→r))→(((s→s)→(t→p))→(q→(t→r)))
I and others next found fifty-two additional single axioms of this
length for
BCI.
BCI-29
below was discovered by John Halleck and Larry Wos. Working shortly thereafter
from a preliminary list of candidates I had circulated privately, Halleck also
showed that the formulas shown below as
BCI-73
and
BCI-74
are single axioms, and Wos showed that
BCI-75,
BCI-76,
and
BCI-77
are as well.
BCI-78,
BCI-79, and
BCI-80 were shown to be single axioms by Mark
Stickel.
BCI-29.
CCCppCqCrsCCstCrCqt / ((p→p)→(q→(r→s)))→((s→t)→(r→(q→t)))
– Halleck and Wos
BCI-30.
CCCppCqCrsCCtrCtCqs / ((p→p)→(q→(r→s)))→((t→r)→(t→(q→s)))
BCI-31.
CCCppCqCrsCrCCstCqt / ((p→p)→(q→(r→s)))→(r→((s→t)→(q→t)))
BCI-32.
CCCppCqCrsCrCCtqCts / ((p→p)→(q→(r→s)))→(r→((t→q)→(t→s)))
BCI-33.
CCCppCqrCqCCsCrtCst / ((p→p)→(q→r))→(q→((s→(r→t))→(s→t)))
BCI-34.
CCpCCqqCrsCCtrCtCps / (p→((q→q)→(r→s)))→((t→r)→(t→(p→s)))
BCI-35.
CCpCqrCCsCCttpCqCsr / (p→(q→r))→((s→((t→t)→p))→(q→(s→r)))
BCI-36.
CCpCqrCqCCCssCtpCtr / (p→(q→r))→(q→(((s→s)→(t→p))→(t→r)))
BCI-37.
CCpqCCCCCrrCsttpCsq / (p→q)→(((((r→r)→(s→t))→t)→p)→(s→q))
BCI-38.
CCpqCCCrrCsCqtCpCst / (p→q)→(((r→r)→(s→(q→t)))→(p→(s→t)))
BCI-39.
CCpqCCCrrCsCtpCtCsq / (p→q)→(((r→r)→(s→(t→p)))→(t→(s→q)))
BCI-40.
CCpqCCrCCssCqtCpCrt / (p→q)→((r→((s→s)→(q→t)))→(p→(r→t)))
BCI-41.
CCpqCrCCCssCtCrpCtq / (p→q)→(r→(((s→s)→(t→(r→p)))→(t→q)))
BCI-42.
CpCCqCCrrCpsCCstCqt / p→((q→((r→r)→(p→s)))→((s→t)→(q→t)))
BCI-43.
CpCCCqqCrsCCtCprCts / p→(((q→q)→(r→s))→((t→(p→r))→(t→s)))
BCI-44.
CpCCqCCrrCpsCCtqCts / p→((q→((r→r)→(p→s)))→((t→q)→(t→s)))
BCI-45.
CpCCqCCrrsCCsCptCqt / p→((q→((r→r)→s))→((s→(p→t))→(q→t)))
BCI-46.
CCpCqrCsCCCttCsqCpr / (p→(q→r))→(s→(((t→t)→(s→q))→(p→r)))
BCI-47.
CCpqCCrCCssCtpCtCrq / (p→q)→((r→((s→s)→(t→p)))→(t→(r→q)))
BCI-48.
CpCCqCrsCCCttCprCqs / p→((q→(r→s))→(((t→t)→(p→r))→(q→s)))
BCI-49.
CpCCqrCCCssCrCptCqt / p→((q→r)→(((s→s)→(r→(p→t)))→(q→t)))
BCI-50.
CCCCCppqrsCCqCtrCts / ((((p→q)→q)→r)→s)→((q→(t→r))→(t→s))
BCI-51.
CCCCpqqrCCCssCtpCtr / (((p→q)→q)→r)→(((s→s)→(t→p))→(t→r))
BCI-52.
CCCCpqrsCCCttCqrCps / (((p→q)→r)→s)→(((t→t)→(q→r))→(p→s))
BCI-53.
CCCppCCCqrrsCCtqCts / ((p→p)→(((q→r)→r)→s))→((t→q)→(t→s))
BCI-54.
CCCppCCCqrstCCrsCqt / ((p→p)→(((q→r)→s)→t))→((r→s)→(q→t))
BCI-55.
CCpqCpCCCrrCsCqtCst / (p→q)→(p→(((r→r)→(s→(q→t)))→(s→t)))
BCI-56.
CpCCqCprCCCssCtqCtr / p→((q→(p→r))→(((s→s)→(t→q))→(t→r)))
BCI-57.
CpCCpqCCCrrCsCqtCst / p→((p→q)→(((r→r)→(s→(q→t)))→(s→t)))
BCI-58.
CpCCqrCCrCCssCptCqt / p→((q→r)→((r→((s→s)→(p→t)))→(q→t)))
BCI-59.
CCCCCppCqrrsCCtqCts / ((((p→p)→(q→r))→r)→s)→((t→q)→(t→s))
BCI-60.
CCCCpCqrrsCCCttpCqs / (((p→(q→r))→r)→s)→(((t→t)→p)→(q→s))
BCI-61.
CCCppqCCCCqCrsstCrt / ((p→p)→q)→((((q→(r→s))→s)→t)→(r→t))
BCI-62.
CCpCqrCqCCsCCttpCsr / (p→(q→r))→(q→((s→((t→t)→p))→(s→r)))
BCI-63.
CCCppCqCrsCtCCtrCqs / ((p→p)→(q→(r→s)))→(t→((t→r)→(q→s)))
BCI-64.
CCCppCCCqrCCsqrtCst / ((p→p)→(((q→r)→((s→q)→r))→t))→(s→t)
BCI-65.
CCpqCCCCqrrCCsstCpt / (p→q)→((((q→r)→r)→((s→s)→t))→(p→t))
BCI-66.
CCpqCCCCrpqCCsstCrt / (p→q)→((((r→p)→q)→((s→s)→t))→(r→t))
BCI-67.
CpCCCqqCrCpsCCstCrt / p→(((q→q)→(r→(p→s)))→((s→t)→(r→t)))
BCI-68.
CpCCCqqCrCstCCpsCrt / p→(((q→q)→(r→(s→t)))→((p→s)→(r→t)))
BCI-69.
CpCCqCCrrCstCCpsCqt / p→((q→((r→r)→(s→t)))→((p→s)→(q→t)))
BCI-70.
CpCCqCprCCsCCttqCsr / p→((q→(p→r))→((s→((t→t)→q))→(s→r)))
BCI-71.
CpCCqrCCsCCttCpqCsr / p→((q→r)→((s→((t→t)→(p→q)))→(s→r)))
BCI-72.
CpCCpqCCrCCssCqtCrt / p→((p→q)→((r→((s→s)→(q→t)))→(r→t)))
BCI-73.
CCCppCqrCsCCtCsqCtr / ((p→p)→(q→r))→(s→((t→(s→q))→(t→r)))
– Halleck
BCI-74.
CCpqCCCCCrrCqsstCpt / (p→q)→(((((r→r)→(q→s))→s)→t)→(p→t))
– Halleck
BCI-75.
CCpqCCCCrssCCttpCrq / (p→q)→((((r→s)→s)→((t→t)→p))→(r→q))
– Wos
BCI-76.
CCCCpqCCrpqCCsstCrt / (((p→q)→((r→p)→q))→((s→s)→t))→(r→t)
– Wos
BCI-77.
CCCCCppCqrCCsqrtCst / ((((p→p)→(q→r))→((s→q)→r))→t)→(s→t)
– Wos
BCI-78.
CpCCqrCCCssCtCpqCtr / p→((q→r)→(((s→s)→(t→(p→q)))→(t→r)))
– Stickel
BCI-79.
CCCCCppCqrstCCrsCqt / ((((p→p)→(q→r))→s)→t)→((r→s)→(q→t))
– Stickel
BCI-80.
CCpqCCCCCrrCspqtCst / (p→q)→(((((r→r)→(s→p))→q)→t)→(s→t))
– Stickel
OPEN
QUESTIONS
The only BCI theorems of length 19 whose status as single axioms for that
system remain open are the following. If you can resolve the status of any of
these, please e-mail me (dulrich at purdue dot edu). Those
that have now been shown not to be single axioms are "deleted" by being
highlighted in grey.
BCI-Candidate 1
.
CCpCCqqrCCCCsttpCsr / (p→((q→q)→r))→((((s→t)→t)→p)→(s→r))
BCI-Candidate 2 .
CCCCpqqCCrrsCCstCpt / (((p→q)→q)→((r→r)→s))→((s→t)→(p→t))
BCI-Candidate 3 .
CCCCpqqCCrrsCCtpCts / (((p→q)→q)→((r→r)→s))→((t→p)→(t→s))
BCI-Candidate 4 .
CCCCpqrCCsstCCqrCpt / (((p→q)→r)→((s→s)→t))→((q→r)→(p→t))
BCI-Candidate 5 .
CCCCpqqrCCrCCsstCpt / (((p→q)→q)→r)→((r→((s→s)→t))→(p→t))
BCI-Candidate 6.
CCCCpqqrCCrCCsssCps
/ (((p→q)→q))→r)→((r→((s→s)→s))→(p→s)
BCI-Candidate 7.
CCpCCqqCqrCCspCqCsr
/ (p→((q→q)→(q→r)))→((s→p)→(q→(s→r)))
BCI-Candidate 8.
CCpCCqqr CCrCqsCqCps
/ (p→((q→q)→r))→((r→(q→s))→(q→(p→s)))
BCI-Candidate 9.
CCpCqrCCCssCrsCqCps
/ (p→(q→r))→(((s→s)→(r→s))→(q→(p→s)))
BCI-Candidate 10.
CCpCqrCCCssCspCqCsr
/ (p→(q→r))→(((s→s)→(s→p))→(q→(s→r)))
BCI-Candidate 11.
CCpCqrCqCCCssCrsCps
/ (p→(q→r))→(q→(((s→s)→(r→s))→(p→s)))
BCI-Candidate 12.
CCpCqrCsCCCrrCsqCpr
/ (p→(q→r))→(s→(((r→r)→(s→q))→(p→r)))
BCI-Candidate 13.
CCpqCCCCrpqCCsssCrs
/ (p→q)→((((r→p)→q)→((s→s)→s))→(r→s))
BCI-Candidate 14.
CCpqCCCCrssCCsspCrq
/ (p→q)→((((r→s)→s)→((s→s)→p))→(r→q))
UP-DATE:
John Halleck has found a syntactic proof that BCI-candidate
14 is not a single axiom for
BCI.
BCI-Candidate
15.
CCpqCCCrrCCCspqrCsr
/ (p→q)→(((r→r)→(((s→p)→q)→r))→(s→r))
BCI-Candidate
16.
CpCCCqqCqrCCrCpsCqs
/ p→(((q→q)→(q→r))→((r→(p→s))→(q→s)))
BCI-Candidate 17.
CpCCCqqCrqCCsCprCsq
/ p→(((q→q)→(r→q))→((s→(p→r))→(s→q)))
BCI-Candidate 18.
CpCCqCCppCprCCsqCsr
/ p→((q→((p→p)→(p→r)))→((s→q)→(s→r)))
BCI-Candidate 19.
CpCCqCprCCCssCsqCsr
/ p→((q→(p→r))→(((s→s)→(s→q))→(s→r)))
BCI-Candidate 20.
CpCCqrCCrCCppCpsCqs
/ p→((q→r)→((r→((p→p)→(p→s)))→(q→s)))
|