A Fuzzy Logic for Semi-Overlap Functions and Their Residua

Abstract

Semi-overlap functions as a generalization of left-continuous t-norms also have residua. In this paper, we develop a new residuated logic, SOL-logic, based on semi-overlap functions and their residua. The corresponding algebraic structures, SOL-algebras, are defined, and the completeness of SOL with respect to SOL-algebras is proved.

1. Introduction

Fuzzy logics based on t-norms and their residua have been extensively investigated. Hájek’s basic fuzzy logic (BL) [1] is a logic of continuous t-norms and their residua. Esteva and Godo’s Monoidal t-norm logic (MTL) [2] is a logic of left-continuous t-norms and their residua. Note that both BL and MTL are extensions of Höhle’s monoidal logic (ML) [3] whose algebraic counterpart is the class of residuated lattices. T-norms have 1 as an identity. Yager and Rybalov [4] introduced uninorms as a generalization of t-norms, which have $e\in [0,1]$ as an identity. Uninorm logic (UL) was introduced by Metcalfe [5] (and Montagna [6]) as a logic of left-continuous uninorms and their residua. Moreover, Yager [7,8] introduced micanorm as a generalization of uninorms by removing the associativity condition in its definition. Micanorm is a class of monotonic identity commutative aggregation (MICA) operators. Yang [9] characterized the micanorm-based logics by extending Cintula et al.’s MICAL [10,11].

Bustince et al. [12,13] and Fodor et al. [14] also pointed out that the associativity of the t-norm is unnecessary in some applications, such as decision making and classification problems. Overlap functions were introduced by Bustince et al. [12] as a special class of non-necessarily associative aggregation operators. Later, Miguel et al. [15] relaxed two boundary conditions of overlap functions and introduced the concept of general overlap functions. Based on overlap and grouping functions, some new equivalence operators [16], symmetric differences [17], (G,N)-implications [18], and binary relations [19] were introduced. In particular, residual implications derived from overlap functions were introduced by Dimuro and Bedregal [20]. Note that a fuzzy conjunction [21] and its corresponding fuzzy implication can form a residual pair if and only if it is left-continuous. Zhang et al. [22] removed the right-continuity condition of general overlap functions and introduced the concept of semi-overlap functions. They provided several algebraic properties of semi-overlap functions and their residua.

Semi-overlap functions are non-associative generalizations of left-continuous t-norms. Another important difference between semi-overlap functions and left-continuous t-norms is the identity, which is not required in the definition of the former. This results in semi-overlap functions and their residua to not require the ordering property (OP), i.e., $u\le v$ iff $u\Rightarrow v=1$. The ordering property is one of the most important property in fuzzy logics and is defined as follows:

• A formula A is valid (or a tautology) in MTL and BL logics iff $e\left(A\right)\ge 1$ for all valuations e on BL- and MTL-algebras, respectively. In MTL and BL logics, $A\Rightarrow B$ is valid iff $e\left(A\right)\le e\left(B\right)$ for all valuations e on the corresponding algebras. Note that here, $e\left(A\right)\le e\left(B\right)$ is used instead of $e(A\to B)=1$ because the ordering property is valid for residual implications derived from left-continuous t-norms.
• For residual implications derived from left-continuous uninorms, $u\le v$ iff $u\Rightarrow v\ge t$ holds where t is the identity element based on the definition that a formula A is valid (or a tautology) iff $e\left(A\right)\ge t$ for all valuations e on UL-algebra. In UL logic, this result of $A\Rightarrow B$ being valid iff $e\left(A\right)\le e\left(B\right)$ for all valuations e on UL-algebra still holds.

So, in these logics, the order is interpreted by residual implications. However, it is difficult to interpret the order by the residual implications derived from the semi-overlap functions in the logical setting. To overcome this, we adopt Goldblatt’s idea [23] of binary logics, which is about ordered pairs of formulas under certain rules, for example, $A{⊢}_{O}B$ (or $\langle A,B\rangle \in O$) in a binary logic O iff $e\left(A\right)\le e\left(B\right)$ for all valuations e on the corresponding algebra [24,25,26]. In this sense, MTL, BL, and UL are unary logics, which refer to sets of formulas under certain rules. Note that when the deduction theorem holds, a unary logic O can be used in place of a binary logic O of all pairs $\langle A,B\rangle$ such that ${⊢}_{O}A\Rightarrow B$.

In MTL and its extensions, the residuation property (RP) is a significant feature, defined as the condition where $u\ast v\le w$ iff $u\le v\to w$. RP is represented by two axioms: $\left(A7a\right)(u\ast v\to w)\to (u\to (v\to w\left)\right)$ and $\left(A7b\right)(u\to (v\to w\left)\right)\to (u\ast v\to w)$. It is important to note that (A7a) and (A7b) are constructed based on both the OP and RP. Additionally, (A7a) and (A7b) also signify that $u\ast v\to w=u\to (v\to w)$, denoted as the strong residuation property (SRP). However, it is imperative to acknowledge that the RP and SRP are not synonymous. Notably, the semi-overlap function and its residua adhere to the RP but not the SRP, thereby rendering the application of (A7a) and (A7b) insufficient for respecting the RP in the context of the semi-overlap function and its residua. Hence, there arises the need for the introduction of novel axioms to aptly reflect the RP within the realm of the semi-overlap function and its residua.

In this paper, based on the concepts of semi-overlap functions and their residua, we introduce a new class of algebras called SOL-algebras and develop a specific formal logic called SOL-logic. This article is structured as follows. In Section 2, some preliminaries concerning semi-overlap functions and their residua are presented. In Section 3, we present a class of algebras called SOL-algebras, which are weakenings of residuated lattices. In Section 4, we introduce the SOL-logic with corresponding algebraic semantics and provide the completeness results of SOL with respect to SOL-algebras. In Section 5, conclusions are provided.

