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:

. CCpqCCqrCpr        /     (pq)((qr)(pr))                    [also known as Syl]
          K.  CpCqp                       /     p(qp)                                                  [also known as Simp]
          W. CCpCpqCpq            /     (p(pq))(pq)                             [also known as Hilbert]

          S.  CCpCqrCCpqCpr   /    (p(qr))((pq)(pr))           [also known as Frege]
          K.  CpCqp                       /     p(qp)                                                  [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(qr))(pr)), and I've recently discovered that S'/Frege' = CCpqCCqCqrCpr / (pq)((q(qr))(pr)), 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   /   ((pq)r)(s((q(r t))(qt)))
.  CpCCqrCCCsqCrtCqt   /   p((qr)(((sq)(rt))(qt)))



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(qr))(s(((tp)q)(pr)))
          HI-4.  CpCCqCrsCCCtqrCqs   /   p((q(rs))(((tq)r)(qs)))
          HI-5.  CCCpqrCCqCrsCtCqs   /   ((pq)r)((q(rs))(t(qs)))
          HI-6.  CCpCqrCCCspqCtCpr  /   (p(qr))(((sp)q)(t(pr)))
          HI-7.  CpCCCqrsCCrCstCrt    /    p(((qr)s)((r(st))(rt)))

I have since discovered five additional single axioms:

          HI-8.   CCpqCCCrCspCqtCpt   /   (pq)(((r(sp))(qt))(pt))   [proof]
          HI-9.   CCpqCCqCCrpsCtCps   /   (pq)((q((rp)s))(t(ps)))  [proof]
          HI-10. CCpqCrCCCspCqtCpt   /   (pq)(r(((sp)(qt))(pt)))  [proof]
          HI-11. CpCCCqrsCCsCstCrt     /   p(((qr)s)((s(st))(rt))))   [proof]
          HI-12. CCCpqrCsCCrCrtCqt    /   ((pq)r)(s((r(rt))(qt)))    [proof]

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   /  ((pq)(rs))(((tq)r)(qs))
   HI-Candidate 2.  CCCpqCrsCCqrCtCqs   /  ((pq)(rs))((qr)(t(qs)))
   HI-Candidate 3.  CCCpqrCCCsqCrtCqt   /  ((pq)r)(((sq)(rt))(qt))
   HI-Candidate 4.  CCCpqrCCCsrCrtCqt   /  ((pq)r)(((sr)(rt))(qt))
   HI-Candidate 5.  CCCpqrCCrCrsCtCqs   /  ((pq)r)((r(rs))(t(qs))
   HI-Candidate 6.  CCpCqrCCCsCtpqCpr  /  (p(qr))(((s(tp))q)(pr))
   HI-Candidate 7.  CCCCpqrsCCsCstCrt    /  (((pq)r)s)((s(st))(rt))
   HI-Candidate 8.  CCCpCqrCstCCrsCrt    /  ((p(qr))(st))((rs)(rt))
   HI-Candidate 9.  CCCpqCrsCtCCqrCqs  /  ((pq)(rs))(t((qr)(qs)))

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.
   HI-Candidate 12. CCCpqrCCqCrCrsCqs            
   HI-Candidate 13.
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.
   HI-Candidate 16. CCCpqrCCrCrsCpCqs            
   HI-Candidate 17.
   HI-Candidate 18. CCCCpqrsCCsCsqCrq            
   HI-Candidate 19.
   HI-Candidate 20. CCCpqCrsCpCCqrCqs           
HI-Candidate 21.
   HI-Candidate 22. CCCpqrCpCCqCrsCqs           
   HI-Candidate 23.
   HI-Candidate 24. CCpCqrCCCsCspqCpr           
   HI-Candidate 25.
   HI-Candidate 26. CCpCqrCCCspqCsCpr           
   HI-Candidate 27.
   HI-Candidate 28. CCpqCCCrCrpCqsCps           
   HI-Candidate 29.
       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.
   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.
   HI-Candidate 34. CCpqCrCCCrpCqsCps           
   HI-Candidate 35.

© 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 |
| BCK | C-pure intuitionism | Classical equivalence | A few more systems |

| D-complete axioms for (classical) equivalence | Exit page |