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 /  (p→q)→((q→r)→(p→r))      [B', Syl]
           CpCqp                 /  p→(q→p)                                 [K, Simp]
           CCCpqqCCqpp /  ((p→q)→q)→(q→p)→p)      [Inversion]
           CCCpqCqpCqp /  ((p→q)→(q→p))→(q→p)    [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 / ((p→q)→q)→(((p→q)→(q→p))→p)
That simplification eventually led me, in turn, to the following single axiom of type <37, 8>:
          CCCpCqpCCCCCCrssCCCrsCsrrCtuCvuwCCvtw  / ((p→(q→p))→((((((r→s)→s)→(((r→s)→(s→r))→r))→(t→u)))→(v→u))→w)→((v→t)→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 |