2. Preliminaries

2.1. Fuzzy Conjunction, Fuzzy Implication, and Residuated Lattice

Definition 1

([21]). A mapping $\sqcap :{[0,1]}^2\to [0,1]$ is called a fuzzy conjunction if the following conditions hold for any $u,v\in [0,1]$:

(C1) 

⊓ is increasing;

(C2) 

$1\sqcap 1=1$;

(C3) 

$0\sqcap 0=1\sqcap 0=0\sqcap 1=0$.

Based on the fuzzy conjunction ⊓, we can define a function

$$\begin{array}{c}\hfill u{\to }_{\sqcap }v=sup\{w\in [0,1]|u\sqcap w\le v\},\forall u,v\in [0,1].\end{array}$$

(1)

Theorem 1

([21]). The function ${\to }_{\sqcap }$ is a fuzzy implication derived from ⊓ if and only if the fuzzy conjunction ⊓ satifies

$$\begin{array}{c}\hfill 1\sqcap v>0,\forall v\in (0,1].\end{array}$$

(2)

The pair $(\sqcap ,{\to }_{\sqcap })$ satisfies the residuation property (RP) if

$$\begin{array}{c}\hfill u\sqcap v\le w\mathrm{iff}u\le v{\to }_{\sqcap }w,\forall u,v,w\in [0,1].\end{array}$$

(3)

Theorem 2

([21]). Let ⊓ be a fuzzy conjunction satisfying Equation (2) and ${\to }_{\sqcap }$ be a fuzzy implication derived from ⊓. Then, the following statements are equivalent:

(i) 

⊓ is left-continuous with respect to the second variable;

(ii) 

The pair $(\sqcap ,{\to }_{\sqcap })$ satisfies the residuation property (RP);

(iii) 

$u{\to }_{\sqcap }v=sup\{w\in [0,1]|u\sqcap w\le v\},\forall u,v\in [0,1]$.

Definition 2

([27]). A mapping $\ast :{[0,1]}^2\to [0,1]$ is called a t-norm if it is commutative, associative, non-decreasing in both arguments, and $1\ast x=x,\forall x\in [0,1]$.

Clearly, a t-norm is a fuzzy conjunction. Let * be a left-continuous t-norm, and the residual implication derived from * is defined as follows:

$$\begin{array}{c}\hfill u{\to }_{\ast }v=max\left(w\in [0,1]|u\ast w\le v\right),\forall u,v\in [0,1].\end{array}$$

(4)

where ${\to }_{\ast }$ satisfies the ordering property (OP), i.e.,

$$\begin{array}{c}\hfill u\le v\mathrm{iff}u{\to }_{\ast }v=1,\forall u,v\in [0,1].\end{array}$$

(5)

The pair $(\ast ,{\to }_{\ast })$ satisfies the RP, i.e.,

$$\begin{array}{c}\hfill u\ast v\le w\mathrm{iff}u\le v{\to }_{\ast }w,\forall u,v,w\in [0,1].\end{array}$$

(6)

Definition 3

([28]). A residuated lattice $\mathcal{L}$ is an algebra of type (2,2,2,2,0,0), i.e.,

$$\begin{array}{c}\hfill \mathcal{L}=<L,\wedge ,\vee ,\ast ,\Rightarrow ,0,1>\end{array}$$

(7)

such that we have the following:

(SO1) 

$(L,\wedge ,\vee ,0,1)$ is a lattice with the greatest element 1 and the least element 0 with respect to the lattice ordering ≤;

(SO2) 

* satisfies the following for all $a,b,c\in L$:

(i) 

$a\ast b=b\ast a$;

(ii) 

$a\ast (b\ast c)=(a\ast b)\ast c$;

(iii) 

$1\ast a=a$.

(SO3) 

$(\otimes ,\Rightarrow )$ is a residuated pair, i.e., for all $a,b,c\in L$,

(iv) 

$a\otimes b\le c$ iff $a\le b\Rightarrow c$.

2.2. Semi-Overlap Functions and Their Residua

Definition 4

([22]). A mapping $\otimes :{[0,1]}^2\to [0,1]$ is called a semi-overlap function if the following conditions hold for any $u,v\in [0,1]$:

(S1) 

$u\otimes v=v\otimes u$;

(S2) 

If $uv=0$, then $u\otimes v=0$;

(S3) 

If $uv=1$, then $u\otimes v=1$;

(S4) 

⊗ is increasing;

(S5) 

⊗ is left-continuous.

Let ⊗ be a semi-overlap function, its residuum $\Rightarrow :{[0,1]}^2\to [0,1]$ is defined as

$$\begin{array}{c}\hfill u\Rightarrow v=sup\{w\in [0,1\left]\right|u\otimes w\le v\}.\end{array}$$

(8)

The pair $(\otimes ,\Rightarrow )$ satisfies the residuation property (RP), i.e.,

$$\begin{array}{c}\hfill u\otimes v\le w\mathrm{iff}u\le v\Rightarrow w,\forall u,v,w\in [0,1].\end{array}$$

(9)

In

Table 1. Two semi-overlap functions and their residual implications.

