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; 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.
In fuzzy logic, rather than regarding statements as being either true or false, we associate each statement with a numerical "confidence" in that statement. By convention the confidences range over the unit interval formula_1, where the maximal confidence formula_2 corresponds to the classical concept of true and the minimal confidence formula_3 corresponds to the classical concept of false.
T-norms are binary functions on the real unit interval [0, 1] which in fuzzy logic are often used to represent a conjunction connective; if formula_4 are the confidences we ascribe to the statements formula_5 and formula_6 respectively, then one uses a t-norm formula_7 to calculate the confidence formula_8 ascribed to the compound statement ‘formula_5 and formula_6’. A t-norm formula_7 has to satisfy the properties of
Notably absent from this list is the property of "idempotence" formula_18; the closest one gets is that formula_19. It may seem strange to be less confident in ‘formula_5 and formula_5’ than in just formula_5, but we generally do want to allow for letting the confidence formula_8 in a combined ‘formula_5 and formula_6’ be less than both the confidence formula_26 in formula_5 and the confidence formula_28 in formula_6, and then the ordering formula_30 by monotonicity requires formula_31. Another way of putting it is that the t-norm can only take into account the confidences as numbers, not the reasons that may be behind ascribing those confidences; thus it cannot treat ‘formula_5 and formula_5’ differently from ‘formula_5 and formula_6, where we are equally confident in both’.
Because the symbol formula_36 via its use in lattice theory is very closely associated with the idempotence property, it can be useful to switch to a different symbol for conjunction that is not necessarily idempotent. In the fuzzy logic tradition one sometimes uses formula_37 for this "strong" conjunction, but this article follows the substructural logic tradition of using formula_38 for the strong conjunction; thus formula_8 is the confidence we ascribe to the statement formula_40 (still read ‘formula_5 and formula_6’, perhaps with ‘strong’ or ‘multiplicative’ as qualification of the ‘and’).
Having formalised conjunction formula_38, one wishes to continue with the other connectives. One approach to doing that is to introduce negation as an order-reversing map formula_44, then defining remaining connectives using De Morgan's laws, material implication, and the like. A problem with doing so is that the resulting logics may have undesirable properties: they may be too close to classical logic, or if not conversely not support expected inference rules. An alternative that makes the consequences of different choices more predictable is to instead continue with implication formula_45 as the second connective: this is overall the most common connective in axiomatisations of logic, and it has closer ties to the deductive aspects of logic than most other connectives. A confidence counterpart formula_46 of the implication connective may in fact be defined directly as the residuum of the t-norm.
The logical link between conjunction and implication is provided by something as fundamental as the inference rule modus ponens formula_47: from formula_5 and formula_49 follows formula_6. In the fuzzy logic case that is more rigorously written as formula_51, because this makes explicit that our confidence for the premise(s) here is that in formula_52, not those in formula_5 and formula_49 separately. So if formula_26 and formula_28 are our confidences in formula_5 and formula_6 respectively, then formula_59 is the sought confidence in formula_49, and formula_61 is the combined confidence in formula_52. We require that
since our confidence formula_28 for formula_6 should not be less than our confidence formula_61 in the statement formula_52 from which formula_6 logically follows. This bounds the sought confidence formula_59, and one approach for turning formula_46 into a binary operation like formula_7 would be to make it as large as possible while respecting this bound:
Taking formula_73 gives formula_74, so the supremum is always of a nonempty bounded set and thus well-defined. For a general t-norm there remains the possibility that formula_75 has a jump discontinuity at formula_76, in which case formula_77 could come out strictly larger than formula_28 even though formula_79 is defined as the least upper bound of formula_80s satisfying formula_81; to prevent that and have the construction work as expected, we require that the t-norm formula_7 is left-continuous. 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.
More algebraically, we say that an operation formula_46 is a residuum of a t-norm formula_7 if for all formula_26, formula_28, and formula_87 it satisfies
This equivalence of numerical comparisons mirrors the equivalence of entailments
that exists because any proof of formula_92 from the premise formula_40 can be converted into a proof of formula_94 from the premise formula_5 by doing an extra implication introduction step, and conversely any proof of formula_94 from the premise formula_5 can be converted into a proof of formula_92 from the premise formula_40 by doing an extra implication elimination step. 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 formula_100 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 formula_101 or "formula_102tautologies." The set of all formula_102tautologies is called the "logic" of the t-norm formula_101 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."
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:
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:
The following are its axiom schemata:
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. 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 formula_127 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 formula_138), all MV-algebras, all BL-algebras, etc. Since the residuation condition can equivalently be expressed by identities, MTL-algebras form a variety.
Interpretation of the logic MTL in MTL-algebras.
The connectives of MTL are interpreted in MTL-algebras as follows:
With this interpretation of connectives, any evaluation "e"v 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":
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, "p" → "p") 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 formula_151 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):
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:
Linear semantics.
Like algebras for other fuzzy logics, MTL-algebras enjoy the following "linear subdirect decomposition property":
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 formula_130. The standard MTL-algebra determined by a left-continuous t-norm formula_130 is usually denoted by formula_154 In formula_155 implication is represented by the residuum of formula_156 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):
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).