Standard completeness of predicate logic MTL∀ for left-continuous t-norms

Hiroakira Ono

                             ono@jaist.ac.jp

School of Information Science, JAIST

1 Fuzzy logics of left-continuous t-norms and residuated lattices

The present paper is based on my joint paper with F. Montanga [8] in which we discussed Kripke semantics, undecidability and standard completeness of predicate logic MTL∀ for left-continuous t-norm, introduced by Esteva and Godo [2]. Here, we will focus our attention on the standard completeness.

In fuzzy set theory, the unit interval [0,1] is taken for the set of truth values. It is linearly ordered, and hence forms a bounded complete lattice. A binary function T from [0, 1] × [0, 1] to [0, 1] is called a t-norm, if the following holds for x, y, z;

1. T (x, T (y, z)) = T (T (x, y), z),

2. T (x, y) = T (y, x),

3. T (x, 1) = x,

4. x ≤ y implies T (x, z) ≤ T (y, z).

Thus, ⟨[0, 1], ∗, 1; ≤⟩ forms a partially ordered commutative monoid with a product ∗, which is defined by x ∗ y = T (x, y). We say that T is continuous ( and left-continuous ), when it is continuous ( and left-continuous, respectively ) as a function over the interval [0,1]. ( Hereafter, we use ∗ instead of T. ) Typical examples of continuous t-norms are the following: min, × and max{x + y − 1, 0}.

Algebraic structures corresponding to the logic without contraction rule FL_{ew} are called residuated lattices. Here, a residuated lattice is an algebra A = ⟨A, ∩, ∪, ·, →, 0, 1⟩ satisfying the following:

(i) ⟨A, ∩, ∪, 0, 1⟩ is a bounded lattice with the greatest element 1 and the least 0,

(ii) ⟨A, ·, 1⟩ is a commutative monoid,

(iii) for x, y ∈ A, x · y ≤ z if and only if x ≤ y → z ( the law of residuation ).

For more information on residuated lattices, see e.g. [6, 9]. A residuated lattice A is complete if it is complete as a lattice. We can show that in any complete residuated lattice, the following holds:

(sup x_{i}) · y = y · (sup x_{i}) = sup(x_{i} · y).

Note that when · is a t-norm, the above condition means the left-continuity. We have the following.

Proposition 1 Suppose that an algebra A = ⟨A, ∩, ∪, ·, 0, 1⟩ satisfies the above conditions (i),(ii) and ⟨A, ∩, ∪⟩ is moreover complete. Then A is residuated ( i.e. → is defined in A and satisfies the law of residuation ) if and only if · is left-continuous.

To show that the if-part, it suffices to define → by y → z = max{x : x · y ≤ z}.

Corollary 2 Let A be any structure of the form ⟨[0, 1], min, max, ∗, 0, 1⟩ with a t-norm ∗. Then, A forms a residuated lattice with the residuum → defined as above if and only if ∗ is left-continuous.

Thus, we can say that any structure of the above form with a left-continuous t-norm determines a logic over FL_{ew}. For instance, t-norms min, × and max{x + y − 1, 0} give us Dummett-Gödel logic, product logic and Łukasiewicz logic, respectively.

2 Basic logic BL of continuous t-norms

To capture the logic of continuous t-norms, Hájek [4] introduced the basic propositional logic BL, which is obtained from FL_{ew} by adding the prelinearlity axiom (φ ⊃ ψ) ∨ (ψ ⊃ φ) and the axiom for hoops (φ ∧ ψ) ⊃ (φ ∗ (φ ⊃ ψ)). Then, the following is shown in [1], which is called the standard completeness of BL.

Proposition 3 Basic propositional logic BL is complete with respect to continuous t-norms over the unit interval [0, 1]. More precisely, a formula φ is provable in BL if and only if it is valid in any complete residuated lattice on [0, 1] with a continuous t-norm.

The continuity is essential in validating the axiom for hoops. In fact, the following holds.

Lemma 4 Let A be any complete residuated lattice on [0, 1] with a left-continuous t-norm ∗. Then, the axiom for hoops is valid in A if and only if ∗ is continuous.

Here, we will give a proof of the if-part ( see [4] ). For this purpose, it is enough to show that for any x, y in [0, 1], x > y implies that y ≤ x ∗ (x → y). Define a mapping f on [0, 1] by f(z) = x ∗ z. By our assumption, f is continuous and weakly increasing satisfying f(0) = 0 and f(1) = x. By the intermediate value theorem, f(w) = y for some w. Let V = {w : f(w) = y} and v = sup V. Then, using the left-continuity of f, we have that f(v) = y. Therefore, v = max{w : x ∗ w ≤ y} = x → y. Hence, x ∗ (x → y) = f(x → y) = y.

The basic predicate logic BL∀ is the logic obtained from the predicate logic FL_{ew} by adding the above two axioms with the axiom of constant domains: ∀x(ϕ ∨ ψ) ⊃ (ϕ ∨ ∀xψ), where x is not free in ϕ. We have the following.

Proposition 5 The standard completeness does not hold for BL∀.

For, while the set of all formulas provable in BL∀ is obviously recursively enumerable, the set of all formulas valid in every residuated lattice on [0,1] with a continuous t-norm is not recursively enumerable; even is not arithmetical ( see [7] ).

3 Logic MTL of left-continuous t-norms and the standard completeness