Semi-Overlap Functions	Residual Implications
$u\otimes v=min\{u^p,v^p\}$	$u\Rightarrow v=\left\{\begin{array}{cc}1,& \mathrm{if}{u}^p\le v,\\ \sqrt[p]{v},& \mathrm{if}{u}^p>v.\end{array}\right.$
$u\otimes v=u^p\times v^p$	$u\Rightarrow v=\left\{\begin{array}{cc}1,& \mathrm{if}{u}^p\le v,\\ {\displaystyle \frac{\sqrt[p]{v}}{u}},& \mathrm{if}{u}^p>v.\end{array}\right.$

, for $p>0$, we provide two examples of semi-overlap functions that are not left-continuous t-norms when $p\ne 1$.

Lemma 1

([22]). Let ⊗ be a semi-overlap function and ⇒ be its residuum. Then, ⇒ satisfies the ordering property, i.e.,

$$\begin{array}{c}\hfill u\le v\mathrm{iff}u\Rightarrow v=1,\forall u,v\in [0,1],\end{array}$$

(10)

iff ⊗ has 1 as the neutral element, i.e.,

$$\begin{array}{c}\hfill 1\otimes u=u,\forall u\in [0,1].\end{array}$$

(11)

Lemma 2.

Let ⊗ be a semi-overlap function and ⇒ be its residuum. Then, $(\otimes ,\Rightarrow )$ satisfy the strong residuation property (SRP)

$$\begin{array}{c}\hfill u\Rightarrow (v\Rightarrow w)=u\otimes v\Rightarrow w,\forall u,v,w\in [0,1]\end{array}$$

(12)

iff ⊗ is associative, i.e.,

$$\begin{array}{c}\hfill u\otimes (v\otimes w)=(u\otimes v)\otimes w,\forall u,v,w\in [0,1]\end{array}$$

(13)

Proof. 

SRP to associativity: For any $a\in [0,1]$,

$$\begin{array}{ccc}\hfill (u\otimes v)\otimes w\le a& \mathrm{iff}& u\otimes v\le w\Rightarrow a\hfill \\ & \mathrm{iff}& u\le v\Rightarrow (w\Rightarrow a)\hfill \\ & \mathrm{iff}& u\le (v\otimes w)\Rightarrow a\hfill \\ & \mathrm{iff}& u\otimes (v\otimes w)\le a.\hfill \end{array}$$

Because of the arbitrariness of a, we have $(u\otimes v)\otimes w=u\otimes (v\otimes w)$.

Associativity to SRP: For any $a\in [0,1]$,

$$\begin{array}{ccc}\hfill a\le u\Rightarrow (v\Rightarrow w)& \mathrm{iff}& a\otimes u\le v\Rightarrow w\hfill \\ & \mathrm{iff}& (a\otimes u)\otimes v\le w\hfill \\ & \mathrm{iff}& a\otimes (u\otimes v)\le w\hfill \\ & \mathrm{iff}& a\le s(u\otimes v)\Rightarrow w.\hfill \end{array}$$

Because of the arbitrariness of a, we have $u\Rightarrow (v\Rightarrow w)=u\otimes v\Rightarrow w$. □

Unfortunately, the property of associativity is not included in the definition of semi-overlap functions, which means that the SRP may fail for semi-overlap functions and their residua by Lemma 1 (ii); see the following examples.

Example 1.

Consider the semi-overlap function $u\otimes v=min\{u^p,v^p\},\forall u,v\in [0,1]$. Its residuum is

$$u\Rightarrow v=\left\{\begin{array}{cc}1,& \mathrm{if}{u}^p\le v,\\ \sqrt[p]{v},& \mathrm{if}{u}^p>v.\end{array}\right.$$

Let $p=2$. Then, we have $0.8\Rightarrow (0.8\Rightarrow 0.36)=0.8\Rightarrow 0.6=\sqrt{0.6}$ and $(0.8\otimes 0.8)\Rightarrow 0.36)=0.64\Rightarrow 0.36=0.6$. Thus, $0.8\Rightarrow (0.8\Rightarrow 0.5)\ne (0.8\otimes 0.8)\Rightarrow 0.5$.

Moreover, we have $(u\otimes v)\otimes w=min\{u^p,v^p\}\otimes w=min\{u^{2p},v^{2p},w^p\}$ and $u\otimes (v\otimes w)=u\otimes min\{v^p,w^p\}=min\{u^{2p},v^{2p},w^p\}$. Thus, $(u\otimes v)\otimes w\ne u\otimes (v\otimes w)$.

Example 2.

Consider the semi-overlap function $u\otimes v=u^p·v^p,\forall u,v\in [0,1]$. Its residuum is

$$u\Rightarrow v=\left\{\begin{array}{cc}1,& \mathrm{if}{u}^p\le v,\\ {\displaystyle \frac{\sqrt[p]{v}}{u}},& \mathrm{if}{u}^p>v.\end{array}\right.$$

Let $p=2$. Then, we have $0.8\Rightarrow (0.8\Rightarrow 0.36)=0.8\Rightarrow {\displaystyle \frac{0.6}{0.8}}=0.8\Rightarrow 0.75=1$ and $(0.8\otimes 0.8)\Rightarrow 0.36)=0.64\Rightarrow 0.36={\displaystyle \frac{0.6}{0.64}}=0.9375$. Thus, $0.8\Rightarrow (0.8\Rightarrow 0.25)\ne (0.8\otimes 0.8)\Rightarrow 0.25$.

Moreover, we have $(u\otimes v)\otimes w=min\{u^p,v^p\}\otimes w=min\{u^{2p},v^{2p},w^p\}$ and $u\otimes (v\otimes w)=u\otimes min\{v^p,w^p\}=min\{u^{2p},v^{2p},w^p\}$. Thus, $(u\otimes v)\otimes w\ne u\otimes (v\otimes w)$.

Remark 1.

From (S2)–(S4), we know that the semi-overlap function is a fuzzy conjunction. Additionally, according to (S5) and Theorem 2, the semi-overlap function and its residuum satisfy the residuation property (RP).

Remark 2.

In [29], Equation (12) was used as the residuation property. Here, we know that the  SRP  is stronger than the  RP. The  SRP is valid for left-continuous t-norms and their residua, but invalid for semi-overlap functions and their residua.

3. SOL-Algebras

In this section, we present the definition of an SOL-algebra.

Definition 5.

An SOL-algebra $\mathcal{S}$ is an algebra of type (2,2,2,2,0,0), i.e.,

$$\begin{array}{c}\hfill \mathcal{S}=<L,\wedge ,\vee ,\otimes ,\Rightarrow ,0,1>\end{array}$$

(14)

such that we have the following:

(SO1) 

$(L,\wedge ,\vee ,0,1)$ is a lattice with greatest element 1 and the least element 0 with respect to the lattice ordering ≤;

(SO2) 

⊗ satisfies the following for all $a,b\in L$:

(i) 

$a\otimes b=b\otimes a$;

(ii) 

$a\otimes 0=0$;

(iii) 

$1\otimes 1=1$.

(SO3) 

$(\otimes ,\Rightarrow )$ is a residuated pair, i.e., for all $a,b,c\in L$,

(iv) 

$a\otimes b\le c$ iff $a\le b\Rightarrow c$.

Remark 3.

(SO2)(i) expresses that ⊗ is commutative. (SO2)(ii) is motivated by (S2) of the semi-overlap: if $uv=0$, then $u\otimes v=0$. (SO2)(iii) is motivated by (S3) of the semi-overlap: if $uv=1$, then $u\otimes v=1$. (SO3) expresses the residuation property.

Theorem 3.

In each SOL-algebra, the following properties hold for all $a,b,c\in L$:

(i) 

$a\otimes (a\Rightarrow b)\le b$ and $a\le (b\Rightarrow (a\otimes b\left)\right)$;

(ii) 

$a\le b$ implies $a\otimes c\le b\otimes c$, $c\Rightarrow a\le c\Rightarrow b$ and $b\Rightarrow c\le a\Rightarrow c$.

Proof. 

(i)

$a\otimes (a\Rightarrow b)\le b$ follows from $(a\Rightarrow b)\le (a\Rightarrow b)$ by (SO3). $a\le (b\Rightarrow (a\otimes b\left)\right)$ follows from $(a\otimes b)\le (a\otimes b)$ by (SO3).

(ii)

Assume that $a\le b$. By (i) $b\le (c\Rightarrow (b\otimes c\left)\right)$, we have $a\le (c\Rightarrow (b\otimes c\left)\right)$. Then, by (SO3), we have $a\otimes c\le b\otimes c$.

Assume that $a\le b$. By (i) $c\otimes (c\Rightarrow a)\le a$, we have $c\otimes (c\Rightarrow a)\le b$. Then, by (SO3), we have $c\Rightarrow a\le c\Rightarrow b$. By $a\otimes (b\Rightarrow c)\le b\otimes (b\Rightarrow c)\le c$ and (SO3), we have $b\Rightarrow c\le a\Rightarrow c$. □

$\left(\right[0,1],min,max,\otimes ,\Rightarrow ,0,1)$ is an SOL-algebra where ⊗ is a semi-overlap function and ⇒ is its residuum.

Definition 6

([28]). A residuated lattice $\mathcal{S}$ is an algebra $\mathcal{S}=<L,\wedge ,\vee ,\otimes ,\Rightarrow ,0,1>$ such that (SO1) and (SO3) hold, and $<L,\otimes ,1>$ is a commutative monoid, i.e., for all $a,b,c\in L$:

(i) 

$a\otimes b=b\otimes a$;

(ii) 

$(a\otimes b)\otimes c=a\otimes (b\otimes c)$;

(iii) 

$a\otimes 1=a$.

Lemma 3.

A residuated lattice is an SOL-algebra if and only if ⊗ satisfies Equations (11) and (13).

Proof. 

We only need to prove that (SO2)(ii) and (iii) are properties of a residuated lattice. (SO2)(ii) For any $a\in L$, $a\otimes 0\le 1\otimes 0=0$. (SO2)(iii) is a direct consequence of Equation (11). □

4. The Logic SOL

4.1. Our Calculus

Definition 7.

(1). 

The language of the SOL-logic consists of propositional variables $p,q,r,\cdots$, binary connectives $\wedge ,\vee ,\&,\to$, and a constant $\overline{0}$ (falsity).

(2). 

Each propositional variable is a formula, $\overline{0}$ is a formula, and if A and B are formulas, then $A\wedge B$, $A\vee B$, $A\&B$, and $A\to B$ are formulas Further, we introduce the following shorts:

(a) 

$\neg A$ is $A\to \overline{0}$;

(b) 

$\overline{1}$ is $\overline{0}\to \overline{0}$.

(3). 

The set of all formulas for the given language F is denoted by $\mathcal{F}$. Let F be a language of SOL-logic and $\mathcal{S}=<L,\wedge ,\vee ,\otimes ,\Rightarrow ,0,1>$ be an SOL-algebra. A truth evaluation $e:\mathcal{F}\to L$ is defined as follows: if $p\in \mathcal{F}$ is a propositional variable, then $e\left(p\right)\in L$. Furthermore, for any $A,B\in \mathcal{F}$, we have the following:

(a) 

$e\left(\overline{0}\right)=0$;

(b) 

$e(A\wedge B)=e\left(A\right)\wedge e\left(B\right)$;

(c) 

$e(A\vee B)=e\left(A\right)\vee e\left(B\right)$;

(d) 

$e(A\&B)=e\left(A\right)\otimes e\left(B\right)$;

(e) 

$e(A\Rightarrow B)=e\left(A\right)\to e\left(B\right)$.

(4). 

A formula A is a tautology, denoted by $\vDash A$, if $e\left(A\right)=1$ for each evaluation e.

(5). 

A formula B is a logical consequence of a formula A, denoted by $A\vDash B$, if $e\left(A\right)\le e\left(B\right)$ for each evaluation e.

Our system (that has no axioms) is determined as a set of rules. Each rule has the form

$$\begin{array}{c}\hfill {\displaystyle \frac{A_1⊢B_1,\cdots ,A_n⊢B_n}{A⊢B}}\end{array}$$

(15)

(If $B_1$ is inferred from $A_1$, …, $B_n$ is inferred from $A_n$, and then B could be inferred from A.) The configurations $A_1⊢B_1,\cdots ,A_n⊢B_n$ represent the premises of the rule, while $A⊢B$ is the conclusion. An improper rule is a rule in which the set of premises is empty. Instead of ${\displaystyle \frac{\varnothing }{A⊢B}}$, we will write $A⊢B$; instead of $\overline{1}⊢B$, we will write $⊢B$.

$$Rulesof\mathit{SOL}$$

$$\begin{array}{ccc}\hfill \left(R1\right)& A⊢A\hfill & \hfill \left(identity\right)\\ \hfill \left(R2\right)& {\displaystyle \frac{A⊢B,B⊢C}{A⊢C}}\hfill & \hfill \left(transitivity\right)\\ \hfill \left(R3\right)& A\&B⊢B\&A\hfill & \\ \hfill \left(R4\right)& A\&\overline{0}⊢\overline{0}\hfill & \\ \hfill \left(R5\right)& {\displaystyle \frac{⊢A,⊢B}{⊢A\&B}}\hfill & \hfill (\&-introduction)\\ \hfill \left(R6\right)& {\displaystyle \frac{A\&B⊢C}{A⊢B\Rightarrow C}}\hfill & \\ \hfill \left(R7\right)& {\displaystyle \frac{A⊢B\Rightarrow C}{A\&B⊢C}}\hfill & \\ \hfill \left(R8\right)& A\wedge B⊢A\hfill & \hfill (\wedge -elimination)\\ \hfill \left(R9\right)& A\wedge B⊢B\wedge A\hfill & \hfill (\wedge -commutativity)\\ \hfill \left(R10\right)& {\displaystyle \frac{A⊢B,A⊢C}{A⊢B\wedge C}}\hfill & \hfill \left(intersectioninferencerule\right)\\ \hfill \left(R11\right)& A⊢A\vee B\hfill & \\ \hfill \left(R12\right)& A\vee B⊢B\vee A\hfill & \hfill (\vee -commutativity)\\ \hfill \left(R13\right)& {\displaystyle \frac{A⊢C,B⊢C}{A\vee B⊢C}}\hfill & \\ \hfill \left(R14\right)& \overline{0}⊢A\hfill \end{array}$$

Remark 4.

SOL-logic is characterized by the SOL-algebra in the sense that $A\vDash B$ if $e\left(A\right)\le e\left(B\right)$ for each evaluation e on all SOL-algebras. Thus, a tautology $\vDash B$ is a special case of $A\vDash B$ when $A=\overline{1}$.

Remark 5.

Comments on some rules. (R3) expresses the commutativity of &. (R4) is motivated by property (S2) of the semi-overlap function: if $uv=0$, then $u\otimes v=0$. (R6) and (R7) express the residuation property. (R14) says that $e\left(\overline{0}\right)\le e\left(A\right)$ for any formula A and any evaluation e.

Remark 6.

We have the rule $A⊢A$, but do not have the rule $⊢A\Rightarrow A$. Consider the implication $u\Rightarrow v=\left\{\begin{array}{cc}1,& \mathrm{if}\sqrt{u}\le v,\\ v^2,& \mathrm{if}\sqrt{u}>v.\end{array}\right.$ derived from the semi-overlap function $u\otimes v=min\{\sqrt{u},\sqrt{v}\}$. Obviously, $0.5\Rightarrow 0.5=0.25\ne 1$. From this, we also know that the deduction theorem does not hold.

Remark 7.

In BL and MTL logics, the residuation property are expressed by two axioms:

$$\begin{array}{ccc}\hfill \left(A1\right)& ⊢(A\Rightarrow (B\Rightarrow C\left)\right)\Rightarrow (A\&B\Rightarrow C);\hfill & \\ \hfill \left(A2\right)& ⊢(A\&B\Rightarrow C)\Rightarrow (A\Rightarrow (B\Rightarrow C\left)\right).\hfill \end{array}$$

However, neither $(A\Rightarrow (B\Rightarrow C\left)\right)\Rightarrow (A\&B\Rightarrow C)$ nor $(A\&B\Rightarrow C)\Rightarrow (A\Rightarrow (B\Rightarrow C\left)\right)$ are tautologies in SOL. Therefore, we cannot replace (R7) and (R6) with (A1) and (A2), respectively.

4.2. Main Properties

Theorem 4.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R15\right)& ⊢\overline{1}\hfill & \\ \hfill \left(R16\right)& A⊢\overline{1}\hfill & \\ \hfill \left(R17\right)& ⊢A\Rightarrow (\overline{1}\&A)\hfill & \\ \hfill \left(R18\right)& {\displaystyle \frac{⊢A,⊢A\Rightarrow B}{⊢B}}\hfill & \hfill \left(MPrule\right)\end{array}$$

Proof. 

(R15) follows immediately from (R1); thus, $\overline{1}⊢\overline{1}$.

(R16) follows from (R4) $A\&\overline{0}⊢\overline{0}$; using (R6), we have $A⊢\overline{0}\Rightarrow \overline{0}$, and thus $A⊢\overline{1}$.

(R17) follows immediately from (R1) $\overline{1}\&A⊢\overline{1}\&A$; using (R6), we have $\overline{1}⊢A\Rightarrow (\overline{1}\&A)$.

(R18) follows from the assumption and (R15); then (R18) is proved in the following way:

$${\displaystyle \frac{\frac{\overline{1}⊢A\Rightarrow B}{\overline{1}\&A⊢B}\left(R8\right),\frac{⊢\overline{1},⊢A}{⊢\overline{1}\&A}\left(R5\right)}{⊢B}}\left(R2\right)$$

□

Remark 8.

Note that the MP rule is a derived rule rather than a fundamental rule within the SOL logic.

Theorem 5.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R19\right)& A\&(A\Rightarrow B)⊢B\hfill & \\ \hfill \left(R20\right)& A⊢B\Rightarrow (A\&B)\hfill & \\ \hfill \left(R21\right)& {\displaystyle \frac{A⊢B}{A\&C⊢B\&C}}\hfill & \\ \hfill \left(R22\right)& {\displaystyle \frac{A⊢B}{C\Rightarrow A⊢C\Rightarrow B}}\hfill & \\ \hfill \left(R23\right)& {\displaystyle \frac{A⊢B}{B\Rightarrow C⊢A\Rightarrow C}}\hfill & \\ \hfill \left(R24\right)& {\displaystyle \frac{A_1⊢B_1,A_2⊢B_2}{A_1\&A_2⊢B_1\&B_2}}\hfill \end{array}$$

Proof. 

(R19) follows from (R1) $A\Rightarrow B⊢A\Rightarrow B$ and from using (R7).

(R20) follows from (R1) $A\&B⊢A\&B$ and from using (R6).

(R21) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{A⊢B,B⊢C\Rightarrow (B\&C)\left(R20\right)}{\frac{A⊢C\Rightarrow (B\&C)}{A\&C⊢B\&C}\left(R7\right)}}\left(R2\right)\end{array}$$

