Monoidal t-norm logic

Last updated

In mathematical logic, monoidal t-norm based logic (or shortly MTL), the logic of left-continuous t-norms, is one of the 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.

Contents

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 , where the maximal confidence corresponds to the classical concept of true and the minimal confidence corresponds to the classical concept of false.

T-norms are binary functions on the real unit interval [0, 1] that in fuzzy logic are often used to represent a conjunction connective; if are the confidences we ascribe to the statements and respectively, then one uses a t-norm to calculate the confidence ascribed to the compound statement ‘ and ’. A t-norm has to satisfy the properties of

commutativity,
associativity,
monotonicity — if and then ,
and having 1 as identity element.

Notably absent from this list is the property of idempotence; the closest one gets is that . It may seem strange to be less confident in ‘ and ’ than in just , but we generally do want to allow for letting the confidence in a combined ‘ and ’ be less than both the confidence in and the confidence in , and then the ordering by monotonicity requires . 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 ‘ and ’ differently from ‘ and , where we are equally confident in both’.

Because the symbol 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 for this "strong" conjunction, but this article follows the substructural logic tradition of using for the strong conjunction; thus is the confidence we ascribe to the statement (still read ‘ and ’, perhaps with ‘strong’ or ‘multiplicative’ as qualification of the ‘and’).

Having formalised conjunction , one wishes to continue with the other connectives. One approach to doing that is to introduce negation as an order-reversing map , 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 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 of the traditional 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 : from and follows . In the fuzzy logic case that is more rigorously written as , because this makes explicit that our confidence for the premise(s) here is that in , not those in and separately. So if and are our confidences in and respectively, then is the sought confidence in , and is the combined confidence in . We require that

since our confidence for should not be less than our confidence in the statement from which logically follows. This bounds the sought confidence , and one approach for turning into a binary operation like would be to make it as large as possible while respecting this bound:

.

Taking gives , so the supremum is always of a nonempty bounded set and thus well-defined. For a general t-norm there remains the possibility that has a jump discontinuity at , in which case could come out strictly larger than even though is defined as the least upper bound of s satisfying ; to prevent that and have the construction work as expected, we require that the t-norm 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 is a residuum of a t-norm if for all , , and it satisfies

if and only if .

This equivalence of numerical comparisons mirrors the equivalence of entailments

if and only if

that exists because any proof of from the premise can be converted into a proof of from the premise by doing an extra implication introduction step, and conversely any proof of from the premise can be converted into a proof of from the premise 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 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 tautologies. The set of all tautologies is called the logic of the t-norm since these formulae represent the laws of fuzzy logic (determined by the t-norm) that 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 that 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:

In MTL, the definition is equivalent to

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 and derive

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. [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 is an MTL-algebra if

  • is a bounded lattice with the top element 0 and bottom element 1
  • is a commutative monoid
  • and form an adjoint pair, that is, if and only if where is the lattice order of for all x, y, and z in , (the residuation condition)
  • holds for all x and y in L (the prelinearity condition)

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 ), 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:

  • Strong conjunction by the monoidal operation
  • Implication by the operation (which is called the residuum of )
  • Weak conjunction and weak disjunction by the lattice operations and respectively (usually denoted by the same symbols as the connectives, if no confusion can arise)
  • The truth constants zero (top) and one (bottom) by the constants 0 and 1
  • The equivalence connective is interpreted by the operation defined as
Due to the prelinearity condition, this definition is equivalent to one that uses instead of thus
  • Negation is interpreted by the definable operation

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:

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 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 . The standard MTL-algebra determined by a left-continuous t-norm is usually denoted by In implication is represented by the residuum of 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

Related Research Articles

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

<span class="mw-page-title-main">Logical connective</span> Symbol connecting sentential formulas in logic

In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .

Many-valued logic is a propositional calculus in which there are more than two truth values. Traditionally, in Aristotle's logical calculus, there were only two possible values for any proposition. Classical two-valued logic may be extended to n-valued logic for n greater than 2. Those most popular in the literature are three-valued, four-valued, nine-valued, the finite-valued with more than three values, and the infinite-valued (infinitely-many-valued), such as fuzzy logic and probability logic.

