The implicational fragment of Łukasiewicz's infinite-valued sentential calculus Lalepho was first axiomatized by  Alan Rose [Formalization du calcul propositional implicatif á alepho-valeurs de Łukasiewicz, Comptes rendus hebdomadaires des séances de l'Académie des Sciences, vol. 243 (1956), pp. 1183-1185] and, independently, by R. K. Meyer [Pure denumerable Łukasiewicz implication, Journal of Symbolic Logic, vol. 31 (1966), pp. 575-580] who used the following four axioms:
        
 CCpqCCqrCpr (pq)((qr)(pr))      [B', Syl]
           CpCqp                 / 
p(qp)                                 [K, Simp]
           CCCpqqCCqpp /  ((p
q)q)(qp)p)      [Inversion]
           CCCpqCqpCqp /  ((p
q)(qp))(qp)    [Linearity]
The methods of A. Rezus
[On a theorem of Tarski, Libertas Mathematica, vol 2 (1982), pp. 63-97] ensure the existence of single axioms for all logics whose theorems include the first two of these, albeit typically quite long axioms.  The Rezus-style  axiom for C-pure Lo has been formulated by K. Harris; it is of type <69, 17>, i.e., it is 69 symbols in length and contains occurrences of 17 distinct sentence letters:
        
 CCCfCgfCCCCCCCCCcdCCecCedCCaCbazzCCCCxyyCCyxxwwCCCCtuCutCutssCCqCrqpp
 
     
   

NEW RESULTS
I've discovered that Inversion and Linearity can, in the presence of B and K, be replaced [proof here] with the single formula
        
 CCCpqqCCCpqCqpp / ((pq)q)(((pq)(qp))p)
That
simplification eventually led me, in turn, to the following single axiom of type <37, 8>:
        
 CCCpCqpCCCCCCrssCCCrsCsrrCtuCvuwCCvtw  / ((p(qp))((((((rs)s)(((rs)(sr))r))(tu)))(vu))w)((vt)w)

 

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