The implicational fragment of Łukasiewicz's infinite-valued sentential calculus Lo was first axiomatized by  Alan Rose [Formalization du calcul propositional implicatif á o-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 |