In [2], Esteva and Godo introduced a propositional logic MTL, called the monoidal t-norm based logic, and showed that MTL is complete with respect to linearly ordered MTL-algebras. Here, MTL is obtained from BL just by dropping the axiom for hoops. The predicate logic MTL∀ is defined similarly.

They conjectured that it is complete with respect to the left-continous t-norms over [0,1]. Jenei and Montagna [5] succeeded to show the following standard completeness for MTL.

Proposition 6 The propositional logic MTL is complete with respect to left-continuous t-norms over [0, 1].

The technique used there is applied also to some extensions of MTL, in order to get the standard completeness for them ( see [3] ). In the rest of the paper, we will give an outline of the proof of the standard completeness of MTL∀. First, by applying the method developed in [4], we can show the following ( see also [2] ).

Proposition 7 For any predicate formula φ, φ is provable in MTL∀ if and only if g(φ) = 1 in every countable linearly ordered residuated lattice and every safe evaluation g on it.

Suppose now that a formula ψ is not provable in MTL∀. Then, by the above proposition, there is a countable linearly ordered residuated lattice A and a safe evaluation g such that g(ψ) < 1. To get the standard MTL∀, it is necessary to show that A is embedded into a residuated lattice B with the underlying set [0,1] in which the left-continuity holds, and that this embedding is moreover a complete embedding, i.e. an embedding which preserves all exisiting meets and joins in A.

Lemma 8 Any countable linearly ordered residuated lattice A can be embedded by a complete embedding f into a countable dense linearly ordered commutative monoid S with a monoidal operation ∘ which is left-continuous in the order toplogy. Moreover, f can be taken so as to preserve all the residua in A.

Since S is order isomorphic to Q ∩ [0, 1], we can suppose that the underlying set of S is Q ∩ [0, 1] and that the order of S is the natural order of Q ∩ [0, 1]. Then, the identity mapping is a complete embedding of S into a linearly ordered commutative monoid R on [0, 1], with the monoid operation · by letting α · β = 0 if either α = 0 or β = 0, and letting, for α, β ∈ (0, 1],

α · β = sup{a ∘ b : a, b ∈ Q ∩ [0, 1], a < α and b < β}

As in [5], we can see that · is commutative, associative, weakly increasing, and that 1 · α = α for every α, and that · coincides with ∘ on the rationals (for the last claim we need the left continuity of ∘). Moreover, · is left-continuous: let ⟨α_{n} : n ∈ ω⟩ and ⟨β_{n} : n ∈ ω⟩ be weakly increasing sequences of reals in [0, 1] such that sup{α_{n} : n ∈ ω} = α, and sup{β_{n} : n ∈ ω} = β. Then clearly α · β is an upper bound of {α_{n} · β_{n} : n ∈ ω}. Moreover, if q ∈ Q ∩ [0, 1] and q < α · β, then by the definition of · there are r, s ∈ Q ∩ [0, 1] such that r < α, s < β, and q ≤ r ∘ s. But then for some n ∈ ω, r < α_{n} and s < β_{n} (since α = sup{α_{n} : n ∈ ω} and β = sup{β_{n} : n ∈ ω}). Thus q ≤ r ∘ s ≤ α_{n} · β_{n} for some n. It follows that for all q ∈ Q ∩ [0, 1], q < α · β iff for some n ∈ ω, q < α_{n} · β_{n} iff q < sup{α_{n} · β_{n} : n ∈ ω}. Hence sup{α_{n} · β_{n} : n ∈ ω} = α · β.

Thus, R equipped with the residuum ⇒ of · forms a complete residuated lattice, which we call B. Moreover, the mapping f given in the above lemma can be regarded as an complete embedding of A into B which preserves the residua. Now, define an evaluation h on B by letting for every atomic formula γ, h(γ) = f(g(γ)). Using the fact the f is a complete embedding, by induction on φ we obtain that for every closed formula φ, h(φ) = f(g(φ)). It follows that h(ψ) < 1. Thus, we have the standard completeness of MTL∀.

Theorem 9 The predicate logic MTL∀ is complete with respect to left-continuous t-norms on [0, 1].

References

[1] R. Cignoli, F. Esteva, L. Godo and A. Torrens, Basic fuzzy logic is the logic of continuous t-norms and their residua, Soft Computing 4, (2000) 106-112.

[2] F. Esteva and L. Godo, Monoidal t-norm based logic: towards a logic for left-continuous t-norms, Fuzzy Sets and Systems 124, (2001) 271-288.

[3] F. Esteva, L. Godo, J. Gispert and F. Montagna, On the standard completeness of some axiomatic extensions of the monoidal t-norm logic, to appear in Studia Logica.

[4] P. Hájek, Metamathematics of Fuzzy Logic, Trends in Logic 4, Kluwer Academic Publishers, 1998.

[5] S. Jenei and F. Montagna, A proof of standard completeness for Esteva’s and Godo’s logic MT L, to appear in Studia Logica.

[6] T. Kowalski and H. Ono, Residuated Lattices: An algebraic glimpse at logics without contraction, monograph, March, 2001.

[7] F. Montanga, Three complexity problems in predicate fuzzy logic, Studia Logica 68, (2001) 143-152.

[8] F. Montagna and H. Ono, Kripke semantics, undecidability and standard completeness for Esteva and Godo’s logic MTL∀, draft, 2001.

[9] H. Ono, Logics without the contraction rule and residuated lattices I, Festschrift on the occasion of R.K. Meyer’s 65^{th} birthday, to appear.