(R22) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{A⊢B,C\&(C\Rightarrow A)⊢A\left(R19\right)}{\frac{C\&(C\Rightarrow A)⊢B)}{C\Rightarrow A⊢C\Rightarrow B}\left(R6\right)}}\left(R2\right)\end{array}$$

(R23) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A⊢B}{A\&(B\Rightarrow C)⊢B\&(B\Rightarrow C)}\left(R21\right),B\&(B\Rightarrow C⊢C\left(R19\right)}{\frac{A\&(B\Rightarrow C⊢C}{B\Rightarrow C⊢A\Rightarrow C}\left(R6\right)}}\left(R2\right)\end{array}$$

(R24) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A_1⊢A_2}{A_1\&B_2⊢A_2\&B_2}\left(R21\right),\frac{B_1⊢B_2}{A_1\&B_1⊢A_1\&B_2}\left(R21\right)}{A_1\&A_2⊢B_1\&B_2}}\left(R2\right)\end{array}$$

□

Theorem 6.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R25\right)& {\displaystyle \frac{A⊢B}{A\wedge C⊢B\wedge C}}\hfill & \\ \hfill \left(R26\right)& {\displaystyle \frac{A⊢B}{A\vee C⊢B\vee C}}\hfill & \\ \hfill \left(R27\right)& {\displaystyle \frac{A_1⊢A_2,B_1⊢B_2}{A_1\wedge B_1⊢A_2\wedge B_2}}\hfill & \\ \hfill \left(R28\right)& {\displaystyle \frac{A_1⊢A_2,B_1⊢B_2}{A_1\vee B_1⊢A_2\vee B_2}}\hfill & \\ \hfill \left(R29\right)& A⊢A\wedge (A\vee B)\hfill & \\ \hfill \left(R30\right)& A\vee (A\wedge B)⊢A\hfill & \\ \hfill \left(R31\right)& A\wedge (B\wedge C)⊢(A\wedge B)\wedge C\hfill & \\ \hfill \left(R32\right)& A\wedge (B\wedge C)⊢(A\wedge B)\wedge C\hfill & \\ \hfill \left(R33\right)& (A\vee B)\vee C⊢A\vee (B\vee C)\hfill & \\ \hfill \left(R34\right)& (A\vee B)\vee C⊢A\vee (B\vee C)\hfill \end{array}$$

