Monoidal t-norm logic

Monoidal t-norm based logic (or shortly MTL), the logic of left-continuous t-norms, is one of t-norm fuzzy logics. 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 (known as Höhle's monoidal logic, Ono's FLew, or intuitionistic logic without contraction) by the axiom of prelinearity.

Motivation

T-norms are binary functions on the real unit interval [0, 1] which are often used to represent a conjunction connective in fuzzy logic. Every left-continuous t-norm * has a unique residuum, that is, a function \Rightarrow such that for all x, y, and z,

x*y\le z if and only if x\le (y\Rightarrow z).

The residuum of a left-continuous t-norm can explicitly be defined as

(x\Rightarrow y)=\sup\{z\mid z*x\le y\}.

This ensures that the residuum is the largest function such that for all x and y,

x*(x\Rightarrow y)\le y.

The latter can be interpreted as a fuzzy version of the modus ponens rule of inference. The residuum of a left-continuous t-norm thus can be characterized as the weakest function that makes the fuzzy modus ponens valid, which makes it a suitable truth function for implication in fuzzy logic. Left-continuity of the t-norm is the necessary and sufficient condition for this relationship between a t-norm conjunction and its residual implication to hold.

Truth functions of further propositional connectives can be defined by means of the t-norm and its residuum, for instance the residual negation \neg x=(x\Rightarrow 0). In this way, the left-continuous t-norm, its residuum, and the truth functions of additional propositional connectives (see the section Standard semantics below) determine the truth values of complex propositional formulae in [0, 1]. Formulae that always evaluate to 1 are then called tautologies with respect to the given left-continuous t-norm *, or *\mbox{-}tautologies. The set of all *\mbox{-}tautologies is called the logic of the t-norm *, since these formulae represent the laws of fuzzy logic (determined by the t-norm) which hold (to degree 1) regardless of the truth degrees of atomic formulae. Some formulae are tautologies with respect to all left-continuous t-norms: they represent general laws of propositional fuzzy logic which are independent of the choice of a particular left-continuous t-norm. These formulae form the logic MTL, which can thus be characterized as the logic of left-continuous t-norms.[2]

Syntax

Language

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

The following are the most common defined logical connectives:

\neg A \equiv A \rightarrow \bot
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).
A \vee B \equiv ((A \rightarrow B) \rightarrow B) \wedge ((B \rightarrow A) \rightarrow A)
\top \equiv \bot \rightarrow \bot

Well-formed formulae of MTL are defined as usual in propositional logics. In order to save parentheses, it is common to use the following order of precedence:

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.[3] 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 axioms (MTL2) and (MTL3) of the original axiomatic system were shown to be redundant (Chvalovský, 2012) and (Cintula, 2005). All the other axioms were shown to be independent (Chvalovský, 2012).

Semantics

Like in other propositional t-norm fuzzy logics, algebraic semantics is predominantly used for MTL, with three main classes of algebras with respect to which the logic is complete:

General semantics

MTL-algebras

Algebras for which the logic MTL is sound are called MTL-algebras. They can be characterized as prelinear commutative bounded integral residuated lattices. In more detail, an algebraic structure (L,\wedge,\vee,\ast,\Rightarrow,0,1) is an MTL-algebra if

Important examples of MTL algebras are standard MTL-algebras on the real unit interval [0, 1]. Further examples include all Boolean algebras, all linear Heyting algebras (both with \ast=\wedge), all MV-algebras, all BL-algebras, etc. Since the residuation condition can equivalently be expressed by identities,[4] MTL-algebras form a variety.

Interpretation of the logic MTL in MTL-algebras

The connectives of MTL are interpreted in MTL-algebras as follows:

x\Leftrightarrow y \equiv (x\Rightarrow y)\wedge(y\Rightarrow x)
Due to the prelinearity condition, this definition is equivalent to one that uses \ast instead of \wedge, thus
x\Leftrightarrow y \equiv (x\Rightarrow y)\ast(y\Rightarrow x)

