Łukasiewicz logic

The propositional connectives of Łukasiewicz logic are \rightarrow ("implication"), and the constant \bot ("false"). Additional connectives can be defined in terms of these: \begin{align} \neg A & =_{def} A \rightarrow \bot \\ A \vee B & =_{def} (A \rightarrow B) \rightarrow B \\ A \wedge B & =_{def} \neg( \neg A \vee \neg B) \\ A \leftrightarrow B &=_{def} (A \rightarrow B) \wedge (B \rightarrow A) \\ \top & =_{def} \bot \rightarrow \bot \end{align} The \vee and \wedge connectives are called weak disjunction and conjunction, because they are non-classical, as the law of excluded middle does not hold for them. In the context of substructural logics, they are called additive connectives. They also correspond to lattice min/max connectives. In terms of substructural logics, there are also strong or multiplicative disjunction and conjunction connectives, although these are not part of Łukasiewicz's original presentation: \begin{align} A \oplus B &=_{def} \neg A \rightarrow B \\ A \otimes B &=_{def} \neg (A \rightarrow \neg B) \end{align} There are also defined modal operators, using the Tarskian Möglichkeit: \begin{align} \Diamond A &=_{def} \neg A \rightarrow A \\ \Box A &=_{def} \neg \Diamond \neg A \end{align} == Axioms ==

The original system of axioms for propositional infinite-valued Łukasiewicz logic used implication and negation as the primitive connectives, along with modus ponens: \begin{align} A &\rightarrow (B \rightarrow A) \\ (A \rightarrow B) &\rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C)) \\ ((A \rightarrow B) \rightarrow B) &\rightarrow ((B \rightarrow A) \rightarrow A) \\ (\neg B \rightarrow \neg A) &\rightarrow (A \rightarrow B). \end{align} Propositional infinite-valued Łukasiewicz logic can also be axiomatized by adding the following axioms to the axiomatic system of monoidal t-norm logic: ; Divisibility: (A \wedge B) \rightarrow (A \otimes (A \rightarrow B)) ; Double negation: \neg\neg A \rightarrow A. That is, infinite-valued Łukasiewicz logic arises by adding the axiom of double negation to basic fuzzy logic (BL), or by adding the axiom of divisibility to the logic IMTL. Finite-valued Łukasiewicz logics require additional axioms. == Proof Theory ==

A hypersequent calculus for three-valued Łukasiewicz logic was introduced by Arnon Avron in 1991. Sequent calculi for finite and infinite-valued Łukasiewicz logics as an extension of linear logic were introduced by A. Prijatelj in 1994. However, these are not cut-free systems. Hypersequent calculi for Łukasiewicz logics were introduced by A. Ciabattoni et al in 1999. However, these are not cut-free for n > 3 finite-valued logics. A labelled tableaux system was introduced by Nicola Olivetti in 2003. A hypersequent calculus for infinite-valued Łukasiewicz logic was introduced by George Metcalfe in 2004. == Real-valued semantics ==

Infinite-valued Łukasiewicz logic is a real-valued logic in which sentences from sentential calculus may be assigned a truth value of not only 0 or 1 but also any real number in between (e.g. 0.25). Valuations have a recursive definition where: • w(\theta \circ \phi) = F_\circ(w(\theta), w(\phi)) for a binary connective \circ, • w(\neg\theta) = F_\neg(w(\theta)), • w\left(\overline{0}\right) = 0 and w\left(\overline{1}\right) = 1, and where the definitions of the operations hold as follows: • Implication: F_\rightarrow(x,y) = \min\{1, 1-x+y\} • Equivalence: F_\leftrightarrow(x, y) = 1-|x-y| • Negation: F_\neg(x) = 1-x • Weak conjunction: F_\wedge(x, y) = \min\{x, y\} • Weak disjunction: F_\vee(x, y) = \max\{x, y\} • Strong conjunction: F_\otimes(x, y) = \max\{0, x+y-1\} • Strong disjunction: F_\oplus(x, y) = \min\{1, x+y\}. • Modal functions: F_\Diamond(x) = \min\{1,2x\}, F_\Box(x) = \max\{0, 2x-1\} The truth function F_\otimes of strong conjunction is the Łukasiewicz t-norm and the truth function F_\oplus of strong disjunction is its dual t-conorm. Obviously, F_\otimes(.5,.5) = 0 and F_\oplus(.5,.5)=1, so if T(p)=.5, then T(p\wedge p)=T(\neg p \wedge \neg p) = 0 while the respective logically-equivalent propositions have T(p\vee p)= T(\neg p\vee \neg p) = 1. The truth function F_\rightarrow is the residuum of the Łukasiewicz t-norm. All truth functions of the basic connectives are continuous. By definition, a formula is a tautology of infinite-valued Łukasiewicz logic if it evaluates to 1 under each valuation of propositional variables by real numbers in the interval [0, 1]. == Finite-valued and countable-valued semantics ==