Proof. 

(R25) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A⊢B,A\wedge C⊢A\left(R8\right)}{A\wedge C⊢B}\left(R2\right),A\wedge C⊢C\left(R8\right)}{A\wedge C⊢B\wedge C}}\left(R10\right)\end{array}$$

(R26) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A⊢B,B⊢C\vee B\left(R11\right)}{A\wedge C⊢B}\left(R2\right),C⊢B\vee C\left(R11\right)}{A\vee C⊢B\vee C}}\left(R13\right)\end{array}$$

(R27) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A_1⊢A_2,A_1\wedge B_1⊢A_1\left(R8\right)}{A_1\wedge B_1⊢A_2}\left(R2\right),\frac{B_1⊢B_2,A_1\wedge B_1⊢B_1\left(R8\right)}{A_1\wedge B_1⊢B_2}\left(R2\right)}{A_1\wedge B_1⊢A_2\wedge B_2}}\left(R10\right)\end{array}$$

(R28) is proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A_1⊢A_2,A_2⊢A_2\vee B_2\left(R11\right)}{A_1⊢A_2\vee B_2}\left(R2\right),\frac{B_1⊢B_2,B_2⊢A_2\vee B_2\left(R11\right)}{B_1⊢A_2\vee B_2}\left(R2\right)}{A_1\vee B_1⊢A_2\vee B_2}}\left(R13\right)\end{array}$$