Fuzzy logic is a form of many-valued logic in which the truth value of variables may be any real number between 0 and 1. It is employed to handle the concept of partial truth, where the truth value may range between completely true and completely false. By contrast, in Boolean logic, the truth values of variables may only be the integer values 0 or 1.

In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or — in philosophical logic — a cluster concept. As a normal form, it is useful in automated theorem proving.

In mathematics, the distributive property of binary operations is a generalization of the distributive law, which asserts that the equality is always true in elementary algebra. For example, in elementary arithmetic, one has Therefore, one would say that multiplication distributes over addition.

Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but not universally, called relevant logic by British and, especially, Australian logicians, and relevance logic by American logicians.

In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ab of implication such that (ca) ≤ b is equivalent to c ≤ (ab). From a logical standpoint, AB is by this definition the weakest proposition for which modus ponens, the inference rule AB, AB, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

A lattice is an abstract structure studied in the mathematical subdisciplines of order theory and abstract algebra. It consists of a partially ordered set in which every pair of elements has a unique supremum and a unique infimum. An example is given by the power set of a set, partially ordered by inclusion, for which the supremum is the union and the infimum is the intersection. Another example is given by the natural numbers, partially ordered by divisibility, for which the supremum is the least common multiple and the infimum is the greatest common divisor.

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high-complexity objects to be included in the theory's transitive models without disrupting the usual well-ordering and recursion-theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.

In mathematics, a t-norm is a kind of binary operation used in the framework of probabilistic metric spaces and in multi-valued logic, specifically in fuzzy logic. A t-norm generalizes intersection in a lattice and conjunction in logic. The name triangular norm refers to the fact that in the framework of probabilistic metric spaces t-norms are used to generalize the triangle inequality of ordinary metric spaces.

In abstract algebra, a branch of pure mathematics, an MV-algebra is an algebraic structure with a binary operation , a unary operation , and the constant , satisfying certain axioms. MV-algebras are the algebraic semantics of Łukasiewicz logic; the letters MV refer to the many-valued logic of Łukasiewicz. MV-algebras coincide with the class of bounded commutative BCK algebras.

In logic, a functionally complete set of logical connectives or Boolean operators is one that can be used to express all possible truth tables by combining members of the set into a Boolean expression. A well-known complete set of connectives is { AND, NOT }. Each of the singleton sets { NAND } and { NOR } is functionally complete. However, the set { AND, OR } is incomplete, due to its inability to express NOT.

In abstract algebra, a skew lattice is an algebraic structure that is a non-commutative generalization of a lattice. While the term skew lattice can be used to refer to any non-commutative generalization of a lattice, since 1989 it has been used primarily as follows.

In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued as well as infinitely-many-valued (0-valued) variants, both propositional and first order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.

T-norm fuzzy logics are a family of non-classical logics, informally delimited by having a semantics that takes the real unit interval [0, 1] for the system of truth values and functions called t-norms for permissible interpretations of conjunction. They are mainly used in applied fuzzy logic and fuzzy set theory as a theoretical basis for approximate reasoning.

In mathematical logic, basic fuzzy logic, the logic of the continuous t-norms, is one of the t-norm fuzzy logics. It belongs to the broader class of substructural logics, or logics of residuated lattices; it extends the logic MTL of all left-continuous t-norms.

Łukasiewicz–Moisil algebras were introduced in the 1940s by Grigore Moisil in the hope of giving algebraic semantics for the n-valued Łukasiewicz logic. However, in 1956 Alan Rose discovered that for n ≥ 5, the Łukasiewicz–Moisil algebra does not model the Łukasiewicz logic. A faithful model for the ℵ0-valued (infinitely-many-valued) Łukasiewicz–Tarski logic was provided by C. C. Chang's MV-algebra, introduced 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.

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).