1 Introduction and terminology

A residuated lattice is an algebra \({\mathbf {A}}=(A,\wedge ,\vee ,\cdot ,{\backslash },{/}, 1)\) where \((A,\wedge ,\vee )\) is a lattice, \((A,\cdot ,1)\) is a monoid and \({\backslash },/\) are the left and right residuals of \(\cdot \), i.e., \(xy\le z\iff y\le x{\backslash }z\iff x\le z/y\) for all \(x,y,z\in A\).

A residuated lattice is commutative if it satisfies the identity \(xy=yx\), or equivalently \(x {\backslash }y = y {/}x\). It is called integral if it satisfies \(x \le 1\). A Brouwerian algebra is a residuated lattice where multiplication and meet coincide: \(xy=x\wedge y\). Using a slightly modified signature, it is an algebra \({\mathbf {A}}=(A,\wedge ,\vee ,\cdot , \rightarrow , \top )\) that is a lattice with top \(\top \) such that for all \(x,y,z\in A\)

$$\begin{aligned} x\wedge y\le z\iff y\le x\rightarrow z. \end{aligned}$$

It follows that it is commutative, integral and distributive. Heyting algebras are defined as bounded Brouwerian algebras expanded with a constant \(\bot \) denoting the least element.

A generalized bunched implication algebra (or GBI-algebra) is an algebra

$$\begin{aligned} {\mathbf {A}}=(A,\wedge ,\vee ,\rightarrow ,\top ,\cdot ,{\backslash },/,1) \end{aligned}$$

such that \((A,\wedge ,\vee ,\cdot ,{\backslash },{/}, 1)\) is a residuated lattice and \((A,\wedge ,\vee ,\cdot ,\mathbin {\rightarrow }, \top )\) is a Brouwerian algebra. Alternatively one may also call these algebras residuated Brouwerian algebras. Bounded GBI-algebras are expansions of GBI-algebras with an additional constant \(\bot \) which is defined to be the bottom element. Hence GBI-algebras have Brouwerian algebra reducts, while bounded GBI-algebras have Heyting algebra reducts, so these algebras are also referred to as residuated Heyting algebras. Residuated operations always distribute over lattice joins, hence Heyting algebras, Brouwerian algebras and (bounded) GBI-algebras have distributive lattice reducts. The intuitionistic negation is defined by \(\lnot x=x\rightarrow \bot \). A bunched implication algebra (or BI-algebra) is a commutative bounded GBI-algebra. These algebras are the algebraic semantics of bunched implication logic which is part of separation logic, a programming logic for modeling mutable data structures and concurrent processes [19, 20]. Heyting algebras are (term equivalent to) the subvariety of bounded BI-algebras that satisfy \(x\wedge y=xy\) (or equivalently \(x\rightarrow y=x{\backslash }y=y{/}x\)). A recent publication [4] on MV-algebras expanded with a Gödel algebra implication considers another subvariety of bounded BI-algebras.

Well known examples of (noncommutative) bounded GBI-algebras come from algebras of binary relations. Let \({\mathcal {R}}\) be a collection of binary relations on a set X such that \({\mathcal {R}}\) is closed under \(\cap ,\cup ,\rightarrow ,;,\backslash ,/\) and contains a largest relation \(\top \), the empty relation \(\emptyset \), as well as a relation E such that \(E\circ R=R\circ E=R\) for all \(R\in {\mathcal {R}}\). Here the operation \(\rightarrow \) is defined by \(R\rightarrow S=R^c\cup S\) (where \(^c\) is complementation with respect to \(\top \)), relation composition is written ;  and \(\backslash ,/\) are defined by the usual expressions for residuals on binary relations: \(R\backslash S=(R^{\smallsmile }; S^c)^c\) and \(R/S=(R^c; S^{\smallsmile })^c\), where \(^{\smallsmile }\) denotes the converse operation \(R^\smallsmile =\{(x,y):(y,x)\in R\}\). The algebra \(({\mathcal {R}},\cap ,\cup ,\rightarrow ,\top ,\emptyset ,\cdot ,\backslash ,/, E)\) is a bounded GBI-algebra and, in fact, (term equivalent to) a representable relation algebra.

Originally Tarski [21] and Jónsson and Tarski [16] defined the variety \(\mathsf {RA}\) of (abstract) relation algebras as Boolean algebras \((A,\wedge ,\vee ,\lnot ,\top ,\bot )\) with an associative binary operator \(\cdot \) (i.e., distributes over \(\vee \) in each argument) and a unary operator \(^\smallsmile \) such that \(\cdot \) has a unit element 1, \(x^{\smallsmile \smallsmile }=x\), \((xy)^\smallsmile =y^\smallsmile x^\smallsmile \) and \(x^\smallsmile \cdot \lnot (xy)\le \lnot y\). Alternatively, relation algebras are of the form \((A,\wedge ,\vee , \lnot ,\top ,\bot ,\cdot ,^\smallsmile ,1)\) where \((A,\wedge ,\vee ,\lnot ,\top ,\bot )\) is a Boolean algebra, \((A,\cdot , 1)\) is a monoid and for all \(x,y,z\in A\)

$$\begin{aligned} xy\wedge z=\bot \iff (z\cdot y^\smallsmile )\wedge x=\bot \iff (x^\smallsmile \cdot z)\wedge y=\bot . \end{aligned}$$

In the above example of algebras of binary relations, \(R^c=R\rightarrow \emptyset =\lnot R\) and \(R^\smallsmile =\lnot (R{\backslash }\lnot E)\). Conversely, given the abstract relation algebra signature \(\wedge ,\vee ,\lnot ,\top ,\bot , \cdot ,1,^\smallsmile \) the terms for the GBI-signature are defined as in the representable case: \(x\rightarrow y=\lnot x\vee y\) and \(x{\backslash }y=\lnot (x^\smallsmile \cdot \lnot y)\), \(x{/}y=\lnot (\lnot x\cdot y^\smallsmile )\). Again it is easy to check that every (abstract) relation algebra is a bounded GBI-algebra. However relation algebras are a proper subvariety since they have Boolean algebra reducts and satisfy additional identities (see Lemma 1.1).

In relation algebras the composition of complementation and converse behaves like an involution for the residuated lattice reduct. More specifically, we consider the context of pointed residuated lattices (also known as FL-algebras), which are expansions of residuated lattices by an arbitrary negation constant 0 and by the linear negation terms \({\sim }x=x{\backslash }0\) and \({-}x=0{/}x\). In this signature we consider the identities \({\sim }{-}x=x= {-}{\sim }x\) (involutivity) and \({\sim }x={-}x\) (cyclicity), defining the varieties \(\mathsf {InFL}\) of involutive FL-algebras and \(\mathsf {CyInFL}\) of cyclic involutive FL-algebras [10]. The importance of involution stems from the fact that in \(\mathsf {InFL}\) the residuals are expressible in terms of multiplication \(\cdot \) and the linear negations: \(x{\backslash }y={\sim }(-y\cdot x)={\sim }x+y\) and \(x/y=-(y\cdot {\sim }x)=x+-y\) hold in \(\mathsf {InFL}\), where \(x+y={\sim }((-y)(-x))=-(({\sim }y)({\sim }x))\) is the dual of multiplication with respect to the linear negations. Involutive FL-algebras can be defined in the signature \({\wedge , \vee , \cdot , {\backslash }, {/}, 1, 0}\), but also in the signature \({\wedge , \vee , \cdot , {\sim }, {-}, 1, 0}\), or even in \({\wedge , \cdot , {\sim }, {-}, 1}\).

In relation algebras \({\sim }\) is definable as complement-converse since \({\sim }x=x{\backslash }0=\lnot (x^\smallsmile \cdot \lnot 0)=\lnot (x^\smallsmile \cdot 1)=\lnot (x^\smallsmile )\). Since converse and complement commute in relation algebras, it follows that \({\sim }{\sim }x=x\) and applying \({-}\) on both sides gives cyclicity. Therefore all relation algebras have reducts in \(\mathsf {CyInFL}\), but the situation is even better explained in the context of pointed GBI-algebras, as then we can capture the full signature of relation algebras.

We denote by \(\mathsf {InGBI}\) the variety of involutive GBI-algebras. Since \(\top \) is the greatest element in a GBI-algebra, in the involutive case it is easy to see that \({\sim }\top = {-}\top \) and that this is a least element, denoted by \(\bot \). In other words involutive GBI-algebras are automatically bounded, hence they have Heyting algebra reducts. Furthermore, they admit a dual Heyting algebra structure as well, where the join operation has a dual residual:

$$\begin{aligned} z \le x \vee y \Leftrightarrow {\sim }(({-}x) \mathbin {\rightarrow }({-}z)) \le y. \end{aligned}$$

Therefore involutive GBI-algebras have bi-Heyting algebra reducts. Relation algebras are precisely cyclic involutive GBI-algebras that satisfy a few more identities as is shown in the lemma below. Among other things in relation algebras the elements 1 and 0 are complements.

Lemma 1.1

Relation algebras are term equivalent to cyclic involutive GBI-algebras that satisfy \(\lnot \lnot x=x\), \({\sim }{\lnot }x={\lnot }{\sim }x\) and \({\lnot }{\sim }(xy)={\lnot }{\sim }y\cdot {\lnot }{\sim }x\) (where \(\lnot x=x\rightarrow \bot \)). The term-equivalence is given by \(x^\smallsmile =\lnot {\sim }x\) and \({\sim }x=\lnot (x^\smallsmile )\).

Proof

Let \(\mathbf{A}=(A,\wedge ,\vee ,\lnot ,\bot ,\top ,\cdot ,^\smallsmile ,1)\) be a relation algebra. It is well known that \(\mathbf{A}\) is a residuated Boolean algebra [10, 18], hence (term-equivalent to) a GBI-algebra with \(x\rightarrow y=\lnot x\vee y\), \(x{\backslash }y=\lnot (x^\smallsmile \cdot \lnot y)\) and \(x{/}y=\lnot (\lnot x\cdot y^\smallsmile )\). The identity \(\lnot \lnot x=x\) holds since \(x\rightarrow \bot \) is complementation in a Boolean algebra. The involutive constant is \(0=\lnot 1\), hence cyclicity holds: \(x{\backslash }0=\lnot (x^\smallsmile \cdot 1)=\lnot (x^\smallsmile )=\lnot (1\cdot x^\smallsmile )=0{/}x\). Defining \({\sim }x=\lnot (x^\smallsmile )\) and recalling that \(\lnot ,^\smallsmile \) commute in relation algebras, we obtain \({\sim }{\sim }x=x\) and \(x^\smallsmile =\lnot {\sim }x\), whence the second and third identity also hold.

Conversely, assume \(\mathbf{A}=(A,\wedge ,\vee ,\rightarrow ,\bot ,\top ,\cdot ,{\sim },1)\) is a cyclic involutive GBI-algebra that satisfies the three identities. Then \((A,\cdot ,1)\) is a monoid, \((A,\wedge ,\vee ,\rightarrow ,\bot ,\top )\) is a Heyting algebra and the identity \(\lnot \lnot x=x\) implies it is a Boolean algebra. Defining \(x^\smallsmile =\lnot {\sim }x\), it suffices to prove that \(xy\wedge z=\bot \iff (z\cdot y^\smallsmile )\wedge x=\bot \iff (x^\smallsmile \cdot z)\wedge y=\bot \) then \((A,\wedge ,\vee ,\lnot ,\bot ,\top ,\cdot ,^\smallsmile ,1)\) is a relation algebra. Using complementation and residuation we have \(xy\wedge z=\bot \iff xy\le \lnot z\iff x\le \lnot z/y\iff \lnot (\lnot z/y)\le \lnot x \iff \lnot (\lnot z/y)\wedge x=\bot \). Using cyclic involution and the last two identities, we get \(\lnot (\lnot z/y)=\lnot {\sim }(y\cdot {\sim }\lnot z)=z\cdot \lnot {\sim }y=z\cdot y^\smallsmile \), proving the first equivalence, and the second one follows similarly. \(\square \)

Skew relation algebras [7] are defined as Boolean InFL\('\)-algebras (where \(x'=\lnot x\)), or equivalently as involutive GBI-algebras that have a Boolean reduct (i.e., satisfy \(\lnot \lnot x=x\)). In [7] it is proved that skew relation algebras that satisfy \({\lnot }{\sim }(xy)={\lnot }{\sim }y\cdot {\lnot }{\sim }x\) are relation algebras. This shows that cyclicity and \({\sim }{\lnot }x={\lnot }{\sim }x\) are not needed in the preceding lemma.

Examples of non-Boolean involutive algebras of concrete binary relations are obtained as follows: let \({\mathcal {R}}\) be a collection of binary relations on some set X that are closed under \(\cap ,\cup ,\rightarrow ,;,{\sim }\) (where \({\sim }\) is complement-converse) and contain a biggest relation \(\top \) as well as a relation E that contains the identity relation on X such that \(E;R=R=R;E\) for all \(R\in {\mathcal {R}}\). Then \({\mathcal {R}}\) with the above operations is a cyclic involutive GBI-algebra. Such algebras are called representable since they are based on binary relations. Note that E is a preorder since it is reflexive and \(E;E=E\). In addition every \(R\in {\mathcal {R}}\) satisfies \(E;R;E\subseteq R\), and relations with this property are called weakening relations with respect to the preorder E: if \(x'Ex\), xRy and \(yEy'\), the weaker condition \(x'Ey'\) also holds. We will be investigating such algebras of weakening relations in Section 6.

This paper describes the algebraic structure of GBI-algebras and involutive bounded GBI-algebras, in a way that is inspired by and connects to relation algebras. Weakening relations provide an interesting model of cyclic involutive GBI-algebras, as well as a generalization of representable relation algebras. We describe a general construction of a double-division conucleus and show that when applied to algebras of relations it yields algebras of weakening relations. Several constructions on relation algebras are examined from this point of view and turn out to behave well in this non-classical setting. It should also be noted that the varieties of (cyclic) involutive residuated lattices and distributive residuated lattices have decidable equational theories [8, 9] while this is not the case for relation algebras.

From the point of view of relation algebras, bounded GBI-algebras are an interesting class of Heyting algebras with operators, positioned between Boolean algebras with operators and lattices with operators. From the perspective of algebraic logic, Heyting algebras with operators provide the algebraic semantics for intuitionistic polymodal logic.

2 Congruences in relation algebras and residuated lattices

We begin with a brief review of congruence ideals in relation algebras [17]. Since they have Boolean algebra reducts, a congruence \(\theta \) on a relation algebra \({\mathbf {A}}\) is determined by the \(\bot \)-congruence class \(I=[\bot ]_{\theta }\). Such a set I is called a congruence ideal, and is always a Boolean algebra ideal. Moreover the congruence relation can be recovered from a congruence ideal: \(\theta =\{(x,y):x\oplus y\in I\}\) where \(\oplus \) is the symmetric difference \(x\oplus y=(x\wedge \lnot y)\vee (\lnot x\wedge y)\). In a similar way congruence filters are defined as the congruence classes of \(\top \).

Theorem 2.1

([17]). An ideal I of a relation algebra is a congruence ideal if and only if for all \(x\in I\) we have \(\top x\top \in I\).

In the forward direction, observe that \(\top x\top \ \theta \ \top \bot \top =\bot \) since \(\bot x=x\bot =\bot \) in any residuated lattice, hence also in any relation algebra. Therefore any congruence ideal I has the property that \(x\in I\) implies \(\top x\top \in I\). Conversely, let I be an ideal with the property that \(x\in I\) implies \(\top x\top \in I\). To conclude that I is a congruence ideal, it suffices to show that \(x\oplus y\in I\) implies \(x^\smallsmile \oplus y^\smallsmile , xz\oplus yz, zx\oplus zy\in I\). Since \(x^{\smallsmile }\le x^{\smallsmile }\cdot x\cdot x^{\smallsmile }\le \top x\top \), it follows that I is closed under converse. Therefore \(x\oplus y\in I\) implies \((x\oplus y)^{\smallsmile }=x^{\smallsmile }\oplus y^{\smallsmile }\in I\), which shows that \(x\theta y\) implies \(x^{\smallsmile }\theta y^{\smallsmile }\). Moreover, if \(x\oplus y\in I\) then \(x\wedge \lnot y\in I\), hence

$$\begin{aligned} xz\wedge \lnot (yz)&=(x\wedge (y\vee \lnot y))z\wedge \lnot (yz)\\&=((x\wedge y)z\vee (x\wedge \lnot y)z)\wedge \lnot (yz)\\&\le (yz\wedge \lnot (yz))\vee ((x\wedge \lnot y)z\wedge \lnot (yz))\\&\le \bot \vee \top (x\wedge \lnot y)\top \wedge \lnot (yz)\\&\le \top (x\wedge \lnot y)\top \in I. \end{aligned}$$

By the same argument \(\lnot (xz)\wedge yz\in I\) follows from \(\lnot x\wedge y\in I\), so we conclude that \(xz\oplus yz\in I\). The proof for \(zx\oplus zy\in I\) is similar.

We will be working with congruence filters instead of congruence ideals, due to the asymmetry of (non-involutive) GBI-algebras. The following result is obtained by taking the dual of the term \(\top x \top \), which is \(\bot + x + \bot = \top {\backslash }x {/}\top \). We will generalize this result in Theorem 4.1.

Corollary 2.2

A filter F of a relation algebra is a congruence filter if and only if for all \(x\in F\) we have \(\top {\backslash }x {/}\top \in F\).

Residuated lattices are considerably more general than relation algebras, so characterizing their congruences requires a slightly different strategy. A congruence \(\theta \) on a residuated lattice \({\mathbf {A}}\) is determined by \([1]_{\theta }\) since \(x\theta y\iff x{\backslash }y\wedge y{\backslash }x\wedge 1\in [1]_{\theta }\), so \({\mathbf {A}}\) is 1-regular. The terms \(\lambda _{a}(x)=(a{\backslash }xa)\wedge 1\) and \(\rho _{a}(x)=(ax/a)\wedge 1\) are the left and right conjugates. A third term \(\kappa _{a}(x,y)=(a\vee x)\wedge y\) implies convexity for sublattices closed under it. Together the terms \(\kappa _{a},\lambda _{a},\rho _{a}\) form a set of Gumm-Ursini ideal terms [11] for residuated lattices. A convex normal subalgebra is a subset H that is closed under \(\wedge ,\vee ,\cdot ,1,{\backslash },/,\kappa _{a},\lambda _{a},\rho _{a}\) for all \(a\in A\).

Theorem 2.3

([2]) For a residuated lattice \({\mathbf {A}}\), a subset N of A is the 1-congruence class of some \(\theta \in Con (\mathbf{A})\) if and only if N is a convex normal subalgebra. Moreover, Con\(({\mathbf {A}})\) is isomorphic to the lattice of convex normal subalgebras via the bijection \(\theta \mapsto [1]_{\theta }\) and \(N\mapsto \{(x,y):x{\backslash }y\wedge y{\backslash }x\wedge 1\in N\}\).