(R29) follows from (R1) $A⊢A$, (R11) $A⊢A\vee B$, and from using (R10).

(R30) follows from (R1) $A⊢A$, (R11) $A\wedge B⊢A$, and from using (R13).

For (R31), first, $A\wedge (B\wedge C)⊢(A\wedge B)$ and $A\wedge (B\wedge C)⊢C$ are proved in the following way:

$$\begin{array}{c}\hfill {\displaystyle \frac{A\wedge (B\wedge C)⊢A\left(R8\right),\frac{A\wedge (B\wedge C)⊢(B\wedge C)\left(R8\right),B\wedge C⊢B\left(R8\right)}{A\wedge (B\wedge C)⊢B}\left(R2\right)}{A\wedge (B\wedge C)⊢(A\wedge B)}}\left(R10\right)\end{array}$$

$$\begin{array}{c}\hfill {\displaystyle \frac{A\wedge (B\wedge C)⊢(B\wedge C)\left(R8\right),B\wedge C⊢C\left(R8\right)}{A\wedge (B\wedge C)⊢C}}\left(R2\right)\end{array}$$

Then, using (R10), we have $A\wedge (B\wedge C)⊢(A\wedge B)\wedge C$.

For (R32)–(R34), their proofs are similar to that of (R31). □

Definition 8.

