Mianorm-based logics with n -contraction and n -mingle axioms

Abstract

This paper investigates standard completeness for substructural fuzzy logics based on mianorms with n-contraction and n-mingle axioms. For this, first, right and left n-contractive and n-mingle logic systems based on mianorms, their corresponding algebraic structures, and their algebraic completeness results are discussed. Next, completeness with respect to algebras whose lattice reduct is [0, 1], known as standard completeness, is established for these systems via Yang’s construction in the style of Jenei–Montagna. Finally, further standard completeness results are introduced for their fixpointed involutive extensions.

Keywords

Mianorms substructural logic fuzzy logic semilinear logic mianorm-based logic

1 Introduction

This is an investigation on logical and algebraic properties of fuzzy logic, in particular semilinear logic. Fuzzy logic deals with vagueness (or vague propositions) among various kinds of uncertainty. The term “fuzzy logic” has wide and narrow meanings made by Zadeh (see [35]). As Yang [34] already mentioned, according to Zadeh [36], fuzzy logic in its wide sense is fuzzily synonymous with the fuzzy set theory which is the theory of classes with unsharp boundaries and fuzzy logic in its narrow sense (briefly, FLn) is a logical system which aims at a formalization of approximating reasoning. Many fuzzy logicians have accepted this distinction in some variations (see e.g. [17]).

Recall that FLn is a logic having fuzzy propositions, i.e., propositions with truth degrees, and in this sense FLn is an extension of infinite-valued logic studied since the 1920s (see [34]). One important trend in it is to introduce such logics having more general structures. Its good example is to introduce substructural fuzzy logics deleting structural axioms (see e.g. [5 , 31–33]). Associated with this, a general algebraic framework to study fuzzy logics as a subfamily of substructural logics with SL (the bounded version of GL1) as the basic logic has been developed in [5 , 8]. In particular, these fuzzy logics have been introduced as semilinear logics, which are complete with respect to (w.r.t.) linearly ordered matrices.2. Note that SL^ℓ denotes theweakest semilinear logic extending SL.

The most important and intended semantics in semilinear logic is based on algebraic structures over the unit interval [0, 1]. This semantics, completeness w.r.t. this semantics, and semilinear logic complete w.r.t. this semantics are called standard semantics, standard completeness, and core semilinear logic, respectively. Therefore, to show that a logic is standard complete is of crucial importance to the field of substructural fuzzy logic in FLn.

The first step of this investigation is Hájek’s introduction of BL (Basic fuzzy logic). In [17], he introduced BL as the logic for all continuous t-norms3 and considered the well-known infinite-valued logics Ł (Łukasiewicz logic), G (Dummett-Gödel logic), and Π (Product logic) as particular continuous t-norm-based logics. After two years, the standard completeness of BL was proved by Cignoli et al. [4]. Since then, logic systems based on more general structures such as uninorms, micanorms, and mianorms have been introduced.4 For instance, MTL (Monoidal t-norm logic) obtained by dropping the divisibility axiom from BL was introduced by Esteva and Godo [9] as the most basic t-norm logic and its standard completeness was proved on left-continuous t-norms by Jenei and Montagna [20]. By Metcalfe and Montagna [22], UL (Uninorm logic) obtained by dropping the weakening (or integrality) axiom from MTL was introduced and its standard completeness was proved on left-continuous uninorms. By Yang [31, 32], MICAL (Micanorm logic) and MIAL (Mianorm logic), each of which is obtained by dropping the associativity axiom from UL and the commutativity axiom from MICAL, respectively, were introduced and their standard completeness results were provided on left-continuous micanorms and left-continuous mianorms, respectively. Interestingly, MIAL is the same as SL^ℓsynthetically.

The aim of this paper is to introduce standard completeness results for substructural semilinear logics based on mianorms with n-contraction and n-mingle axioms. We have two basic reasons to do this. First, the reason to introduce logics with these axioms is this: Extensions of basic core semilinear logics with the n-potency axiom (P_n) φ^n-1 ↔ φⁿ have been extensively investigated.5 Interestingly, then-potency axiom can be regarded as n-contraction axiom (C_n) φ^n-1 → φⁿ plus n-mingle axiom (M_n) φⁿ → φ^n-1.6 However, micanorm- and mianorm-based logics with each of these axioms have not yet been investigated. Furthermore, we can divide n-contraction and n-mingle axioms into right and left ones in the context of non-commutative logic.

Second, the reason to study standard completeness is this: As we mentioned above, standard completeness is an important property in the field of substructural fuzzy/semilinear logic in that this property is the criterion for a logic to be a core one. Note that some logics obtained from MTL by eliminating structural axioms are semilinear but not core semilinear. For instance, HpsUL and C_nHpsUL, obtained by deleting the commutativity axiom from UL and C_nUL, respectively, are not complete w.r.t. their corresponding standard semantics (see [26, 28]).7 On the one hand, mianorm-based logics with the right and left n-contraction and n-mingle axioms seem to enjoy standard completeness in that MIAL is standard complete. On the other hand, such logics seem not to enjoy it in that, like HpsUL, MIAL drops the commutativity axiom. Therefore, to study standard completeness of these logics is an important and interesting discussion.

The paper is organized as follows. In Section 2, we discuss some axiomatic extensions (briefly, extensions) of MIAL having right and left n-contraction and n-mingle axioms, along with their corresponding algebras. In Section 3, we define mianorms satisfying right and left n-contraction and n-mingle properties and provide some examples as their applications. In Section 4, we establish standard completeness for those logics using the Jenei–Montagna–style construction introduced in [10, 20]. Especially, standard completeness is established for these systems via Yang’s construction introduced in [31, 32] in place of Wang’s construction introduced in [24], since the former construction in the style of Jenei–Montagna gives standard completeness for the logics with the n-contraction axiom, where n = 2, whereas the latter construction does not. Note that Wang [25] provided standard completeness for C_nIUL, an involutive extension of C_nUL. In Section 5, we consider similar extensions of the above logics. Namely, we establish standard completeness for their fixpointed involutive extensions via Yang’s construction introduced in [31, 33]. We further note that this construction does not work for their non-fixpointed involutiveextensions.

For convenience, we adopt notations and terminology similar to those in [5 , 31–33], and we assume reader familiarity with them (along with the results therein).

2 Preliminaries: logics and algebraic semantics

The term “mianorm-based logics” refers to substructural semilinear logics with mianorm-based semantics, where the (strong) conjunction andimplication connectives ‘&,’ ‘→,’ and ‘⇝’ are interpreted by a left-continuous conjunctive mianorm and its residuated pair. In this framework, the weakest logic is MIAL (= SL^ℓ).8 This logic and its extensions can be based on a countable propositional language with formulas Fm, built inductively as usual from a set of propositional variables VAR, binary connectives →, ⇝ , & , ∧ , ∨, and constants $⊤, ⊥, \bar{0}, \bar{1}$ , with a defined connective:

df1. φ ↔ ψ:= (φ → ψ) ∧ (ψ → φ).

We further define $φ_{\bar{1}}$ as $φ \land \bar{1}$ . For the rest of this paper, we follow the customary notations and terminology. We use the axiom systems to provide a consequence relation.

We start with the following axiomatization of MIAL, the most basic semilinear logic introduced here.

Definition 1. ([5, 6]) MIAL consists of the following axiom schemes and rules:

(φ ∧ ψ) → φ, (φ ∧ ψ) → ψ (∧-elimination, ∧-E)

((φ → ψ) ∧ (φ → χ)) → (φ → (ψ ∧ χ)) (∧-introduction, ∧-I)

φ → (φ ∨ ψ), ψ → (φ ∨ ψ) (∨-introduction, ∨-I)

((φ → χ) ∧ (ψ → χ)) → ((φ ∨ ψ) → χ) (∨-elimination, ∨-E)

⊥ → φ (ex falsum quodlibet, EF)

$(\bar{1} \to φ) \leftrightarrow φ$ (push and pop, PP)

φ → (ψ → (ψ & φ)) (&-adjunction, &-Adj)

φ → (ψ ⇝ (φ & ψ)) (&-adjunction, &-Adj_⇝)

$(φ_{\bar{1}} & ψ_{\bar{1}}) \to (φ \land ψ)$ (&∧)

