Keywords

1 Introduction

Relation algebras are a kind of Boolean algebras with operators that provide algebraisation of binary relations [20]. The class of all relation algebras, denoted as \(\mathbf{RA}\), consists of algebras of the signature \(\{ 0, 1, +, -, ;, {}^{\smile }, \mathbf{1}' \}\), and all those algebras obey certain axioms. The class of representable relation algebras, \(\mathbf{RRA}\), consists of algebras isomorphic to set relation algebras. \(\mathbf{RRA}\) is a subclass of \(\mathbf{RA}\), but the converse inclusion does not hold. That is, there exist non-representable relation algebras [22]. Moreover, the class \(\mathbf{RRA}\) is not a finitely axiomatisable variety [24] with neither Sahlqvist [29] nor canonical axiomatisation [19]. The problem of determining whether a given finite relation algebra is representable is undecidable, see [12].

For this reason, we are interested in reducts since one may extract more positive results in the aspects of decidability, representability, and finite axiomatisability. There are several results on reducts of relation algebras that have no finite axiomatisation. The examples of non-finitely axiomatisable classes are ordered monoids [10], distributive residuated lattices [1], join semilattice-ordered semigroups [2], meet semilattice-ordered semigroups with converses [18], etc. On the other hand, such classes as representable residuated semigroups [1] and ordered domain algebras [15] are finitely axiomatisable. There are also subsignatures for which the question of finite axiomatisability remains open, see, e.g., [2].

The other direction we discuss is related to finite representability. A finite algebra of relations has the finite representation property if it is isomorphic to some algebra of relations over a finite base. The investigation of this problem is of interest to study such aspects as decidability of membership of \(\mathbf{R}(\tau )\) for finite structures. The finite representation property also implies recursivity of the class of all finite representable \(\tau \)-structures [9], if the whole class is finitely axiomatisable. Here, \(\tau \) is a subsignature of operations and predicates definable in \(\{ 0, 1, +, -, ;, {}^{\smile }, \mathbf{1 } \}\). The examples of the class having the finite representation property are some classes of algebras [9, 15, 23], the subsignature of which contains the domain and range operators. The other kind of algebras of binary relations having the finite representation property is semigroups with so-called demonic refinement has been recently studied by Hirsch and Šemrl [16], but the same authors have recently shown that semigroups with demonic joins fail to have the finite representation property [8].

There are subsignatures \(\tau \) such that the class \(\mathbf{R}(\tau )\) of representable reducts fails to have the finite representation property, for example, \(\{;, \cdot \}\), see [16, Theorem 4.1]. In general, (un)decidability of determining whether a finite relation algebra has a finite representation is an open question [13, Problem 18.18].

In this paper, we consider reducts of relation algebras the signature of which consists of composition, residuals, and the binary relation symbol that denotes partial ordering. That is, we study the class of representable residuated semigroups. We show that \(\mathbf{R}(;, \setminus , /, \le )\) has the finite representation property. As a result, Problem 19.17 of [13] has a positive solution. The solution is based on the Dedekind-MacNeille completions and relational representations of quantales. We embed a finite residuated semigroup into a finite quantale by mapping every element to its lower cone. After that, we apply the relational representation for quantales. As a result, the original finite residuated semigroup has a Zaretski-style representation [30] and this satisfies the finite base requirement.

In the final section, we study the class of representable join semilattice-ordered semigroups, denoted as \(\mathbf{R}(;,+)\). It is already known that this class is not finitely axiomatisable [2]. We show that \(\mathbf{R}(;,+)\) has a recursively enumerable axiomatisation. For that, we define networks and representability games. This class is axiomatised with the axioms of join semilattice-ordered semigroups plus the countable set of universal formulas claiming that \(\exists \) has a winning strategy on every finite step. The question of finite representability for this class remains open, see [27, Problem 2].

2 Definitions

2.1 Relation Algebras and Their Reducts

Let us introduce some basic definitions related to relation algebras. See [13, Section 3] to have more details.

Definition 1

A relation algebra is an algebra \(\mathcal {R} = \langle R, 0, 1, +, -, ;, {}^{\smile }, \mathbf{1 }\rangle \) such that \(\langle R, 0, 1, +, - \rangle \) is a Boolean algebra, \(\langle R, ;, \mathbf{1} \rangle \) is a monoid, and the following equations hold, for all \(a, b, c \in R\):

  1. 1.

    \((a + b) ; c = (a ; c) + (b ; c)\),

  2. 2.

    \(a^{\smile \smile } = a\),

  3. 3.

    \((a + b)^{\smile } = a^{\smile } + b^{\smile }\),

  4. 4.

    \((a ; b)^{\smile } = b^{\smile } ; a^{\smile }\),

  5. 5.

    \(a^{\smile } ; (- (a ; b)) \le - b\).

where \(a \le b\) is defined usually as \(a + b = b\). \(\mathbf{RA}\) is the class of all relation algebras.

Definition 2

A proper relation algebra (or, a set relation algebra) is an algebra \(\mathcal {R} = \langle R, 0, 1, \cup , -, ;, {}^{\smile }, \mathbf{1 }\rangle \) such that \(R \subseteq \mathcal {P}(W)\), where X is a base set, \(W \subseteq X \times X\) is an equivalence relation, \(0 = \emptyset \), \(1 = W\), \(\cup \) and − are set-theoretic union and complement respectively, ;  is relation composition, \({}^{\smile }\) is relation converse, \(\mathbf{1}'\) is the identity relation restricted to W, that is:

  1. 1.

    \( a ; b = \{ (x, z) \in W \, | \, \exists y \, (x, y) \in a \, \& \, (y, z) \in b \}\)

  2. 2.

    \(a^{\smile } = \{ (x, y) \in W \, | \, (y, x) \in a \}\)

  3. 3.

    \(\mathbf{1}' = \{ (x, y) \in W \, | \, x = y \}\)

\(\mathbf{PRA}\) is the class of all proper relation algebras. \(\mathbf{RRA}\) is the class of all representable relation algebras, that is, the closure of \(\mathbf{PRA}\) under isomorphic copies.

Let \(\tau \) be a subset of operations and predicates definable in \(\mathbf{RA}\). \(\mathbf{R}(\tau )\) is the class of subalgebras of \(\tau \)-subreducts of algebras belonging to \(\mathbf{RRA}\). We also assume that \(\mathbf{R}(\tau )\) is closed under isomorphic copies. A \(\tau \)-structure is representable if it is isomorphic to some algebra of relations of this signature. A representable finite \(\tau \)-structure has a finite representation over a finite base if it is isomoprhic to some finite representable over a finite base. \(\mathbf{R}(\tau )\) has the finite representation property if every \(\mathcal {A} \in \mathbf{R}(\tau )\) has a finite representation over a finite base.

2.2 Residuated Semigroups

A residuated semigroup is a structure \(\mathcal {A} = \langle A, ;, \le , \setminus , / \rangle \) such that, for all \(a, b, c \in ~\mathcal {A}\):

  1. 1.

    \(\le \) is reflexive, antisymmetric, and transitive.

  2. 2.

    \(a ; (b ; c) = (a ; b) ; c\).

  3. 3.

    \(a \le b \Rightarrow a ; c \le b ; c\) and \(a \le b \Rightarrow c ; a \le c ; b\).

  4. 4.

    \(b \le a \setminus c \Leftrightarrow a ; b \le c \Leftrightarrow a \le c \, / \, b\).

We can express residuals in every \(\mathcal {R} \in \mathbf{RA}\) using Boolean negation, inversion, and composition as follows:

  1. 1.

    \(a \setminus b = -(a^{\smile } ; -b)\)

  2. 2.

    \(a \, / \, b = - (- a ; b^{\smile })\)

These residuals have the following explicit definition in \(\mathcal {R} \in \mathbf{PRA}\):

  1. 1.

    \(a \setminus b = \{ (x, y) \, | \, \forall z \, (z, x) \in a \Rightarrow (z, y) \in b \}\)

  2. 2.

    \(a \, / \, b = \{ (x, y) \, | \, \forall z \, (y, z) \in b \Rightarrow (x, z) \in a \}\)

One can visualise residuals in \(\mathbf{RRA}\) with the following triangles:

figure a

Thus, in particular, every relation algebra is a residuated lattice.

2.3 Join Semilattice-Ordered Semigroups

A join semilattice-ordered semigroup is an algebra \(\mathcal {A} = \langle A, ;, + \rangle \) such that \(\langle A, ; \rangle \) is a semigroup, \(\langle A, + \rangle \) is a join-semilattice, and the following identities hold, for all \(a, b, c \in A\):

  1. 1.

    \(a ; (b + c) = a ; b + a ; c\),

  2. 2.

    \((a + b) ; c = a ; c + b ; c\).

A join semilattice-ordered semigroup is also a poset and ordering is defined as \(a \le b\) iff \(a + b = b\).

Definition 3

A representation R of a join semilattice-ordered semigroup \(\mathcal {A}\) is a one-to-one map \(R : \mathcal {A} \rightarrow 2^{D \times D}\) (where D is a non-empty base set) such that

  1. 1.

    \((a + b)^R = a^R \cup b^R\),

  2. 2.

    \((a ; b)^R = a^R ; b^R\).

A join semilattice-ordered semigroup \(\mathcal {A}\) is representable, if there exists a representation \(R : \mathcal {A} \rightarrow 2^{D \times D}\) for some non-empty base set D.

2.4 Order-theoretic Definitions

Let us also remind the reader several order-theoretic notions, see [4, Chapter 1] for more details. Let \(\langle P, \le \rangle \) be a partial order. An upper cone generated by x is the set \({\uparrow }\,x = \{ a \in P \, | \, x \le a \}\). Let \(A \subseteq P\), then \({\uparrow }\,A = \bigcup \limits _{x \in A} {\uparrow }\,x = \{ a \in P \, | \, \exists x \in P \, x \le a \}\). The set of all upper cones of a poset \(\langle P, \le \rangle \) is denoted as \({\text {Up}}(P)\). Given \(a \in P\), the lower cone generated by a is a subset \({\downarrow }\,a = \{ x \in P \, | \, x \le a \}\). The lower cone generated by a subset is defined similarly.

A closure operator on a poset \(\langle P, \le \rangle \) is a monotone map \(j : P \rightarrow P\) such that for all \(a \in P\) we have \(a \le j a = j j a\).

2.5 Pseudo-elementary Classes

The following definitions are due to [13, Section 9]. Let \(\mathcal {K}\) be a class of structures of a first-order signature \(\mathcal {L}\). \(\mathcal {K}\) is called a pseudo-elementary class if there are:

  1. 1.

    a two-sorted language \(\mathcal {L}^{s}\) with disjoint sorts \(\mathbf{a}\) and \(\mathbf{r}\) that contains all symbols of \(\mathcal {L}\) as \(\mathbf{a}\)-sorted symbols,

  2. 2.

    an \(\mathcal {L}^{s}\)-theory T, the defining theory.

such that \(\mathcal {K} = \{ \mathcal {M}^\mathbf{a} \upharpoonright _{\mathcal {L}} \, | \, \mathcal {M} \models T \}\). More generally, a pseudo-elementary class is a reduct of an elementary class, see [5].

A pseudo-elementary class is pseudo-universal if

  1. 1.

    a function symbol in \(\mathcal {L}^{s}\) that differs from copies of \(\mathcal {L}\) ones takes values in sort \(\mathbf{r}\),

  2. 2.

    Every sentence in T is built from atomic formulas and negated-atomic formulas using \(\vee \), \(\wedge \), \(\forall x^\mathbf{a}\), \(\forall x^\mathbf{r}\), \(\exists x^\mathbf{r}\).

We are going to use the following fact to axiomatise the class of representable join semilattice-ordered semigroups, see [13, Corollary 9.15, Theorem 9.28]:

Theorem 1

 

  1. 1.

    If \(\mathcal {K}\) is a pseudo-universal class, then \(\mathcal {K}\) is elementary and universally axiomatisable.

  2. 2.

    Let \(\mathcal {K} = \{ \mathcal {M}^\mathbf{a} \upharpoonright _{\mathcal {L}} \, | \, \mathcal {M} \models T \}\) be a pseudo-universal class of \(\mathcal {L}\)-structures, where T is an \(\mathcal {L}^{s}\)-theory and \(\mathcal {L}\), \(\mathcal {L}^{s}\), T are recursively enumerable. Then there exists the set of \(\mathcal {L}\)-sentences \(\{ \eta _n \}_{n < \omega }\) from T such that \(\mathcal {A} \in \mathcal {K}\) iff \(\mathcal {A} \models \{ \eta _n \}_{n < \omega }\). That is, \(\{ \eta _n \}_{n < \omega }\) axiomatises \(\mathcal {K}\).

3 The Finite Representation Property for Residuated Semigroups

The problem we are interested in is the following [13, Problem 19.17]:

$$\text {Does } \mathbf{R}(;, \setminus , /, \le )\text { have the finite representation property?}$$

The class \(\mathbf{R}(;, \setminus , /, \le )\) consists of the following structures, here is the explicit definition:

Definition 4

Let A be a set of binary relations on some base set W such that \(R = \cup A\) is transitive and W is a domain of R. A relational residuated semigroup is an algebra \(\mathcal {A} = \langle A, ;, \setminus , /, \subseteq \rangle \) where, for all \(a, b \in A\):

  1. 1.

    \( a ; b = \{ (x, z) \, | \, \exists y \in W \, ((x, y) \in a \, \& \, (y, z) \in b) \}\),

  2. 2.

    \(a \setminus b = \{ (x, y) \, | \, \forall z \in W \, ((z, x) \in a \Rightarrow (z, y) \in b)\}\),

  3. 3.

    \(a \, / \, b = \{ (x, y) \, | \, \forall z \in W \, ((y, z) \in b \Rightarrow (x, z) \in a)\}\),

  4. 4.

    \(a \le b\) iff \(a \subseteq b\).

A residuated semigroup is called representable if it is isomorphic to some algebra that belongs to \(\mathbf{R}(;, \setminus , /, \le )\).

Definition 5

Let \(\tau = \{ ;, \setminus , /, \le \}\), let \(\mathcal {A}\) be a \(\tau \)-structure and X a base set. An interpretation R over a base X maps every \(a \in \mathcal {A}\) to a binary relation \(a^R \subseteq X \times X\). A representation of \(\mathcal {A}\) is an interpretation R that interprets operations and \(\le \) as above.

Andréka and Mikulás proved the representation theorem for residuated semigroups ([1]) in the step-by-step fashion. See this paper to learn more about step-by-step representations in general [11]. The representation theorem for residuated semigroups obviously implies that the class \(\mathbf{R}(;, \setminus , /, \le )\) is finitely axiomatisable. As it is well known, the logic of such structures is the Lambek calculus [21], so we also have the relational completeness of the Lambek calculus. With our result, we also have a version of the finite model property for the Lambek calculus since one can refute any unprovable sequent in some finite relational residuated semigroup over a finite base. This is a corollary of our result and the fact that the Lambek calculus is complete w.r.t finite residuated semigroups, see [6, Chapter 7, Sect. 7.4] to have an even stronger result.

It is sufficient to show that any finite residuated semigroup has a representation over a finite base in order to show that \(\mathbf{R}(;, \setminus , /, \le )\) has the finite representation property. For that, we will use the representation of residuated semigroups as subalgebras of quantales and the relational representation of quantales.

A quantale is a complete lattice-ordered semigroup. That is, a binary operation respects suprema in both arguments. Quantales have been introduced by Mulvey to provide a noncommutative generalisation of locales, see [25].

Definition 6

A quantale is a structure \(\mathcal {Q} = \langle Q, ;, \varSigma \rangle \) such that \(\mathcal {Q} = \langle Q, \varSigma \rangle \) is a complete lattice, where \(\varSigma \) denotes an infinite join, \(\langle Q, ; \rangle \) is a semigroup, and the following conditions hold for all \(a \in Q\) and \(A \subseteq Q\):

  1. 1.

    \(a \, ; \, \varSigma A = \varSigma \{ a ; q \, | \, q \in A \}\),

  2. 2.

    \(\varSigma A \, ; \, a = \varSigma \{ q ; a \, | \, q \in A \}\).

Definition 7

Given a quantale \(\mathcal {Q} = \langle Q, ;, \varSigma \rangle \), a set of generators is a subset \(G \subseteq \mathcal {Q}\), if

  1. 1.

    For all \(q \in Q\) one has \(q \le \varSigma \{ g \in G \, | \, g \le q \}\),

  2. 2.

    For all \(g \in G\) and \(q_1, q_2 \in \mathcal {Q}\), \(g \le q_1 ; q_2\) implies \(g \le q_1 ; r\) for some \(r \in G\) with \(r \le q_2\).

The existence of a set of generators for an arbitrary quantale has been shown here [3, Lemma 3.12].

Note that any quantale is a residuated semigroup as well. Given a quantale \(\mathcal {Q} = \langle Q, ;, \varSigma \rangle \), One may express residuals with supremum and product as follows for all \(a, b \in Q\):

  1. 1.

    \(a \setminus b = \varSigma \{ c \in Q \, | \, a ; c \le b \}\),

  2. 2.

    \(a \, / \, b = \varSigma \{ c \in Q\, | \, b ; c \le a \}\).

It is readily checked that residuals are unique.

A quantic nucleus is a closure operator on a quantale. Such an operator is a noncommutative generalisation of a nucleus operator from locale theory. The following definition and the proposition below are due to [26, Definition 3.1.1, Theorem 3.1.1] respectively.

Definition 8

A quantic nucleus on a quantale \(\langle A, ;, \varSigma \rangle \) is a mapping \(j : A \rightarrow A\) such that j a closure operator satisfying \(j a ; j b \le j (a ; b)\).

Proposition 1

Let \(\mathcal {A} = \langle A, ;, \varSigma \rangle \) be a quantale and j a quantic nucleus, the set \(\mathcal {A}_j = \{ a \in A \, | \, j a = a \}\) forms a quantale, where \(a ;_j b = j(a ; b)\) and \(\varSigma _j A = j (\varSigma A)\) for all \(a, b \in {A}_j\) and \(A \subseteq \mathcal {A}_j\).

One can embed any residuated semigroup into some quantale with using Dedekind-MacNeille completion (see, for example, [28]) as follows. According to Goldblatt [7], residuated semigroups have the following representation based on quantic nuclei and the Galois connection. We need the construction for the solution, so we discuss it briefly. See Goldblatt’s paper to have a complete argument in more detail [7].

Let \(\mathcal {A} = \langle A, \le , ;, \setminus , / \rangle \) be a residuated semigroup. Then \(\langle \mathcal {P}(A), ;, \bigcup \rangle \) is a quantale with pairwise product of subsets.

Let \(X \subseteq A\). We put lX and uX as the sets of lower and upper bounds of X in A. We also put \(m X = lu X\). Note that the lower cone of an arbitrary x is m-closed, that is, \(m ({\downarrow }\,x) = {\downarrow }\,x\).

\(m : \mathcal {P}(A) \rightarrow \mathcal {P}(A)\) is a closure operator and the set

$$(\mathcal {P}(A))_m = \{ X \in \mathcal {P}(S) \, | \, m X = X\}$$

forms a complete lattice with \(\varSigma _{m} \mathcal {X} = m ( \bigcup \mathcal {X})\) and \(\varPi _{m} = \bigcap \mathcal {X}\), see [4, Theorem 7.3]. The key observation is that m is a quantic nucleus on \(\mathcal {P}(A)\), that is, \(m A ; m B \subseteq m (A ; B)\). We refer here to the aforementioned paper by Goldblatt. Thus, according to Proposition 1, \(\langle (\mathcal {P}(A))_m, \subseteq , ;_m \rangle \) is a quantale itself since m is a quantic nucleus.

We define a map \(f_m : \mathcal {A} \rightarrow (\mathcal {P}(A))_m\) such that \(f_m : a \mapsto {\downarrow }\,a\). This map is well-defined since any lower cone generated by a point is m-closed. Moreover, \(f_m\) preserves products, residuals, and existing suprema. In particular, \(f_m\) is a residuated semigroup embedding. As a result, we have the following representation theorem [7, Corollary 2].

Theorem 2

Every residuated semigroup is isomorphic to the subalgebra of some quantale.

In turn, quantales are representable with quantales of binary relations. The notion of a relational quantale has been introduced by Brown and Gurr to represent quantales as quantales of relations [3].

Definition 9

Let A be a non-empty set. A relational quantale on A is an algebra \(\langle R, \subseteq , ; \rangle \), where

  1. 1.

    \(R \subseteq \mathcal {P}(A \times A)\),

  2. 2.

    \(\langle R, \subseteq \rangle \) is a complete join-semilattice,

  3. 3.

    ;  is a relational composition that respects all suprema in both coordinates.

The uniqueness of residuals in any quantale implies the following fact.

Proposition 2

Let \(\mathcal {A}\) be a relational quantale over a base set X, then for all \(a, b \in \mathcal {A}\)

  1. 1.

    \(a \setminus b = \{ (x, y) \in X^2 \, | \, \forall z \in X ( (z, x) \in a \Rightarrow (z, y) \in b) \}\),

  2. 2.

    \(a \, / \, b = \{ (x, y) \in X^2 \, | \, \forall z \in X ( (y, z) \in b \Rightarrow (x, z) \in b )\}\).

Now let us discuss the representation theorem for quantales. Let \(\mathcal {Q}\) be a quantale, Q its carrier, and \(\langle G \rangle \) a set of its generators. Given \(a \in \mathcal {Q}\), define the binary relation \(\hat{a} \subseteq Q \times Q\) as:

$$\hat{a} = \{ (g,p) \, | \, g \in \langle G \rangle , p \in Q \,\, g \le a ; p \}$$

Denote \(\widehat{Q}\) as \(\{ \hat{a} \, | \, a \in \mathcal {Q} \}\).

The mapping \(a \mapsto \hat{a}\) satisfies the following conditions:

  1. 1.

    \(a \le b\) iff \(\hat{a} \subseteq \hat{b}\),

  2. 2.

    \(\widehat{\varSigma A} = \varSigma \widehat{A}\), \(\hat{a} ; \hat{b} = \widehat{a ; b}\), and \(\langle \widehat{\mathcal {Q}}, \subseteq , \varSigma \rangle \) is a complete lattice,

  3. 3.

    \(\langle \widehat{\mathcal {Q}}, \subseteq , ; \rangle \) is a relational quantale,

  4. 4.

    \(\mathcal {Q}\) is isomorphic to \(\langle \widehat{\mathcal {Q}}, \subseteq , ; \rangle \) and \(a \mapsto \hat{a}\) is a quantale isomorphism.

We summarise the construction above with the following theorem proved by Brown and Gurr, see [3, Theorem 3.11].

Theorem 3

Every quantale \(\mathcal {Q} = \langle Q, ;, \varSigma \rangle \) is isomorphic to a relational quantale on Q as a base set.

Let \(\mathcal {A}\) be a residuated semigroup and \(\mathcal {Q}_{\mathcal {A}}\) a quantale of Galois closed subsets of \(\mathcal {A}\). \(\widehat{\mathcal {Q}_{\mathcal {A}}}\) is the corresponding relational quantale. Let us define an interpretation \(R : \mathcal {A} \rightarrow \widehat{\mathcal {Q}_{\mathcal {A}}}\) such that:

$$R : a \mapsto a^{R} = \widehat{{\downarrow }\,a}$$

According to the lemma below, such an interpretation is a representation. As we have already said above, the function \(a \mapsto {\downarrow }\,a\) is order-preserving and it commutes with products and residuals.

Lemma 1

Let \(\mathcal {A}\) be a residuated semigroup, then the interpretation \(R : \mathcal {A} \rightarrow \widehat{\mathcal {Q}_{\mathcal {A}}}\) such that \(R : a \mapsto a^{R} = \widehat{{\downarrow }\,a}\) is a representation.

Proof

By Theorem 2, \(\mathcal {A}\) emdeds to \(\mathcal {Q}_{\mathcal {A}}\), but by Theorem 3, \(\mathcal {Q}_{\mathcal {A}}\) is isomorphic to \(\widehat{\mathcal {Q}_{\mathcal {A}}}\). The fact that R is an injective homomorphism follows from the construction of the embedding of a residuated semigroup to the quantale of its Galois-stable subsets, the isomorphism of \(\mathcal {Q}_{\mathcal {A}}\) with \(\widehat{\mathcal {Q}_{\mathcal {A}}}\), and Proposition 2.

The lemma above implies the following statement.

Theorem 4

Every residuated semigroup is isomorphic to the subalgebra of some relational quantale. Moreover, \(\mathbf{R}(;, \setminus , /, \le )\) has the finite representation property.

Proof

Let \(\mathcal {A}\) be a finite residuated semigroup. The representation of \(\mathcal {A}\) as a subalgebra of the relational quantale of \(\widehat{\mathcal {Q}_{\mathcal {A}}}\) belongs to \(\mathbf{R}(;, \setminus , /, \le )\) by Lemma 1. This representation has the following form:

$$\widehat{\mathcal {A}} = \langle \{ \widehat{{\downarrow }\,a} \}_{a \in \mathcal {A}}, ;, \setminus , /, \subseteq \rangle $$

.

Moreover, such a representation with the corresponding relational quantale has the finite base, if the original algebra is finite. The base set of the quantale \(\widehat{\mathcal {Q}_{\mathcal {A}}}\) is the set of Galois stable subsets of \(\mathcal {A}\), which is finite.

4 Join Semilattice-Ordered Semigroups: The Explicit Axiomatisation

We note that a similar construction does not work for finite representable upper semilattice-ordered semigroups. From the one hand, the notions of a finite upper semilattice-ordered semigroup and finite quantale are quite close to each other. From the other hand, the relational representation of quantales does not have to represent joins as set-theoretic unions generally. Moreover, there is a countable sequence of non-representable upper semilattice-ordered semigroups with a non-representable ultraproduct, see [2, Theorem 3.1]. Thus, \(\mathbf{R}(;,+)\) is not finitely axiomatisable. Although, as we will see below, this class has a universal recursively enumerable axiomatisation. For that, we characterise representability using representability games on networks. The construction is somewhat similar to the proof of [10, Proposition 5].

Definition 10

Let \(\mathcal {A}\) be a join-semilattice ordered semigroup. A prenetwork over \(\mathcal {A}\) is a tuple (VEl), where V is a set of vertices, E is a set of edges such that \(\langle V, E \rangle \) is a directed graph, and l is a labelling function \(l : E \rightarrow {\text {Up}}(\mathcal {A})\).

A prenetwork over \(\mathcal {A} = (V, E, l)\) is a network if the following hold:

  1. 1.

    (Saturation condition) For all \(u, v \in V\) and for all \(x,y,z \in \mathcal {A}\), \(z \in l(u, v)\) and \(z \le x \, ; \, y\) implies \(x \in l(u, w)\) and \(y \in l(w, v)\) for some \(w \in V\).

  2. 2.

    (Coherence condition) For all \(u, v, w \in V\), one has \(l(u, v) ; l(v, w) \subseteq l(u, w)\).

  3. 3.

    (Join-primeness) For all \(u, v \in V\), l(uv) is join-prime. That is, for all \(a, b \in \mathcal {A}\) if \(a + b \in l(u,v)\), then either \(a \in l(u,v)\) or \(b \in l(u,v)\).

If \(\mathcal {N}\) is a prenetwork, then we will denote its sets of nodes as \({\text {Nodes}}(\mathcal {N})\) occasionally.

Let I be a non-empty index set and let \(\{ \mathcal {N}_i \}_{i \in I}\) be an indexed set of prenetworks (where each \(\mathcal {N}_i = (V_i, E_i, l_i)\)), then \(\mathcal {N} = \bigcup \limits _{i \in I} \mathcal {N}_i\) defined as (VEl), where

  1. 1.

    \(V = \bigcup \limits _{i \in I} V_i\) and \(E = \bigcup \limits _{i \in I} E_i\).

  2. 2.

    \(l(x, y) = \bigcup \limits _{ i \in I } l_i(x, y)\) for all \(x, y \in V\).

Definition 11

Let \(n \le \omega \) and \(\mathcal {A}\) a join semilattice-ordered semigroup. A play of the game \(\mathcal {G}_n(\mathcal {A})\) has n rounds and consists of n prenetworks. As usual, we have two players, \(\forall \) (Abelard, he/his) and \(\exists \) (Héloïse, she/her).

  1. 1.

    Round 0: \(\forall \) picks \(a, b \in \mathcal {A}\) such that \(a \not \le b\). \(\exists \) responds with a prenetwork \(\mathcal {N}_0 = (V_0 = \{ x_0, x_1 \}, E_0 = \{ (x_0, x_1)\}, l_0)\) such that \(l_0(x_0, x_1) = {\uparrow }\,a\).

  2. 2.

    Round \(n + 1\). Suppose, the prenetwork \(\mathcal {N}_n = (V_n, E_n, l_n)\) has been played. \(\forall \) has the following three options:

    1. (a)

      (Composition move): \(\forall \) picks \(x, y, z \in V_n\) with \(b \in l_n(x, y)\) and \(c \in l_n(y, z)\). We denote such a move as N(xyzbc). Then \(\exists \) responds with \(\mathcal {N}_{n + 1} = (V_{n + 1}, E_{n + 1}, l_{n + 1})\) such that \(\mathcal {N}_{n + 1}\) is the same as \(\mathcal {N}_n\), but \(l_{n + 1}(x, z) = {\uparrow }\,(l_{n}(x, z) \cup \{ b \, ; \, c \})\).

    2. (b)

      (Witness move): \(\forall \) picks an edge \((x, y) \in E_n\) and \(d, e \in \mathcal {A}\) such that \(c \le d ; e\) for \(c \in l_n(x, y)\). \(\exists \) has to find a witness. She has to find a z which is either a fresh node or an old one. If z is fresh, then she defines the prenetwork T, the edges of which are xyz with labelling:

      1. 1.

        \(l_T(x, z) = {\uparrow }\,d\)

      2. 2.

        \(l_T(z, y) = {\uparrow }\,e\)

      If z is already an element of \(\mathcal {A}\), then her response is similar. For her response, \(\exists \) plays \(\mathcal {N}_{n + 1} = \mathcal {N}_n \cup T\).

    3. (c)

      (Join move): \(\forall \) picks an edge \((x, y) \in E_n\) and \(c + d\) for \(c, d \in \mathcal {A}\). \(\exists \) has the following two alternatives for her response:

      1. 1.

        \(\exists \) chooses c and responds with the prenetwork \(\mathcal {N}_{n + 1} = \langle V_{n + 1}, E_{n + 1}, l_{n + 1} \rangle \), where \(l_{n+1}(x, y) = {\uparrow }\,(l_n(x,y) \cup \{ c \})\).

      2. 2.

        \(\exists \) chooses b. The response is similar but \(l_{n + 1}(x, y) = {\uparrow }\,(l_n(x,y) \cup \{ d \})\).

\(\forall \) wins the play if \(b \notin l_{\mathcal {N}_i}(x,y)\) for some \(i < n\). Otherwise, \(\exists \) wins the play.

Let \(a \in \mathcal {A}\) and \(\mathcal {N}\) a network, define a game \(\mathcal {G}(\mathcal {N}, \mathcal {A}, a)\) such that \(\forall \) picks a in the initial round and \(\mathcal {N}_0 = \mathcal {N}\). The rules of the game are the same as previously.

Lemma 2

Let \(\mathcal {A} = \langle A, ;, + \rangle \) be a join semilattice-ordered semigroup,

  1. 1.

    If \(\mathcal {A}\) is representable then \(\exists \) has a winning strategy in \(\mathcal {G}_{\omega }(\mathcal {A})\).

  2. 2.

    If \(|\mathcal {A}| \le \omega \) and \(\exists \) has a winning strategy in \(\mathcal {G}_{\omega }(\mathcal {A})\) then \(\mathcal {A}\) is representable.

Proof

 

  1. 1.

    Let \(h : \mathcal {A} \rightarrow 2^{D \times D}\) be a representation of some base set \(D \ne \emptyset \). \(\exists \) maintains a map \({}^{'} : {\text {Nodes}}(\mathcal {N}) \rightarrow D\), where \(\mathcal {N}\) is a network being played, such that \(a \in l_{\mathcal {N}}(x,y)\) implies \((x',y') \in h(a)\).

  2. 2.

    Given \(a \in \mathcal {A}\), we consider a play of the game where \(\forall \) picks a and b with \(a \not \le b\) in the initial round and plays \((\mathcal {N}, x, y, z, c, d)\) in the further rounds for all \(x, y, z \in {\text {Nodes}}(\mathcal {N})\) and \(c,d \in \mathcal {A}\). Here, \(c \in l_N(x, y)\) and \(d \in l_N(y, z)\). \(\forall \) also plays all rounds \((\mathcal {N},x,y,c,d)\) for all \(x, y \in {\text {Nodes}}(\mathcal {N})\) and \(c,d \in \mathcal {A}\) such that there is \(e \in \mathcal {A}\) such that \(e \le c ; d\) and \(e \in l_N(x,y)\). \(\forall \) picks also \(c + d\) and vertices \(x,y \in {\text {Nodes}}(\mathcal {N})\) for \(c, d \in \mathcal {A}\). Note that \(\mathcal {A}\) is at most countable, so we can schedule all these moves. We have the following play of a game where Héloïse uses a winning strategy:

    $$\mathcal {N}_0 \subseteq \mathcal {N}_1 \subseteq \mathcal {N}_2 \dots $$

    Let us put \(\mathcal {N}^{*}(a, b) = \bigcup \limits _{i < \omega } \mathcal {N}_i\). \(\mathcal {N}^{*}(a,b)\) is clearly a network. Let us put the following network assuming that \(\mathcal {N}^{*}(a_1, a_2)\) and \(\mathcal {N}^{*}(b_1, b_2)\) are disjoint for \(a_1 \ne a_2\) and \(b_1 \ne b_2\):

    $$ \mathcal {N} = \bigcup \limits _{a,b \in \mathcal {A}, a \not \le b} \mathcal {N}^{*}(a,b) $$

    Note that \(\mathcal {N} = \langle V, E, l \rangle \) is a well-defined network since it is the disjoint union of networks. Define \({\text {rep}} : \mathcal {A} \rightarrow E\) as:

    $$ {\text {rep}}(a) = \{ (x, y) \, | \, \exists b \le a \,\, b \in l_{\mathcal {N}}(x, y)\} $$

    Let us check that \({\text {rep}}\) is a representation. Let us show that \({\text {rep}}(a + b) = {\text {rep}}(a) \cup {\text {rep}}(b)\) Suppose \((x, y) \in {\text {rep}}(a + b)\). That is, there exists \(c \le a + b\) with \(c \in l_{\mathcal {N}}(x, y)\), so does \(a + b\) since \(l_{\mathcal {N}}\) is an upper cone. \(a + b \in l_{\mathcal {N}}(x, y)\), that is,

    $$ a + b \in \bigcup \limits _{ \begin{array}{c} c_1, c_2 \in \mathcal {A} \\ c_1 \not \le c_2 \end{array}} l_{\mathcal {N}^{*}(c_1, c_2)}(x,y) $$

    That is, there is \(c \in \mathcal {A}\) with such that \(a + b \in l_{\mathcal {N}^{*}(c_1, c_2)}(x,y)\), but \(l_{\mathcal {N}^{*}(c_1, c_2)}(x,y)\) is join-prime, so we have either \(a \in l_{\mathcal {N}^{*}(c_1, c_2)}(x,y)\) or \(b \in l_{\mathcal {N}^{*}(c_1, c_2)}(x,y)\). Thus, \({\text {rep}}(a + b) \subseteq {\text {rep}}(a) \cup {\text {rep}}(b)\). Suppose for the converse, \((x, y) \in {\text {rep}}(a)\). We need \((x, y) \in {\text {rep}}(a + b)\). In other words, we have some \(c \in \mathcal {A}\) with \(c \le a\) and \(c \in l_{\mathcal {N}}(x, y)\). We have \(c \le a \le a + b\), so \((x, y) \in {\text {rep}}(a + b)\). Let us show that \({\text {rep}}(a ; b) = {\text {rep}}(a) ; {\text {rep}}(b)\). Suppose \((x, y) \in {\text {rep}}(a ; b)\). We need some z with \((x, z) \in {\text {rep}}(a)\) and \((z, y) \in {\text {rep}}(b)\). There is \(c \le a ; b\) with \(c \in l_{\mathcal {N}}(x,y)\). That is, there are \(a_1, a_0 \in \mathcal {A}\) and \(\mathcal {N}_i\) such that \(c \in l_{\mathcal {N}_i}(x, y)\) where \(\forall \) plays \((a_1, a_0)\) for the initial round. By the condition, \(\forall \) makes the witness moves and \(\exists \) responds with a witness. Her response is a node z such that \(l_{\mathcal {N}_{i + 1}}(x, z) = {\uparrow }\,(l_{\mathcal {N}_i}(x, z) \cup \{ a \})\) and \(l_{\mathcal {N}_{i + 1}}(z, y) = {\uparrow }\,(l_{\mathcal {N}_i}(z, y) \cup \{ b\})\). The inclusion \({\text {rep}}(a ; b) \subseteq {\text {rep}}(a) ; {\text {rep}}(b)\) holds since all witness moves have been played. Suppose \((x, y) \in {\text {rep}}(a) ; {\text {rep}}(b)\). We need \((x, y) \in {\text {rep}}(a;b)\). There exists \(z \in {\text {Nodes}}(\mathcal {N})\) with \((x, z) \in {\text {rep}}(a)\) and \((z, y) \in {\text {rep}}(b)\). So, there are cd such that \(c \le a\) with \(c \in l_{\mathcal {N}}(x, z)\) and \(d \le b\) with \(d \in l_{\mathcal {N}}(z, y)\). We also know that \(l_{\mathcal {N}}(x, z) ; l_{\mathcal {N}}(z, y) \subseteq l_{\mathcal {N}}(x, y)\) because all composition moves have been played. So \(c ; d \in l_{\mathcal {N}}(x, y)\). That makes \((x, y) \in {\text {rep}}(a;b)\) since \(c ; d \le a ; b\). For injectivity, suppose \(a \le b\) and \((x, y) \in {\text {rep}}(a)\), that is, there is \(c \le a\) such that \(c \in l_{\mathcal {N}}(x, y)\), but \(c \le a \le b\), so \((x, y) \in {\text {rep}}(b)\). Suppose \(a \not \le b\), then there are \(x, y \in {\text {Nodes}}(\mathcal {N}(a, b))\) such that \(a \in l_{\mathcal {N}}(x, y)\) and \(b \notin l_{\mathcal {N}}(x, y)\). These elements are \(x_0, x_1\) that \(\exists \) picks as her response in the zero round. \(\exists \) has a winning strategy, so \(b \notin l(x_0, x_1)\), but \((x,y) \in {\text {rep}}(a)\), but \((x,y) \notin {\text {rep}}(b)\).

The following proposition is a version of [13, Proposition 7.24] and the right-to-left part is proved using König’s lemma [17, Exercise 5.6.5].

Proposition 3

Let \(\mathcal {A}\) be a join semilattice-ordered semigroup and \(\mathcal {N}\) a network, iff \(\exists \) has a winning strategy in \(\mathcal {G}_n(\mathcal {A}, \mathcal {N})\) for all \(n < \omega \) iff she has a winning strategy in \(\mathcal {G}_{\omega }(\mathcal {A}, \mathcal {N})\).

Our purpose is to axiomatise of \(\mathbf{R}(;, +)\) with a recursively enumerable set of universal formulas. See [13, Chapter 9] for the discussion in detail to have a more general methodology.

Definition 12

Let \({\text {Var}} = \{ v_0, v_1, \dots \}\) be a set of variables. The set of terms is generated by the following grammar:

$$t_1, t_2 \,::\,= v \, | \, (t_1 + t_2) \, | \, (t_1 ; t_2)$$

Definition 13

A term network is a finite network \(\langle V, E, l \rangle \), where \(\langle V, E \rangle \) is a directed graph and \(l : E \rightarrow 2^{Term}\) is a labelling function such that every l(xy) is finite for all \((x, y) \in E\).

Let \(\mathcal {A}\) be a join semilattice-ordered semigroup and \(\vartheta : {\text {Var}} \rightarrow \mathcal {A}\) a valuation. The value of complex terms is defined inductively for \(a, b \in T\):

  1. 1.

    \((a ; b)^{\vartheta } = a^{\vartheta } ; b^{\vartheta }\)

  2. 2.

    \((a + b)^{\vartheta } = a^{\vartheta } + b^{\vartheta }\)

Let \(\mathcal {N} = \langle V, E, l \rangle \) be a term network, \(\mathcal {A}\) be a join-semilattice ordered semigroup and \(\vartheta : {\text {Var}} \rightarrow {\mathcal {A}}\) a valuation. Let us define the prenetwork \(\mathcal {N}^{\vartheta }\) with the same edges and vertices with labelling \(l^{\vartheta }(x, y) = {\uparrow }\,\vartheta [l_{\mathcal {N}}(x, y)]\). We define the following three extensions of \(\mathcal {N}\) reflecting the composition, witness, and join moves respectively:

  1. 1.

    Let \(x, y \in {\text {Nodes}}(\mathcal {N})\) and let t be a term. \(\mathcal {N}_c\) is the extension of \(\mathcal {N}\), where \({\text {Nodes}}(\mathcal {N}_c) = {\text {Nodes}}(\mathcal {N})\) and \(l_{\mathcal {N}_c}(x, y) = l_{\mathcal {N}}(x, y) \cup \{ t\}\) and \(l_{\mathcal {N}_c}(u, v) = l_{\mathcal {N}}(u, v)\) for all \(u \ne x\) and \(v \ne y\). We denote this network as \(\mathcal {N}_c(\mathcal {N}, x, y, t)\).

  2. 2.

    Let \(x, y \in {\text {Nodes}}(\mathcal {N})\), let z be a node (regardless of whether z is fresh or not), and \(t_1\), \(t_2\) any terms. Let us define a network T such that \({\text {Nodes}}(T) = \{ x, y, z\}\). We define labelling as \(l_{T}(x, y) = \{ t_1 \}\) and \(l_{T}(y, z) = \{ t_2 \}\). So we put \(\mathcal {N}_w = \mathcal {N} \cup T\). We denote this network as \(\mathcal {N}_w(\mathcal {N}, x,y,z, t_1, t_2)\).

  3. 3.

    Let \(x, y \in {\text {Nodes}}(\mathcal {N})\) and let \(t_1, t_2\) be terms. We define \(T_i = \langle \{ x, y\}, \{ (x, y) \}, l_{T_i} \rangle \), where \(l_{T_i}(x, y) = l_{\mathcal {N}}(x, y) \cup \{ t_i \}\) for \(i = 1,2\). So \(\mathcal {N}_{j_1} = \mathcal {N} \cup T_1\) and \(\mathcal {N}_{j_2} = \mathcal {N} \cup T_2\).

Lemma 3

For all \(n < \omega \) there exists a first-order sentence \(\rho _n\) such that \(\exists \) has a winning strategy in \(\mathcal {G}_n(\mathcal {A})\) iff \(\mathcal {A} \models \rho _n\).

Proof

As usual, for each \(n < \omega \) we construct a formula \(\sigma _n\) claiming that \(\exists \) has a winning strategy in the game of lenght n. To be more precise, our purpose is to have

$$\exists \text { has a winning strategy in }\mathcal {G}_n(\mathcal {N}^{\vartheta }, \mathcal {A}, \vartheta (v))\text { if and only if }\mathcal {A} \models \sigma _{n}(\mathcal {N}, v)$$

where \(\mathcal {A}\) is a join semilattice-ordered semigroup, \(\vartheta : {\text {Var}} \rightarrow \mathcal {A}\) is a variable assignment, and \(\mathcal {N}\) is a term network.

We define the following sequence of formulas \(\{ \sigma _n \}_{n < \omega }\) inductively:

  1. 1.

    \(\sigma _0(\mathcal {N}, v) = \bigwedge \limits _{a \in l_{\mathcal {N}}(x, y)} \lnot (a \le v)\) \(\sigma _0(\mathcal {N}, v)\) merely claims that \(\exists \) has a winning strategy in the zero length game.

  2. 2.

    Suppose \(\sigma _{n}(\mathcal {N}, v)\) are already constructed for some \(n < \omega \). Let us define a formula \(\sigma _{n + 1}\) claiming that \(\exists \) always has a proper response for a network \(\mathcal {N}\) being played. \(\sigma _{n + 1}(\mathcal {N}, v)\) is defined as follows:

    $$\sigma _{n + 1}(\mathcal {N}, v) = {\sigma _{n + 1}}_c(\mathcal {N}, v) \wedge {\sigma _{n + 1}}_w(\mathcal {N}, v) \wedge {\sigma _{n + 1}}_j(\mathcal {N}, v)$$

    where

    • \({\sigma _{n + 1}}_c(\mathcal {N}, v) = \bigwedge \limits _{ \begin{array}{c} x, y, z \in {\text {Nodes}}(\mathcal {N}) \\ t_1 \in l_{\mathcal {N}}(x, y) \\ t_2 \in l_{\mathcal {N}}(y, z) \end{array}} \sigma _{n}(\mathcal {N}_c(x, z, t_1, t_2), v)\)

    • \({\sigma _{n + 1}}_w(\mathcal {N}, v) = \bigwedge \limits _{\begin{array}{c} x,y \in {\text {Nodes}}(\mathcal {N}) \\ t \in l_{\mathcal {N}}(x,y) \end{array}} \forall u_1, u_2 (t \le u_1 ; u_2 \rightarrow \bigvee \limits _{w \in {\text {Nodes}}(\mathcal {N}) \cup \{ z \}}\)\( \mathcal {N}_c(x,y,w, u_1, u_2))\), where \(z \notin {\text {Nodes}}(\mathcal {N})\).

    • \({\sigma _{n + 1}}_j(\mathcal {N}, v) = \forall a \, \forall b (v = a + b \rightarrow \bigwedge \limits _{x, y \in {\text {Nodes}}(\mathcal {N})} \sigma _{n}(\mathcal {N}_{j_1}(\mathcal {N}, x, y, a), v) \vee \sigma _{n}(\mathcal {N}_{j_2}(\mathcal {N}, x, y, b), v))\)

So, \(\exists \) has a winning strategy iff these formulas are true under the valuation \(\vartheta \) since the formulas \(\{ \sigma _n \}_{n < \omega }\) encode the presence of a winning strategy for \(\exists \) in every finite round.

Let \(v_0\) be any variable, \(\mathcal {N}_{v_0}\) denotes the term network having the form \(\langle \{ \{ x_0, x_1 \}, \{ (x_0, x_1) \}, l \} \rangle \), where \(l(x,y) = \{ v_0 \}\). We define the following sequence of formulas \((\rho _n)_{n < \omega }\):

$$\rho _n = \forall v_0 \forall v_1 (\lnot (v_0 \le v_1) \rightarrow \sigma (\mathcal {N}_{v_0}, v_0))$$

This inductive sequence of formulas provides us the explicit axiomatisation of the class of representable join semilattice-ordered semigroups.

Theorem 5

A join semilattice-ordered semigroup \(\mathcal {A}\) is representable iff \(\mathcal {A} \models \{ \rho _n \}_{n < \omega }\). Moreover, \(\mathbf{R}(;,+)\) has a recursively enumerable universal axiomatisation.

Proof

Let us define a two sorted language with sorts \(\mathbf{a}\) (algebra) and \(\mathbf{r}\) (representation). \(\mathbf{R}(;,+)\) clearly forms a pseudo-elementary class, see [14, Introduction] for more details. Moreover, this class is pseudo-universal and it satisfies the condition of the second item of Theorem 1.

By Proposition 3, Lemma 2, and Lemma 3, a countable join semilattice-ordered semigroup \(\mathcal {A}\) is representable iff \(A \models \{ \rho _n \}_{n < \omega }\). Suppose \(\mathcal {A}\) is uncountable. The class is pseudo-elementary, so it is closed under elementary equivalence, so, by the downward Löwenheim-Skolem theorem [17, Corollary 3.1.5], we can take \(\mathcal {A}_0 \preceq \mathcal {A}\), a countable elementary substructure of \(\mathcal {A}\). Then \(\mathcal {A}_0 \models \{ \rho _n \}_{n < \omega }\) iff \(\mathcal {A} \models \{ \rho _n \}_{n < \omega }\). Therefore, if \(\mathcal {A}_0\) is representable, so is \(\mathcal {A}\).

As we have already discussed, the finite representation property for \((;,+)\)-structures remains an open question. If the solution is positive, then the problem of representability for finite join semilattice-ordered semigroups is decidable since finite representability and recursive axiomatisability imply decidability.