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  
   HI-Candidate 14. CCCpqrCCrCrCrsCqs             
   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 
   HI-Candidate 30. CCpqCCCrpCqCpsCps           
   HI-Candidate 31. CCpqCCCrpCqCqsCps 
   HI-Candidate 32. CCpqCCqCCrpCqsCps           
   HI-Candidate 33. CCpqCCqCCrpsCrCps 
   HI-Candidate 34. CCpqCrCCCrpCqsCps           
   HI-Candidate 35. CpCCCpqrCCrCrsCqs


© 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 |