Monoidal t-norm logic

From Wikipedia, the free encyclopedia

Monoidal t-norm based logic (or shortly MTL), the logic of left-continuous t-norms, is a formal system of propositional fuzzy logic. It belongs to the broader class of substructural logics, or logics of residuated lattices;^[1] it extends the logic of commutative bounded integral residuated lattices (Höhle's monoidal logic, also called Ono's FL_ew) by the axiom of prelinearity.

1 Language
2 Axioms
3 Bibliography
4 References

[edit] Language

The language of the propositional logic MTL consists of countably many propositional variables and the following primitive logical connectives:

Implication $\rightarrow$ (binary)
Strong conjunction $\otimes$ (binary). The sign & is a more traditional notation for strong conjunction in the literature on fuzzy logic, while the notation $\otimes$ follows the tradition of substructural logics.
Weak conjunction $\wedge$ (binary). Unlike BL and stronger fuzzy logics, weak conjunction is not definable in MTL and has to be included among primitive connectives.
Bottom $\bot$ (nullary — a propositional constant); $0$ or $\overline{0}$ are common alternative signs and zero a common alternative name for the propositional constant (as the constants bottom and zero of substructural logics coincide in MTL).

The following are the most common defined logical connectives:

Negation $\neg$ (unary), defined as

$\neg A \equiv A \rightarrow \bot$

Equivalence $\leftrightarrow$ (binary), defined as

$A \leftrightarrow B \equiv (A \rightarrow B) \wedge (B \rightarrow A)$

In MTL, the definition is equivalent to $(A \rightarrow B) \otimes (B \rightarrow A).$

(Weak) disjunction $\vee$ (binary), defined as

$A \vee B \equiv ((A \rightarrow B) \rightarrow B) \wedge ((B \rightarrow A) \rightarrow A)$

Top $\top$ (nullary), also called one and denoted by $1$ or $\overline{1}$ (as the constants top and zero of substructural logics coincide in MTL), defined as

$\top \equiv \bot \rightarrow \bot$

In order to save parentheses, it is common to use the following order of precedence:

Unary connectives (bind most closely)
Binary connectives other than implication and equivalence
Implication and equivalence (bind most loosely)

[edit] Axioms

A Hilbert-style deduction system for MTL has been introduced by Esteva and Godo (2001). Its single derivation rule is modus ponens:

from

A

and $A \rightarrow B$ derive

B .

The following are its axiom schemata:

$\begin{array}{ll} {\rm (MTL1)}\colon & (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C)) \\ {\rm (MTL2)}\colon & A \otimes B \rightarrow A\\ {\rm (MTL3)}\colon & A \otimes B \rightarrow B \otimes A\\ {\rm (MTL4a)}\colon & A \wedge B \rightarrow A\\ {\rm (MTL4b)}\colon & A \wedge B \rightarrow B \wedge A\\ {\rm (MTL4c)}\colon & A \otimes (A \rightarrow B) \rightarrow A \wedge B\\ {\rm (MTL5a)}\colon & (A \rightarrow (B \rightarrow C)) \rightarrow (A \otimes B \rightarrow C)\\ {\rm (MTL5b)}\colon & (A \otimes B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))\\ {\rm (MTL6)}\colon & ((A \rightarrow B) \rightarrow C) \rightarrow (((B \rightarrow A) \rightarrow C) \rightarrow C)\\ {\rm (MTL7)}\colon & \bot \rightarrow A \end{array}$

The traditional numbering of axioms, given in the left column, is derived from the numbering of axioms of Hájek's basic fuzzy logic BL.^[2] The axioms (MTL4a)–(MTL4c) replace the axiom of divisibility (BL4) of BL. The axioms (MTL5a) and (MTL5b) express the law of residuation and the axiom (MTL6) corresponds to the condition of prelinearity. The axiom (MTL3) of the original axiomatic system was shown to be redundant (Cintula, 2005).^[3]

[edit] Bibliography

Esteva F. & Godo L., 2001, "Monoidal t-norm based logic: Towards a logic of left-continuous t-norms". Fuzzy Sets and Systems 124: 271–288.
Cintula P., 2005, "Short note: On the redundancy of axiom (A3) in BL and MTL". Soft Computing 9: 942.

[edit] References

^ Ono, H., 2003, "Substructural logics and residuated lattices — an introduction". In F.V. Hendricks, J. Malinowski (eds.): Trends in Logic: 50 Years of Studia Logica, Trends in Logic 20: 177–212.
^ Hájek P., 1998, Metamathematics of Fuzzy Logic. Dordrecht: Kluwer.
^ Also the axiom (MTL2) (in the presence of (MTL3)) was shown to be redundant by Stephan Lehmke's The Simple Prover (the result has not been published, but can be verified by using the Simple Prover).