Two classical axiomatizations of the
implicational fragment,
HI, of Heyting's intuitionistic sentential calculus using
substitution and detachment/modus ponens as rules are due,
respectively, to Hilbert and to Łukasiewicz:
B'.
CCpqCCqrCpr /
(p→q)→((q→r)→(p→r))
[also known as Syl]
K. CpCqp
/ p→(q→p) [also known
as Simp]
W. CCpCpqCpq
/ (p→(p→q))→(p→q) [also known as Hilbert]
S. CCpCqrCCpqCpr / (p→(q→r))→((p→q)→(p→r)) [also known as Frege]
K. CpCqp
/ p→(q→p) [Simp]
Many variations are known and continue to be discovered. Wajsberg, for
instance, showed long ago that S / Frege can be replaced in the
second set with its commutation, S* / Frege* =
CCpqCCpCqrCpr / (p→q)→((p→(q→r))→(p→r)), and I've recently discovered that
S'/Frege' = CCpqCCqCqrCpr
/ (p→q)→((q→(q→r))→(p→r)),
where the second 'p'
in Frege* has been replaced with 'q', works as well [proof
here].
The shortest known single axioms
producing the same theorems are of length 17. The first two such axioms were found by C. A. Meredith [HI-1
immediately below in C. A Meredith, A single axiom of positive logic,
Journal of computing systems, vol. 1 (1953), pp. 169-170, and HI-2
in C. A. Meredith and A. N. Prior,
Notes on the axiomatics of the
propositional calculus, Notre Dame Journal of Formal Logic, vol 4
(1963), pp. 171-187]:
HI-1.
CCCpqrCsCCqCrtCqt / ((p→q)→r)→(s→((q→(r→ t))→(q→t)))
HI-2. CpCCqrCCCsqCrtCqt / p→((q→r)→(((s→q)→(r→t))→(q→t)))
|
|
|
NEW RESULTS
Five more
single axioms of this same length are provided in D. Ulrich, New axioms for positive
implication, Bulletin of the Section of Logic (University of Lódź),
vol. 28
(1999), pp. 39-42. As noted there,
they come from Meredith's
HI-1 by
permuting its
first three
antecedents in all possible ways:
HI-3.
CCpCqrCsCCCtpqCpr / (p→(q→r))→(s→(((t→p)→q)→(p→r)))
HI-4.
CpCCqCrsCCCtqrCqs / p→((q→(r→s))→(((t→q)→r)→(q→s)))
HI-5.
CCCpqrCCqCrsCtCqs / ((p→q)→r)→((q→(r→s))→(t→(q→s)))
HI-6.
CCpCqrCCCspqCtCpr
/ (p→(q→r))→(((s→p)→q)→(t→(p→r)))
HI-7.
CpCCCqrsCCrCstCrt
/ p→(((q→r)→s)→((r→(s→t))→(r→t)))
I have
since discovered five additional single axioms:
HI-8.
CCpqCCCrCspCqtCpt / (p→q)→(((r→(s→p))→(q→t))→(p→t))
[proof]
HI-9.
CCpqCCqCCrpsCtCps / (p→q)→((q→((r→p)→s))→(t→(p→s))) [proof]
HI-10.
CCpqCrCCCspCqtCpt / (p→q)→(r→(((s→p)→(q→t))→(p→t))) [proof]
HI-11.
CpCCCqrsCCsCstCrt
/ p→(((q→r)→s)→((s→(s→t))→(r→t))))
[proof]
HI-12.
CCCpqrCsCCrCrtCqt
/ ((p→q)→r)→(s→((r→(r→t))→(q→t)))
[proof]
OPEN QUESTIONS
My conjecture is that every 17-symbol single axiom for HI must contain
occurrences of exactly five distinct sentence letters. There are only nine theorems of
HI
of that sort that I have not yet been able to eliminate as single axioms.
I would be delighted to hear (e-mail
dulrich at purdue dot edu)
from anyone who can settle the status of any of these.
HI-Candidate 1. CCCpqCrsCCCtqrCqs / ((p→q)→(r→s))→(((t→q)→r)→(q→s))
HI-Candidate 2. CCCpqCrsCCqrCtCqs / ((p→q)→(r→s))→((q→r)→(t→(q→s)))
HI-Candidate 3. CCCpqrCCCsqCrtCqt / ((p→q)→r)→(((s→q)→(r→t))→(q→t))
HI-Candidate 4. CCCpqrCCCsrCrtCqt / ((p→q)→r)→(((s→r)→(r→t))→(q→t))
HI-Candidate 5. CCCpqrCCrCrsCtCqs / ((p→q)→r)→((r→(r→s))→(t→(q→s))
HI-Candidate 6. CCpCqrCCCsCtpqCpr / (p→(q→r))→(((s→(t→p))→q)→(p→r))
HI-Candidate 7. CCCCpqrsCCsCstCrt / (((p→q)→r)→s)→((s→(s→t))→(r→t))
HI-Candidate 8. CCCpCqrCstCCrsCrt / ((p→(q→r))→(s→t))→((r→s)→(r→t))
HI-Candidate 9. CCCpqCrsCtCCqrCqs / ((p→q)→(r→s))→(t→((q→r)→(q→s)))
There are
twenty-six additional 17-symbol theorems of HI that
I
have not yet been able to
rule out as single axioms for HI; each happens to contain occurrences of exactly four distinct sentence
letters. Of course I would like to hear from anyone who can settle the
status of any of these, as well:
HI-Candidate 10.
CCCpqrCCCpqCrsCqs
HI-Candidate 11.
CCCpqrCCCprCrsCqs
HI-Candidate 12.
CCCpqrCCqCrCrsCqs
HI-Candidate
13.
CCCpqrCCrCqCrsCqs
UP-DATE:
John Halleck has shown that
this is not a single axiom for HI:
with
HI-Candidate 13 as sole axiom, only
the candidate itself can be
used
as "major"
premise for a condensed detachment, so only instances of its
consequent
can be obtained from it as theorems. Obviously neither Syl,
Simp,
nor Hilbert is of such a form, so Candidate 13 cannot be a single
axiom for
HI.
HI-Candidate
14.
CCCpqrCCrCrCrsCqs
UP-DATE:
By a similar argument,
Halleck has shown that HI-Candidate
14 is not a
single axiom for HI.
HI-Candidate
15.
CCCpqrCCqCrsCpCqs
HI-Candidate 16.
CCCpqrCCrCrsCpCqs
HI-Candidate
17.
CCCCpqrsCCsCspCrp
HI-Candidate 18.
CCCCpqrsCCsCsqCrq
HI-Candidate
19.
CCCpqCrsCCqrCpCqs
HI-Candidate 20.
CCCpqCrsCpCCqrCqs
HI-Candidate
21.
CCCpqCrsCCCpqrCqs
HI-Candidate 22.
CCCpqrCpCCqCrsCqs
HI-Candidate
23.
CCCpqrCpCCrCrsCqs
HI-Candidate 24.
CCpCqrCCCsCspqCpr
HI-Candidate
25.
CCpCqrCCCspCpqCpr
HI-Candidate 26.
CCpCqrCCCspqCsCpr
HI-Candidate
27.
CCpCqrCsCCCspqCpr
HI-Candidate 28.
CCpqCCCrCrpCqsCps
HI-Candidate
29.
CCpqCCCrpCpCqsCps
UP-DATE:
Halleck has shown, with
an argument like that used for HI-
Candidate 13
above, that Candidate 29 is not a single axiom for HI.
HI-Candidate 30.
CCpqCCCrpCqCpsCps
HI-Candidate
31.
CCpqCCCrpCqCqsCps
HI-Candidate 32.
CCpqCCqCCrpCqsCps
UP-DATE:
Again,
Halleck has used an
argument like that used for HI-
Candidate 13 above to show that
Candidate 32 is not a single axiom for HI.
HI-Candidate
33.
CCpqCCqCCrpsCrCps
HI-Candidate 34.
CCpqCrCCCrpCqsCps
HI-Candidate 35.
CpCCCpqrCCrCrsCqs
|