With this interpretation of connectives, any evaluation ev of propositional variables in L uniquely extends to an evaluation e of all well-formed formulae of MTL, by the following inductive definition (which generalizes Tarski's truth conditions), for any formulae A, B, and any propositional variable p:

\begin{array}{rcl}
   e(p)                  &=& e_{\mathrm v}(p)
\\ e(\bot)               &=& 0
\\ e(\top)               &=& 1
\\ e(A\otimes B)         &=& e(A) \ast e(B)
\\ e(A\rightarrow B)     &=& e(A) \Rightarrow e(B)
\\ e(A\wedge B)          &=& e(A) \wedge e(B)
\\ e(A\vee B)            &=& e(A) \vee e(B)
\\ e(A\leftrightarrow B) &=& e(A) \Leftrightarrow e(B)
\\ e(\neg A)             &=& e(A) \Rightarrow 0
\end{array}

Informally, the truth value 1 represents full truth and the truth value 0 represents full falsity; intermediate truth values represent intermediate degrees of truth. Thus a formula is considered fully true under an evaluation e if e(A) = 1. A formula A is said to be valid in an MTL-algebra L if it is fully true under all evaluations in L, that is, if e(A) = 1 for all evaluations e in L. Some formulae (for instance, pp) are valid in any MTL-algebra; these are called tautologies of MTL.

The notion of global entailment (or: global consequence) is defined for MTL as follows: a set of formulae Γ entails a formula A (or: A is a global consequence of Γ), in symbols \Gamma\models A, if for any evaluation e in any MTL-algebra, whenever e(B) = 1 for all formulae B in Γ, then also e(A) = 1. Informally, the global consequence relation represents the transmission of full truth in any MTL-algebra of truth values.

General soundness and completeness theorems

The logic MTL is sound and complete with respect to the class of all MTL-algebras (Esteva & Godo, 2001):

A formula is provable in MTL if and only if it is valid in all MTL-algebras.

The notion of MTL-algebra is in fact so defined that MTL-algebras form the class of all algebras for which the logic MTL is sound. Furthermore, the strong completeness theorem holds:[5]

A formula A is a global consequence in MTL of a set of formulae Γ if and only if A is derivable from Γ in MTL.

Linear semantics

Like algebras for other fuzzy logics,[6] MTL-algebras enjoy the following linear subdirect decomposition property:

Every MTL-algebra is a subdirect product of linearly ordered MTL-algebras.

(A subdirect product is a subalgebra of the direct product such that all projection maps are surjective. An MTL-algebra is linearly ordered if its lattice order is linear.)

In consequence of the linear subdirect decomposition property of all MTL-algebras, the completeness theorem with respect to linear MTL-algebras (Esteva & Godo, 2001) holds:

Standard semantics

Standard are called those MTL-algebras whose lattice reduct is the real unit interval [0, 1]. They are uniquely determined by the real-valued function that interprets strong conjunction, which can be any left-continuous t-norm \ast. The standard MTL-algebra determined by a left-continuous t-norm \ast is usually denoted by [0,1]_{\ast}. In [0,1]_{\ast}, implication is represented by the residuum of \ast, weak conjunction and disjunction respectively by the minimum and maximum, and the truth constants zero and one respectively by the real numbers 0 and 1.

The logic MTL is complete with respect to standard MTL-algebras; this fact is expressed by the standard completeness theorem (Jenei & Montagna, 2002):

A formula is provable in MTL if and only if it is valid in all standard MTL-algebras.

Since MTL is complete with respect to standard MTL-algebras, which are determined by left-continuous t-norms, MTL is often referred to as the logic of left-continuous t-norms (similarly as BL is the logic of continuous t-norms).

Bibliography

References

  1. Ono (2003).
  2. Conjectured by Esteva and Godo who introduced the logic (2001), proved by Jenei and Montagna (2002).
  3. Hájek (1998), Definition 2.2.4.
  4. The proof of Lemma 2.3.10 in Hájek (1998) for BL-algebras can easily be adapted to work for MTL-algebras, too.
  5. A general proof of the strong completeness with respect to all L-algebras for any weakly implicative logic L (which includes MTL) can be found in Cintula (2006).
  6. Cintula (2006).
This article is issued from Wikipedia - version of the Tuesday, May 06, 2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.