Łukasiewicz logic

Axioms

The original system of axioms for propositional infinite-valued Łukasiewicz logic used implication and negation as the primitive connectives, along with modus ponens:

${\displaystyle \begin{array}{cc}A& \to (B\to A)\\ (A\to B)& \to ((B\to C)\to (A\to C))\\ ((A\to B)\to B)& \to ((B\to A)\to A)\\ (\mathrm{\neg }B\to \mathrm{\neg }A)& \to (A\to B).\end{array}}$

Propositional infinite-valued Łukasiewicz logic can also be axiomatized by adding the following axioms to the axiomatic system of monoidal t-norm logic:

Divisibility

${\displaystyle (A\wedge B)\to (A\otimes (A\to B))}$

Double negation

${\displaystyle \mathrm{\neg }\mathrm{\neg }A\to 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 ${\displaystyle 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:

• ${\displaystyle w(\theta \circ \varphi )=F_{\circ }(w(\theta ),w(\varphi ))}$ for a binary connective ${\displaystyle \circ ,}$
• ${\displaystyle w(\mathrm{\neg }\theta )=F_{\mathrm{\neg }}(w(\theta )),}$
• ${\displaystyle w\left(\overline{0}\right)=0}$ and ${\displaystyle w\left(\overline{1}\right)=1,}$

and where the definitions of the operations hold as follows:

• Implication: ${\displaystyle F_{\to }(x,y)=min\{1,1-x+y\}}$
• Equivalence: ${\displaystyle F_{\leftrightarrow }(x,y)=1-|x-y|}$
• Negation: ${\displaystyle F_{\mathrm{\neg }}(x)=1-x}$
• Weak conjunction: ${\displaystyle F_{\wedge }(x,y)=min\{x,y\}}$
• Weak disjunction: ${\displaystyle F_{\vee }(x,y)=max\{x,y\}}$
• Strong conjunction: ${\displaystyle F_{\otimes }(x,y)=max\{0,x+y-1\}}$
• Strong disjunction: ${\displaystyle F_{\oplus }(x,y)=min\{1,x+y\}.}$
• Modal functions: ${\displaystyle F_{◊}(x)=min\{1,2x\},F_{◻}(x)=max\{0,2x-1\}}$

The truth function ${\displaystyle F_{\otimes }}$ of strong conjunction is the Łukasiewicz t-norm and the truth function ${\displaystyle F_{\oplus }}$ of strong disjunction is its dual t-conorm. Obviously, ${\displaystyle F_{\otimes }(.5,.5)=0}$ and ${\displaystyle F_{\oplus }(.5,.5)=1}$, so if ${\displaystyle T(p)=.5}$, then ${\displaystyle T(p\wedge p)=T(\mathrm{\neg }p\wedge \mathrm{\neg }p)=0}$ while the respective logically-equivalent propositions have ${\displaystyle T(p\vee p)=T(\mathrm{\neg }p\vee \mathrm{\neg }p)=1}$.

The truth function ${\displaystyle F_{\to }}$ 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 { 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:

The following conditions are equivalent:

• ${\displaystyle A}$ is provable in propositional infinite-valued Łukasiewicz logic
• ${\displaystyle A}$ is valid in all MV-algebras (general completeness)
• ${\displaystyle A}$ is valid in all linearly ordered MV-algebras (linear completeness)
• ${\displaystyle A}$ is valid in the standard MV-algebra (standard completeness).

Here valid means necessarily evaluates to 1.

Font, Rodriguez and Torrens introduced in 1984 the Wajsberg algebra as an alternative model for the infinite-valued Łukasiewicz logic.

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 ℵ₀-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 MV_n-algebras. MV_n-algebras are a subclass of LM_n-algebras, and the inclusion is strict for n ≥ 5. In 1982 Roberto Cignoli published some additional constraints that added to LM_n-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,

${\displaystyle \begin{array}{cc}◊A& {=}_{def}\mathrm{\neg }A\to A\\ ◻A& {=}_{def}\mathrm{\neg }◊\mathrm{\neg }A\end{array}}$

A third doubtful operator has been proposed, ${\displaystyle \odot A{=}_{def}A\leftrightarrow \mathrm{\neg }A}$.

From these we can prove the following theorems, which are common axioms in many modal logics:

${\displaystyle \begin{array}{cc}A& \to ◊A\\ ◻A& \to A\\ A& \to (A\to ◻A)\\ ◻(A\to B)& \to (◻A\to ◻B)\\ ◻(A\to B)& \to (◊A\to ◊B)\end{array}}$

We can also prove distribution theorems on the strong connectives:

${\displaystyle \begin{array}{cc}◻(A\otimes B)& \leftrightarrow ◻A\otimes ◻B\\ ◊(A\oplus B)& \leftrightarrow ◊A\oplus ◊B\\ ◊(A\otimes B)& \to ◊A\otimes ◊B\\ ◻A\oplus ◻B& \to ◻(A\oplus B)\end{array}}$

However, the following distribution theorems also hold:

${\displaystyle \begin{array}{cc}◻A\vee ◻B& \leftrightarrow ◻(A\vee B)\\ ◻A\wedge ◻B& \leftrightarrow ◻(A\wedge B)\\ ◊A\vee ◊B& \leftrightarrow ◊(A\vee B)\\ ◊A\wedge ◊B& \leftrightarrow ◊(A\wedge B)\end{array}}$

In other words, if ${\displaystyle ◊A\wedge ◊\mathrm{\neg }A}$, then ${\displaystyle ◊(A\wedge \mathrm{\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, ${\displaystyle ◊A\wedge ◊\mathrm{\neg }A\leftrightarrow \odot A}$.