$⊢A\equiv B$ iff $A⊢B$ and $B⊢A$.

Now, we prove some derived rules of equivalence of SOL.

Theorem 7.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R35\right)& ⊢A\equiv A\hfill & \\ \hfill \left(R36\right)& {\displaystyle \frac{⊢A\equiv B}{⊢B\equiv A}}\hfill & \\ \hfill \left(R37\right)& {\displaystyle \frac{⊢A\equiv B,⊢B\equiv C}{⊢A\equiv C}}\hfill & \\ \hfill \left(R38\right)& ⊢A\equiv A\wedge (A\vee B)\hfill & \\ \hfill \left(R39\right)& ⊢A\vee (A\wedge B)\equiv A\hfill & \\ \hfill \left(R40\right)& {\displaystyle \frac{⊢A\equiv B}{⊢A\wedge C\equiv B\wedge C}}\hfill & \\ \hfill \left(R41\right)& {\displaystyle \frac{⊢A\equiv B}{⊢A\vee C\equiv B\vee C}}\hfill & \\ \hfill \left(R42\right)& {\displaystyle \frac{⊢A\equiv B}{⊢A\&C\equiv B\&C}}\hfill & \\ \hfill \left(R43\right)& {\displaystyle \frac{⊢A\equiv B}{⊢A\Rightarrow C\equiv B\Rightarrow C}}\hfill & \\ \hfill \left(R44\right)& {\displaystyle \frac{⊢A\equiv B}{⊢C\Rightarrow A\equiv C\Rightarrow B}}\hfill & \\ \hfill \left(R45\right)& {\displaystyle \frac{⊢A\equiv B}{⊢\neg A\equiv \neg B}}\hfill & \\ \hfill \left(R46\right)& ⊢A\wedge A\equiv A\hfill & \\ \hfill \left(R47\right)& ⊢A\vee A\equiv A\hfill & \\ \hfill \left(R48\right)& ⊢A\wedge B\equiv B\wedge A\hfill & \\ \hfill \left(R49\right)& ⊢A\vee B\equiv B\vee A\hfill & \\ \hfill \left(R50\right)& ⊢A\wedge (B\wedge C)\equiv (A\wedge B)\wedge C\hfill & \\ \hfill \left(R51\right)& ⊢A\vee (B\vee C)\equiv (A\vee B)\vee C\hfill & \\ \hfill \left(R52\right)& ⊢A\&B\equiv B\&A\hfill & \\ \hfill \left(R53\right)& ⊢A\&\overline{0}\equiv \overline{0}\hfill & \\ \hfill \left(R54\right)& ⊢\overline{1}\&\overline{1}\equiv \overline{1}\hfill \end{array}$$

Proof. 

(R35), (R36), and (R37) are immediately from (R1) and (R2).

(R38) is immediately from (R8) and (R29).

(R39) is immediately from (R11) and (R30).

(R40), (R41), (R42), (R43), and (R44) are immediately from (R25), (R26), (R21), (R22), and (R23), respectively.

(R45) is immediately from (R39) by letting C be $\overline{1}$.

(R46) is immediately from (R1), (R8), and (R10).

(R47) is immediately from (R1), (R11), and (R13).

(R48) and (R49) are immediately from (R9) and (R12), respectively.

(R50) and (R51) are immediately from (R31), (R32), (R33), and (R34), respectively.

(R52), (R53), and (R54) are from (R3), (R4), (R14), (R5), and (R16), respectively. □

Theorem 8.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R55\right)& {\displaystyle \frac{A⊢B}{\neg B⊢\neg A}}\hfill & \\ \hfill \left(R56\right)& A⊢\neg \neg A\hfill & \\ \hfill \left(R57\right)& A\&\neg A⊢\overline{0}\hfill & \\ \hfill \left(R58\right)& \neg A\vee \neg B⊢\neg (A\wedge B)\hfill & \\ \hfill \left(R59\right)& \neg (A\vee B)⊢\neg A\wedge \neg B)\hfill \end{array}$$

Proof. 

(R55) is immediately from (R23) by letting C be $\overline{1}$.

(R56) through using (R55) twice and (R2).

(R57) through using (R56) and (R7).

(R58) is immediately from

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A\wedge B⊢A\left(R9\right)}{\neg A⊢\neg (A\wedge B)},\left(R55\right),\frac{A\wedge B⊢B\left(R8\right)}{\neg B⊢\neg (A\wedge B)},\left(R55\right)}{\neg A\vee \neg B⊢\neg (A\wedge B)}}\left(R13\right).\end{array}$$

(R59) is immediately from

$$\begin{array}{c}\hfill {\displaystyle \frac{\frac{A⊢A\vee B\left(R11\right)}{\neg (A\vee B)⊢\neg A},\left(R55\right),\frac{B⊢A\vee B\left(R11\right)}{\neg (A\vee B)⊢\neg B},\left(R55\right)}{\neg (A\vee B)⊢\neg A\wedge \neg B)}}\left(R10\right).\end{array}$$

□

Theorem 9.

The following are derived rules of SOL:

$$\begin{array}{ccc}\hfill \left(R60\right)& ⊢A\wedge \overline{1}\equiv A\hfill & \\ \hfill \left(R61\right)& ⊢A\vee \overline{0}\equiv A\hfill & \end{array}$$

Proof. 

(R60) $A⊢A\wedge \overline{1}$ is from (R1) $A⊢A$ and (R16) $A⊢\overline{1}$ through using (R13). Then, (R9) $A\wedge \overline{1}⊢A$ holds. Thus, $⊢A\wedge \overline{1}\equiv A$.

