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 |
||
© 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 | | D-complete axioms for (classical) equivalence | Exit page | |