Using exactly the same valuation formulas as for real-valued semantics Łukasiewicz (1922) also defined (up to isomorphism) semantics over • any finite set of cardinality n ≥ 2 by choosing the domain as {{nowrap|{ 0, 1/(n − 1), 2/(n − 1), ..., 1 }}} • any countable set by choosing the domain as { p/q | 0 ≤ p ≤ q where p is a non-negative integer and q is a positive integer }. == General algebraic semantics ==

The standard real-valued semantics determined by the Łukasiewicz t-norm is not the only possible semantics of Łukasiewicz logic. General algebraic semantics of propositional infinite-valued Łukasiewicz logic is formed by the class of all MV-algebras. The standard real-valued semantics is a special MV-algebra, called the standard MV-algebra. Like other t-norm fuzzy logics, propositional infinite-valued Łukasiewicz logic enjoys completeness with respect to the class of all algebras for which the logic is sound (that is, MV-algebras) as well as with respect to only linear ones. This is expressed by the general, linear, and standard completeness theorems: A 1940s attempt by Grigore Moisil to provide algebraic semantics for the n-valued Łukasiewicz logic by means of his Łukasiewicz–Moisil (LM) algebra (which Moisil called Łukasiewicz algebras) turned out to be an incorrect model for n ≥ 5. This issue was made public by Alan Rose in 1956. C. C. Chang's MV-algebra, which is a model for the ℵ0-valued (infinitely-many-valued) Łukasiewicz–Tarski logic, was published in 1958. For the axiomatically more complicated (finite) n-valued Łukasiewicz logics, suitable algebras were published in 1977 by Revaz Grigolia and called MVn-algebras. MVn-algebras are a subclass of LMn-algebras, and the inclusion is strict for n ≥ 5. In 1982 Roberto Cignoli published some additional constraints that added to LMn-algebras produce proper models for n-valued Łukasiewicz logic; Cignoli called his discovery proper Łukasiewicz algebras. == Complexity ==

Łukasiewicz logics are co-NP complete. == Modal Logic ==

Łukasiewicz logics can be seen as modal logics, a type of logic that addresses possibility, using the defined operators, \begin{align} \Diamond A &=_{def} \neg A \rightarrow A \\ \Box A &=_{def} \neg \Diamond \neg A \\ \end{align} A third doubtful operator has been proposed, \odot A =_{def} A \leftrightarrow \neg A . From these we can prove the following theorems, which are common axioms in many modal logics: \begin{align} A & \rightarrow \Diamond A \\ \Box A & \rightarrow A \\ A & \rightarrow (A \rightarrow \Box A) \\ \Box (A \rightarrow B) & \rightarrow (\Box A \rightarrow \Box B) \\ \Box (A \rightarrow B) & \rightarrow (\Diamond A \rightarrow \Diamond B) \\ \end{align} We can also prove distribution theorems on the strong connectives: \begin{align} \Box (A \otimes B) & \leftrightarrow \Box A \otimes \Box B \\ \Diamond (A \oplus B) & \leftrightarrow \Diamond A \oplus \Diamond B \\ \Diamond (A \otimes B) & \rightarrow \Diamond A \otimes \Diamond B \\ \Box A \oplus \Box B & \rightarrow \Box (A \oplus B) \end{align} However, the following distribution theorems also hold: \begin{align} \Box A \vee \Box B & \leftrightarrow \Box (A \vee B) \\ \Box A \wedge \Box B & \leftrightarrow \Box (A \wedge B) \\ \Diamond A \vee \Diamond B & \leftrightarrow \Diamond (A \vee B) \\ \Diamond A \wedge \Diamond B & \leftrightarrow \Diamond (A \wedge B) \end{align} In other words, if \Diamond A \wedge \Diamond \neg A, then \Diamond (A \wedge \neg A), which is counter-intuitive. However, these controversial theorems have been defended as a modal logic about future contingents by A. N. Prior. Notably, \Diamond A \wedge \Diamond \neg A \leftrightarrow \odot A. == References ==