(R61) $A\vee \overline{0}⊢A$ is from (R1) $A⊢A$ and (R14) $\overline{0}⊢A$ through using (R10). Then, (R11) $A⊢A\vee \overline{0}$ holds. Thus, $⊢A\vee \overline{0}\equiv A$. □

4.3. The Soundness and Completeness Theorems

Our calculus is adequate with respect to our semantic characterization because of the following soundness and completeness theorems.

Theorem 10.

(Soundness) If $A⊢B$, then $A\vDash B$.

Proof. 

(R1) and (R2) are immediately from properties of lattice ordering ≤. (R3), (R4), and (R5) are from (SO2). To verify (R6) and (R7), we use the residuation of $(\otimes ,\Rightarrow )$. (R8)–(R13) are from the properties of ∨ and ∧. (R14) is obviously from the minimality of 0. □

Lemma 4.

The following is equivalent for every formula $A,B$:

(i) 

$A⊢B$;

(ii) 

$⊢A\wedge B\equiv A$;

(iii) 

$⊢A\vee B\equiv B$.

Proof. 

(i) to (ii): From the assumption $A⊢B$ and (R1) $A⊢A$, we have $A⊢A\wedge B$ using (R10). $A\wedge B⊢A$ is obvious. Thus, $⊢A\wedge B\equiv A$.

(ii) to (i): By the definition of $⊢A\wedge B\equiv A$, we have $A⊢A\wedge B$. And from (R8) $A\wedge B⊢B$, and using (R2), we have $A⊢B$.

(i) to (iii): From the assumption $A⊢B$ and (R1) $B⊢B$, we have $A\vee B⊢B$ using (R13). $B⊢A\vee B$ is obvious. Thus, $⊢A\vee B\equiv B$.

(iii) to (i): By the definition of $⊢A\vee B\equiv B$, we have $A\vee B⊢B$. And from (R11) $A⊢A\vee B$, and using (R2), we have $A⊢B$. □

Definition 9.

Putting

$$\begin{array}{c}\hfill A\approx Biff⊢A\equiv B,A,B\in \mathcal{F}.\end{array}$$

From (R35), (R36), and (R37), we know that ≈ is an equivalence on $\mathcal{F}$. Let us denote an equivalence class of A by $\left[A\right]$ and set $\overline{L}=\left\{\left[A\right]\right|A\in \mathcal{F}\}$. Finally, we define

$$\begin{array}{ccc}\hfill 0& =\left[\overline{0}\right]\hfill & \\ \hfill 1& =\left[\overline{1}\right]\hfill & \\ \hfill \left[A\right]\wedge \left[B\right]& =[A\wedge B]\hfill & \\ \hfill \left[A\right]\vee \left[B\right]& =[A\vee B]\hfill & \\ \hfill \left[A\right]\otimes \left[B\right]& =[A\&B]\hfill & \\ \hfill \left[A\right]\to \left[B\right]& =[A\Rightarrow B].\hfill \end{array}$$

Lemma 5.

The algebra $\overline{\mathcal{S}}=<\overline{L},\wedge ,\vee ,\otimes ,\to ,0,1>$ is an SOL-algebra.

Proof. 

Note that we have

$$\begin{array}{ccc}\hfill & \left[A\right]\le \left[B\right]\mathrm{iff}\left[A\right]\wedge \left[B\right]=\left[A\right]\mathrm{iff}\left[A\right]\vee \left[B\right]=\left[B\right]\hfill & \\ \hfill & \mathrm{iff}A⊢B\mathrm{iff}⊢A\wedge B\equiv A\mathrm{iff}⊢A\vee B\equiv B\hfill \end{array}$$

For the lattice properties of $<\overline{L},\wedge ,\vee ,0,1>$, see (R46)–(R51). (R14) and (R16) show that 0 and 1 are the greatest element and the least element with respect to ≤.

For (SO2), see (R52)–(R54).

(SO3) follows from (R6) and (R7). □

Corollary 1.

If $⊢B$, then $\vDash B$.

Theorem 11.

(Completeness) The following is equivalent for every formula $A,B$:

(i) 

$A⊢B$;

(ii) 

$A\vDash B$, i.e., $e\left(A\right)\le e\left(B\right)$, for every SOL-algebra $\mathcal{S}$ and a truth evaluation $e:\mathcal{F}\to L$.

Proof. 

The implication of (i) to (ii) is soundness.

(ii) to (i): By Lemma 3, the algebra $\overline{\mathcal{S}}$ of the equivalence classes of the formulas is an SOL-algebra. Thus, if (ii) holds, then it holds also for $e:\mathcal{F}\to \overline{L}$. If $e\left(A\right)\le e\left(B\right)$, then it means that $\left[A\right]\le \left[B\right]$, and so, $A⊢B$. □

Corollary 2.

The following is equivalent for every formula A:

(i) 

$⊢A$;

(ii) 

$\vDash A$, i.e., $e\left(A\right)=1$, for every SOL-algebra $\mathcal{S}$ and a truth evaluation $e:\mathcal{F}\to L$.

5. Conclusions

In this paper, we introduced the concept of an SOL-algebra based on the ideas of semi-overlap functions and their residua. An essential distinction between SOL-algebras and residuated lattices is the identity, which is not required in the former. Hence, the ordering property, i.e., $u\le v$ iff $u\Rightarrow v=1$, is dropped. To overcome this, we adopt Goldblatt’s idea of binary logic [23] in which the order is given between formulas, not from the property of implication. We developed an SOL logic that has no axioms but a set of rules for SOL-algebras and proved its completeness.

For the future, we plan to investigate the extensions of SOL logic by adding new axioms. Also, some applications of the developed system will be explored. Moreover, this logic system will be used to provide a logical framework for fuzzy reasoning based on semi-overlapping functions.