Since Brouwerian algebras and Heyting algebras are residuated lattices (with \(xy=x\wedge y\) and a \(\bot \) element in the latter case) the preceding result specializes to these algebras. In particular, a congruence \(\theta \) on a Brouwerian algebra is determined by the lattice filter \(F=[\top ]_\theta \), which ends up being exactly the characterization of convex normal subalgebras in this residuated lattice. Conversely, given a lattice filter F, the relation \(\theta _F=\{(x,y):(x\rightarrow y)\wedge (y\rightarrow x)\in F\}\) is a congruence on the Brouwerian algebra. The term \((x\rightarrow y)\wedge (y\rightarrow x)\) is usually abbreviated \(x\leftrightarrow y\).

3 Congruences on GBI-algebras

We now consider the case of congruences on GBI-algebras. Note that the results in this section are new even for BI-algebras. Commutativity of \(\cdot \) makes the conjugates \(\lambda _a,\rho _a\) superfluous but it does not substantially simplify the interaction of \(\wedge ,\rightarrow \) with \(\cdot ,{\backslash },{/}\).

Since GBI-algebras are residuated lattices in two ways, congruences are determined by either their congruence class of \(\top \) or their congruence class of 1. We first give a characterization of the congruence classes of \(\top \).

3.1 Congruences via their classes of \(\top \)

For a GBI-algebra \(\mathbf{A}\) we would like to find conditions on a filter F such that \(\theta _F =\{(x,y):x\leftrightarrow y\in F\}\) is a congruence on \(\mathbf{A}\). Properties of \(\leftrightarrow \) ensure that \(\theta _F\) is an equivalence relation. It remains to show that \(a\ \theta _F\ c\) implies \(a*b\ \theta _F\ c*b\) and \(b*a\ \theta _F\ b*c\) for all \(a,b,c\in A\) and \({*}\in \{\cdot ,{\backslash },{/},\mathbin {\rightarrow }\}\). That \(\theta _F\) is compatible with \(\mathbin {\rightarrow }\) is easy to see and also follows from the characterization of congruences in Brouwerian algebras by lattice filters. So given \(a\rightarrow c\in F\) we want to conclude that

$$\begin{aligned} ab\rightarrow cb, \ ba\rightarrow bc, \ c{\backslash }b\rightarrow a{\backslash }b, \ b{\backslash }a\rightarrow b{\backslash }c, \ a/b\rightarrow c/b, \ b/c\rightarrow b/a\in F \end{aligned}$$

for all \(b\in A\).

We will consider the first condition: \(a\rightarrow c\in F\) implies \( ab\rightarrow cb \in F\). By the upward closure of F, \(a\rightarrow c\in F\) is equivalent to the existence of an \(x \in F\) such that \(x\le a\rightarrow c\), namely \(a \wedge x\le c\). Likewise, \(ab\rightarrow cb \in F\) is equivalent to the existence of \(y \in F\) such that \(y\le ab\rightarrow cb\). If F is closed under the term

$$\begin{aligned} u_{a,b}(x)=ab\rightarrow (x\wedge a)b \end{aligned}$$

then we can take \(y=u_{a,b}(x)\) and it follows that \(y=ab\rightarrow (x\wedge a)b\le ab\rightarrow cb\), hence \(ab\rightarrow cb\in F\).

Conversely, if F is a congruence filter, say \(F=[\top ]_\theta \) then it is indeed the case that F is closed under the term \(u_{a,b}(x)\) for all \(x\in F\) and all \(a,b\in A\): let \(x\in F\), then \(x\theta \top \), hence

$$\begin{aligned} u_{a,b}(x)\ \theta \ u_{a,b}(\top )= ab\rightarrow (\top \wedge a)b=ab\rightarrow ab=\top \end{aligned}$$