(ψ & (φ & (φ → (ψ → χ)))) → χ (residuation, Res^′)

((φ & (φ ⇝ (ψ → χ))) & ψ) → χ (residuation, ${Res}_{⇝}^{'}$ )

((φ → (φ & (φ → ψ))) & (ψ → χ)) → (φ → χ) (T^′)

((φ ⇝ ((φ ⇝ ψ) & φ))) & (ψ → χ)) → (φ ⇝ χ) ( $T_{⇝}^{'}$ )

$(φ \to ψ)_{\bar{1}} \lor ((δ & ɛ) \to (δ & (ɛ & (ψ \to φ)_{\bar{1}})))$ (PL_{_αδ,ɛ})

$(φ \to ψ)_{\bar{1}} \lor ((δ & ɛ) \to ((δ & (ψ \to φ)_{\bar{1}}) & ɛ))$ ( $PL α_{δ, ɛ}^{'}$ )

$(φ \to ψ)_{\bar{1}} \lor ((δ \to (ɛ \to ((ɛ & δ) & (ψ \to φ)_{\bar{1}})))$ (PL_{_βδ,ɛ})

$(φ \to ψ)_{\bar{1}} \lor ((δ \to (ɛ ⇝ ((ɛ & δ) & (ψ \to φ)_{\bar{1}})))$ ( $PL β_{δ, ɛ}^{'}$ )

φ → ψ, φ ⊢ ψ (modus ponens, mp)

$φ ⊢ φ_{\bar{1}}$ (adj_u)

φ ⊢ (δ & ɛ) → (δ & (ɛ & φ)) (α)

φ ⊢ (δ & ɛ) → ((δ & φ) & ɛ) (α′)

φ ⊢ δ → (ɛ → ((ɛ & δ) & φ)) (β)

φ ⊢ δ → (ɛ ⇝ ((δ & ɛ) & φ)) (β′)

Let φⁿ and ⁿφ stand for ${\overset{︷}{((. . . (φ & φ) & \dots & φ) & φ}}^{n φ^{'} s}$ and ${\overset{︷}{φ & (φ & \dots & (φ & φ) . . .))}}^{n φ^{'} s}$ , respectively. Right and left n-contractive and n-mingle semilinear logics are defined by extending MIAL with suitable axiom schemes. Especially, we introduce the following extensions.

Definition 2. Let 2 ≤ n.

$C_{n}^{r}$ MIAL is MIAL plus $(c_{n}^{r})$ φ^n-1 → φⁿ

right n-contraction.

$C_{n}^{l}$ MIAL is MIAL plus $(c_{n}^{l})$ ^n - 1φ→ ⁿφ

left n-contraction.

$M_{n}^{r}$ MIAL is MIAL plus $(m_{n}^{r})$ φⁿ → φ^n-1

right n-mingle.

$M_{n}^{l}$ MIAL is MIAL plus $(m_{n}^{l})$ ⁿφ→ ^n - 1φ

left n-mingle.

For easy reference, we let Ls be the set of the semilinear logics introduced in Definition 2.

Definition 3. Ls = { $C_{n}^{r}$ MIAL, $C_{n}^{l}$ MIAL, $M_{n}^{r}$ MIAL, $M_{n}^{l}$ MIAL}.

Remark 1.

The system dropping the prelinearity axioms (PL_{_αδ,ɛ}), ( ${PL}_{α_{δ, ε}^{'}}$ ), (PL_{_βδ,ɛ}), and ( ${PL}_{β_{δ, ɛ}^{'}}$ ) from MIAL is the substructural logic SL. Thus, $C_{n}^{r}$ MIAL, $C_{n}^{l}$ MIAL, $M_{n}^{r}$ MIAL, and $M_{n}^{l}$ MIAL eliminating those axioms may be instead denoted as ${SL}_{C_{n}^{r}}$ , ${SL}_{C_{n}^{l}}$ , ${SL}_{M_{n}^{r}}$ , and ${SL}_{M_{n}^{l}}$ , respectively, and considered as substructural logics.

For n ≥ 2, the systems $P_{n}^{r}$ MIAL and $P_{n}^{l}$ MIAL are MIAL plus $(p_{n}^{r})$ φ^n-1 ↔ φⁿ (right n-potency) and MIAL plus $(p_{n}^{l})$ ^n - 1φ↔ ⁿφ (left n-potency), respectively. ( $P_{n}^{r}$ MIAL was introduced (but with the name MIAL_{_cn}) by Yang in [32].) Note that (right n-potency) is $(c_{n}^{r})$ plus $(m_{n}^{r})$ and similarly for (left n-potency).

For convenience, ‘∧,’ ‘∨,’ ‘⊤,’ and ‘⊥’ are used ambiguously as propositional connectives and constants and as algebraic operators and special elements, but context should clarify their meaning.

Suitable algebraic structures for right and left n-contractive and n-mingle (semilinear) logics are obtained as varieties of rlu-groupoids in the sense of [13].

Definition 4.

A pointed, bounded rlu-groupoid is a structure (A, ⊤ , ⊥ , t, f, ∧, ∨, ∗, ∖ , /) such that:

(A, ⊤ , ⊥ , ∧ , ∨) is a bounded lattice with top element ⊤ and bottom element ⊥.

(A, ∗ , t) is a groupoid with unit.

y ≤ x ∖ z iff x ∗ y ≤ z iff x ≤ z/y, for all x, y, z ∈ A (residuation).

Since the class of pointed, bounded rlu-groupoids characterizes the system SL, we henceforth call these groupoids SL-algebras.

Let x_t be x ∧ t. An MIAL-algebra is an SL-algebra satisfying: for all x, y, z, w ∈ A,

t ≤ (x ∖ y) _t ∨ ((z ∗ w) ∖ (z ∗ (w ∗ (y ∖ x) _t)))

t ≤ (x ∖ y) _t ∨ ((z ∗ w) ∖ ((z ∗ (y ∖ x) _t) ∗ w))

t ≤ (x ∖ y) _t ∨ ((z ∖ (w ∖ ((w ∗ z) ∗ (y ∖ x) _t)))

t ≤ (x ∖ y) _t ∨ ((z ∖ (((w ∗ z) ∗ (y ∖ x) _t)/w)).

An $A$ -evaluation is a function $v : Fm \to A$ satisfying: v (♯ (φ₁, …, φ_m)) = $♯^{A}$ (v (φ₁, …, φ_m)), where $♯ \in {\to, ⇝, \land, \lor, &, ⊤, ⊥, \bar{1}, \bar{0}}$ and $♯^{A}$ ∈ {∖, /, ∧, ∨, ∗, ⊤, ⊥, t, f}. A formula φ is valid in $A$ if v (φ) ≥ t for each $A$ -evaluation v. An $A$ -evaluation v is an $A$ -model of T if v (φ) ≥ t for each φ ∈ T.

Definition 5. For L an extension of MIAL, a MIAL-algebra $A$ is an L-algebra if all axioms of L are valid in $A$ . Especially, for all x ∈ A and n ≥ 2,

A $C_{n}^{r}$ MIAL-algebra is a MIAL-algebra satisfying ( $c_{n}^{r} A$ ) x^n-1 ≤ xⁿ.

A $C_{n}^{l}$ MIAL-algebra is a MIAL-algebra satisfying ( $c_{n}^{l} A$ ) ^n - 1x≤ ⁿx.

An $M_{n}^{r}$ MIAL-algebra is a MIAL-algebra satisfying ( $m_{n}^{r} A$ ) xⁿ ≤ x^n-1.

An $M_{n}^{r}$ MIAL-algebra is a MIAL-algebra satisfying ( $m_{n}^{l} A$ ) ⁿx≤ ^n - 1x.

For convenience, we call all these algebras L-algebras.

Theorem 1. (Strong completeness) Let T be a theory over L ∈ Ls and φ a formula. T ⊢ _Lφ iff for every linearly ordered L-algebra $A$ and an $A$ -evaluation v, if v is an $A$ -model of T, then v (φ) ≥ t.

Proof. Theorem 3.2.1 in [8] says that finitary weakly implicative logics9 with prelinearity axioms are semilinear, i.e., complete w.r.t. linearly ordered their corresponding algebras. Then, since L is a finitary weakly implicative logic and has the prelinearity axioms (PL_{_αδ,ɛ}), ( ${PL}_{α_{δ, ε}^{'}}$ ), (PL_{_βδ,ɛ}), and ( ${PL}_{β_{δ, ε}^{'}}$ ), the claim follows from Theorem 3.2.1 in [8] as its corollary.□

This theorem ensures that L ∈ Ls is a semilinear logic.

3 Some mianorms and their examples

In this section, by ‘1,’ ‘0,’ ‘e,’ and ‘∂,’ we denote ⊤, ⊥, identity t, and any f, respectively, on the real unit interval [0, 1]. We first define standard L-algebras and L-mianorms as right and left n-contractive and n-mingle mianorms.

Definition 6. An L-algebra $A$ is standard if $A$ has the real unit interval [0, 1] as its carrier set.

In standard L-algebras, the groupoid operator ∗ is a mianorm.

Definition 7.

(Mianorm, [32]) A mianorm is a function ∘ : [0, 1] ² → [0, 1] such that, for some e ∈ [0, 1], and for all x, y, z ∈ [0, 1]:

e ∘ x = x ∘ e = x (identity), and

x ≤ y implies x ∘ z ≤ y ∘ z and z ∘ x ≤ z ∘ y (monotonicity).

(L-mianorm) For $L^{A} \in$ { $c_{n}^{r} A$ , $c_{n}^{l} A$ , $m_{n}^{r} A$ , $m_{n}^{l} A$ }, a mianorm satisfying $L^{A}$ is said to be an L-mianorm.

A commutative mianorm is a micanorm; an associative micanorm is a uninorm; and a uninorm satisfying e = 1 is a t-norm. A mianorm ∘ is called conjunctive if 0 ∘ 1 =1 ∘ 0 =0 and disjunctive if 0 ∘ 1 =1 ∘ 0 =1.

In order to emphasize right and left n-contraction and n-mingle properties, we also call L-mianorms as follows:

A mianorm satisfying $c_{n}^{r} A$ ( $c_{n}^{l} A$ resp) is said to be a right (left resp) n-contractive mianorm; it is said to be an n-contractive mianorm if $c_{n}^{r} A$ = $c_{n}^{l} A$ .

A mianorm satisfying $m_{n}^{r} A$ ( $m_{n}^{l} A$ resp) is said to be a right (left resp) n-mingle mianorm; it is said to be an n-mingle mianorm if $m_{n}^{r} A$ = $m_{n}^{l} A$ .

Now we introduce several simple examples of right and left n-contractive and n-mingle mianorms. Before introducing them, we note two significant features of uninorms. Let ∘ be a uninorm operation. First, since the identity e can lie anywhere in [0, 1], we have that: for all x ∈ [0, 1], x ≤ x ∘ x if e ≤ x and otherwise x ∘ x ≤ x. This implies that uninorms are 2-contractive, i.e., x ≤ x², w.r.t. e ≤ x and 2-mingle, i.e., x² ≤ x, w.r.t. x ≤ e.10 Second, a uninorm has subalgebras isomorphic to t-norm and t-conorm: for e ∈ (0, 1), ∗ : [0, 1] ⌈ _[0,e] × [0, 1] ⌈ _[0,e] → [0, 1] ⌈ _[0,e] is isomorphic to a t-norm and ∘ : [0, 1] ⌈ _[e,1] × [0, 1] ⌈ _[e,1] → [0, 1] ⌈ _[e,1] to at-conorm.

T-norms and t-conorms can be defined using ordinal sums (see [16]). In particular, continuous t-norms are defined as ordinal sums of either MV, product, or Gödel chains (see [4]). By generalizing it, we can introduce right and left n-contractive and n-mingle mianorms. Here we consider some examples using a generalization of Łukasiewicz and Gödel t-norms and t-conorms below.

T^Ł (x, y) = max {0, x + y - 1} (Łukasiewicz t-norm),

T^G (x, y) = min {x, y} (Gödel t-norm),

S^Ł (x, y) = min {1, x + y} (Łukasiewicz t-conorm),

S^G (x, y) = max {x, y} (Gödel t-conorm).

In (1) - (4), take e in place of 1 as identity. we first introduce n-contractive and n-mingle mianorms having subalgebras isomorphic to t-norms and t-conorms in (1) - (4).

Example 1. Let identity e exist in (0, 1] and 2 ≤ n.

An n-contractive mianorm ∘₁ is defined by: $x \circ_{1} y = {\begin{matrix} \min {1, x + y - e} & if e \leq x, y; \\ \min {x, y} & if x, y \leq e; \\ \max {x, y} & if 0 < x < e < y; \\ \min {x, y} & otherwise. \end{matrix}$

An n-mingle mianorm ∘₂ is defined by: $x \circ_{2} y = {\begin{matrix} \max {x, y} & if e \leq x, y; \\ \max {0, x + y - e} & if x, y \leq e; \\ \max {x, y} & if 0 < x < e < y; \\ \min {x, y} & otherwise. \end{matrix}$

In ∘₁, the parts of x, y ≤ e and e ≤ x, y form algebras isomorphic to Gödel t-norm and Łukasiewicz t-conorm, respectively. In ∘₂, those parts form algebras isomorphic to Łukasiewicz t-norm and Gödel t-conorm, respectively. Since t-norms and t-conorms are commutative, right and left ones are the same and thus ∘₁ is n-contractive and ∘₂ is n-mingle.

Instead, by giving non-commutative definitions to the parts of x, y ≤ e and e ≤ x, y, we may introduce right and left n-contractive and n-mingle mianorms.

Example 2. Let identity e exist in (0, 1] and 2 ≤ n.

A right (left) n-contractive mianorm ∘₃ is defined by: $x \circ_{3} y = {\begin{matrix} \min {1, x + y - e} & if e \leq x, y and x \leq y; \\ \min {1, \max {x, y, 2 y - e}} & if e \leq x, y and otherwise; \\ \min {x, y} & otherwise. \end{matrix}$

A right (left) n-mingle mianorm ∘₄ is defined by: $x \circ_{4} y = {\begin{matrix} \max {0, x + y - e} & if x, y \leq e and y \leq x; \\ \max {0, \min {x, y, 2 x - e}} & if x, y \leq e and otherwise; \\ \max {x, y} & otherwise. \end{matrix}$

Let

e = \frac{1}{2}

in ∘₃ and consider

x = \frac{5}{8}

. Then

3 x = \frac{7}{8} \neq \frac{3}{4} = x^{3}

. This shows that ∘₃ is right and left n-contractive but not n-contractive. Similarly, ∘₄ is right and left n-mingle but not n-mingle.

4 Standard completeness

In this section, we provide standard completeness results for Ls using Yang’s construction in the style of Jenei–Montagna in [31, 32].

Fact 1. (Strong standard completeness, Yang [32]) For MIAL, the following are equivalent:

T ⊢ _MIALφ.

For every standard MIAL-algebra and evaluation v, if v (ψ) ≥ e for all ψ ∈ T, then v (φ) ≥ e.

We first show that finite or countable, linearly ordered L-algebras are embeddable into a standard algebra. (For convenience, we add the ‘less than or equal to’ relation symbol “≤” to such algebras.)

Proposition 1. For every finite or countable, linearly ordered L-algebra A = (A, ≤ _A, ⊤ , ⊥ , t, f, ∧, ∨ , ∗ , ∖ , /), there is a countable ordered set X, a binary operation ∘ on X, and a map h from A into X such that the following conditions hold:

X is densely ordered and has a maximum Max, a minimum Min, and special elements e and ∂.

(X, ∘ , ⪯ , e) is a linearly ordered, monotonic groupoid with unit.

∘ is conjunctive and left-continuous w.r.t. the order topology on (X, ⪯).

h is an embedding of the structure (A, ≤ _A, ⊤ , ⊥ , t, f, ∧ , ∨ , ∗) into (X, ⪯ , Max, Min, e, ∂, min, max, ∘), and, for all m, n ∈ A, h (m ∖ n) and h (n/m) are the residuated pair of h (m) and h (n) in (X, ⪯, Max, Min, e, ∂, max, min, ∘).

∘ satisfies right and left n-contraction and n-mingle properties corresponding to ∗.

Proof. For convenience, we assume A as a subset of Q ∩ [0, 1] with finite or countable elements, where 0 and 1 are least and greatest elements, each of which corresponds to ⊤ and ⊥, respectively.Let

X = {(m, x) : m ∈ A \ {0 (= ⊥)} and x ∈ Q ∩ (0, m]} ∪ {(0, 0)}.

For (m, x) , (n, y) ∈ X, we define: (m, x) ⪯ (n, y) iff either m < _An, or m = _An and x ≤ y.

For convenience, we henceforth drop the index A in ≤_A and = _A, if we need not distinguish them. Context should clarify the intention.

We first note that, w.r.t. $C_{n}^{r}$ MIAL and $C_{n}^{l}$ MIAL, 2 ≤ n, the definition of ∘ is as follows. For (m, x) , (n, y) ∈ X:11.

$\begin{matrix} (m, x) \circ (n, y) \\ = {\begin{matrix} \max {(m, x), (n, y)} & if m * n = m \lor n, m \neq n, and \\ (m, x) ⪯ e (= (t, t)) or (n, y) ⪯ e; \\ \min {(m, x), (n, y)} & if m * n = m \land n, and \\ (m, x) ⪯ e or (n, y) ⪯ e; \\ (m * n, m * n) & otherwise. \end{matrix} \end{matrix}$

W.r.t. $M_{n}^{r}$ MIAL and $M_{n}^{l}$ MIAL, 2 ≤ n, the definition of ∘ is as follows. For (m, x) , (n, y) ∈ X:12.

$\begin{matrix} (m, x) \circ (n, y) \\ = {\begin{matrix} \max {(m, x), (n, y)} & if m * n = m \lor n, and \\ (m, x) ≻ e or (n, y) ≻ e; \\ \min {(m, x), (n, y)} & if m * n = m \land n, and \\ (m, x) ⪯ e or (n, y) ⪯ e; \\ (m * n, m * n) & otherwise. \end{matrix} \end{matrix}$

For the proof of the conditions (I) to (IV), see Proposition 2 in [32]. We prove the condition (V).

For $C_{n}^{r}$ MIAL, we have to further prove right n-contraction, i.e., (m, x) ^n-1 ⪯ (m, x) ⁿ for 2 ≤ n and (m, x) ∈ X.

Case 1. e ⪯ (m, x). We obtain (m, x) ∘ (m, x) = (m², m²), (m², m²) ∘ (m, x) = (m³, m³) and thus (m, x) ^n-1 = (m^n-1, m^n-1) and (m, x) ⁿ = (mⁿ, mⁿ). Therefore, we have (m, x) ^n-1 ⪯ (m, x) ⁿ since m^n-1 ≤ mⁿ.

Case 2. (m, x) ≺ e. If m ≤ m², then (m, x) ∘ (m, x) = (m, x) and thus (m, x) ^n-1 ⪯ (m, x) ⁿ since m = m². Otherwise, we have m² < m < t and thus (m, x) ∘ (m, x) = (m², m²). Hence, similarly we also have (m², m²) ∘ (m, x) = (m³, m³) and thus (m, x) ^n-1 = (m^n-1, m^n-1) and (m, x) ⁿ = (mⁿ, mⁿ). Therefore, we have (m, x) ^n-1 ⪯ (m, x) ⁿ since m^n-1 ≤ mⁿ.

For $C_{n}^{l}$ MIAL, we have to further prove left n-contraction, i.e., ^n - 1 (m, x)⪯ ⁿ (m, x) for 2 ≤ n and (m, x) ∈ X. The proof is analogous to that of right n-contraction.

For $M_{n}^{r}$ MIAL, we have to further prove right n-mingle, i.e., (m, x) ⁿ ⪯ (m, x) ^n-1 for 2 ≤ n and (m, x) ∈ X.

Case 1. e ≺ (m, x). If m² ≤ m, then (m, x) ∘ (m, x) = (m, x) and thus (m, x) ⁿ ⪯ (m, x) ^n-1 since m = m². Otherwise, we have t < m < m² and thus (m, x) ∘ (m, x) = (m², m²). Hence, as above, we also have (m², m²) ∘ (m, x) = (m³, m³) and thus (m, x) ^n-1 = (m^n-1, m^n-1) and (m, x) ⁿ = (mⁿ, mⁿ). Therefore, we have (m, x) ⁿ ⪯ (m, x) ^n-1 since mⁿ ≤ m^n-1.

Case 2. (m, x) ⪯ e. If m² < m, we obtain (m, x) ∘ (m, x) = (m², m²), (m², m²) ∘ (m, x) = (m³, m³) and thus, as above, (m, x) ⁿ ⪯ (m, x) ^n-1. Otherwise, since m² = m ≤ t, we have (m, x) ∘ (m, x) = (m, x) and thus (m, x) ⁿ ⪯ (m, x) ^n-1.

For $M_{n}^{l}$ MIAL, we have to further prove left n-mingle, i.e., ⁿ (m, x)⪯ ^n - 1 (m, x) for 2 ≤ n and (m, x) ∈ X. The proof is analogous to that of right n-mingle. This completes the proof.□

Proposition 2. Every countable, linearly ordered L-algebra can be embedded into a standard algebra.

Proof. In an analogy to the proof of Proposition 3 in [32], we prove this. Let X, A, etc. be as in Proposition 1. Since (X, ⪯) is a countable, dense, linearly-ordered set with maximum and minimum, it is order isomorphic to (Q ∩ [0, 1], ≤). Let g be such an isomorphism. If (I) to (V) in Proposition 1 hold, letting, for α, β ∈ [0, 1], α ∘ ′β = g (g^-1 (α) ∘ g^-1 (β)), and, for all m ∈ A, h′ (m) = g (h (m)), we obtain that Q ∩ [0, 1] , ≤ , 1, 0, e, ∂, ∘ ′, h′ satisfy the conditions (I) to (V) of Proposition 1 whenever X, ⪯ , Max, Min, e, ∂, ∘, and h do. Thus, without loss of generality, we can assume that X = Q ∩ [0, 1] and ⪯ = ≤, and so ∘ = ∘ ′.

Now, we define for α, β ∈ [0, 1], $α \hat{\circ} β = \sup_{x \in X : x \leq α} \sup_{y \in X : y \leq β} x \circ y .$ The monotonicity and identity of $\hat{\circ}$ are easy consequences of the definition. Furthermore, it follows from the definition that $\hat{\circ}$ is conjunctive, i.e., 0 $\hat{\circ}$ 1 = 1 $\hat{\circ}$ 0 = 0. For the left-continuity of $\hat{\circ}$ , see Proposition 3 in [32].

We prove right and left n-contraction and n-mingle properties. Suppose that 〈α_i : i ∈ N〉 is an increasing sequence of reals in [0, 1] such that sup {α_i : i ∈ N} = α. First note that α^n-1 = sup {q^n-1 : q ∈ Q ∩ [0, 1] , q ≤ α} and αⁿ = sup {qⁿ : q ∈ Q ∩ [0, 1] , q ≤ α}. For the right n-contraction of $\hat{\circ}$ , we have to show that α^n-1 ≤ αⁿ, 2 ≤ n. Since q^n-1 ≤ qⁿ, we have that sup {q^n-1 : q ∈ Q ∩ [0, 1] , q ≤ α} ≤sup {qⁿ : q ∈ Q ∩ [0, 1] , q ≤ α}; therefore, α^n-1 ≤ αⁿ. The proof of the left n-contraction of $\hat{\circ}$ is analogous. For the right n-mingle of $\hat{\circ}$ , we have to show that αⁿ ≤ α^n-1, 2 ≤ n. Since qⁿ ≤ q^n-1, we have that sup {qⁿ : q ∈ Q ∩ [0, 1] , q ≤ α} ≤sup {q^n-1 : q ∈ Q ∩ [0, 1] , q ≤ α}; therefore, αⁿ ≤ α^n-1. The proof of the left n-mingle of $\hat{\circ}$ is analogous.

It is an easy consequence of the definition that $\hat{\circ}$ extends ∘. By (I) to (V), h is an embedding of (A, ≤ _A, ⊤ , ⊥ , t, f, ∧ , ∨ , ∗) into ([0, 1] , ≤ , 1, 0, e, ∂, min, $\max, \hat{\circ})$ . Finally, for the fact that $\hat{\circ}$ has a residuated pair of implications, calling it $(\hat{∖}, \hat{/})$ , see Proposition 3 in [32].□

Theorem 2. (Strong standard completeness) For L ∈ Ls, the following are equivalent:

T ⊢ _Lφ.

For every standard L-algebra and evaluation v, if v (ψ) ≥ e for all ψ ∈ T, then v (φ) ≥ e.

Proof. (1) → (2): This follows from the definition. (2) → (1): Let φ be a formula such that T_notvdashLφ, A be a linearly ordered L-algebra, and v be an evaluation in A such that v (ψ) ≥ t for all ψ ∈ T and v (φ) < t. Let h′ be the embedding of A into the standard L-algebra as in Proposition 2. Then, h′ ∘ v is an evaluation into the standard L-algebra such that h′ ∘ v (ψ) ≥ e, and yet h′ ∘ v (φ) < e.□ Theorem 2 ensures that L is complete w.r.t. left-continuous conjunctive corresponding mianorms and their residua. Therefore, we can say that L is a core semilinear logic.

Let lcc mianorm be an abbreviation of left-continuous conjunctive mianorm. Table 1 summarizes the mianorm-based logics introduced in Section 2 and their corresponding algebras and standard algebras.

Table 1
MIAL and its right and left n-contractive and n-mingle extensions

System MIAL Algebra MIAL-algebra Standard algebra lcc mianorm

$C_{n}^{r}$ MIAL = MIAL + $(c_{n}^{r})$ $C_{n}^{r}$ MIAL-algebra lcc $c_{n}^{r}$ -mianorm

$C_{n}^{l}$ MIAL = MIAL + $(c_{n}^{l})$ $C_{n}^{l}$ MIAL-algebra lcc $c_{n}^{l}$ -mianorm

$M_{n}^{r}$ MIAL = MIAL + $(m_{n}^{r})$ $M_{n}^{r}$ MIAL-algebra lcc $m_{n}^{r}$ -mianorm

$M_{n}^{l}$ MIAL = MIAL + $(m_{n}^{l})$ $M_{n}^{l}$ MIAL-algebra lcc $m_{n}^{l}$ -mianorm

System MIAL	Algebra MIAL-algebra	Standard algebra lcc mianorm
$C_{n}^{r}$ MIAL = MIAL + $(c_{n}^{r})$	$C_{n}^{r}$ MIAL-algebra	lcc $c_{n}^{r}$ -mianorm
$C_{n}^{l}$ MIAL = MIAL + $(c_{n}^{l})$	$C_{n}^{l}$ MIAL-algebra	lcc $c_{n}^{l}$ -mianorm
$M_{n}^{r}$ MIAL = MIAL + $(m_{n}^{r})$	$M_{n}^{r}$ MIAL-algebra	lcc $m_{n}^{r}$ -mianorm
$M_{n}^{l}$ MIAL = MIAL + $(m_{n}^{l})$	$M_{n}^{l}$ MIAL-algebra	lcc $m_{n}^{l}$ -mianorm

Remark 2.

For L ∈ Ls, L_e is L plus (e, exchange) (φ & ψ) → (ψ & φ). By almost the same construction, we can prove standard completeness for L_e. But this construction does not work for L_a, L plus (a, associativity) (φ & ψ) & χ ↔ φ & (ψ & χ), since the operation ∘ for L_a does not satisfy associativity (see Theorem 7 (v) in [31]).

The operation ∘ in Wang’s construction in the style of Jenei–Montagna introduced in [24] satisfies associativity (see Theorem 4.3 in [24]). But this construction does not work for n-contraction, n = 2, since (m, x) notpreceq (m, x) ∘ (m, x) (see p. 212 in [24]).

5 Fixpointed involutive extensions

In this section, we introduce fixpointed involutive extensions of L ∈ Ls and their standard completeness. We first define negation connectives and then introduce such extensions.

df2. ¬φ $:= φ \to \bar{0}$ and

df3.-φ $:= φ ⇝ \bar{0}$ .

Definition 8.

([33]) IMIAL is MIAL plus (double negation elimination(1), DNE(1)) - ¬ φ → φ and (DNE(2)) ¬ - φ → φ.

FIMIAL is IMIAL plus (fixpoint, F) $\bar{1} \leftrightarrow \bar{0}$ .

Definition 9. Let 2 ≤ n.

For L ∈ Ls, IL is L plus (DNE(1)) and (DNE(2)). The set of these systems is denoted as ILs, i.e., ILs = { $C_{n}^{r}$ IMIAL, $C_{n}^{l}$ IMIAL, $M_{n}^{r}$ IMIAL, $M_{n}^{l}$ IMIAL}, and IL ∈ ILs is said to be an involutive extension of L.

For IL ∈ ILs, FIL is IL plus (F). We denote the set of these systems as FILs, i.e., FILs = { $C_{n}^{r}$ FIMIAL, $C_{n}^{l}$ FIMIAL, $M_{n}^{r}$ FIMIAL, $M_{n}^{l}$ FIMIAL}, and FIL ∈ FILs is said to be a fixpointed involutive extension of L.

Remark 3. For L ∈ Ls, L proves (double negation introduction(1), DNI(1)) φ → - ¬ φ and (DNI(2)) φ → ¬ - φ and thus IL proves (involution(1), INV(1)) φ ↔ - ¬ φ and (INV(2)) φ ↔ ¬ - φ. In general, logics proving (INV(1)) and (INV(2)) are called involutive. Therefore, we call IL an involutive extension of L. Note that FIL further has the axiom for fixpoint. Therefore, we call FIL a fixpointed involutive extension of L.

Suitable algebraic structures for the systems are defined as follows.

Definition 10. For x ∈ A, let ¬x = x ∖ f and -x = f/x.

([33]) An IMIAL-algebra is a MIAL-algebra satisfying (DNE(1) $A$ ) - ¬ x ≤ x and (DNE(2) $A$ ) ¬ - x ≤ x.

([33]) A FIMIAL-algebra is an IMIAL-algebra satisfying (F $A$ ) t = f.

IL-algebras are L-algebras satisfying (DNE(1) $A$ ) and (DNE(2) $A$ ) and FIL-algebras are IL-algebras satisfying (F $A$ ).

Note that algebraic semantics based on IMIAL- and FIMIAL-algebras in Definition 10 (i) and (ii) are for the systems IMIAL and FIMIAL, respectively, in Definition 8 (see [33]). Let us define evaluations and models as in Section 2. The below theorem shows that algebraic semantics based on IL- and FIL-algebras in Definition 10 (iii) are for their corresponding IL and FIL systems, respectively, introduced in Definition 9 (i) and (ii).

Theorem 3. (Strong completeness)

Let T be a theory over IL ∈ ILs and φ a formula. T ⊢ _ILφ iff for every linearly ordered IL-algebra $A$ and an $A$ -evaluation v, if v is an $A$ -model of T, then v (φ) ≥ t.

Let T be a theory over FIL ∈ FILs and φ a formula. T ⊢ _FILφ iff for every linearly ordered FIL-algebra $A$ and an $A$ -evaluation v, if v is an $A$ -model of T, then v (φ) ≥ t.

Proof. The proof of (i) and (ii) is analogous to that of Theorem 1.□

For all x ∈ [0, 1], let ¬x and -x be x ∖ ∂ and ∂/x, respectively. A residuated pair of implications (∖ , /) is involutive if it further satisfies (DNE(1) $A$ ) and (DNE(2) $A$ ). It is clear that the operator ∗ of any standard IMIAL-algebra is a conjunctive mianorm with identity e and involutively residuated pair of implications (∖ , /) (for short, involutive mianorm); conversely, any involutive mianorm gives rise to an IMIAL-algebra.

An involutive pair of negations (¬, -) is called cyclic if ¬x = - x for all x ∈ [0, 1]. Thus, an involutive pair of negations can be expressed as only one negation ¬ (or -) if it is cyclic. Note that, in Section 3, we introduced some examples of right and left n-contractive and n-mingle mianorms in Example 2. Here we give simple examples of fixpointed such mianorms defined by a cyclic involutive negation ¬.

Example 3. Let ¬ be a cyclic involutive negation and identity e (= ¬ e)) exist in (0, 1].

A right (left) n-contractive mianorm ∘₅ and its involutively residuated pair (∖₅, /₅) are defined by: $\begin{matrix} x \circ_{5} y \\ = {\begin{matrix} \min {x, y} & if x \leq \neg y; \\ \min {1, x + y - e} & if x > \neg y and x \leq y; \\ \min {1, \max {x, y, 2 y - e}} & otherwise. \end{matrix} \end{matrix}$ x ∖₅ y = ¬ (¬ y ∘ ₅x) and y /₅ x = ¬ (x ∘ ₅ ¬ y) .

A right (left) n-mingle mianorm ∘₆ and its involutively residuated pair (∖₆, /₆) are defined by: $\begin{matrix} x \circ_{6} y \\ = {\begin{matrix} \max {x, y} & if x > \neg y; \\ \max {0, x + y - e} & if x \leq \neg y and y \leq x; \\ \max {0, \min {x, y, 2 x - e}} & otherwise. \end{matrix} \end{matrix}$ x ∖₆ y = ¬ (¬ y ∘ ₆x) and y /₆ x = ¬ (x ∘ ₆ ¬ y) .

Let

e = \frac{1}{2}

and ¬x = 1 - x in ∘₅ and consider

x = \frac{5}{8}

. As ∘₃ in Example 2,

3 x = \frac{7}{8} \neq \frac{3}{4} = x^{3}

. Thus, ∘₅ is also right and left n-contractive. Moreover, The fact that

\frac{1}{2} /_{5} (\frac{5}{8} ∖_{5} \frac{1}{2})

\frac{1}{2} /_{5} \frac{3}{8}

\frac{5}{8}

shows that its residuated pair (∖₅, /₅) is involutive. Similarly, ∘₆ is right and left n-mingle and its residuated pair (∖₆, /₆) isinvolutive.

Now we consider standard completeness of the fixpointed involutive extensions.

Fact 2. ([33]) For every finite or countable, linearly ordered IMIAL-algebra A = (A, ≤ _A, ⊤, ⊥ , 1, 0, ∧ , ∨ , ∗ , ∖ , /), there is a countable ordered set X, a binary operation ∘ on X, and a map h from A into X such that the conditions (I) to (IV) in Proposition 1 and the following condition hold:

For all x ∈ X, x is involutive, i.e., it satisfies (DNE(1) $A$ ) and (DNE(2) $A$ ).

Proposition 3. For every finite (but at least three) or countable, linearly ordered FIL-algebra A = (A, ≤ _A, ⊤ , ⊥ , 1, 0, ∧ , ∨ , ∗ , ∖ , /), there is a countable ordered set X, a binary operation ∘ on X, and a map h from A into X such that the conditions (I) to (V) in Proposition 1, (VI) in Fact 2, and (F $A$ ).

Proof. Let m⁺ denote the successor of m if it exists, otherwise m⁺ = m, for each m ∈ A. Notice first that, since the pair of negations in A, defined as ¬m:= m ∖ ∂ and -m:= ∂/m, is involutive, we have that: m = (¬ n) ⁺ iff n = (¬ m) ⁺ and m = (- n) ⁺ iff n = (- m) ⁺; moreover, if m < m⁺, then (¬ (m⁺)) ⁺ = ¬m and (- (m⁺)) ⁺ = -m. Here, we use Y below in place of the X above. Let (Y, ⪯) be the linearly ordered set, defined by Y = {(m, m) : m ∈ A} ∪ {(m, x) : ∃ m′ ∈ A such that m = _Am^′+ > _Am′, and x ∈ Q ∩ (0, m)},

with ⪯ being the corresponding lexicographic ordering as above. In order to distinguish the two ∘’s introduced in Proposition 1, we denote the first and second circles as ∘_{Y
₁} and ∘_{Y
₂}, respectively.

Now, we define new operations ⊙_{Y
₁} on Y, based on ∘_{Y
₁}, and ⊙_{Y
₂} on Y, based on ∘_{Y
₂}, as follows (but, for convenience, henceforth dropping each index if we do not have to distinguish them):13 $(m, x) ⊙ (n, y) = {\begin{matrix} \min {\partial, (m, x) \circ (n, y)} & if m = (\neg n)^{+} and \frac{p}{q} + \frac{p^{'}}{q^{'}} \leq 1, \\ where x = m \frac{p}{q} and y = n \frac{p^{'}}{q^{'}}, or \\ m < (\neg n)^{+}; or \\ if m = (- n)^{+} and \frac{p}{q} + \frac{p^{'}}{q^{'}} \leq 1, \\ where x = m \frac{p}{q} and y = n \frac{p^{'}}{q^{'}}, or \\ m < (- n)^{+}; \\ (m, x) \circ (n, y) & otherwise . \end{matrix}$

Note that ⊙_{Y
₁} is for $C_{n}^{r}$ FIMIAL and $C_{n}^{l}$ FIMIAL, 2 ≤ n, and ⊙_{Y
₂} is for $M_{n}^{r}$ FIMIAL and $M_{n}^{l}$ FIMIAL, 2 ≤ n.

Let (m, x) ⁿ and ⁿ (m, x) stand for ${\overset{︷}{((. . . ((m, x) ⊙ (m, x)) ⊙ \dots ⊙ (m, x)) ⊙ (m, x)}}^{n φ^{'} s}$ and ${\overset{︷}{(m, x) ⊙ ((m, x) ⊙ \dots ⊙ ((m, x) ⊙ (m, x) . . .))}}^{n φ^{'} s}$ , respectively. For the proof of the conditions (I) to (IV) and (VI), see Proposition 2 in [33]. The condition (F $A$ ) holds since t = f and thus e = (t, t) = (f, f) = ∂. We prove the condition (V).

For $C_{n}^{r}$ FIMIAL, we have to further prove right n-contraction. For this, we show (m, x) ^n-1 ⪯ (m, x) ⁿ for 2 ≤ n and (m, x) ∈ X.

Case 1. m = (¬ m) ⁺ and $2 \frac{p}{q} \leq 1$ , where $x = m \frac{p}{q}$ , or m < (¬ m) ⁺.

Subcase 1.1. m ≤ m². Since t < m is not the case, we have m = m² ≤ t = f < (¬ m) ⁺ and thus (m, x) ⊙ _{Y
₁} (m, x) = min {∂, (m, x) ∘ _{Y
₁} (m, x)} = (m, x) ∘ _{Y
₁} (m, x) = (m, x); therefore, (m, x) ^n-1 ⪯ (m, x) ⁿ.

Subcase 1.2. m > m². We need to show (m, x) ^n-1 ⪯ (m, x) ⁿ for 2 < n. Since the condition implies m² < m < t, we have (m, x) ⊙ _{Y
₁} (m, x) = min {∂, (m, x) ∘ _{Y
₁} (m, x)} = (m, x) ∘ _{Y
₁} (m, x); therefore, (m, x) ^n-1 ⪯ (m, x) ⁿ since m³ = m² and thus mⁿ = m^n-1 for 2 < n.

Case 2. m = (- m) ⁺ and $2 \frac{p}{q} \leq 1$ , where $x = m \frac{p}{q}$ , or m < (- m) ⁺. The proof is analogous to that of Case 1.

Case 3. Otherwise. The proof is reducible to that of the right n-contraction for $C_{n}^{r}$ MIAL in Proposition 1.

For $C_{n}^{l}$ FIMIAL, we have to further prove left n-contraction. For this, we show ^n - 1 (m, x)⪯ ⁿ (m, x) for 2 ≤ n and (m, x) ∈ X. The proof is analogous to that of right n-contraction.

For $M_{n}^{r}$ FIMIAL, we have to further prove right n-mingle, i.e., (m, x) ⁿ ⪯ (m, x) ^n-1 for 2 ≤ n and (m, x) ∈ X.

Case 1. m = (¬ m) ⁺ and $2 \frac{p}{q} \leq 1$ , where $x = m \frac{p}{q}$ , or m < (¬ m) ⁺.

Subcase 1.1. m² ≤ m. It suffices to consider the case m ≤ t = f ≤ (¬ m) ⁺. Then, we have (m, x) ⊙ _{Y
₂} (m, x) = min {∂, (m, x) ∘ _{Y
₂} (m, x)} = (m, x) ∘ _{Y
₂} (m, x); therefore, (m, x) ⁿ ⪯ (m, x) ^n-1 since the proof is reducible to that of the right n-mingle for $M_{n}^{r}$ MIAL in Proposition 1.

Subcase 1.2. m² > m. This is not the case since the condition implies t < m ≤ (¬ m) ⁺ ≤ f, which is contrary to the condition (F $A$ ) t = f.

Case 2. m = (- m) ⁺ and $2 \frac{p}{q} \leq 1$ , where $x = m \frac{p}{q}$ , or m < (- m) ⁺. The proof is analogous to that of Case 1.

Case 3. Otherwise. The proof is reducible to that of the right n-mingle for $M_{n}^{r}$ MIAL in Proposition 1.

For $M_{n}^{l}$ FIMIAL, we have to further prove left n-mingle, i.e., ⁿ (m, x)⪯ ^n - 1 (m, x) for 2 ≤ n and (m, x) ∈ X. The proof is analogous to that of right n-mingle. This completes the proof.□

Proposition 4. Every countable, linearly ordered FIL-algebra can be embedded into a standard algebra.

Proof. The proof of this claim is analogous to that of Proposition 2.□

Theorem 4. (Strong standard completeness) For FIL ∈ FILs, the following are equivalent:

T ⊢ _FILφ.

For every standard FIL-algebra and evaluation v, if v (ψ) ≥ e for all ψ ∈ T, then v (φ) ≥ e.

Proof. (1) → (2): This follows from the definition. (2) → (1): Let φ be a formula such that T_notvdashFILφ, A be a linearly ordered FIL-algebra, and v be an evaluation in A such that v (ψ) ≥ t for all ψ ∈ T and v (φ) < t. Let h′ be the embedding of A into the standard FIL-algebra as in Proposition 2. Then, h′ ∘ v is an evaluation into the standard FIL-algebra such that h′ ∘ v (ψ) ≥ e, and yet h′ ∘ v (φ) < e.□ Theorem 4 ensures that FIL is complete w.r.t. left-continuous conjunctive fixpointed corresponding mianorms and their involutive residua. Therefore, we can say that FIL is a core semilinear logic.

The proof of standard completeness in Theorem 4 does not work for IL ∈ ILs because the definitions of ⊙_{Y
₁} and ⊙_{Y
₂} do not work for corresponding algebras. We finally verify this fact.

Theorem 5. The proof of standard completeness in Theorem 4 does not work for IL ∈ ILs.

Proof.

Case 1. $C_{n}^{r}$ IMIAL and $C_{n}^{l}$ IMIAL, for 2 ≤ n.

For $C_{2}^{r}$ IMIAL and $C_{2}^{l}$ IMIAL, consider the following case: f < m < (¬ m) ⁺, (- m) ⁺ < t. Since m = m ∗ m, we have (m, x) ⊙ (m, x) = min {∂, (m, x) ∘ (m, x)} = ∂ ≺ (m, x); therefore, (m, x) notpreceq (m, x) ⊙ (m, x). For $C_{n}^{r}$ IMIAL and $C_{n}^{l}$ IMIAL, for 2 < n, consider the following case: f², m ∗ f, f ∗ m < f < m < (¬ m) ⁺, (- m) ⁺ < t. We have (m, x) ⊙ (m, x) =∂, (m, x) ³ = ∂ ⊙ (m, x) = (f ∗ m, f ∗ m) notsucceq∂= (m, x) ², and ³ (m, x) = (m, x) ⊙ ∂ = (m ∗ f, m ∗ f) notsucceq∂ = ² (m, x); therefore, (m, x) ^n-1notpreceq (m, x) ⁿ and ^n - 1 (m, x) notpreceq ⁿ (m, x), for given 2 < n.

Case 2. $M_{n}^{r}$ IMIAL and $M_{n}^{l}$ IMIAL, for 2 < n.

Consider the following case: t < m < (¬ m) ⁺, (- m) ⁺ < f < m² ≤ m ∗ f, f ∗ m < f². We have (m, x) ⊙ (m, x) = ∂, (m, x) ³ = ∂ ⊙ (m, x) = (f ∗ m, f ∗ m) notpreceq (m, x) ², and ³ (m, x) = (m, x) ⊙ ∂ = (m ∗ f, m ∗ f) notpreceq ² (m, x); therefore, (m, x) ⁿnotpreceq (m, x) ^n-1 and ⁿ (m, x) notpreceq ^n - 1 (m, x), for given 2 < n.

□ Let fi-mianorm be an abbreviation of fixpointed involutive mianorm. Table 2 summarizes the fi-mianorm-based logics introduced in this section and their corresponding algebras and standard algebras. We finally note that the classes of (standard) algebras introduced in Table 2 are subclasses of (standard) algebras introduced in Table 1. For instance,

C_{n}^{r}

FIMIAL-algebras are

C_{n}^{r}

MIAL-algebras satisfying involution and fixpoint properties and similarly lcc

c_{n}^{r}

-fi-mianorms are lcc

c_{n}^{r}

-mianorms satisfying those properties.

Table 2
FIMIAL and its right and left n-contractive and n-mingle extensions

System FIMIAL Algebra FIMIAL-algebra Standard algebra lcc fi-mianorm

$C_{n}^{r}$ FIMIAL = FIMIAL + $(c_{n}^{r})$ $C_{n}^{r}$ FIMIAL-algebra lcc $c_{n}^{r}$ -fi-mianorm

$C_{n}^{l}$ FIMIAL = FIMIAL + $(c_{n}^{l})$ $C_{n}^{l}$ FIMIAL-algebra lcc $c_{n}^{l}$ -fi-mianorm

$M_{n}^{r}$ FIMIAL = FIMIAL + $(m_{n}^{r})$ $M_{n}^{r}$ FIMIAL-algebra lcc $m_{n}^{r}$ -fi-mianorm

$M_{n}^{l}$ FIMIAL = FIMIAL + $(m_{n}^{l})$ $M_{n}^{l}$ FIMIAL-algebra lcc $m_{n}^{l}$ -fi-mianorm

System FIMIAL	Algebra FIMIAL-algebra	Standard algebra lcc fi-mianorm
$C_{n}^{r}$ FIMIAL = FIMIAL + $(c_{n}^{r})$	$C_{n}^{r}$ FIMIAL-algebra	lcc $c_{n}^{r}$ -fi-mianorm
$C_{n}^{l}$ FIMIAL = FIMIAL + $(c_{n}^{l})$	$C_{n}^{l}$ FIMIAL-algebra	lcc $c_{n}^{l}$ -fi-mianorm
$M_{n}^{r}$ FIMIAL = FIMIAL + $(m_{n}^{r})$	$M_{n}^{r}$ FIMIAL-algebra	lcc $m_{n}^{r}$ -fi-mianorm
$M_{n}^{l}$ FIMIAL = FIMIAL + $(m_{n}^{l})$	$M_{n}^{l}$ FIMIAL-algebra	lcc $m_{n}^{l}$ -fi-mianorm

6 Conclusion

In this paper, we introduced substructural semilinear logics based on mianorms with right and left n-contraction and n-mingle axioms and established standard completeness for these systems and their fixpointed involutive extensions via Yang’s construction in the style of Jenei–Montagna. However, we did not extend these systems to non-fixpointed involutive ones. To consider standard completeness for such systems remains a problem.

Note that, as mentioned in Section 1, several logical and algebraic properties for t-norm-based logics have been already investigated. However, we just investigated standard completeness among those properties. To investigate other properties such as local finiteness, finite embeddability property, finite model property, decidability etc., for mianorm-based logics with right and left n-contraction and n-mingle axioms also remains an another problem.

We finally note that one important application area of substructural fuzzy logics is to introduce algebraic structures for such logics with states interpreted as the probability of fuzzy events (see [11 , 23]). In particular, Zhao and He [37] recently considered states on more general structures, i.e., on non-commutative residuated lattices. Their work may be generalized to non-associative ones. This is also an interesting subject to study in the area.

Footnotes

The system GL, obtained by dropping the associativity axiom from FL (Full Lambek logic), is the most basic substructural logic whose algebraic semantics is given by the variety of residuated lattice-ordered unital groupoids (briefly, rlu-groupoids) introduced by Galatos and Ono [14, ] as a non-associative generalization of FL.

The term “semilinear” was inspired by the tradition in Universal Algebra of calling a class of algebras ‘semiX’ whenever their subdirectly irreducible members are X. For some more detailed reasons to take the name “semilinear” instead of “fuzzy”, see [6 –]

T-norms are commutative, associative, increasing, binary functions with identity 1 on the real unit interval [0, 1].

Uninorms were introduced by Yager and Rybalov [27] as a generalization of t-norms where the identity can lie anywhere in [0, 1]. Micanorms are uninorms dropping associativity and mianorms are micanorms eliminating commutativity (see [31, ]).

In 2002, Ciabattoni, Esteva, and Godo [3] introduced MTL and IMTL (Involutive MTL) with the n-potency axiom and provided standard completeness for them; In 2007, Horčík, Noguera, and Petrík [19] considered more extensions and discussed logical and algebraic properties such as local finiteness, finite embeddability property, finite model property, decidability, and standard completeness of the considered logics; In 2011, Bianchi and Montagna [2] considered four families of extensions of BL with the n-potency axiom and studied their local finiteness, completeness, computational complexity, amalgamation, and interpolation properties. In 2012–13, Wang [24, 25] introduced UL and IUL (Involutive UL) with the n-potency axiom and provided standard completeness for them; In 2013 and 2015–16, Cintula, Horčík, and Noguera [5] and Yang [31, ] independently introduced MICAL (= SL $e^{ℓ}$ ) and MIAL (= SL^ℓ) with the n-potency axiom and provided standard completeness for them. (The index e in $S L_{e}^{l}$ denotes the exchange (commutativity) axiom.)

n-Contraction and n-mingle axioms were first introduced by Hori et al. in [12]. Baldi [] introduced Wang’s C_nUL, for n > 2, (the n-potent UL) as UL with both the n-contraction and n-mingle axioms.

For more non-standard completeness results, see [18, ].

For the detailed reasons to use the name MIAL in place of SL^ℓ, see [].

Finitary weakly implicative logic is a logic having reflexivity, transitivity, modus ponens, and congruence w.r.t. connectives (see []).

The first one is called square increasing and the second one is called square decreasing.

This definition was introduced in []

This definition was introduced in [].

Acknowledgment

A draft of this paper was presented in the conference of TACL 2017. This work was supported by the Ministry of Education of the Republic of Korea and the National Research Foundation of Korea (NRF-2016S1A5A8018255).

References

Baldi

, A note on standard completeness for some extensions of uninorm logic, Soft Computing 18 (2014), 1463–1470.

Bianchi

, Montagna

, n-Contractive BL-Logics, Archive for Mathematical Logic 50 (2011), 257–285.

Ciabattoni

, Esteva

, Godo

, T-norm based logics with n-contraction, Neural Network World 12 (2002), 441–453.

Cignoli

, Esteva

, Godo

, Torrens

, Basic fuzzy logic of continuous t-norms and their residua, Soft Computing 4 (2000), 106–112.

Cintula

, Horčĺk

and Noguera

, Non-associative substructural logics and their semilinear extensions: Axiomatization and completeness properties, Review of Symbolic Logic 6 (2013), 394–423.

Cintula

, Horčĺk

and Noguera

, The quest for the fuzzy logic, Injek on Mathematical Fuzzy Logic, In Petr Hájek on Mathematical Fuzzy Logic, Montagna

, ed., Dordrecht, Springer, 2015, pp. 245–290 basic.

Cintula

, Noguera

, Implicational (semiliear) logics I: A new hierarchy, Archive for Mathematical Logic 49 (2010), 417–446.

Cintula

, Noguera

, A general framework for mathematical fuzzy logic, In Handbook of Mathematical Fuzzy Logic, vol 1, Cintula

, Hájek

and Noguera

, eds, London, College Publications, 2011, pp. 103–207.

Esteva

, Godo

, Monoidal t-norm based logic: Towards a logic for left-continuous t-norms, Fuzzy Sets and Systems 124 (2001), 271–288.

10.

Esteva

, Gispert

, Godo

, Montagna

, On the standard and rational completeness of some axiomatic extensions of the monoidal tnorm logic, Studia Logica 71 (2002), 393–420.

11.

Flaminio

, Godo

, A study for reasoning about the probability of fuzzy events, Fuzzy Sets and Systems 158 (2007), 625–638.

12.

Hori

, Ono

, Schellinx

, Extending intuitionistic linear logic with knotted structural rules, Studia Logica 35 (1994), 219–242.

13.

Galatos

, Jipsen

, Kowalski

, Ono

, Residuated lattices: An algebraic glimpse at substructural logics, Amsterdam, Elsevier, 2007.

14.

Galatos

, Ono

, Non-associative substructural logics: Algebraization, cut elimination and separation, In Conference on Residuated Structures and Many-Valued Logics, Patras University, Greece, 2004.

15.

Galatos

, Ono

, Cut elimination and strong separation for substructural logics, Annals of Pure and Applied Logic 161 (2010), 1097–1133.

16.

Gottwald

, A Treatise on Many-valued Logics, Baldock, Research studies press LTD, 2001.

17.

Hájek

, Metamathematics of Fuzzy Logic, Amsterdam, Kluwer, 1998.

18.

Horčĺk

, Algebraic semantics: Semilinear FL-algebras, In Handbook of Mathematical Fuzzy Logic, vol 1, Cintula

, Hájek

and Noguera

, eds, London, College Publications, 2011, pp. 283–353.

19.

Horčĺk

, Noguera

and Petrík

, On n-contractive fuzzy logics, Mathematical Logic Quarterly 53 (2007), 268–288.

20.

Jenei

, Montagna

, A Proof of Standard completeness for Esteva and Godo’s Logic MTL, Studia Logica 70 (2002), 183–192.

21.

Liu

L.Z.

, Zhang

X.Y.

, States on finite linearly ordered IMTL-algebras, Soft Computing 15 (2011), 2012–2028.

22.

Metcalfe

, Montagna

, Substructural fuzzy logics, The Journal of Symbolic Logic 72 (2007), 834–864.

23.

Mundici

, Averaging the truth-value in Lukasiewicz sentential logic, Studia Logica 55 (1995), 113–127.

24.

Wang

, Uninorm logic with the n-potency axiom, Fuzzy Sets and Systems 205 (2012), 116–126.

25.

Wang

, Involutive uninorm logic with the n-potency axiom, Fuzzy Sets and Systems 218 (2013), 1–23.

26.

Wang

, Logics for residuated pseudo-uninorms and their residua, Fuzzy Sets and Systems 218 (2013), 24–31.

27.

Yager

R.R.

, Rybalov

, Uninorm aggregation operators, Fuzzy Sets and Systems 80 (1996), 111–120.

28.

Wang

, Zhao

, HpsUL is not the logic of pseudo-uninorms and their residua, Logic Journal of IGPL 17 (2009), 413–419.

29.

Yang

, On the standard completeness of an axiomatic extension of the uninorm logic, Korean Journal of Logic 12(2) (2009), 115–139.

30.

Yang

, An axiomatic extension of the uninorm logic revisited, Korean Journal of Logic 17 (2014), 323–348.

31.

Yang

, Weakening-free, non-associative fuzzy logics: Micanorm-based logics, Fuzzy Sets and Systems 276 (2015), 43–58.

32.

Yang

, Basic substructural core fuzzy logics and their extensions: Mianorm-based logics, Fuzzy Sets and Systems 301 (2016), 1–18.

33.

Yang

, Involutive basic substructural core fuzzy logics: Involutive mianorm-based logics, Fuzzy Sets and Systems 320 (2017), 1–16.

34.

Yang

, Implicational tonoid fuzzy logics, In Frontiers in Artificial Intelligence and Applications: Fuzzy Systems and Data Mining IV, vol 309, Tallón-Ballesteros

A.J.

and Li

, eds., Amsterdam, IOS press, 2018, pp. 223–230.

35.

Zadeh

L.A.

, Fuzzy logic and approximate reasoning, Synthese 30 (1975), 407–428.

36.

Zadeh

L.A.

, Preface, In Fuzzy Logic Technology and Applications, II Marks

R.J.

, eds., Piscataway, IEEE, 1994.

37.

Zhao

, He

, On non-commutative residuated lattices with internal states, IEEE Transactions on Fuzzy Systems 26 (2018), 13877–1400.