and we conclude that \(u_{a,b}(x)\in F\). Consequently, the first condition is equivalent to closure of F under the term \(u_{a,b}(x)=ab\rightarrow (x\wedge a)b\). Similarly, the second term \(ba\rightarrow bc\) will be in F if and only if for all \(a,b\in A\) and all \(x\in F\) we have \(u'_{a,b}(x)=ba\rightarrow b(a\wedge x)\in F\).

Furthermore, closure of F under \(u_{a,b}\) and \(u'_{a,b}\) is equivalent to the conditions that for all \(a,b\in A\),

$$\begin{aligned} U_{a,b}&{:}\ \forall x \in F,\ \exists y \in F,\ y\wedge ab \le (x \wedge a)b\\ U'_{a,b}&{:}\ \forall x\in F,\ \exists y \in F,\ ba \wedge y \le b(a \wedge x) \end{aligned}$$

since F is upward closed. We also define the terms

$$\begin{aligned} v_{a,b}(x)=a\mathbin {\rightarrow }(x\wedge ab) {/}b&,&v'_{a,b}(x)=a\mathbin {\rightarrow }b {\backslash }(ba\wedge x)&,&w(x)=\top {\backslash }x/\top \end{aligned}$$

and their corresponding conditions

$$\begin{aligned} V_{a,b}&{:}\ \forall x \in F,\ \exists y \in F,\ (y \wedge a)b \le x\wedge ab\\ V'_{a,b}&{:}\ \forall x \in F,\ \exists y \in F,\ b(a \wedge y) \le ba \wedge x\\ W&{:}\ \forall x \in F,\ \exists y \in F,\ \top y \top \le x \end{aligned}$$

The full characterization of congruence filters for GBI-algebras is as follows.

Theorem 3.1

A lattice filter F of a GBI-algebra \(\mathbf{A}\) is a congruence filter if and only if for all \(a,b\in A\) the set F is closed under

$$\begin{aligned} u_{a,b},u'_{a,b},w \end{aligned}$$

or equivalently under

$$\begin{aligned} u_{a,b},u'_{a,b},v_{a,b}, v'_{a,b}. \end{aligned}$$

Also, closure under each term corresponds to the validity of the corresponding condition for all \(a,b\in A\).

Proof

To see that congruence filters of GBI-algebras satisfy the closure condition, it suffices to check that for \(x=\top \) each of the terms evaluates to \(\top \).

For the reverse implication, we have already observed that if F is closed under \(u_{a,b}(x),u'_{a,b}(x)\) then \(\theta _F=\{(a,c): a\leftrightarrow c\in F\}\) is preserved by the monoid operation.

Let \(a\rightarrow c\in F\). To see that \(a/b\rightarrow c/b\in F\) and \(b{\backslash }a\rightarrow b{\backslash }c\in F\) holds, one uses the terms \(a/b\rightarrow (a\wedge x)/b\) and \(b{\backslash }a\rightarrow b{\backslash }(a\wedge x)\). We will show that these terms can be replaced with \(v_{a,b}(x)\) and \(v'_{a,b}(x)\) or alternatively with the simpler term w(x). For the first of these claims, note that closure under the term \(b{\backslash }a\rightarrow b{\backslash }(a\wedge x)\) is equivalent to closure under \(v'_{a,b}(x) = a \mathbin {\rightarrow }b {\backslash }(ba \wedge x)\). The forward direction is obtained by setting \(a:= ba\) and using that \(a \le b{\backslash }ba\); the backward direction is obtained by setting \(a:=b {\backslash }a\) and using that \(b(b {\backslash }a) \le a\). Likewise, we obtain closure under \(v_{a,b}(x)\).

Now assume F is closed under w, and let \(x=a\rightarrow c\in F\), hence \(a\wedge x\le c\). Now

$$\begin{aligned} w(x)=\top {\backslash }x/\top \le x/\top =\top \rightarrow x/\top \le a/b\rightarrow x/b \end{aligned}$$

since \(\top {\backslash }x\le 1{\backslash }x=x\), \(a/b\le \top \) and \(b\le \top \). Moreover,

$$\begin{aligned} a/b\rightarrow x/b&=\top \wedge (a/b\rightarrow x/b)\\&=(a/b\rightarrow a/b)\wedge (a/b\rightarrow x/b)\\&=a/b\rightarrow ((a/b)\wedge (x/b))\\&=a/b\rightarrow (a\wedge x)/b \end{aligned}$$

so closure of F under w(x) implies closure of F under \(a/b\rightarrow (a\wedge x)/b\). Similarly \(w(x)\le b{\backslash }a\rightarrow b{\backslash }(a\wedge x)\).

Next, we show that closure under \(u, u', v, v'\) implies that the following conditions hold for all \(a,b\in A\)

$$\begin{aligned} Q_{a,b}&{:}\ \forall x \in F,\ \exists y \in F,\ a {/}(b \wedge x) \le y \mathbin {\rightarrow }(a {/}b)\\ Q'_{a,b}&{:}\ \forall x \in F,\ \exists y \in F,\ (x \wedge b) {\backslash }a \le y \mathbin {\rightarrow }(b {\backslash }a) \end{aligned}$$

We show that \(Q'_{a,b}\) for all \(a, b \in A\), follows from \(U_{a,b}, V'_{a,b}\) for all \(a,b \in A\). In particular, we will show that if \(x \in F\) and \(a,b \in A\), then there exists \(y \in F\) such that \((x \wedge b) {\backslash }a \le y \mathbin {\rightarrow }(b {\backslash }a)\) namely \(y \wedge (x \wedge b) {\backslash }a \le b {\backslash }a\). We first note that by \(V'_{1,b}\) there is \(z \in F\) such that \(b(1 \wedge z)\le b1 \wedge x\). Also, by \(U_{1, (1 \wedge z) {\backslash }(b {\backslash }a)}\) applied to z, there is \(y \in F\) such that \(y\wedge 1[(1 \wedge z) {\backslash }(b {\backslash }a)] \le (1 \wedge z)[(1 \wedge z) {\backslash }(b {\backslash }a)]\). Consequently, combining all of the above we have

$$\begin{aligned} y\wedge [(x \wedge b) {\backslash }a]\le & {} y\wedge [b(1 \wedge z) {\backslash }a] = y\wedge [(1\wedge z) {\backslash }(b {\backslash }a)]\\\le & {} (1\wedge z)[(1\wedge z) {\backslash }(b{\backslash }a)]\le b {\backslash }a \end{aligned}$$

which yields the result. Condition \(Q_{a,b}\) follows in a similar way.

Now suppose F satisfies the conditions \(Q_{a,b}\), \(Q'_{a,b}\) for all \(a,b\in A\). Assume that \(x=a\rightarrow c\in F\) and let \(b\in A\). From \(Q_{b,a}\) we get \(y\in F\) such that \(b {/}(a \wedge x) \le y \mathbin {\rightarrow }(b {/}a)\), or equivalently \(y\le b {/}(a \wedge x) \mathbin {\rightarrow }(b {/}a)\). Hence

$$\begin{aligned} a\wedge x\le c\implies b/c\le b/(a\wedge x)\implies y \le b/c\rightarrow b/a. \end{aligned}$$

The argument for \(c{\backslash }b\rightarrow a{\backslash }b\) is similar. \(\square \)

In the above characterization, in contrast with Corollary 2.2 for relation algebras, the term w is not enough by itself, as can be seen by considering integral GBI-algebras, i.e., where \(\top =1\) since in this case \(w(x)=x\).

Corollary 3.2

For a GBI-algebra \({\mathbf {A}}\), \(Con ({\mathbf {A}})\) is isomorphic to the lattice of congruence filters via the bijection \(\theta \mapsto [\top ]_{\theta }\) and \(F\mapsto \{(x,y):x\leftrightarrow y\in F\}\).

The characterization of a congruence filter F can also be expressed by conditions similar to normality in groups. For a set X and a binary operation \(*\in \{\wedge ,\vee ,\cdot ,{\backslash },/,\rightarrow \}\), let \(X*a=\{x*a : x\in X\}\). Note that condition \(U_{a,b}\) states that for all \(x\in F\) there exists \(y\in F\) such that \(y\wedge ab\le (x\wedge a)b\). This can be rephrased by the condition \((F\wedge a)b\subseteq {\uparrow }(F\wedge ab)\). Similar calculations for the other terms give the following result.

Corollary 3.3

A lattice filter F in a GBI-algebra A is a congruence filter if and only if it satisfies the following conditions for all \(a,b\in A\),

$$\begin{aligned} {\uparrow }((F\wedge a)b)= {\uparrow }(F\wedge ab)={\uparrow }(a(b\wedge F)) \end{aligned}$$

or equivalently the conditions for all \(a,b\in A\),

$$\begin{aligned} (F\wedge a)b\subseteq {\uparrow }(F\wedge ab), \quad a(b\wedge F)\subseteq {\uparrow }(ab\wedge F)\ \text { and }\ F\subseteq {\uparrow }(\top F\top ). \end{aligned}$$

Given a GBI-algebra \(\mathbf{A}\), an element \(d \in A\) is called a filter element if there exists a congruence \(\theta \) on \(\mathbf{A}\) such that d is the smallest element of \([\top ]_\theta \), or equivalently the principal filter \({\uparrow } d\) is a congruence filter.

The next corollary follows by instantiating the conditions for \(F=\mathord {\uparrow }d\) according to Corollary 3.3; the easiest way to do that is to see that if we chose \(x=d\) in the conditions, then we can also choose \(y=d\).

Corollary 3.4

An element d is a filter element of a GBI-algebra if and only if for all \(a,b\in A\)

$$\begin{aligned} (d\wedge a)b = ab\wedge d= a(b\wedge d) \end{aligned}$$

or equivalently for all \(a,b\in A\)

$$\begin{aligned} d\wedge ab\le (d\wedge a)b,\quad ab\wedge d\le a(b\wedge d)\ \text { and }\ \top d\top =d. \end{aligned}$$

For a finite GBI-algebra, all congruence filters are principal, so the set of filter elements is in one-one correspondence with congruences of the algebra.

3.2 Congruences via their classes of 1

While it is more convenient to work with congruence filters in GBI-algebras than with congruence classes of 1, the latter approach is well known for residuated lattices, so we also extend it to GBI-algebras.

As mentioned before, a subset N of a residuated lattice \(\mathbf{A}\) is equal to \([1]_\theta \) for some congruence \(\theta \) if and only if it is a convex normal subalgebra of \(\mathbf{A}\), or equivalently, if it is a subalgebra of \(\mathbf{A}\) and it is closed under the terms, for all \(a\in A\),

$$\begin{aligned} \lambda _{a}(x)=(a{\backslash }xa)\wedge 1, \quad \rho _{a}(x)=(ax/a)\wedge 1, \quad \kappa _{a}(x,y)=(a\vee x)\wedge y. \end{aligned}$$

In [10] it is also shown that a subset M of a residuated lattice \(\mathbf{A}\) is equal to \([1]_\theta ^-\) for some congruence \(\theta \) if and only if it is a convex normal submonoid of \(\mathbf{A}^-\), or equivalently, if it is a submonoid of \(\mathbf{A}\) and it is closed under the terms, for all \(a\in A\),

$$\begin{aligned} \lambda _{a}(x)=(a{\backslash }xa)\wedge 1, \quad \rho _{a}(x)=(ax/a)\wedge 1, \quad \kappa _{a}(x,1)=(a\vee x)\wedge 1. \end{aligned}$$

The correspondence between convex normal subalgebras N and submonoids M of a residuated lattice is given by \(M=N^-\) and \(N=\{x: m \le x \le 1 {/}m\) for some \(m \in M\}\); here \(X^{-}=\{ x \in X : x \le 1\}\).

It is easy to see that M is a convex normal submonoid if and only if it is a convex submonoid and it satisfies the conditions of normality

$$\begin{aligned} N_a: \forall x \in M, \exists y \in M, ya \le ax \text { and } \forall x \in M, \exists y \in M, ay \le xa \end{aligned}$$

or equivalently that \(\mathord {\uparrow }(Ma) = \mathord {\uparrow }(aM)\).

To extend the above to the setting of GBI-algebras, we consider the terms

$$\begin{aligned} r_{a,b}(x)=(a\rightarrow (ax\wedge b))/b\wedge 1,\quad s_{a,b}(x)=((a\rightarrow xb)/(a\rightarrow b))\wedge 1 \end{aligned}$$

and \(t_{a,b}(x)=((a\rightarrow b)/(xa\rightarrow b))\wedge 1\). For a convex normal submonoid M of \(\mathbf{A}^-\), we also consider the corresponding conditions

$$\begin{aligned} R_{a,b}&{:}\ \forall x \in M,\ \exists y \in M,\ a \wedge yb \le ax \wedge b,\\ S_{a,b}&{:}\ \forall x \in M,\ \exists y \in M,\ y(a \mathbin {\rightarrow }b) \le a \mathbin {\rightarrow }xb, \\ T_{a,b}&{:}\ \forall x \in M,\ \exists y \in M,\ xa \mathbin {\rightarrow }b \le y {\backslash }(a \mathbin {\rightarrow }b). \end{aligned}$$

Note that under the assumption of \(N_a\) for all \(a\in A\), the condition \(R_{a,b}\) is equivalent to

$$\begin{aligned} R'_{a,b}&{:}\ \forall x \in M,\ \exists y \in M,\ ay \wedge b \le a\wedge xb. \end{aligned}$$

Indeed, if \(x \in M\), and \(a,b \in A\), then by \(N_b\) there exists \(x' \in M\) such that \(bx' \le xb\). Also, \(R_{b,a}\) applied to \(x'\) yields an \(x'' \in M\) such that \(b \wedge x''a \le bx' \wedge a\). Finally, by \(N_a\) applying to \(x''\) we obtain a \(y \in M\) such that \(ay \le x''a\). Therefore, we have

$$\begin{aligned} ay \wedge b \le b \wedge x''a \le bx' \wedge a = a \wedge bx'\le a\wedge xb. \end{aligned}$$

Similarly, in the presence of normality, R follows from \(R'\).

Theorem 3.5

For a GBI-algebra \({\mathbf {A}}\), a subset N is equal to \([1]_\theta \) for some congruence \(\theta \) on \(\mathbf{A}\) if and only if N is a convex normal subalgebra of the residuated lattice reduct of \(\mathbf{A}\) that is closed under \(r_{a,b}\) for all \(a,b\in A\), or equivalently, under \(s_{a,b}\) and \(t_{a,b}\) for all \(a,b\in A\).

Proof

By Theorem 2.3, \(N=[1]_\theta \), so to check that N is closed under the terms \(s_{a,b}\) and \(t_{a,b}\) it suffices to check that \(s_{a,b}(1)=t_{a,b}(1)=1\). This is true since \(1\le y/y\) holds in any residuated lattice.

For the reverse implication, assume \(a\theta c\) and let \(d=c/a\wedge 1\). Then \(1=(a/a\wedge 1)\ \theta \ (c/a\wedge 1)\), hence \(d\in [1]_\theta =N\) from which we conclude that \(t_{a,b}(d)\in N\). Now

$$\begin{aligned} t_{a,b}(d)=((a\rightarrow b)/((c/a\wedge 1)a\rightarrow b)\wedge 1\le ((a\rightarrow b)/(c\rightarrow b)\wedge 1 \end{aligned}$$

since \((c/a\wedge 1)a\le (c/a)a\le c\) and the term \((c/a\wedge 1)a\) occurs in an order-preserving position. It follows that \((a\rightarrow b)/(c\rightarrow b)\wedge 1 \in N\), and the same calculation with ac interchanged shows that \((c\rightarrow b)/(a\rightarrow b) \wedge 1 \in N\), hence \((a\rightarrow b)\ \theta \ (c\rightarrow b)\).

Next assume \(b\theta c\) and let \(d=c/b\wedge 1\). Again we have \(x\in N\), hence \(s_{a,b}(d)\in N\). The calculation

$$\begin{aligned} s_{a,b}(d)=((a\rightarrow (c/b\wedge 1)b)/(a\rightarrow b)\wedge 1\le ((a\rightarrow c)/(a\rightarrow b)\wedge 1 \end{aligned}$$

and a similar with bc interchanged show that \((a\rightarrow b)\ \theta \ (a\rightarrow c)\).

We now observe that the term \(t_{a,b}(x)\) can be replaced by the term \(r_{a,b}(x)=(a\rightarrow (ax\wedge b))/b\wedge 1\), since \(r_{a,b}(1)=1\) and if \(x=b/a\wedge 1\) then

$$\begin{aligned} r_{a,b\rightarrow c}(b/a\wedge 1)= & {} (a\rightarrow ((b/a\wedge 1)x\wedge (b\rightarrow c)))/(b\rightarrow c)\wedge 1\\\le & {} (a\rightarrow c)/(b\rightarrow c)\wedge 1 \end{aligned}$$

and similarly for ab interchanged. Hence if N is closed under \(r_{a,b\rightarrow c}(x)\) then \(a\theta b\) implies \((a\rightarrow c)\ \theta \ (b\rightarrow c)\).

Finally we show that condition \(S_{a,b}\) follows from the rest. Let \(x \in N^-\) and \(a,b \in A\). By condition \(R'_{a,b}\) there exists \(z\in N^-\) such that \(az \wedge b\le a\wedge xb\). Also by \(R_{a,a\rightarrow b}\) there exists \(y\in N^-\) such that

$$\begin{aligned} a \wedge y(a \mathbin {\rightarrow }b)\le & {} az \wedge (a \mathbin {\rightarrow }b) \le (a \mathbin {\rightarrow }az) \wedge (a \mathbin {\rightarrow }b) \\= & {} a \mathbin {\rightarrow }(az \wedge b) \le a \mathbin {\rightarrow }(a \wedge xb)=(a \mathbin {\rightarrow }a) \wedge (a \mathbin {\rightarrow }xb)=a \mathbin {\rightarrow }xb \end{aligned}$$

so \(a\wedge a\wedge y(a \mathbin {\rightarrow }b) \le xb\) and hence \(y(a \mathbin {\rightarrow }b) \le a \mathbin {\rightarrow }xb\). \(\square \)

We define \(N\subseteq A\) to be a convex normal subalgebra of a GBI-algebra \({\mathbf {A}}\) if it satisfies the conditions of the above theorem. In other words normality in the setting of GBI-algebras requires one more condition than normality for residuated lattices.

Corollary 3.6

For a GBI-algebra \({\mathbf {A}}\), Con\(({\mathbf {A}})\) is isomorphic to the lattice of convex normal subalgebras of \(\mathbf{A}\) via the bijections

$$\begin{aligned} \theta \mapsto [1]_{\theta }\quad \text {and}\quad N\mapsto \{(x,y):x/ y\wedge y/ x\wedge 1\in N\}. \end{aligned}$$

Corollary 3.7

A subset N of a GBI-algebra \(\mathbf{A}\) is a convex normal subalgebra of \(\mathbf{A}\) if and only if it is a convex normal subalgebra of the residuated-lattice reduct of \(\mathbf{A}\) and for all \(a,b\in A\)

$$\begin{aligned} {\uparrow }(aN^-\wedge b)= {\uparrow }(a \wedge N^{-}b). \end{aligned}$$

It follows that the properties

$$\begin{aligned} aN\wedge b&\subseteq {\uparrow }(N^{-}b\wedge a)&a\rightarrow Nb&\subseteq {\uparrow }(N^{-}(a\rightarrow b))&Na \mathbin {\rightarrow }b \subseteq \mathord {\downarrow }(N^{-} {\backslash }(a \mathbin {\rightarrow }b)) \end{aligned}$$

also hold for all \(a,b\in A\).

Proof

This is a direct translation of the conditions R, \(R'\), S and T. \(\square \)

An element c in a residuated lattice \(\mathbf{A}\) is called a congruence element if it is the least element of a convex normal subalgebra of \(\mathbf{A}\). Recall that an element c is called central if \(ac=ca\) for all \(a\in A\). In Lemma 3.51 of [10] it is shown that c is a congruence element of a residuated lattice if and only if c is a central negative idempotent element. An element c of a GBI-algebra \(\mathbf{A}\) is called a congruence element of \(\mathbf{A}\) if it is the minimum of some convex normal subalgebra of \(\mathbf{A}\). Note that then c is a fortiori a congruence element of the residuated-lattice reduct of \(\mathbf{A}\).

Corollary 3.8

An element c is a congruence element of a GBI-algebra \(\mathbf{A}\) if and only if

\(xc=cx=x\wedge c\top \) for all \(x\in A\).

Moreover, a congruence element c satisfies \(c^2=c\le 1\), \(a\wedge cb=ac\wedge b\), \(c(a\rightarrow b)\le a\rightarrow cb\) and \(ca \mathbin {\rightarrow }b \le c {\backslash }(a \mathbin {\rightarrow }b)\) for all \(a,b\in A\).

Proof

For a congruence element c, the conditions \(c^2=c\le 1\), \(ac=ca\), \(a\wedge cb=ac\wedge b\), \(c(a\rightarrow b)\le a\rightarrow cb\) and \(ca \mathbin {\rightarrow }b \le c {\backslash }(a \mathbin {\rightarrow }b)\) follow easily by noting that if \(x=c\) in the conditions \(N, R, R', S, T\), then the choice \(y=c\) is necessary and sufficient. Taking \(a=x\) and \(b=\top \) gives \(x\wedge c\top =xc\wedge \top =xc\).

Conversely, if \(xc=cx=x\wedge c\top \) for all \(x\in A\) then \(c^2=c\wedge c\top =c\), \(c=c1=1\wedge c\top \le 1\) and \(a\wedge cb=a\wedge b\wedge c\top =a\wedge c\top \wedge b=ac\wedge b\). \(\square \)

3.3 Correspondence between congruences classes

The following result explains how we can move between the congruence class of 1 and the congruence class of \(\top \) for congruences on GBI-algebras. For notational convenience, we define \(\mathord {\uparrow }^- Y=\{x : y \le x \le 1\text { for some }y\in Y\}\).

Theorem 3.9

For GBI-algebras there is a one-one correspondence between congruence filters F and negative parts \(M=N^-\) of convex normal subalgebras N via the mutually inverse lattice isomorphisms

\(F \mapsto \mathord {\uparrow }^- (F \wedge 1)\) and \(M \mapsto \mathord {\uparrow }(M \top ) \quad [= \mathord {\uparrow }(N \top )]\).

Proof

Let F be a congruence filter of a GBI-algebra. Clearly all elements of \(\mathord {\uparrow }^-(F \wedge 1)\) are negative and the set is convex.

To show that \(\mathord {\uparrow }^-(F \wedge 1)\) is closed under multiplication, let \(x,y \in \mathord {\uparrow }^-(F \wedge 1)\). Then there exist \(d_1, d_2 \in F\), with \(d_1 \wedge 1 \le x\le 1\) and \(d_2 \wedge 1 \le y \le 1\), so if we show that \((1 \wedge d_1)(1 \wedge d_2) \in \mathord {\uparrow }^-(F \wedge 1)\), then we will also get \(xy \in \mathord {\uparrow }^-(F \wedge 1)\) by order preservation. With that goal in mind, note that by condition \(U'_{1, 1 \wedge d_1}\) there exists \(d'_2 \in F\) such that \((1 \wedge d_1)1 \wedge d'_2 \le (1 \wedge d_1)(1 \wedge d_2)\), hence

$$\begin{aligned} 1 \wedge d_1 \wedge d'_2 \le (1 \wedge d_1)1 \wedge d'_2 \le (1 \wedge d_1)(1 \wedge d_2) \le 1. \end{aligned}$$

Since F is closed under meet, we have that \( d_1 \wedge d'_2 \in F\), so \(1 \wedge d_1 \wedge d'_2 \in F \wedge 1\) and \((1 \wedge d_1)(1 \wedge d_2) \in \mathord {\uparrow }^-(F \wedge 1)\).

We now show normality of \(\mathord {\uparrow }^-(F \wedge 1)\). Let \(a \in A\) and \(d \in F\). Then by conditions \(U_{1,a}\) on d and \(V'_{1,a}\) on \(d'\) we get the existence of elements \(d', d'' \in F\), respectively, such that

$$\begin{aligned} a(1 \wedge d'') \le a\cdot 1 \wedge d' = d'\wedge 1 \cdot a\le (d\wedge 1)a \end{aligned}$$

where the existence of \(d''\) depends on \(d'\), so it makes sense to read the above line from right to left.

Now let \(a, b \in A\) and \(d \in F\). By conditions \(U'_{1,a}\) and \(V_{1,b}\) we have that there exist \(d', d'' \in F\) such that

$$\begin{aligned} a \wedge (d''\wedge 1)b \le a \wedge d'\wedge 1b = a1 \wedge d' \wedge b \le a(1 \wedge d) \wedge b. \end{aligned}$$

So, for all \(a,b \in A\) and \(x \in \mathord {\uparrow }^-(F \wedge 1)\), there exists \(y \in \mathord {\uparrow }^-(F \wedge 1)\) such that \(a \wedge yb \le ax \wedge b\). Thus we have established \(R_{a,b}\) for all \(a, b \in A\).

Conversely, let N be a convex normal subalgebra of \(\mathbf{A}\) and \(M=N^-\). We will show that \(\mathord {\uparrow }(M \top )= \mathord {\uparrow }(N \top )\) is a congruence filter. It is clear that it is upward closed. Also, that it is closed under meets follows from the fact that for \(c_1, c_2 \in M\) we have \(c_1 \wedge c_2 \in M\) and also \((c_1 \wedge c_2) \top \le c_1\top , c_2 \top \). So, \((c_1 \wedge c_2) \top \le c_1 \top \wedge c_2 \top \).

If \(x \in \mathord {\uparrow }(M \top )\) and \(a,b \in A\), then there is \(c \in M\) with \(c \top \le x\). By using (from right to left in the displayed calculation below) condition \(R'_{a, \top }\), \(N_b\) and \(R_{a, \top }\), there exist \(c', c'', c''' \in M\) such that

$$\begin{aligned} ab \wedge c'''\top \le abc'' \wedge \top =abc'' \le ac'b=(ac'\wedge \top )b \le (a \wedge c\top )b. \end{aligned}$$

So, there is \(y=c'''\top \in M\top \subseteq \mathord {\uparrow }(M \top )\) such that \(y\wedge ab \le (x \wedge a)b\), by order-preservation. This establishes condition \(U_{a,b}\); likewise we obtain \(U'_{a,b}\).

We will now prove condition \(V_{a,b}\), that is we will show that if \(x \in \mathord {\uparrow }(M \top )\) and \(a,b \in A\), there is \(y \in M\top \subseteq \mathord {\uparrow }(M \top )\) such that \((y \wedge a)b \le x\wedge ab\). There exists \(c \in M\) with \(c \top \le x\). By using (from right to left in the displayed calculation below) conditions \(R'\), N and R, we have that there exist \(c', c'', c''' \in M\) such that

$$\begin{aligned} (a \wedge c'''\top )b \le (ac'' \wedge \top )b=ac''b \le abc'=abc' \wedge \top \le ab \wedge c\top \end{aligned}$$

which yields \((c'''\top \wedge a)b \le c\top \wedge ab\) as required.

That the maps are order-preserving is clear. We will show that they are mutually inverse. To show that \(\mathord {\uparrow }[(\mathord {\uparrow }^-(F \wedge 1))\top ]=F\) note that by \(U_{1, \top }\), for \(d \in F\) there exists \(d' \in F\) such that \(d'=1 \top \wedge d' \le (1\wedge d)\top \). So \((F \wedge 1)\top \subseteq \mathord {\uparrow }F\) and by order-preservation of multiplication and the upward closure of F we get \(\mathord {\uparrow }[(\mathord {\uparrow }^-(F \wedge 1))\top ] \subseteq F\). For the reverse inclusion, we have that by \(V_{1, \top }\), for \(d \in F\) there exists \(d' \in F\) such that \( (d'\wedge 1)\top \le d\wedge 1 \top =d\). So \(F \subseteq \mathord {\uparrow }[(F \wedge 1)\top ] \subseteq \mathord {\uparrow }[(\mathord {\uparrow }^-(F \wedge 1))\top ]\).

For the other composition we show that \(\mathord {\uparrow }^- [(\mathord {\uparrow }M \top ) \wedge 1] = M\). We have that for all \(c \in M\), there exists \(c' \in M\) such that \(c'=1c' \wedge \top \le 1 \wedge c\top \), so \(M \top \wedge 1 \subseteq M\) and hence \(\mathord {\uparrow }^- [(\mathord {\uparrow }M \top ) \wedge 1] \subseteq M\). Also, we have that for all \(c \in M\), there exists \(c' \in M\) such that \(1 \wedge c'\top \le 1c \wedge \top =c\le 1\), so \(M \subseteq \mathord {\uparrow }^-(M \top \wedge 1) \subseteq \mathord {\uparrow }^- [(\mathord {\uparrow }M \top ) \wedge 1]\). \(\square \)

Corollary 3.10

Congruence elements c and filter elements d of GBI-algebras are in one-one correspondence via \(c \mapsto \top c\) and \(d \mapsto d \wedge 1\).

Proof

If \(F=\mathord {\uparrow }d\) then the least element of \(\mathord {\uparrow }^-(F \wedge 1)\) is \(d \wedge 1\). Also, if \(N=[c, 1 {/}c]\), then \(M=N^-=[c, 1]\) and the least element of \(\mathord {\uparrow }^-(M \top )\) is \(c \top \). The maps are mutually inverse because \(\top c \wedge 1 = \top \wedge c1=c\) for any congruence element c, and \((d \wedge 1)\top =d \wedge 1\top =d\) for any filter element d. \(\square \)

4 Congruences on involutive GBI-algebras

For involutive GBI-algebras the characterization of congruence filters simplifies further since the residuals \({\backslash },/\) are definable by \(x{\backslash }y={\sim }((-y)x)\) and \(x/y=-(y({\sim }x))\). This implies that only the operations \(\wedge ,\vee ,\rightarrow ,\cdot ,{\sim },-\) need to preserve congruence relations. Filters already characterize Brouwerian algebra congruences, so it suffices to find terms that show \(a\rightarrow c\in F\) implies \(ab\rightarrow cb, ba\rightarrow bc, {\sim }c\rightarrow {\sim }a,-c\rightarrow -a\in F\). Recall that intuitionistic negation is defined by the term \(\lnot x=x\rightarrow \bot \).

Theorem 4.1

For an involutive GBI-algebra, a lattice filter F is a congruence filter if and only if \(\lnot {\sim }x,\lnot {-}x, {\sim }(\top (-x)\top )\in F\), for all \(x\in F\).

Proof

To prove the forward implication, we note that congruence filters are indeed closed under these terms since \(\lnot {\sim }\top =\lnot \bot =\top \), \(\lnot {-}\top =\top \) and \({\sim }(\top (-\top )\top )={\sim }(\top \bot \top )={\sim }\bot =\top \).

For the reverse implication, suppose F is closed under the given terms, and let \(x=a\rightarrow b\in F\). Then \(a\wedge x\le b\), from which we deduce \(-b\le -(a\wedge x)\) and therefore \(-(a\wedge x)\rightarrow -a\le -b\rightarrow -a\). Note that

$$\begin{aligned} \lnot {-}x=-x\rightarrow \bot&\le -x\rightarrow -a=(-a\rightarrow -a)\wedge (-x\rightarrow -a)\\&=(-a\vee -x)\rightarrow -a=-(a\wedge x)\rightarrow -a \end{aligned}$$

hence \(\lnot {-}x\in F\) implies \(-b\rightarrow -a\in F\) as required. By a similar calculation, if \(a\rightarrow b\in F\) then \({\sim }b\rightarrow {\sim }a\in F\).

The term \({\sim }(\top (-x)\top )\) is a translation of \(\top {\backslash }x/\top \)

$$\begin{aligned} (\top {\backslash }x)/\top =({\sim }\top +x)+-\top ={\sim }\top +x+{\sim }\top ={\sim }(\top (-x)\top ). \end{aligned}$$

As in the proof of Theorem 3.1 this term is used to show that \(a\theta c\) implies \(a/b\ \theta \ c/b\), or equivalently \(-(b({\sim }a)) \theta \ -(b({\sim }c))\). Applying \({\sim }\) gives \(b({\sim }a) \theta \ b({\sim }c)\), and replacing ac by \(-a,-c\) we get \(ba\ \theta \ bc\). The proof for \(a\theta c \implies ab\ \theta \ cb\) is similar. \(\square \)

The three congruence terms in the preceding theorem contain no parameters, which means that the variety of involutive GBI-algebras has the congruence extension property and the corresponding logic has a local deduction theorem [10].

The 3-element MV-algebra Ł\(_3=\{0,a,1\}\) with \(0<a<1\), \(aa=0\), \({\sim }a=a\) and \(\lnot a=0\) is a involutive BI-algebra that shows \(a\nleq \lnot {\sim }a\ne {\sim }\lnot a\). The 4-element Boolean involutive BI-algebra \(B_4=\{\bot ,b,1,\top \}\) with \(b\cdot b=\bot \), \(\top \cdot b=b\) and \({\sim }1=1\) shows that \(\lnot {\sim }b\nleq b\).

Hence the terms \(\lnot {\sim }x\), \(\lnot {-}x\) are not decreasing. However, all three terms in Theorem 4.1 are meet-preserving, e.g., \(\lnot {\sim }(x\wedge y)=({\sim }x\vee {\sim }y)\rightarrow \bot =\lnot {\sim }x\wedge \lnot {\sim }y\). Now consider the term

$$\begin{aligned} \tau (x)=x\wedge \lnot {\sim }x\wedge \lnot {-}x\wedge {\sim }(\top ({-}x)\top ). \end{aligned}$$

Corollary 4.2

The following hold for involutive GBI-algebras.

  1. (1)

    A lattice filter F is a congruence filter if and only if \({\sim }F\subseteq {\downarrow }(\lnot F)\), \(-F\subseteq {\downarrow }(\lnot F)\) and \(F\subseteq {\uparrow }(\top F\top )\).

  2. (2)

    The congruence filter generated by a set Y is \({\uparrow }\{\tau ^n(y):y\in \langle Y\rangle , n\in \omega \}\) where \(\langle Y\rangle \) is the lattice filter generated by Y.

  3. (3)

    An element d is a filter element if and only if \(\tau (d)=d\) or, equivalently, if \({\sim }d = {-}d\), \({\sim }d\vee d=\top \) and \(\top d\top =d\).

  4. (4)

    Any filter element d is complemented, with complement \({\sim }d\) that is also a filter element. The set of filter elements is a Boolean subalgebra of the \(\{\wedge ,\vee ,{\sim },\top ,\bot \}\)-reduct of the GBI-algebra.

Proof

(1) The filter F is closed under \(\lnot {\sim }x\) if for all \(x\in F\) there exists a \(y\in F\) such that \(y\le \lnot {\sim }x\). This is equivalent to each of the following equivalent statements:

$$\begin{aligned} \forall x\exists y\,{\sim }x\wedge y\le \bot , \qquad \forall x\exists y\,{\sim }x\le \lnot y, \qquad \forall x\,{\sim }x\in {\downarrow }(\lnot F), \qquad {\sim }F\subseteq {\downarrow }(\lnot F). \end{aligned}$$

The other conditions are derived in a similar way.

(2) Let \(F={\uparrow }\{\tau ^n(y):y\in \langle Y\rangle , n\in \omega \}\). Given \(a,b\in F\) we have \(a\ge \tau ^m(x)\) and \(b\ge \tau ^n(y)\) for some \(x,y\in \langle Y\rangle \). By symmetry we may assume \(m\le n\), so \(a\wedge b\ge \tau ^m(x)\wedge \tau ^n(y)\ge \tau ^n(x)\wedge \tau ^n(y)=\tau ^n(x\wedge y)\in F\) since \(x\wedge y\in \langle Y\rangle \).

Also \(\lnot {\sim }b\ge \lnot {\sim }\tau ^n(y)\ge \tau ^{n+1}(y)\in F\), and \(\lnot {-}b,{\sim }(\top ({-}b)\top )\in F\) is proved the same way.

(3) By Theorem 4.1 a principal filter \({\uparrow }d\) is a congruence filter if and only if \(d\le \lnot {\sim }d\), \(d\le \lnot {-}d\) and \(d\le \top {\backslash }d{/}\top \). The first condition is equivalent to \(d\wedge {\sim }d=\bot \), and by applying \({-}\) we obtain \(-d\vee d=\top \). In a similar way we obtain \(d\wedge {-}d=\bot \) and \({\sim }d\vee d=\top \). Therefore, both \({\sim }d\) and \({-}d\) are complements of d in the distributive lattice \(\mathbf{A}\), hence \({\sim }d = {-}d\). Finally, from \(d\le \top {\backslash }d{/}\top \) we get \(\top d \top \le d\) and the reverse inclusion follows because \(1 \le \top \).

(4) That \({\sim }d\) and \({-}d\) both serve as complements of d follows from (3), and that they are equal follows from uniqueness of complements in distributive lattices. We will now check the three conditions of (3) for the element \({\sim }d\). To show that the two linear negations coincide for the element \({\sim }d={-}d\), we have \({\sim }({\sim }d) = {\sim }({-}d)= d = {-}({\sim }d)\). Furthermore, from \({\sim }d \vee d = \top \) we get \({\sim }({\sim }d) \vee {\sim }d = {\sim }{-}d \vee {\sim }d = d \vee {\sim }d = \top \). Finally, since \(\top d \top = d\), by Lemma 5.4(4) below, it follows that \(\top {\backslash }d {/}\top = d\), hence \(\bot + d + \bot = d\), so \(\top ({\sim }d) \top ={\sim }(\bot + d + \bot )= {\sim }d\).

We now show that if c and d are filter elements, then so is \(c \vee d\), by checking the conditions in (3). We have \({\sim }(c \vee d)={\sim }c \wedge {\sim }d= {-}c \wedge {-}d = {-}(c \vee d)\) and \(\top (c \vee d) \top = \top c \top \vee \top d \top = c \vee d\). Finally, \({\sim }(c \vee d) \vee (c \vee d)= ({\sim }c \wedge {\sim }d) \vee (c \vee d)=({\sim }c \vee c \vee d) \wedge ({\sim }d \vee c \vee d)=(\top \vee d) \wedge (\top \vee c)=\top \).

Therefore filter elements are closed under \({\sim }\) and \(\vee \), and consequently also under \(\wedge \). \(\square \)

Filter elements in relation algebras are easier to describe because the terms \(\lnot {\sim }x\) and \({\sim }\lnot x\) are equal to each other (since \(\lnot \) and \({\sim }\) commute) and they define the converse.

Recall that an algebra is called semisimple if it is a subdirect product of simple algebras.

Lemma 4.3

Every finite involutive GBI-algebra is a direct product of simple algebras. In particular, finite involutive GBI-algebras are semisimple.

Proof

By Lemma 4.2(4) the congruence lattice of a finite involutive GBI-algebra is a Boolean algebra, hence every congruence is a factor congruence. Therefore every finite such algebra decomposes as a direct product of directly indecomposable algebras, which are simple as their only congruence elements are the top and the bottom. \(\square \)

The condition of involutivity cannot be dropped since there are finite Heyting algebras that are subdirectly irreducible but not simple.

Examples of other classes of semisimple involutive GBI-algebras are given in Theorem 5.9 and Corollary 5.12.

5 Double-division conucleus

In this section we present a new method for constructing residuated lattices, called the double-division conucleus construction and we show that it specializes to GBI-algebras. Based on this method we give a range of examples of GBI-algebras and define two subvarieties that are closely related to, but significantly more general than, representable relation algebras and relation algebras.

5.1 The construction

Recall that an interior operator \(\delta \) on a poset is a contractive idempotent monotone function, i.e., \(\delta (\delta (x))=\delta (x) \le x\) and \(x \le y \Longrightarrow \delta (x) \le \delta (y)\) for all \(x,y\in A\).

A weak conucleus \(\delta \) on a residuated lattice is an interior operator that satisfies the conuclear property for multiplication: \(\delta (x)\delta (y)\le \delta (xy)\). It is easy to see that this property is equivalent to the identity \(\delta (\delta (x)\delta (y))=\delta (x)\delta (y)\), and we note that the concept of weak conucleus makes sense even for partially-ordered semigroups.

For a residuated lattice \({\mathbf {A}}=(A,\wedge ,\vee ,\cdot ,\backslash ,/,1)\) define

$$\begin{aligned} A_{\delta }=\{x:\delta (x)=x\}=\{\delta (x):x\in A\}, \\ x\wedge _{\delta }y=\delta (x\wedge y),\quad x\,\backslash _{\delta }\,y=\delta (x\backslash y),\quad \text { and }\quad x\,/_{\delta }\,y=\delta (x/y). \end{aligned}$$

A residuated lattice-ordered semigroup is defined like a residuated lattice, but without the assumption that it has a multiplicative identity, and of course without the constant 1 in the signature. (In [1] it is shown that not all residuated lattice-ordered semigroups can be embedded into residuated lattices.)

Lemma 5.1

If \(\delta \) is a weak conucleus on a residuated lattice-ordered semigroup \({\mathbf {A}}\), then \((A_{\delta },\wedge _{\delta },\vee ,\cdot ,\backslash _{\delta },/_{\delta })\) is a residuated lattice-ordered semigroup. If \(A_\delta \) has an identity element e, then \({\mathbf {A}}_{\delta }=(A_{\delta },\wedge _{\delta },\vee ,\cdot ,\backslash _{\delta },/_{\delta }, e)\) is a residuated lattice.

Proof

This result is a version of [10, 3.41] that does not involve the monoid unit. \(\square \)

A topological interior operator on a meet-semilattice is an interior operator that satisfies the conuclear property for meet: \(\delta (x)\wedge \delta (y)\le \delta (x \wedge y)\) for all \(x,y\in A\); the reverse inequality is true for all interior operators, so the identity \(\delta (x\wedge y)=\delta (x)\wedge \delta (y)\) holds. A weak conucleus on a residuated lattice with this property is called a topological weak conucleus; in other words a topological weak conucleus is precisely a weak conucleus with respect to both multiplication and meet. The following lemma points out that in this case the operation \(\wedge _{\delta }\) coincides with \(\wedge \), so \((A_{\delta },\wedge ,\vee ,\cdot )\) is a subalgebra of the \(\wedge ,\vee ,\cdot \) reduct of \({\mathbf {A}}\).

Lemma 5.2

If \(\delta \) is a topological weak conucleus on a residuated lattice-ordered semigroup \({\mathbf {A}}=(A, \wedge , \vee , \cdot , {\backslash }, {/})\), then \((A_{\delta },\wedge ,\vee ,\cdot ,\backslash _{\delta },/_{\delta })\) is a residuated lattice-ordered semigroup. If \(A_\delta \) has an identity element e, then \({\mathbf {A}}_{\delta }=(A_{\delta },\wedge ,\vee ,\cdot ,\backslash _{\delta }\), \(/_{\delta }, e)\) is a residuated lattice. Moreover, any \(\{\wedge ,\vee ,\cdot \}\)-universal formula that holds in \(\mathbf{A}\) also holds in \(\mathbf{A}_\delta \).

In particular, unlike weak conuclei, the topological ones preserve distributivity. The above result applies to GBI-algebras, in which case we define

$$\begin{aligned} x\rightarrow _{\delta }y=\delta (x\rightarrow y)\qquad \text {and}\qquad \top _{\delta }=\delta (\top ). \end{aligned}$$

Theorem 5.3

If \(\delta \) is a topological weak conucleus on a GBI-algebra \({\mathbf {A}}\) and \(A_\delta \) has an identity element e, then \({\mathbf {A}}_{\delta }=(A_{\delta },\wedge ,\vee ,\rightarrow _{\delta },\top _{\delta },\cdot ,\backslash _{\delta },/_{\delta }, e)\) is a GBI-algebra. If \({\mathbf {A}}\) is bounded or commutative, so is \({\mathbf {A}}_{\delta }\). More generally, any \(\{\wedge ,\vee ,\cdot \}\)-universal formula that holds in \(\mathbf{A}\) also holds in \(\mathbf{A}_\delta \).

Proof

By Lemma 5.1, \((A_{\delta },\wedge _{\delta },\vee ,\cdot ,\backslash _{\delta },/_{\delta })\) is a residuated lattice-ordered semigroup, and since the Brouwerian algebra \((A,\wedge ,\vee ,\rightarrow ,\top )\) is also a residuated lattice with \(\wedge \) as monoid operation, it follows again by Lemma 5.1 that \(A_{\delta }\) is closed under \(\wedge \) and \((A_{\delta },\wedge ,\vee ,\rightarrow _{\delta },\delta (\top ))\) is a Brouwerian algebra. That \(\delta (\top )\) is the top element of \(\mathbf{A}_\delta \) follows from the monotonicity of \(\delta \). \(\square \)

In a residuated lattice-ordered semigroup \(\mathbf{A}\), an element \(p \in A\) is called positive if for all \(x \in A\), \(p{\backslash }x, x {/}p \le x \le px, xp\). Note that in a residuated lattice an element is positive if and only if \(1 \le p\). We also define the following maps on A:

$$\begin{aligned} \delta _{p}(x)=p\backslash x/p\qquad \text {and}\qquad \gamma _p(x)=pxp, \quad \text { where }x\in A. \end{aligned}$$

Lemma 5.4

Let \({\mathbf {A}}\) be a residuated lattice-ordered semigroup, and p a positive idempotent element of A. The following hold:

  1. (1)

    \(x=p\backslash x\) if and only if \(px=x\).

  2. (2)

    \(x=x/p\) if and only if \(xp=x\).

  3. (3)

    \(x = p {\backslash }x {/}p\) iff \(p {\backslash }x = x = x {/}p\). Also, \(x = pxp\) iff \(xp=x=px\).

  4. (4)

    \(p {\backslash }x {/}p=x\) if and only if \(pxp=x\).

  5. (5)

    The maps \(x \mapsto p x\), \(x \mapsto x p\) and \(\gamma _p\) are closure operators.

  6. (6)

    The maps \(x \mapsto p {\backslash }x\), \(x \mapsto x {/}p\) and \(\delta _p\) are weak conuclei.

  7. (7)

    \(\gamma _p\) and \(\delta _p\) have the same image.

Proof

(1) Since p is positive, we have \(p {\backslash }x\le 1{\backslash }x \le x \le px\). Therefore

$$\begin{aligned} x = p {\backslash }x\quad \iff \quad x \le p {\backslash }x\quad \iff \quad px \le x\quad \iff \quad px = x. \end{aligned}$$

The proof of (2) is analogous.

(3) Note that \(x \le px, xp \le pxp\), so \(x=pxp\) implies \(x=px\) and \(x=xp\). The converse is also true, since if \(x=px=xp\), then \(pxp=px=x\). So, \(x=pxp\) if and only if \(x=px=xp\). In a similar way, using that \(p{\backslash }x {/}p \le p {\backslash }x, x {/}p \le x\) one shows that \(x=p {\backslash }x {/}p\iff x=p {\backslash }x=x {/}p\).

(4) This result follows from (1), (2) and (3).

(5) Since p is positive, we have \(x \le px\). From the idempotence of p, we obtain \(ppx=px\). Finally by order preservation of multiplication we get that \(x \mapsto px\) is order-preserving. Likewise \(x \mapsto xp\) is a closure operator, and \(\gamma _p\) is their composition, so it is also a closure operator.

(6) Since p is positive, we have \(p {\backslash }x \le x\). Since p is idempotent, we have \(p{\backslash }p {\backslash }x =p^2 {\backslash }x= p {\backslash }x\). By order preservation of division in the numerator position we get that \(x \mapsto p {\backslash }x\) is order-preserving. Finally we have \((p {\backslash }x)(p {\backslash }y) \le p {\backslash }xy\) because \(p(p {\backslash }x)(p {\backslash }y)\le x(p {\backslash }y)\le x y\), since p is positive. Likewise we get that \(x \mapsto x {/}p\) is a conucleus, and so is \(\delta _p\), being their composition.

(7) This follows from (4), (5) and (6). \(\square \)

For two positive idempotent elements \(p,q \in \mathbf{A}\), the map \(\gamma _{p,q}(x)=pxq\) is a closure operator and \(\delta _{p,q}(x)=p {\backslash }x {/}q\) is a conucleus, with the same set of fixed elements, because they are compositions of the appropriate maps mentioned in the previous theorem. The first two items of the next theorem also hold with this more generalized notion, except for the fact that the image need not have an identity element; we only get that p is a left identity and q is a right identity. Since we are interested in algebras with identity, we do not pursue this direction further. We will see that the double-conucleus construction generalizes a result of Jónsson [15] for relation algebras, which in turn generalizes Comer’s double coset construction [3] for group relation algebras. This construction is defined by taking a subgroup P of a group G and considering double cosets PgP, originally defined by Dresher and Ore [5]. The latter paper also considers two subgroups P and Q of G and double cosets of the form PgQ, therefore it links to the more general maps \(\gamma _{p,q}\) and \(\delta _{p,q}\).

For a residuated lattice or GBI-algebra \(\mathbf{A}\) and positive idempotent p, we define

$$\begin{aligned} p {\backslash }A {/}p= & {} \{p {\backslash }a {/}p : a \in A\},\quad x\,{\backslash }_p\,y=p{\backslash }(x{\backslash }y){/}p, \quad x\,{/}_p\,y=p{\backslash }(x{/}y){/}p \quad \text {and} \\ p {\backslash }\mathbf{A}{/}p= & {} (p {\backslash }A {/}p, \wedge , \vee , \cdot , {\backslash }_p, {/}_p, p). \end{aligned}$$

Theorem 5.5

Let \(\mathbf{A}=(A, \wedge , \vee , \cdot , {\backslash }, {/})\) be a residuated lattice-ordered semigroup and p a positive idempotent. Then the following hold:

  1. (1)

    \(\delta _p\) is a topological weak conucleus.

  2. (2)

    \(p {\backslash }\mathbf{A}{/}p\) is a residuated lattice.

  3. (3)

    If \(\mathbf{A}\) is involutive with negation constant 0 and \({\sim }p= {-}p\), then \(p {\backslash }\mathbf{A}{/}p\) is also involutive with linear negation constant \(\delta _p(0)=p{\backslash }0 {/}p=p{\backslash }0\) and \({\sim }_p p = {-}_p p\) in \(p {\backslash }\mathbf{A}{/}p\). Moreover \(p {\backslash }\mathbf{A} {/}p\) is a subalgebra of \(\mathbf{A}\) with respect to the operations \(\wedge , \vee , \cdot , {\sim }, {-}\) and differs only in the constants for 0 and 1. Hence all constant-free universal formulas are preserved.

  4. (4)

    If \({\mathbf {A}}\) is a GBI-algebra, then \(p {\backslash }{\mathbf {A}} {/}p\) is also a GBI-algebra.

Proof

That the map \(\delta _p\) is a conucleus was proved in Lemma 5.4. That it is topological follows from the fact that divisions distribute over meets in the numerator position. If \(\mathbf{A}\) is involutive with negation constant 0 and \(p {\backslash }0= 0 {/}p\), we have \(\delta _p(0)=p{\backslash }0 {/}p=p{\backslash }(p{\backslash }0)=p{\backslash }0\). We will show that the involutions are the same in the two structures. For all \(x \in p {\backslash }A {/}p\) we have \({\sim }_p x=x {\backslash }_p \delta _p(0)=\delta _p(x {\backslash }\delta _p(0))=p{\backslash }(x {\backslash }(p{\backslash }0) ) {/}p= (pxp) {\backslash }0 {/}p=(pxp){\backslash }(p {\backslash }0)=(p^2 xp) {\backslash }0=(pxp){\backslash }0=x {\backslash }0 = {\sim }x\), since x is a fixed-point of \(\gamma _p\). Likewise \({-}_px={-}x\). Now, \({\sim }_p {-}_p x= {\sim }{-}x=x\) and \({-}_p {\sim }_p x= {-}{\sim }x=x\), by involutivity of \(\mathbf{A}\), hence \(p {\backslash }\mathbf{A} {/}p\) is involutive. Finally, we have \({\sim }_p p = {\sim }p = {-}p = {-}_p p\). \(\square \)

The above construction generalizes a simpler one in semigroups. Given an idempotent element p of a semigroup \(\mathbf{A}\), the subset \(pAp=\{pap :a \in A\}\) is equal to the set \(\{y \in A: py=y=yp\}\) of all elements for which p is a two-sided identity. Also, pAp is a subsemigroup of \(\mathbf{A}\) and it is actually a monoid with identity element p. The map \(\gamma _p(x)=pxp\) in general fails to be a monoid homomorphism (exhibited by a 6-element monoid).

The construction also generalizes a particular case of a result for relation algebras [15] (namely the case where the equivalence elements are positive). Recall that by Lemma 1.1 relation algebras can be defined as cyclic involutive GBI-algebras with Boolean negation and \((xy)^{\smallsmile }=y^{\smallsmile }x^{\smallsmile }\), where the converse is defined by \(x^{\smallsmile }={\sim }\lnot x\).

Lemma 5.6

If \(\mathbf{A}\) is a relation algebra and p is a positive idempotent of \(\mathbf{A}\) such that \(p^{\smallsmile }=p\), then \(p {\backslash }\mathbf{A} {/}p\) is also a relation algebra.

Proof

Note that \(p^{\smallsmile }=p\) is equivalent to \({\sim }\lnot p = p\) and to \(\lnot p = {\sim }p\). We first show that \(p {\backslash }\mathbf{A} {/}p\) is a subalgebra of \(\mathbf{A}\) with respect to converse.

We assume that \(\delta _p(x)=x\) and will show that \(\delta _p(\lnot x)=\lnot x\). We have \(\delta _p(\lnot x)=p {\backslash }\lnot x {/}p = {\sim }p + \lnot x + {\sim }p= \lnot p + \lnot x + \lnot p= \lnot (pxp)=\lnot x\). So, \(p {\backslash }\mathbf{A} {/}p\) is closed under involution, negation (which is Boolean in \(\mathbf{A}\), hence also in \(p {\backslash }\mathbf{A} {/}p\)) and under converse since \(x^{\smallsmile }=\lnot {\sim }x\).

Finally, \((xy)^{{\smallsmile }_p}=y^{{\smallsmile }_p}x^{{\smallsmile }_p}\) for \(x,y \in p {\backslash }\mathbf{A} {/}p\) follows from the fact that \(x^{{\smallsmile }_p}=x^{\smallsmile }\) and the fact that \((xy)^\smallsmile =y^\smallsmile x^\smallsmile \) holds in \(\mathbf{A}\). \(\square \)

5.2 Varieties from double-conuclei images

If \({\mathcal {K}}\) is a class of residuated lattices or GBI-algebras, we denote by \(\mathsf {d}{\mathcal {K}}\) the class \(\{p {\backslash }\mathbf{A} {/}p : \mathbf{A} \in {\mathcal {K}}, 1 \le p = p^2, p \in A\}\) of all double-division conuclei images of algebras in \({\mathcal {K}}\) by positive idempotents. We will show that for certain types of varieties \({\mathcal {V}}\), the subalgebras of \(\mathsf {d}{\mathcal {V}}\) form a variety.

The following lemma guarantees in particular that if a class \({\mathcal {K}}\) is closed under direct products then \(\mathsf {d}{\mathcal {K}}\) is also closed under direct products. We will use \({\mathsf {H}}\), \({\mathsf {S}}\), \({\mathsf {P}}\), \({\mathsf {I}}\), \({\mathsf {V}}\), \(\mathsf {P_U}\) and \(\mathsf {P_S}\) for the usual class operators of homomorphic images, subalgebras, products, isomorphic copies, variety generated by, ultraproducts and subdirect products respectively.

Lemma 5.7

Let \({\mathcal {K}}\) be a class of residuated lattices or GBI-algebras. Then

  1. (1)

    \(\mathsf {dP}{\mathcal {K}} = \mathsf {Pd}{\mathcal {K}}\).

  2. (2)

    \(\mathsf {dS}{\mathcal {K}} \subseteq \mathsf {Sd}{\mathcal {K}}\).

  3. (3)

    \(\mathsf {P_Ud}{\mathcal {K}} \subseteq \mathsf {IdP_U}{\mathcal {K}}\).

  4. (4)

    \(\mathsf {dI}{\mathcal {K}} = \mathsf {Id}{\mathcal {K}}\).

Proof

(1) First note that given \(p_i \in A_i\) for all \(i \in I\), we have that \(p=(p_i)_{i \in I}\) is a positive idempotent in \(\prod _{i \in I} \mathbf{A}_i\) if and only if \(p_i\) is positive idempotent in \(\mathbf{A}_i\) for all \(i \in I\). We will show that if all \(\mathbf{A}_i\) are residuated lattices or GBI-algebras and \(p_i\) is a positive idempotent of \(\mathbf{A}_i\), for all \(i \in I\), then \(\prod _{i \in I} p_i {\backslash }\mathbf{A}_i {/}p_i\) is equal to \(p {\backslash }(\prod _{i \in I} \mathbf{A}_i) {/}p\), where \(p=(p_i)_{i \in I}\). We set \(\mathbf{B}_i = p_i {\backslash }\mathbf{A}_i {/}p_i\), for \(i \in I\), \(\mathbf{B} = \prod _{i \in I} \mathbf{B}_i\) and \(\mathbf{A} = \prod _{i \in I} \mathbf{A}_i\). That the underlying sets of \(\prod _{i \in I} p_i {\backslash }\mathbf{A}_i {/}p_i\) and \(p {\backslash }(\prod _{i \in I} \mathbf{A}_i) {/}p\) are equal follows from the fact that the operations are computed coordinate-wise; the fact that the conucleus \(\delta _p\) is defined by a polynomial (a term with parameters) is what makes this argument work. If \(\star \) is an operation and \(b=(b_i)_{i \in I}, c=(c_i)_{i \in I} \in B\), then the operation in \(\mathbf{B}\) is computed as \(b \star ^{\mathbf{B}} c = (b_i \star ^{\mathbf{B}_i} c_i)_{i \in I}\). On the other hand, when computing the operation in \(p {\backslash }\mathbf{A} {/}p\), we have \(b \star ^{p {\backslash }\mathbf{A} {/}p} c = p {\backslash }(b \star ^{\mathbf{A}} c)_{i \in I} {/}p= (p_i {\backslash }(b_i \star ^{\mathbf{A}_i} c_i) {/}p_i)_{i \in I}\). That \(b_i \star ^{\mathbf{B}_i} c_i=p_i {\backslash }(b_i \star ^{\mathbf{A}_i} c_i) {/}p_i\) follows from the definition of the operations in the conuclear image, therefore \(b \star ^{\mathbf{B}} c=b \star ^{p {\backslash }\mathbf{A} {/}p} c\). The only operation that behaves differently is the constant operation of 1, but the identity element is defined in both algebras and is the same.

(2) Let \(\mathbf{B}\) be a subalgebra of \(\mathbf{A}\) and p a positive idempotent in \(\mathbf{B}\). We will show that \(p {\backslash }\mathbf{B} {/}p\) is a subalgebra of \(p {\backslash }\mathbf{A} {/}p\), noting that p is a positive idempotent in \(\mathbf{A}\). First of all they have the same identity p. Also, if \(b,c \in p {\backslash }B {/}p\) then \(b,c \in B\). Let and \(\star \) be a binary operation. Using the fact that \(\mathbf{B}\) is a subalgebra of \(\mathbf{A}\) we get \(b \star ^{p {\backslash }\mathbf{B} {/}p} c = p {\backslash }(b \star ^{\mathbf{B}} c) {/}p = p {\backslash }(b \star ^{\mathbf{A}} c) {/}p = b \star ^{p {\backslash }\mathbf{A} {/}p} c\).

(3) We will now show that every ultraproduct of a double-division image is isomorphic to a double-division image of some ultraproduct. More concretely, if \(\mathbf{B}_{\mathcal {U}}\) is the ultraproduct of \(\mathbf{B}_i \in {\mathsf {d}}{\mathcal {K}}\), for \(i \in I\), over some ultrafilter \({\mathcal {U}}\) over I, where \(\mathbf{B} = \prod _{i \in I} \mathbf{B}_i\), then there exist \(\mathbf{A}_i \in {\mathcal {K}}\) such that \(\mathbf{B}_i = p_i {\backslash }\mathbf{A}_i {/}p_i\), where \(p_i\) is a positive idempotent of \(\mathbf{A}_i\), for \(i \in I\). We will show that \(\mathbf{B}_{\mathcal {U}}\) is isomorphic to \(p^{\mathbf{A}} {\backslash }\mathbf{A}_{\mathcal {U}} {/}p^{\mathbf{A}}\), where \(\mathbf{A}_{\mathcal {U}}\) is the ultraproduct of the \(\mathbf{A}_i\), \(p^{\mathbf{A}}=[(p_i)_{i \in I}]^{\mathbf{A}}\), for \(i \in I\), over the same ultrafilter \({\mathcal {U}}\); we set \(\mathbf{A} = \prod _{i \in I} \mathbf{A}_i\). Here \([a]^{\mathbf{A}}\) denotes the equivalence class of a in \(\mathbf{A}_{\mathcal {U}}\) and \([b]^{\mathbf{B}}\) denotes the equivalence class of b in \(\mathbf{B}_{\mathcal {U}}\). The isomorphism \(f:\mathbf{B}_{\mathcal {U}} \mathbin {\rightarrow }p^{\mathbf{A}} {\backslash }\mathbf{A}_{\mathcal {U}} {/}p^{\mathbf{A}}\) is given by \(f([b]^{\mathbf{B}})=[b]^{\mathbf{A}}\). This map is well defined, since if \(b, c \in B\) are equivalent, then their coordinates are equal on a set in \({\mathcal {U}}\) and if they are viewed as elements of \(\mathbf{A}\), their coordinates will be equal on the same set of \({\mathcal {U}}\). Also, f is injective, because if \(b, c \in B\) disagree on a set of coordinates in \({\mathcal {U}}\), then the same is true when viewed as elements of \(\mathbf{A}\). Furthermore, the map is onto, since if \(p^{\mathbf{A}} {\backslash }a {/}p^{\mathbf{A}} \in p^{\mathbf{A}} {\backslash }A_{\mathcal {U}} {/}p^{\mathbf{A}}\), we have \(p^{\mathbf{A}} {\backslash }a {/}p^{\mathbf{A}} = [(p_i)_{i \in I}]^{\mathbf{A}} {\backslash }[(a_i)_{i \in I}]^{\mathbf{A}} {/}[(p_i)_{i \in I}]^{\mathbf{A}}= [(p_i)_{i \in I} {\backslash }(a_i)_{i \in I} {/}(p_i)_{i \in I}]^{\mathbf{A}}= [(p_i {\backslash }a_i {/}p_i)_{i \in I}]^{\mathbf{A}}=f([(p_i {\backslash }a_i {/}p_i)_{i \in I}]^{\mathbf{B}})\) because \((p_i {\backslash }a_i {/}p_i)_{i \in I} \in B\).

To show that it is a homomorphism, let \(\star \) be an operation and \(b,c \in B\). Then \(f([b]^{\mathbf{B}} \star ^{\mathbf{B}_{\mathcal {U}}} [c]^{\mathbf{B}})= f([b \star ^{\mathbf{B}} c]^{\mathbf{B}})= [b \star ^{\mathbf{B}} c]^{\mathbf{A}}\) and

$$\begin{aligned} f([b]^{\mathbf{B}}) \star ^{p^{\mathbf{A}} {\backslash }\mathbf{A}_{\mathcal {U}} {/}p^{\mathbf{A}}} f([c]^{\mathbf{B}})&=[b]^{\mathbf{A}} \star ^{p^{\mathbf{A}} {\backslash }\mathbf{A}_{\mathcal {U}} {/}p^{\mathbf{A}}} [c]^{\mathbf{A}}\\&=[(p_i)_{i \in I}]^{\mathbf{A}} {\backslash }([b]^{\mathbf{A}} \star ^{\mathbf{A}_{\mathcal {U}}} [c]^{\mathbf{A}}) {/}[(p_i)_{i \in I}]^{\mathbf{A}}\\&=[(p_i)_{i \in I}]^{\mathbf{A}} {\backslash }([b \star ^{\mathbf{A}} c]^{\mathbf{A}}) {/}[(p_i)_{i \in I}]^{\mathbf{A}}\\&=[p {\backslash }b \star ^{\mathbf{A}} c {/}p]^{\mathbf{A}}=[b \star ^{\mathbf{B}} c]^{\mathbf{A}}. \end{aligned}$$

(4) It is easy to see that \(\mathsf {dI}{\mathcal {K}}\subseteq \mathsf {Id}{\mathcal {K}}\) since a \({\mathsf {d}}\)-image of an algebra \(\mathbf{A}\) is isomorphic to the corresponding \(\mathsf {d}\)-image of an isomorphic copy of \(\mathbf{A}\).

In the reverse direction, if an algebra \(\mathbf{A}\) is isomorphic to \(\delta _p(\mathbf{B})\) for an algebra \(\mathbf{B}\) and positive idempotent \(p\in B\), then one can extend \(\mathbf{A}\) to an algebra \(\mathbf{C}\cong \mathbf{B}\) such that \(\mathbf{A}=\delta _{{{\bar{p}}}}(\mathbf{C})\) where \({\bar{p}}\in C\) is the isomorphic copy of \(p\in B\). \(\square \)

A term c(x) is a unary discriminator term for a bounded GBI-algebra \(\mathbf{A}\) if for all \(a\in A\), \(c(\top )=\top \) and \(c(a)=\bot \) if \(a\ne \bot \). Such a term is called a unary discriminator term for a variety \({\mathcal {V}}\) if it is a unary discriminator for all subdirectly irreducible algebras \(SI({\mathcal {V}})\) in the variety.

Lemma 5.8

If \({\mathcal {V}}\) is a variety of involutive GBI-algebras for which c(x) is a unary discriminator term, then \({\mathcal {V}}\) is a discriminator variety.

Proof

We consider the term \(t(x,y,z)=(c(x \mathbin {\leftrightarrow } y) \wedge z) \vee (\lnot c(x \mathbin {\leftrightarrow } y) \wedge x) \) where \(x \mathbin {\leftrightarrow } y = (x \mathbin {\rightarrow }y) \wedge (y \mathbin {\rightarrow }x)\). For any subdirectly irreducible algebra \(\mathbf{A}\) in \({\mathcal {V}}\) and \(x , y, z \in A\), we have that if \(x = y\) then \(x \mathbin {\leftrightarrow } y = \top \) and \(c(x \mathbin {\leftrightarrow } y)= \top \), so \(t(x,y,z) = (\top \wedge z) \vee (\bot \wedge x)=z\), while if \(x \not = y\) then \(x \mathbin {\leftrightarrow } y \not = \top \) and \(c(x \mathbin {\leftrightarrow } y)= \bot \), so \(t(x,y,z) = (\bot \wedge z) \vee (\top \wedge x)=x\). Thus, t is a ternary discriminator term. \(\square \)

A residuated lattice or a GBI-algebra is called semilinear if it is a subdirect product of linearly ordered algebras. The classes of all semilinear residuated lattices and all GBI-algebras form varieties [10].

Theorem 5.9

The subvariety of involutive GBI-algebras defined by the identity \(\lnot x\vee \lnot \lnot x=\top \) is a discriminator variety with unary discriminator term \(c(x)=\lnot {\sim }x\) (alternatively with \(c(x)=\lnot {-}x\)). In particular the variety of all semilinear involutive GBI-algebras is a discriminator variety.

Proof

Let \(\mathbf{A}\) be a subdirectly irreducible GBI-algebra that satisfies \(\lnot x\vee \lnot \lnot x=\top \). Then \(\mathbf{A}\) has the property that \(\bot \) is meet-irreducible [10] (Lemma 9.67). We have \(c(\top )=\lnot \bot =\top \) and if \(\top \ne a\in A\) then \(c(a)=\lnot {\sim }a\) and \({\sim }a\ne \bot \). Because \({\sim }a\wedge \lnot {\sim }a=\bot \) it follows that \(c(a)=\bot \). \(\square \)

We will be looking at specific examples of bounded GBI-algebras, for which the term \(\top {\backslash }x {/}\top \) is a unary discriminator term. We will show that for such cases the operator \(\mathsf {Sd}\) applied to varieties, produces varieties. Note that this term fails to be a unary discriminator in general, and in particular even for Boolean cyclic involutive GBI-algebras, as can be shown by a 4-element counterexample.

Recall that if \({\mathcal {V}}\) is a discriminator variety then its subdirectly irreducible algebras \(SI({\mathcal {V}})\) are the same as its simple algebras \(Si({\mathcal {V}})\).

Lemma 5.10

Let \({\mathcal {V}}\) be a variety of bounded residuated lattices or bounded GBI-algebras where \(\top {\backslash }x {/}\top \) is a unary discriminator term. Then \(\top {\backslash }x {/}\top \) is a unary discriminator term for \(\mathsf {Sd}Si({\mathcal {V}})\), the subalgebras of double division conucleus images of simple algebras in \({\mathcal {V}}\).

Proof

Since \(\top {\backslash }x {/}\top \) is a unary discriminator term for \({\mathcal {V}}\), \(\top {\backslash }x {/}\top \) is equal to \(\top \) if \(x = \top \) and it is equal to \(\bot \) otherwise in a simple algebra \(\mathbf{A}\) of \({\mathcal {V}}\). Let p be a positive idempotent of \(\mathbf{A}\). We will show that the term \(\top {\backslash }x {/}\top \) is a unary discriminator term for \(p {\backslash }\mathbf{A} {/}p\) and therefore for all of its subalgebras, as well.

For \(x \in p {\backslash }\mathbf{A} {/}p\) we compute \(\top {\backslash }_p x {/}_p \top \). We first note that \(\top {\backslash }_p x= \delta _p(\top {\backslash }x)= p {\backslash }(\top {\backslash }x) {/}p = \top p {\backslash }x {/}p = \top {\backslash }x {/}p\). Likewise, \(y {/}_p \top =\delta _p(y {/}\top )= p {\backslash }y {/}\top \). Hence, \(\top {\backslash }_p x {/}_p \top = (\top {\backslash }x {/}p) {/}_p \top = p {\backslash }(\top {\backslash }x {/}p) {/}\top = \top p {\backslash }x {/}\top p=\top {\backslash }x {/}\top \). (We made use of the fact that \(\top p = p \top = \top \), which holds because p is positive and \(\top \) is the greatest element.) Therefore, the term remains the same when passing from \(\mathbf{A}\) to \(p {\backslash }\mathbf{A} {/}p\) and hence it is a unary discriminator term on \(p {\backslash }\mathbf{A} {/}p\). \(\square \)

Theorem 5.11

Let \({\mathcal {V}}\) be a variety of bounded residuated lattices or bounded GBI-algebras for which \(\top {\backslash }x {/}\top \) is a unary discriminator term. Then \(\mathsf {Sd}{\mathcal {V}}\) is a discriminator variety with the same unary discriminator term. Its class of simple members is exactly \(\mathsf {Sd}Si({\mathcal {V}})\).

Proof

By Lemma 5.8, \({\mathcal {V}}\) is a discriminator variety, so all of its subdirectly irreducible algebras are simple. Therefore,

$$\begin{aligned} {\mathcal {V}} \subseteq \mathsf {P_S}SI({\mathcal {V}}) \subseteq \mathsf {P_S}Si({\mathcal {V}})\subseteq \mathsf {SP}Si({\mathcal {V}}). \end{aligned}$$

By Lemma 5.7, we get

$$\begin{aligned} {\mathsf {d}}{\mathcal {V}} \subseteq \mathsf {dSP}Si({\mathcal {V}}) \subseteq \mathsf {SdP}Si({\mathcal {V}}) \subseteq \mathsf {SPd}Si({\mathcal {V}}). \end{aligned}$$

Therefore,

$$\begin{aligned} \mathsf {Sd}({\mathcal {V}}) \subseteq \mathsf {SPd}Si({\mathcal {V}}) \subseteq \mathsf {Vd}Si({\mathcal {V}}) \end{aligned}$$

We will show the reverse inclusion \(\mathsf {Vd}Si({\mathcal {V}}) \subseteq \mathsf {Sd}({\mathcal {V}})\), thus showing that \(\mathsf {Sd}({\mathcal {V}})=\mathsf {Vd}Si({\mathcal {V}})\) is a variety.

By Jónsson’s Lemma for congruence distributive varieties, the subdirectly irreducible algebras in \({\mathsf {V}}{\mathsf {d}}Si({\mathcal {V}})\) are inside \(\mathsf {HSP_U}{\mathsf {d}}Si({\mathcal {V}})\). Therefore,

$$\begin{aligned} \mathsf {Vd}Si({\mathcal {V}}) \subseteq \mathsf {P_S}SI({\mathsf {V}}{\mathsf {d}}Si({\mathcal {V}})) \subseteq \mathsf {P_S}\mathsf {HSP_U}{\mathsf {d}}Si({\mathcal {V}}). \end{aligned}$$

We will show below that \(\mathsf {HSP_U}{\mathsf {d}}Si({\mathcal {V}})\subseteq \mathsf {Sd}Si({\mathcal {V}}) \cup {\mathcal {T}}\), where \({\mathcal {T}}\) is the class of one-element algebras. Therefore, since \(\mathsf {PS} \le \mathsf {SP}\), we obtain

$$\begin{aligned} \mathsf {Vd}Si({\mathcal {V}}) \subseteq \mathsf {P_S}(\mathsf {Sd}Si({\mathcal {V}}) \cup {\mathcal {T}})\subseteq \mathsf {SP}(\mathsf {Sd}Si({\mathcal {V}}) \cup {\mathcal {T}}) \subseteq \mathsf {SPd}Si({\mathcal {V}}) \cup {\mathcal {T}}. \end{aligned}$$

By Lemma 5.7, \(\mathsf {Pd}Si({\mathcal {V}}) \subseteq \mathsf {dP}Si({\mathcal {V}}) \), so

$$\begin{aligned} \mathsf {Vd}Si({\mathcal {V}}) \subseteq \mathsf {SdP}Si({\mathcal {V}}) \cup {\mathcal {T}} \subseteq \mathsf {Sd}{\mathcal {V}} \end{aligned}$$

We now show that \(\mathsf {HSP_U}{\mathsf {d}}Si({\mathcal {V}})\subseteq \mathsf {Sd}Si({\mathcal {V}}) \cup {\mathcal {T}}\), as promised. First we show that \(\mathsf {Sd}Si({\mathcal {V}})\) is closed under \(\mathsf {P_U}\). By the fact that \(\mathsf {P_U S} \le \mathsf {S P_U}\) and Lemma 5.7, \(\mathsf {P_U} (\mathsf {Sd}Si({\mathcal {V}}))\subseteq \mathsf {SP_U} \mathsf {d}Si({\mathcal {V}})\subseteq \mathsf {S I d P_U}Si({\mathcal {V}})\). We know that the term \(\top {\backslash }x {/}\top \) is a unary discriminator term for \(Si({\mathcal {V}})\). Since that property is a first-order condition, it is preserved under \(\mathsf {P_U}\). Therefore, all algebras in \(\mathsf {P_U}Si({\mathcal {V}})\) have the same unary discriminator term, hence they are all simple. So, \(\mathsf {P_U}Si({\mathcal {V}}) \subseteq Si({\mathcal {V}})\) and thus \(\mathsf {P_U} (\mathsf {Sd}Si({\mathcal {V}}))\subseteq \mathsf {SId}Si({\mathcal {V}})\). Since \(Si({\mathcal {V}})\) is closed under I, by Lemma 5.7(4) we get that \(\mathsf {SId}Si({\mathcal {V}})=\mathsf {Sd}Si({\mathcal {V}})\). Furthermore, by Lemma 5.10, all algebras in \(\mathsf {Sd}Si({\mathcal {V}})\) are simple, so the class \(\mathsf {Sd}Si({\mathcal {V}})\), together with the one-element algebra, is closed under \({\mathsf {H}}\). Finally, \(\mathsf {Sd}Si({\mathcal {V}}) \cup {\mathcal {T}}\) is obviously closed under \({\mathsf {S}}\). \(\square \)

Corollary 5.12

The class \(\mathsf {SdRA}\) is a discriminator variety with unary discriminator term \(\top {\backslash }x{/}\top \).

This variety contains all relation algebras and also all algebras of weakening relations that we saw in the introduction.

6 Weakening relations

We now use the double-division conucleus to construct several interesting classes of GBI-algebras.

6.1 Weakening relations as double division conuclear images of relation algebras

Given a poset \(\mathbf{P}=(P, \le )\), let

$$\begin{aligned} Wk (\mathbf{P})=\{R\subseteq P\times P:{\le }\mathbin {;}R\mathbin {;}{\le }\subseteq R\} \end{aligned}$$

where ;  denotes relation composition. The relations in \( Wk (\mathbf{P})\) are called \(\le \)-weakening relations. An equivalent definition is \( Wk (\mathbf{P})= {\mathcal {O}}(\mathbf{P} \times \mathbf{P}^\partial )\), where \({\mathcal {O}}\) denotes the map that sends a poset to its order-ideals (or downsets). The set of weakening relations is a GBI-algebra \(\mathbf {Wk}(\mathbf{P})\) under union and intersection, composition of relations, complement-converse and an intuitionistic implication, as we prove below. Any binary relation S on P generates a smallest weakening relation \(\gamma _\le (S)={\le }\mathbin {;}S\mathbin {;}{\le }\) that includes S. If \(\mathbf{P}\) is an antichain then \(\mathbf {Wk}(\mathbf{P})\) is the algebra \(\mathbf {Rel} (P)\) of all binary relations on P. If \(\mathbf{P}\) is a chain, on the other hand, such relations are “left-up” closed when graphed on the “xy-plane” \(P\times P\). For example, if S is the graph of a monotone function then the left-up-closure \(\gamma _\le (S)\) is all points in the xy-plane that are on the graph, above the graph or to the left of the graph. In the finite case, a monotone function can be recovered from its left-up-closure R by mapping an element \(x\in P\) to the smallest element of \(\{y:x \mathrel {R} y\}\).

Given a poset \(\mathbf{P}=(P, \le )\), we let \(\mathbf{A}=\mathbf {Rel} (P)\) be the cyclic involutive GBI algebra of all binary relations on the set P, known as the full relation algebra on P. Note that \(p= \le \) is a positive idempotent element of \(\mathbf{A}\), since \(\le \) is reflexive and transitive. The following result shows that full weakening relations are exactly the double-division conucleus images of full relation algebras.

Lemma 6.1

If \(\mathbf{P}=(P, \le )\) is a poset, then \(\mathbf {Wk}(\mathbf{P})={\le } {\backslash }\mathbf {Rel} (P) {/}{\le }\) and it is a cyclic involutive GBI-algebra. The operations are as follows: \(\wedge \) is intersection, \(\vee \) is union, \(\cdot \) is composition, \({\sim }\) is complement-converse, 1 is \(\le \), 0 is \(\not \ge \), \(\top =P \times P\), \(\bot = \emptyset \), and \(R \mathbin {\rightarrow }S = {\le } {\backslash }(R^c \cup S) {/}{\le }= ({\not \ge } \mathbin {;} (R \cap S^c) \mathbin {;} {\not \ge })^c\).

Proof

A relation R on P is a weakening relation if \({\le } \mathbin {;} R \mathbin {;} {\le } \subseteq R\). Since the other inclusion follows from the reflexivity of \(\le \), we get \({\le } \mathbin {;} R \mathbin {;} {\le } = R\), so the weakening relations are exactly the fixed points of \(\gamma _\le \). Since \(\mathbf {Rel} (P)\) is a cyclic involutive GBI-algebra, so is \(\mathbf {Wk}(\mathbf{P})\). By Theorem 5.5(3) the operations \(\wedge , \vee , \circ , {\sim }\) on \({\le } {\backslash }\mathbf {Rel} (P) {/}{\le }\) are the restrictions of the ones in \(\mathbf {Rel}(P)\), so they are intersection, union, composition and complement-converse. \(\square \)

Note that in general neither the complement nor the converse of a weakening relation is again a weakening relation. Also note that for weakening relations R and S, the above definition of the implication can be explicitly given by

$$ \begin{aligned} R \mathbin {\rightarrow }S=\{(x,y): \forall u,v (u \le x \; \& \; y \le v \; \& \; u \mathrel {R} v \Rightarrow u \mathrel {S} v)\} \end{aligned}$$

and

$$ \begin{aligned} \lnot R= \{(x,y): \forall u,v (u \le x \; \& \; y \le v \Rightarrow u \not \mathrel {R} v)\}. \end{aligned}$$

We call \(\mathbf {Wk}(\mathbf{P})\)the full weakening relation algebra on the poset P. Note that full weakening relation algebras are exactly the double-division conuclear images of full relation algebras with respect to partial-order relations. A positive idempotent in a full relation algebra is only a preorder (i.e., a reflexive and transitive relation). However, a double-division conuclear image with respect to a preorder \((Q,\sqsubseteq )\) is isomorphic to the full weakening relation algebra \(\mathbf {Wk}(Q/{\equiv },\le )\) where \(\equiv \) is the equivalence relation determined by the preorder and \(\le \) is the partial order induced on the equivalence classes by \(\sqsubseteq \). This observation is expressed in symbols by \(\mathsf {IFWkRA}=\mathsf {Id}(\mathsf {FRA})\) where \(\mathsf {FWkRA}\) is the class of full weakening relation algebras and \(\mathsf {FRA}\) is the class of full relation algebras.

Recall that representable relational algebras are defined as algebras isomorphic to subalgebras of products of full relation algebras; in symbols \(\mathsf {RRA}=\mathsf {ISP}(\mathsf {FRA})\). In that spirit, we define representable weakening relation algebras as algebras isomorphic to subalgebras of products of full weakening relation algebras; in symbols \(\mathsf {RWkRA}=\mathsf {ISP}(\mathsf {FWkRA})=\mathsf {ISPd}(\mathsf {FRA})\). Note that \(\mathsf {Sd}(\mathsf {RRA})=\mathsf {SdISP}(\mathsf {FRA}) \subseteq \mathsf {ISPd}(\mathsf {FRA}) \subseteq \mathsf {Vd}(\mathsf {RRA}) = \mathsf {VSd}(\mathsf {RRA}) = \mathsf {Sd}(\mathsf {RRA})\), since the latter is a variety by Theorem 5.11. Therefore, \(\mathsf {RWkRA}=\mathsf {Sd}(\mathsf {RRA})\), namely the representable weakening algebras are precisely the subalgebras of conuclear images of representable relation algebras.

Corollary 6.2

  1. (1)

    \(\mathsf {RWkRA}\) is a discriminator variety whose simple members are subalgebras of full weakening relation algebras.

  2. (2)

    \(\mathsf {RRA}\) is the subvariety of \(\mathsf {RWkRA}\) defined by \(\lnot \lnot x=x\).

  3. (3)

    The class \(\mathsf {RWkRA}\) is not finitely axiomatizable relative to the variety of all CyInGBI-algebras.

Proof

(1) It follows from Theorem 5.11.

(2) We first note that if \(\mathbf{P}\) is a poset that is not an antichain then \(\mathbf {Wk}(\mathbf{P})\) is not Boolean. Indeed, assume \(a<b\) in \(\mathbf{P}\). Then \( R= \{(u,v): u \le a \; \& \; b \le v\}\) is a weakening relation; note that \(R^c= \{(u,v): u \not \le a \text { or } b \not \le v\}\) . Using the formula after Lemma 6.1 we have

$$ \begin{aligned} \lnot R&=\{(x,y):\forall u,v(u \not \le x \text { or } y\not \le v \text { or } u \not \le a \text { or } b \not \le v\}\\&=\{(x,y):\forall u(u \not \le x \text { or } u\not \le a)\text { or }\forall v(y\not \le v \text { or } v\not \le b)\}\\&=\{(x,y): \not \exists u(u \le x \; \& \, u\le a)\text { or }\not \exists v(y \le v \; \& \, v\le b)\}\\&=\{(x,y): \mathord {\downarrow }x \cap \mathord {\downarrow }a = \emptyset \text { or } \mathord {\uparrow }y \cap \mathord {\uparrow }b = \emptyset \}. \end{aligned}$$

Then (ba) is not in \(R \cup \lnot R\), hence \(\lnot \) is not classical complementation. Stated contrapositively, if the intuitionistic negation \(\lnot \) on a full weakening relation algebra is Boolean, then the algebra is a full relation algebra. Conversely, it is clear that a full relation algebra satisfies \(\lnot \lnot x=x\).

(3) If \(\mathsf {RWkRA}\) would be finitely axiomatizable, then \(\mathsf {RRA}\) would be as well by (2). \(\square \)

We mention a simple identity that holds in \(\mathsf {RWkRA}\), but not in all of \(\mathsf {CyInGBI}\), as it fails in the 3-element MV-algebra. In RRA this result reduces to the observation that all relations below the identity relation form a Boolean algebra.

Lemma 6.3

The variety \(\mathsf {RWkRA}\) satisfies the property that the interval \([0 \wedge 1, 1]\) is a Boolean lattice and this can be written equationally.

Proof

We prove this result for a full representable weakening relation algebra \(\mathbf {Wk}(\mathbf{P})\). In such an algebra 1 is the \(\le \) relation and 0 is \(\not \ge \). So

$$\begin{aligned} (x,y) \in 1\wedge 0\ \Leftrightarrow \ (x \le y\hbox { and }x \not \ge y)\ \Leftrightarrow \ (x \le y\hbox { and }x \not = y)\ \Leftrightarrow \ x < y. \end{aligned}$$

Therefore, the relations in the interval between < and \(\le \) are precisely the relations of the form \({<} \cup \{(a,a): a \in X\}\) for different subsets X of P. These relations are weakening relations and they clearly form a Boolean lattice isomorphic to \({\mathcal {P}}(X)\).

Furthermore, complementation in the Boolean lattice \([0 \wedge 1, 1]\) is given by the term \({\sim }x \wedge 1\). Indeed, if \(R={<} \cup \Delta _X\) for some subset X of P, where \(\Delta _X = \{(a,a): a \in X\}\), then \({\le } \cap {\sim }R= {\le } \cap ({<} \cup \Delta _X)^{\smallsmile c}={\le } \cap {<}^{\smallsmile c} \cap (\Delta _X)^{\smallsmile c} = {\le } \cap {\not >} \cap (\Delta _X)^c = {\le } \cap (\Delta _X)^c \), because \({\le } \subseteq {\not >}\). Since \((x,y) \in (\Delta _X)^c\) means that (\(x = y \Rightarrow x \not \in X\)) it follows that \({\le } \cap {\sim }R={<} \cup \Delta _{X^c}\), which is clearly the complement of \(R={<} \cup \Delta _X\) in \([0 \wedge 1, 1]\).

The equations can be obtained as follows. First notice that any element of \([0 \wedge 1, 1]\) can be written as \(x_{01}=(0 \wedge 1) \vee (x \wedge 1)\). Then for those elements we have that the term \({\sim }x \wedge 1\) is the complement \(x_{01}\) in \([0 \wedge 1, 1]\) since \(x_{01} \wedge ({\sim }x_{01} \wedge 1) = 0 \wedge 1\) and \(x_{01} \vee ({\sim }x_{01} \wedge 1) = 1\). \(\square \)

As we show below in Lemma 6.4, when \(\mathbf{P}\) is a chain the identity \({0 \le 1}\) holds in \(\mathbf {Wk}(\mathbf{P})\) and the previous result specializes to the fact that the interval [0, 1] is a Boolean lattice. The more general result that in \({\textsf {RWkRA}}\) the interval \([0 \wedge 1, 0 \vee 1]\) is a Boolean lattice fails. To see this take \(P=\{a, b, c\}\) with \(c<a\) and both incomparable to b. Then \(1 \wedge 0 = {<}\) as above, and \(1 \vee 0\) is \(\le \cup \; {||}\), where || is the incomparability relation. Elements of the interval are relations of the form \({<} \cup \{(a,a): a \in X\} \cup I\), where I is a collection of incomparable pairs and \(X \subseteq P\). However, not all such relations are allowed because the pairs (ab) and (cb) are both incomparable pairs, but the first is smaller than the second.

Weakening relations on chains are even more special.

Lemma 6.4

The representable weakening relation algebras on chains are exactly the ones that satisfy the identity \(0 \le 1\).

Proof

Recall that in \( Wk (\mathbf{P})\) we have \(1= {\le }\) and \(0={\not \ge }\). If \(\mathbf{P}\) is totally ordered then \(0 = {<}\), so \(0 \le 1\). Conversely, if \(0 \le 1\), then \(x \not \ge y \Rightarrow x \le y\), hence \(x \ge y\) or \( x \le y\), which shows that \(\mathbf{P}\) is a total order. \(\square \)

We will show in the next section that they also satisfy the identity that multiplication distributes over meet. Further results can be found in [14].

Lemma 6.5

If \(\delta \) is a weak topological conucleus on a cyclic involutive GBI-algebra \(\mathbf{A}\) that preserves the linear negation, and \(\lnot {\sim }x \le {\sim }\lnot x\) holds in \(\mathbf{A}\) then it also holds in \(\mathbf{A}_\delta \). In particular this is true for the double-division conucleus and for relation algebras, so \(\lnot {\sim }x \le {\sim }\lnot x\) holds in \(\mathsf {SdRA}\).

Proof

By assumption \({\sim }_\delta x= {\sim }x\) and \(\lnot _\delta x= \delta (\lnot x)\). So, \(\lnot _\delta {\sim }x = \delta (\lnot {\sim }x) \le \lnot {\sim }x \le {\sim }\lnot x \le {\sim }\delta (\lnot x) = {\sim }\lnot _\delta x\), where we used the contracting property of \(\delta \) and the order reversal property of \({\sim }\). \(\square \)

Note that the variety \(\mathsf {SdRA}\) is a variety that contains all relation algebras and also all representable weakening relation algebras. It deserves to be called the variety of (abstract) weakening relation algebras. Also, it is a discriminator variety with unary discriminator term \(\top {\backslash }x {/}\top \) and that is the only term needed for congruence generation on lattice filters to yield congruence filters. At the moment no axiomatization is known for this variety.

6.2 Weakening relations as residuated maps

Here we provide an alternative characterization of \( Wk (\mathbf{P})\). Recall that a map on f on a poset \(\mathbf{P}\) is called residuated if there exists a map \(f^*\) on P such that \(f(x) \le y\) iff \(x \le f^*(y)\), for all \(x,y \in P\). The map \(f^*\), if it exists, is unique and is called the residual of f. For a subset D of P, we let \(D^u=\{x:\forall y\in D, y\le x\}\) denote the set of all common upper bounds of D.

For a complete join semilattice \(\mathbf{L}\), \(Res(\mathbf{L})\) denotes the residuated lattice of all residuated maps on \(\mathbf{L}\). Under pointwise order, composition, identity and appropriately defined divisions, it forms a residuated lattice \(\mathbf {Res}(\mathbf{L})\) [6].

Lemma 6.6

Given a poset \(\mathbf{P}\), we have \(\mathbf {Wk}(\mathbf{P}) \cong \mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\). The operations \(\wedge ,\vee ,\cdot ,1,0,{\sim }\) on \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) are given by pointwise meet and join, composition, the identity function, the function \(0(D)=((D)^u)^c\) and

$$\begin{aligned} ({\sim }f)(D)=\{y \in P : \exists x \in D, x \not \in f(\mathord {\downarrow }y)\}, \end{aligned}$$

for all \(f \in Res({\mathcal {O}}(\mathbf{P}^\partial ))\) and \(D \in {\mathcal {O}}(\mathbf{P}^\partial )\).

Proof

Every relation R in \( Wk (\mathbf{P})={\mathcal {O}}(\mathbf{P} \times \mathbf{P}^\partial )\) can be identified with a function \(f_R: P \mathbin {\rightarrow }{\mathcal {P}}(P)\) defined by \(f_R(x)=\{y \in P : x \mathrel {R} y\}\), the forward image of R, and R can be recovered by taking the pairs (xy) such that \(y \in f_R(x)\). The condition that R is closed upwards on its second coordinate, translates exactly to the fact that the values \(f_R(x)\) are actually upward closed as subsets of P, hence they are downsets of \(\mathbf{P}^\partial \). So, we can write \(f_R: P \mathbin {\rightarrow }{\mathcal {O}}(\mathbf{P}^\partial )\). Furthermore, the condition that R is closed downwards on its first coordinate is equivalent to the fact that smaller inputs of x give bigger sets \(f_R(x)\), or equivalently that \(f_R\) is an order-preserving function from \(\mathbf{P}^\partial \). In summary weakening relations R correspond exactly to order-preserving functions \(f_R: \mathbf{P}^\partial \mathbin {\rightarrow }{\mathcal {O}}(\mathbf{P}^\partial )\), where the codomain is ordered under inclusion. Furthermore, this correspondence preserves the usual orders on relations and on functions, so \(\mathbf {Wk}(\mathbf{P})\) and \(({\mathcal {O}}(\mathbf{P}^\partial ))^{\mathbf{P}^\partial }\) are isomorphic as posets.

Now functions \(f: \mathbf{P}^\partial \mathbin {\rightarrow }{\mathcal {O}}(\mathbf{P}^\partial )\) can be extended to functions \(g_f: {\mathcal {O}}(\mathbf{P}^\partial ) \mathbin {\rightarrow }{\mathcal {O}}(\mathbf{P}^\partial )\) by \(g_f(X)=\bigcup _{x \in X}f(x)\). Note that the function \(g_f\) distributes over arbitrary unions and, since \({\mathcal {O}}(\mathbf{P}^\partial )\) is a complete lattice, \(g_f\) is residuated. Conversely, every residuated map g on \({\mathcal {O}}(\mathbf{P}^\partial )\) is completely specified by its restriction \(f(x)=g(\mathord {\downarrow }x)\) on \(\mathbf{P}^\partial \); we identify \(\mathbf{P}^\partial \) in \({\mathcal {O}}(\mathbf{P}^\partial )\) by identifying x and \(\mathord {\downarrow }x\). Furthermore, the orders of these functions correspond, so the posets \(({\mathcal {O}}(\mathbf{P}^\partial ))^{\mathbf{P}^\partial }\) and \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) are isomorphic as posets.

In summary if R is a weakening relation on \(\mathbf{P}\) then the corresponding map of \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) is the forward image of R, namely it is given by \(X \mapsto R[X]\). Conversely, given a map f in \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\), then the corresponding relation is given by \(x \mathrel {R}_f y\) iff \(y \in f(\mathord {\downarrow }x)\).

The lattice operations in \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) are pointwise, the multiplication is composition of functions and the identity element is the identity function. The negation constant is obtained from the weakening relation \(0={\ngeq }\).

We follow the process described in the proof of Lemma 6.6 to specify the corresponding function 0. First from \(\not \ge \) we get a function from \(\mathbf{P}^\partial \) to \({\mathcal {O}}(\mathbf{P}^\partial )\) by associating to each \(x \in P\) the downset \(\{y: x \not \ge y\}=(\mathord {\uparrow }x)^c\). Then we extend this to a function from \({\mathcal {O}}(\mathbf{P}^\partial )\) by \(0(D)=\bigcup _{x \in D} (\mathord {\uparrow }x)^c=(\bigcap _{x \in D} \mathord {\uparrow }x)^c=(D^u)^c\). (Note that if \(\mathbf{P}\) is a chain then for all \(D \in {\mathcal {O}}(\mathbf{P}^\partial )\) we have \(D^c \subseteq D^u\) so \(0(D)=(D^u)^c \subseteq (D^c)^c=D=1(D)\), namely \(0 \le 1\), as expected.)

The unary operation \({\sim }\) in \(\mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) can be obtained as follows. For a function \(f \in \mathbf {Res}({\mathcal {O}}(\mathbf{P}^\partial ))\) the corresponding relation is given by \(x \mathrel {R_f} y\) iff \(y \in f(\mathord {\downarrow }x)\). Taking complement converse we get \(x \mathrel {{\sim }R_f} y\) iff \(x \not \in f(\mathord {\downarrow }y)\). Passing to the corresponding map we finally get that \(({\sim }f)(D)=\{y \in P : \exists x \in D, x \not \in f(\mathord {\downarrow }y)\}\). \(\square \)

As a consequence we have the following result.

Corollary 6.7

If \(\mathbf{P}\) is a chain then in \(\mathbf {Wk}(\mathbf{P})\) composition distributes over intersection.

6.3 Distributive \(\ell \)-pregroups (and all \(\ell \)-groups) are RL-subalgebras of representable weakening relation algebras

Let \(\mathbf{P}=(P, {\le })\) be a poset. By \(End(\mathbf{P})\) we denote all order-preserving functions on \(\mathbf{P}\). For \(f \in End(\mathbf{P})\), we define the relation \(\bar{f}\) by \(x \mathrel {\bar{f}} y\mathrel \Leftrightarrow f(x) \le y\). If \(z \le x \mathrel {\bar{f}} y \le w\), then \(z \le x\) and \(f(x) \le y \le w\), so by the order-preservation of f we have \(f(z) \le f(x) \le y \le w\), so \(x \mathrel {\bar{f}} w\). Therefore \(\bar{f} \in Wk (\mathbf{P})\) is a weakening relation and \(\bar{\ } : End(\mathbf{P}) \mathbin {\rightarrow } Wk (\mathbf{P})\) is a well-defined function. Moreover, it is injective, because if \(\bar{f}=\bar{g}\), then \(f(x) \le y\) if and only if \(g(x) \le y\), so \(f=g\). Since the operation of \(\mathbf {Wk}(\mathbf{P})\) is composition of relations, we consider on \(\mathbf {End}(\mathbf{P})\) relational composition of functions and set \(f \mathbin {;} g = g \circ f\), hence \((f \mathbin {;} g)(x)=(g \circ f)(x)=g(f(x))\).

For a chain \(\mathbf{P}\), \(F(\mathbf{P})\) denotes the subset of \(End(\mathbf{P})\) of all maps f that have a residual \({\sim }f\) and that has a residual \({\sim }{\sim }f\), etc, and also that have a dual residual \({-}f\) and that has a dual residual \({-}{-}f\) etc, for ever. By endowing this set with pointwise lattice operations from \(\mathbf{P}\), composition of functions, identity the identity map on P, and involutions \({\sim }\) and \({-}\) as above, we obtain an involutive residuated lattice \(\mathbf{F}(\mathbf{P})\) in which addition coincides with multiplication and the negation constant with the identity; such structures are called \(\ell \)-pregroups. The \(\ell \)-pregroup \(\mathbf{F}(\mathbf{P})\) is distributive and, as shown in [7], all distributive \(\ell \)-pregroups can be embedded in one of this form. This generalizes the Holland embedding theorem for \(\ell \)-groups embedding into the \(\ell \)-group \(\mathbf {Aut}(\mathbf{P})\) of all order-bijections on a chain, since \(\ell \)-groups are exactly the \(\ell \)-pregroups that are cyclic. For a chain \(\mathbf{P}\), \(\mathbf{F}(\mathbf{P})\) is a isomorphic to a subalgebra of \(\mathbf {End}(\mathbf{P})\) with respect to the lattice and monoid operations.

The following theorem shows that for a chain \(\mathbf{P}\), the distributive \(\ell \)-pregroup \(\mathbf{F}(\mathbf{P}^\partial )\) is isomorphic to a residuated-lattice subalgebra of the weakening relation algebra \(\mathbf {Wk}(\mathbf{P})\). Hence every \(\ell \)-pregroup can be embedded in a weakening relation algebra (as a residuated lattice). That subalgebra does not contain the negation constant \(0 = {\not \ge }\) of the a cyclic involutive residuated lattice \(\mathbf {Wk}(\mathbf{P})\), so it is not a subalgebra as an involutive residuated lattice. However, it is an \(\ell \)-pregroup, being isomorphic to \(\mathbf{F}(\mathbf{P}^\partial )\), and its involutions inside \(\mathbf {Wk}(\mathbf{P})\) are given by taking as negation constant the identity element \({1 ={\le }}\). For a weakening relation \(r \in Wk (\mathbf{P})\) we set \({\sim }_1 r= r {\backslash }1\) and \({-}_1 r = 1 {/}r\), as these will be the involutions in the above-mentioned subalgebra.

Instead of giving a lattice-isomorphism from \(\mathbf{F}(\mathbf{P}^\partial )\) to \(\mathbf {Wk}(\mathbf{P})\) and having to work with the dual order of \(\mathbf{P}\), we give a dual lattice-isomorphism \(\mathbf{F}(\mathbf{P})\) to \(\mathbf {Wk}(\mathbf{P})\), since the \(\ell \)-pregroup \(\mathbf{F}(\mathbf{P}^\partial )\) is isomorphic to the dual of the \(\ell \)-pregroup \(\mathbf{F}(\mathbf{P})\).

Theorem 6.8

Let \(\mathbf{P}\) be a poset.

  1. (1)

    The map \(\bar{\ } : End(\mathbf{P}) \mathbin {\rightarrow } Wk (\mathbf{P})\) is a monoid embedding and a join-to-intersection semilattice embedding.

  2. (2)

    If \(\mathbf{P}\) is a chain, then \(\bar{\ } : End(\mathbf{P}) \mathbin {\rightarrow } Wk (\mathbf{P})\) is further a lattice embedding (sending meet to union).

  3. (3)

    The map restricts to \(\bar{\ } : F(\mathbf{P}) \mathbin {\rightarrow } Wk (\mathbf{P})\) and as such it is a residuated-lattice embedding.

  4. (4)

    For every \(f \in F(\mathbf{P})\), \(\overline{{\sim }f} = {\sim }_1 \bar{f}\) and \(\overline{{-}f}= {-}_1 \bar{f}\).

Proof

(1) Observe that if id denotes the identity map on \(\mathbf{P}\), then \(x \mathrel {\overline{id}} y\) iff \(id(x) \le y\) iff \(x \le y\). So, \(\overline{id}= {\le }\), and \(\bar{\ }\) preserves the identity element.

We have \(x \mathrel {(\bar{g} \mathbin {;} \bar{f})} y\) iff there exists a z such that \(x \mathrel {\bar{g}} z\) and \(z \mathrel {\bar{f}} y\) iff \(g(x) \le z\) and \(f(z)\le y\). Using the order-preservation of f, this implies that \(f(g(x)) \le f(z) \le y\), but also conversely if \(f(g(x)) \le y\) then we can chose \(z=g(x)\) in the preceding sentence. Since \(f(g(x)) \le y\) iff \((g \mathbin {;} f)(x) \le y\) iff \(x \mathrel {\overline{g \mathbin {;} f}} y\), we get that \(\bar{g} \mathbin {;} \bar{f} = \overline{g \mathbin {;} f}\). Therefore, \(\bar{\ }\) is a monoid homomorphism.

We have \(x \mathrel {\overline{f \vee g}} y\) iff \((f \vee g)(x) \le y\) iff \(f(x) \vee g(x) \le y\) iff \(f(x), g(x) \le y\) iff \(x \mathrel {\bar{f}} y\) and \(x \mathrel {\bar{g}} y\). So, \(\overline{f \vee g} =\bar{f} \cap \bar{g}\). So, \(\bar{\ }\) is a dual semilattice homomorphism.

(2) If we further assume that \(\mathbf{P}\) is a chain, then \(x \mathrel {\overline{f \wedge g}} y\) iff \((f \wedge g)(x) \le y\) iff \(f(x) \wedge g(x) \le y\) iff \(f(x) \le y\) or \(g(x) \le y\) iff \(x \mathrel {\bar{f}} y\) or \(x \mathrel {\bar{g}} y\). So, \(\overline{f \wedge g} = \bar{f} \cup \bar{g}\). Therefore, \(\bar{\ }\) is a dual lattice homomorphism (sending meets to unions and joins to intersections).

(3) For \(f, g \in F(\mathbf{P})\) we compute \(\bar{f} {\backslash }\bar{g}\), as the other is done in a similar way. Writing \(\gamma (x,y)\) for \(\gamma _\le (\{(x,y)\}\), we have

$$\begin{aligned}&(x,y) \in \bar{f} {\backslash }\bar{g}\ \Leftrightarrow \ \gamma (x,y) \subseteq \bar{f} {\backslash }\bar{g}\ \Leftrightarrow \ \bar{f} \mathbin {;} \gamma (x,y) \subseteq \bar{g}\\&\quad \Leftrightarrow \ \forall z,w,\ (z,w) \in \bar{f} \mathbin {;} \gamma (x,y) \Rightarrow (z,w) \in \bar{g}\\&\quad \Leftrightarrow \ \forall z,w,\ (\exists u,\ (z,u) \in \bar{f}\text { and }(u,w) \in \delta (x,y)) \Rightarrow (z,w) \in \bar{g}\\&\quad \Leftrightarrow \ \forall z,w,\ (\exists u,\ f(z) \le u\text { and }u \le x\text { and }y \le w) \Rightarrow g(z) \le w\\&\quad \Leftrightarrow \ \forall z,w,\ f(z) \le x\text { and }y \le w \Rightarrow g(z) \le w\\&\quad \Leftrightarrow \ \forall z,\ f(z) \le x \Rightarrow g(z) \le y\\&\quad \Leftrightarrow \ \forall z,\ z \le ({\sim }f)(x) \Rightarrow z \le ({\sim }g)(y)\\&\quad \Leftrightarrow \ ({\sim }f)(x) \le ({\sim }g)(y)\\&\quad \Leftrightarrow \ g(({\sim }f) (x)) \le y \ \Leftrightarrow \ ({\sim }f) \mathbin {;} g(x) \le y\ \Leftrightarrow \ (x,y) \in \overline{({\sim }f) \mathbin {;} g}. \end{aligned}$$

So, we have \(\bar{f} {\backslash }\bar{g}=\overline{({\sim }f) \mathbin {;} g}=\overline{({\sim }f) + g}=\overline{f {\backslash }g}\).

(4) We have \(\overline{{\sim }f}= \overline{f {\backslash }1}=\bar{f} {\backslash }\bar{1}=\bar{f} {\backslash }{\le } = {\sim }_1 f\). The other equation is proved analogously. \(\square \)

Corollary 6.9

If \(\mathbf{P}\) is a chain, then \(\mathbf {Wk}(\mathbf{P})\) has a residuated lattice subalgebra isomorphic to \(\mathbf{F}(\mathbf{P}^\partial )\). The involutions of the subalgebra that make it into an \(\ell \)-pregroup are given by \({\sim }_1 r= r {\backslash }1\) and \({-}_1 r = 1 {/}r\).

Corollary 6.10

Every distributive \(\ell \)-pregroup embeds as a residuated lattice in a full weakening relation algebra over a chain. Moreover, the negation constant in the image is the identity element (hence the involutions of the \(\ell \)-pregroup are given in its image by choosing as negation constant the identity element).

7 Examples of non-involutive GBI-algebras

We can take \(\mathbf{A}\) to be \({\mathcal {P}}(\mathbf{M})\), where \(\mathbf{M}\) is a monoid. The positive idempotent elements (\(1 \le p = p^2\)) of \({\mathcal {P}}(\mathbf{M})\) are exactly the submonoids of \(\mathbf{M}\). If \(\mathbf{M}\) is a group and p a subgroup, then \(p {\backslash }{\mathcal {P}}(\mathbf{M}) {/}p\) is Comer’s [3] double coset construction, which is a special case of the result for relation algebras in Lemma 5.6, when applied to group relation algebras.

We find it useful to define the auxiliary relation \(\le _p\) by \(x \le _p y\) iff \(x = ayb\) for some \(a,b \in p\).

Lemma 7.1

  1. (1)

    The relation \(\le _p\) is a preorder and p is its negative cone.

  2. (2)

    For all \(X \subseteq M\), we have \(\mathord {\downarrow }_p X = pXp\). Therefore, the elements of \(p {\backslash }{\mathcal {P}}(\mathbf{M}) {/}p\) are exactly the downsets of \(\le _p\).

Proof

(1) We have that \(x=1x1\) and \(1 \in p\), so \(x \le _p x\). Also, if \(x \le _p y\) and \(y \le _p z\), then \(x=ayb\) and \(y=czd\), for some \(a,b,c,d \in p\), so \(x=aczdb\) and \(ac, db \in p\), as p is closed under multiplication. Finally, \(x \le _p 1\) iff \(x=a1b\) for some \(a,b \in p\) iff \(x \in p\).

(2) \(y \in \mathord {\downarrow }_p X\) iff \(x \le y\) for some \(x \in X\) iff \(x=ayb\) for some \(x \in X\) and \(a,b \in p\) iff \(y \in pXp\). \(\square \)

Note that if \(\mathbf{M}\) is a group and p is a subgroup, then the preorder relation \(\le _p\) is symmetric, hence an equivalence relation, the equivalence classes of which are the double cosets of [3] and [5]. For more interesting examples, we do not take p to be a group (even though \(\mathbf{M}\) can be a group).

We can take \(M={\mathbb {Z}}\) with addition and \(p={\mathbb {N}}\). Then \(\le _p\) is the converse of the usual order on \({\mathbb {Z}}\) and using the characterization of Lemma 7.1 we get that \({\mathbb {N}} {\backslash }{\mathcal {P}}({\mathbb {Z}}) {/}{\mathbb {N}}\) is isomorphic to \({\mathbb {Z}}\) extended with a top and a bottom element, which is an involutive GBI-algebra.

As another example, where now M is not a group, we can take \(M={\mathbb {N}}\) under addition and \(p=E\), the set of even numbers. Note that the auxiliary relation \(\le _p\) is an order consisting of two disjoint chains, the evens E and the odds O, under the converse of the natural order. The downsets in that order, which by Lemma 7.1 are the fixed sets of the conucleus, are therefore unions of a downset of E and a downset of O. Since the downsets of E under the reverse order are either of the form \(\mathord {\downarrow }e\), for some \(e \in E\) or the empty set, and likewise for O, the downsets of the order are of the form \(\mathord {\downarrow }e \cup \mathord {\downarrow }o\), \(\mathord {\downarrow }e \cup \emptyset \), \(\emptyset \cup \mathord {\downarrow }o\) and \(\emptyset \cup \emptyset \), where we use \(\mathord {\downarrow }\) in the reverse ordering. So we can represent them as pairs (eo) where \(e \in \overline{E}=E \cup \{\emptyset \}\) and \(o \in \overline{O}=O \cup \{\emptyset \}\), where the ordering is the reverse of the usual ordering.

So, \(E {\backslash }{\mathcal {P}}({\mathbb {N}}) {/}E\) is isomorphic to \(\bar{E} \times \bar{O}\) (by identifying \(\mathord {\downarrow }e \cup \mathord {\downarrow }o\) with (eo)). It is easy to see that the operation is given by

$$\begin{aligned} (e_1, o_1) + (e_2, o_2)=((e_1+e_2) \wedge (o_1+o_2), (e_1+o_2) \wedge (o_1+e_2)), \end{aligned}$$

which can further be seen to coincide with matrix multiplication, under the identification

$$\begin{aligned} (e,o) \equiv \left[ \begin{array}{c@{\quad }c} e &{} o \\ o &{} e \end{array} \right] \end{aligned}$$

in the semiring \({\mathbb {N}}\) with multiplication and meet.

As a combination of the two examples we can take \(M={\mathbb {Z}}\) with addition and \(p=E_{{\mathbb {N}}}\), the non-negative evens. Then \(\le _p\) becomes a disjoint union of the two chains \(E_{{\mathbb {Z}}}\) and \(O_{{\mathbb {Z}}}\), with the reverse of the usual order. We can see that indeed p is the negative cone of this order. Then \(E {\backslash }{\mathcal {P}}({\mathbb {N}}) {/}E\) is isomorphic to \((E \cup \{- \infty , + \infty \}) \times (O \cup \{- \infty , + \infty \})\).

If we take \(M={\mathbb {Z}}\times {\mathbb {Z}}\) and \(p=E_{{\mathbb {N}}} \times E_{{\mathbb {N}}}\), then the order ends up being the disjoint union of 4 copies of \({\mathbb {Z}}\times {\mathbb {Z}}\).

We also consider an example that yields a noncommutative GBI-algebra. Consider the monoid \(\mathbf{M}\) on the set \(M=\{1, a, b\}\), where 1 is the identity, \(ab=aa=a\), \(ba=bb=b\) and we consider the submonoid \(p=\{1,a\}\). Then \(a \le _p 1\) and \(a \le _p b\) are the only comparabilities and the downsets of \(\le _p\) are \(\emptyset \subseteq \mathord {\downarrow }a \subseteq \mathord {\downarrow }1, \mathord {\downarrow }b \subseteq M\) (\(\mathord {\downarrow }b\) and \(\mathord {\downarrow }1\) are incomparable); \(\mathord {\downarrow }1\) is the identity element, all elements are idempotents. This yields a non-commutative GBI-algebra, as \((\mathord {\downarrow }a) (\mathord {\downarrow }b) = \mathord {\downarrow }a\) but \((\mathord {\downarrow }b) (\mathord {\downarrow }a) = \mathord {\downarrow }b\).

8 Relativizations

So far we have examined the topological conucleus \(\delta _p\) that produces interesting classes of algebras when applied to the varieties RA, RRA or any \(\top {\backslash }x{/}\top \)-discriminator subvariety of cyclic involutive GBI-algebras. We study two more weak conuclei and see that they apply to GBI-algebras.

8.1 Meet conucleus

For a relation algebra \(\mathbf{A}\) another standard construction is the relativization \(\mathbf{A}_e=({\downarrow }e, \wedge ,\vee ,\rightarrow _e,\top _e,\bot ,\cdot ,1_e,{\sim })\), where \(e\in A\) is an equivalence element (\(e=e^2=e^\smallsmile \)), \(x\rightarrow _e y=(x\rightarrow y)\wedge e\), \(\top _e=e\) and \(1_e=1\wedge e\). Note that \(e^\smallsmile \) is defined as \(\lnot {\sim }e\), and that e is not necessarily reflexive (i.e., positive).

We now show that relativization can be generalized to all residuated lattices and GBI-algebras, and that it is again a topological weak conucleus. For a residuated lattice \(\mathbf{A}\) and \(p\in A\), define \(\mu _p(x)=x\wedge p\). Since this map satisfies \(x\le \mu _p(x)=\mu _p(\mu _p(x))\) and \((x\wedge p) \wedge (y\wedge p)=(x\wedge y)\wedge p\) it is always a topological interior operator.

Lemma 8.1

The map \(\mu _p\) is a topological weak conucleus on a residuated lattice or GBI-algebra if and only if p is square-decreasing, i.e., \(p^2\le p\).

Proof

If \(p^2\le p\) then \((x\wedge p)(y\wedge p)\le xy\) and \((x\wedge p)(y\wedge p)\le pp\le p\), hence \(\mu _p(x)\cdot \mu _p(y)\le \mu _p (xy)\). As noted above, \(\mu _p\) is always a topological interior operator, hence it is a topological weak conucleus.

Conversely, if \(\mu _p\) is a weak conucleus then substituting p into \(\mu _p(x)\cdot \mu _p(y)\le \mu _p (xy)\) gives \(pp\le pp\wedge p\le p\). \(\square \)

For a residuated lattice or GBI-algebra \(\mathbf{A}\) and a square decreasing element \(p\in A\) define the relativization by p as the conuclear image of A under \(\mu _p\). The following result follows from [10], Prop. 3.41.

Theorem 8.2

For a residuated lattice or a GBI-algebra \(\mathbf{A}\) and a square-decreasing element p satisfying \(x \le (p \wedge 1)x(p \wedge 1)\) for all negative \(x \le p\) in A, the conuclear image \(\mathbf{A}_p\) is again a residuated lattice or a GBI-algebra.

Proof

The condition \(x \le (p \wedge 1)x(p \wedge 1)\) for all negative \(x \le p\) in A is equivalent to the demand that \(p \wedge 1\) is the unit element for the conuclear image \(\mathbf{A}_p\). \(\square \)

8.2 Multiplication conucleus

In this section we will obtain an internal characterization of homomorphic images of residuated lattices and GBI-algebras whose congruences are finitely generated. In particular, this applies to finite and more generally to complete algebras, since their convex normal subalgebras have a smallest element.

Given a residuated lattice \(\mathbf{A}\) and an element \(p \in A\), we define the map \(m_p\) on A by \(m_p(x)= xp\), and its image is \(Ap=\{ap :a \in A\}\).

Lemma 8.3

Let \(\mathbf{A}\) be a residuated lattice and \(p \in A\).

  1. (1)

    The map \(m_p(x)\) is a weak conucleus on \(\mathbf{A}\) if and only if p is negative and idempotent. Under these conditions p is a right unit for Ap.

  2. (2)

    Under the same conditions, p is a left unit if and only if \(pxp=xp\) for all \(x \in A\), or equivalently, if \(xp \le px\).

  3. (3)

    The map \(m_p(x)= xp\) is topological if and only if \((x \wedge y)p=xp \wedge yp\) for all \(x,y \in A\).

Proof

(1) That \(xp \le p\) for all \(x \in A\) is equivalent to \(p \le 1\). The map \(m_p\) is monotone since multiplication is order-preserving. It is idempotent if and only if \(xpp=xp\) for all \(x \in A\) if and only if \(pp=p\). Finally, p is a right unit as for all \(xp \in Ap\) we have \(xpp=xp\).

(2) Note that \(pxp=xp\) is equivalent to \(xp \le pxp\), since the reverse inclusion follows from the fact that p is negative. Now, if we assume \(xp \le px\), then \(xp=xpp \le pxp\). Conversely, \(xp \le pxp \le px\).

(3) The condition is just a restatement of the preservation of meet under \(m_p\). \(\square \)

If \(\mathbf{A}=(A, \wedge , \vee , \cdot , {\backslash }, {/}, 1)\) is a residuated lattice and \(p \in A\), we define \(\mathbf{A} p=(Ap, \wedge _p, \vee , \cdot , {\backslash }_p, {/}_p, p)\), and if \(\mathbf{A}\) is a GBI-algebra then \(\mathbf{A} p\) is defined to further include the operations \(x \mathbin {\rightarrow }_p y = (x \mathbin {\rightarrow }(y {/}p)) p\) and \(\top _p=\top p\). Note that this definition of the implication is much more general than the standard definition of the implication for topological weak conuclear images, since we do not assume that the operator \(m_p\) is topological (which by Lemma 8.3 is the condition \((x \wedge y)p=xp \wedge yp\) for all \(x,y \in A\)); adding this assumption, would yield a simplified definition of meet and of implication in the conuclear image, as usual. Versions of the next two results, restricted to residuated lattices, are also in [13].

Lemma 8.4

If p is a negative idempotent element of \(\mathbf{A}\) that satisfies \(xp \le px\) for all \(x \in A\), then \(\mathbf{A} p\) is a residuated lattice. If \(\mathbf{A}\) is a GBI-algebra, then \(\mathbf{Ap}\) is also a GBI-algebra.

Proof

It follows from Lemma 8.3 that \(\mathbf{Ap}\) is a residuated lattice-ordered semigroup. That p is a left unit is clear by Lemma 8.3(2) as every element of Ap is of the form xp for \(x \in A\). For \(x,y,z \in Ap\), we have

$$\begin{aligned} x \wedge _p y\le & {} z\Leftrightarrow (x \wedge y)p \le z \Leftrightarrow x \wedge y \le z {/}p \Leftrightarrow y\\\le & {} x \mathbin {\rightarrow }(z {/}p)\Leftrightarrow y \le (x \mathbin {\rightarrow }(z {/}p))p \end{aligned}$$

and the last condition is equivalent to \(y\le x \mathbin {\rightarrow }_p z\). \(\square \)

We recall that, for a congruence element p of a residuated lattice or a GBI-algebra, the congruence \(\theta _p\) generated by (p, 1) has congruence class of 1 equal to \([1]_{\theta _p}=[p, 1 {/}p]\). We use the notation \(\mathbf{A} / [p, 1 {/}p]\) for \(\mathbf{A} / \theta _p\).

Theorem 8.5

  1. (1)

    If p is a negative idempotent element in a residuated lattice \(\mathbf{A}\) such that \(xp \le px\) for all \(x \in A\), then \(m_p: \mathbf{A} \mathbin {\rightarrow }\mathbf{Ap}\) is a homomorphism with respect to \(\wedge , \vee , \cdot , {\backslash }, 1\).

  2. (2)

    If p is a congruence element of a residuated lattice \(\mathbf{A}\) then \(m_p\) is a residuated-lattice homomorphism and \(\mathbf{Ap}\) is isomorphic to \(\mathbf{A} / [p, 1 {/}p]\).

  3. (3)

    If p is a congruence element on a GBI-algebra \(\mathbf{A}\), then \(m_p: \mathbf{A} \mathbin {\rightarrow }\mathbf{Ap}\) is a GBI-homomorphism and \(\mathbf{Ap}\) is isomorphic to \(\mathbf{A} / [p, 1 {/}p]\).

Proof

(1) First note that \(m_p(1)=p\). For join we have \(m_p(x) \vee m_p(y)=xp \vee yp = (x \vee y)p=m_p(x \vee y)\). Using Lemma 8.3(2) we calculate \(m_p(x) m_p(y)=xp \cdot yp= x \cdot pyp=x \cdot yp=m_p(xy)\). For meet we have

$$\begin{aligned} m_p(x) \wedge _p m_p(y)=xp \wedge _p yp = (xp \wedge yp)p = (x \wedge y)p=m_p(x \wedge y), \end{aligned}$$

where the main equality is justified as follows: \((xp \wedge yp)p \le (x1 \wedge y1)p=(x \wedge y)p\) and \((x \wedge y)p \le xp, yp\), so \((x \wedge y)p = (x \wedge y)pp \le (xp \wedge yp)p\).

For \({\backslash }\), we need to check that \(yp {\backslash }_p xp := (yp {\backslash }xp)p = (y{\backslash }x)p\). We have

$$\begin{aligned} y (yp {\backslash }xp)p \le yp (yp {\backslash }xp) \le xp \le x, \end{aligned}$$

so \((yp {\backslash }xp)p \le y {\backslash }x\), hence \((yp {\backslash }xp)p = (yp {\backslash }xp)pp \le (y {\backslash }x)p\). For the reverse inequality, we note that \(yp (y {\backslash }x)p \le y (y {\backslash }x)p \le xp\), so \((y{\backslash }x)p \le yp {\backslash }xp\) and therefore \((y{\backslash }x)p = (y{\backslash }x)pp \le (yp {\backslash }xp)p\).

(2) For \({/}\) we need to check that \(xp {/}_p yp := (xp {/}yp)p = (x{/}y)p\). We have

$$\begin{aligned} xp(x {\backslash }y)p \le x(x {\backslash }y)p \le yp,\ \text { so }\ (x {\backslash }y)p \le xp {\backslash }yp, \end{aligned}$$

hence \((x {\backslash }y)p= (x {\backslash }y)pp \le (xp {\backslash }yp)\). For the reverse inequality, we need to use the centrality of p: we calculate

$$\begin{aligned} (xp {/}yp)p yp= (xp {/}yp)ypp= (xp {/}yp)yp \le xp \end{aligned}$$

whence \((xp {/}yp)p \le yp {\backslash }xp\), and therefore \((xp {/}yp)p = (xp {/}yp)pp\le (yp {\backslash }xp)p\).

To prove the isomorphism of \(\mathbf{A} / [p, 1 {/}p]\) and \(\mathbf{Ap}\) first note that \(m_p\) is onto, so by the first isomorphism theorem we have that \(\mathbf{A} / {\text {Ker}(m_p)}\) is isomorphic to \(\mathbf{Ap}\). We have \(x \in [1]_{\text {Ker}(m_p)}\) iff \(m_p(x)=p\) iff \(xp=x\) iff (\(p \le xp\) and \(xp \le p\)) iff (\(p \le x\) and \(x \le p {/}p\)) iff \(p \le x \le 1 {/}p\) iff \(x \in [p, 1 {/}p]\). For the equivalence of \(p \le xp\) and \(p \le x\) we used the fact that p is negative idempotent. Also the equality \(p {/}p = 1 {/}p\) follows by \((p {/}p) p \le p \le 1\) and \((1 {/}p)p = (1 {/}p)pp \le 1p=p\). Therefore \([p, 1 {/}p]\) is the equivalence class of 1 under both congruences \(\text {Ker}(m_p)\) and \(\theta _p\), so the two congruences are the same.

(3) Since \(\top \) is the top of A it follows that \(\top p\) is the largest element of \(\mathbf{Ap}\).

Finally for the intuitionistic implication we need to check that \(yp \mathbin {\rightarrow }_p xp := [yp \mathbin {\rightarrow }(xp {/}p)]p = (y\mathbin {\rightarrow }x)p\). We have \([yp \wedge (y\mathbin {\rightarrow }x)p]p \le [y \wedge (y \mathbin {\rightarrow }x)]p \le xp\), which implies \(yp \wedge (y\mathbin {\rightarrow }x)p \le xp {/}p\), hence \((y\mathbin {\rightarrow }x)p \le yp \mathbin {\rightarrow }(xp {/}p)\) and it follows that

$$\begin{aligned} (y\mathbin {\rightarrow }x)p = (y\mathbin {\rightarrow }x)pp \le [yp \mathbin {\rightarrow }(xp {/}p)]p. \end{aligned}$$

For the reverse implication we use the characterization of GBI-congruence elements of Corollary 3.8 (and the consequences mentioned there). We have

$$\begin{aligned}&y \wedge [yp \mathbin {\rightarrow }(xp {/}p)]p = y \wedge [yp \mathbin {\rightarrow }(xp {/}p)]pp= y \wedge p[yp \mathbin {\rightarrow }(xp {/}p)]p\\&\quad ={} yp \wedge [yp \mathbin {\rightarrow }(xp {/}p)]p \le yp \wedge [yp \mathbin {\rightarrow }(xp {/}p)p] \le yp \wedge [yp \mathbin {\rightarrow }xp] \le xp \le x, \end{aligned}$$

hence \([yp \mathbin {\rightarrow }(xp {/}p)]p \le y \mathbin {\rightarrow }x\), and therefore \([yp \mathbin {\rightarrow }(xp {/}p)]p = [yp \mathbin {\rightarrow }(xp {/}p)]pp \le (y \mathbin {\rightarrow }x)p\). \(\square \)