Axioms for signatures with domain and demonic composition

Abstract

Demonic composition $*$ is an associative operation on binary relations, and demonic refinement ${\sqsubseteq }$ is a partial order on binary relations. Other operations on binary relations considered here include the unary domain operation D and the left restrictive multiplication operation $\circ$ given by $s\circ t=D(s)*t$. We show that the class of relation algebras of signature $\{\, \sqsubseteq , D, *\, \}$, or equivalently $\{\, \subseteq , \circ , *\, \}$, has no finite axiomatisation. A large number of other non-finite axiomatisability consequences of this result are also given, along with some further negative results for related signatures. On the positive side, a finite set of axioms is obtained for relation algebras with signature $\{\, \sqsubseteq , \circ , *\, \}$, hence also for $\{\, \subseteq , \circ , *\, \}$.

1 Introduction

A binary relation $a\subseteq X\times X$ over a base set X is called left-total if for all $x\in X$ there is $y\in X$ such that $(x, y)\in a$. Let ${{\,\mathrm{\mathsf{Rel}}\,}}(X)$ denote the set of all binary relations on the non-empty set X, ${{\,\mathrm{\mathsf{Lt} }\,}}(X)$ the set of left total binary relations on X, and ${{\,\mathrm{\mathsf Par}\,}}(X)$ the set of partial functions on X. Algebras of binary relations normally include a composition operation ;  defined by

$$\begin{aligned} (x, y)\in (a; b)\iff \exists z\in X : ((x, z)\in a)\wedge ((z, y)\in b). \end{aligned}$$

Since composition is associative, each of ${{\,\mathrm{\mathsf{Rel}}\,}}(X), {{\,\mathrm{\mathsf{Lt} }\,}}(X)$ and ${{\,\mathrm{\mathsf Par}\,}}(X)$ with composition forms a semigroup. Moreover, each is an ordered semigroup (partially ordered, associative, monotonic in each argument) when also equipped with the partial order of set inclusion of binary relations. When we refer to an ordered semigroup of binary relations, we mean a semigroup of binary relations under composition equipped with the partial order of set inclusion.

Other operations we consider include a constant $1'$ that denotes the identity relation, a constant 0 that denotes the empty relation, a constant 1 that denotes the full relation, the unary operation of converse, denoted $^{\smile }$, the boolean operation $+$ of union, or in the absence of union we may still wish to include the set inclusion relation, henceforth denoted by $\le$ when viewed as an order on ${{\,\mathrm{\mathsf{Rel}}\,}}(X)$ (to avoid confusion with its frequent other uses).

In this paper we consider certain natural “demonic” variants of standard “angelic” relational composition, union, inclusion. First, for any relation $a\in {{\,\mathrm{\mathsf{Rel}}\,}}(X)$, define

$$\begin{aligned} {{\,\mathrm{dom}\,}}(a)&=\{\, x\in X\mid \exists y\in X: (x,y)\in a\, \}, \\ {{\,\mathrm{ran}\,}}(a)&=\{\, y\in X\mid \exists x\in X: (x,y)\in a\, \}. \end{aligned}$$

Now we can define demonic composition $*$ by

$$\begin{aligned} a*b=&\{\, (x, y)\in X\times X \mid (\exists z\in X : ((x, z)\in a\wedge (z, y)\in b))\\&\wedge (\forall w\in X : ((x,w)\in a \implies \exists v (w, v)\in b))\, \}\\ =&(a; b ) \cap \{\, (x, y)\in X\times X\mid a(x)\subseteq {{\,\mathrm{dom}\,}}(b))\, \} \end{aligned}$$

for $a, b\in {{\,\mathrm{\mathsf{Rel}}\,}}(X)$, where $a(x)=\{\, y\in X \mid (x, y)\in a\, \}$. So $a*b$ is a domain restriction of the ordinary composition of a and b. Surprisingly, perhaps, it turns out that demonic composition is associative.

The motivation for this operation comes from computer science, and indeed there is a wealth of literature on demonic composition and its relationship to the modelling of programs. The concept seems first to appear explicitly in [2], where it is attributed to [6]. We briefly summarise these approaches next.

We may represent the possible runs of a non-deterministic program p as a binary relation P over the set of program states. Then a state transition (x, y) belongs to $P*Q$ if: (i) there is a possible computation of p starting from x followed by a computation of q leading to y, and (ii) starting from x, all possible runs of p lead to states where q may be executed. In general, demonic composition is related to total correctness, angelic to partial correctness, and the same goes for the other demonic variants of angelic operations and orders considered below.

Note that if b is left total or if a is a partial function then $a*b=a; b$, so demonic composition coincides with ordinary composition over ${{\,\mathrm{\mathsf{Lt} }\,}}(X)$ and ${{\,\mathrm{\mathsf Par}\,}}(X)$. Other demonic relations and operations of interest include demonic refinement $\sqsubseteq$, and demonic join , defined by

So is the domain restriction of $a\cup b$ to the set of points where both a and b are defined, and $a\sqsubseteq b$ if and only if (${{\,\mathrm{dom}\,}}(a)\supseteq {{\,\mathrm{dom}\,}}(b)$ and $b\circ a \le b$). When restricted to left-total relations, $\sqsubseteq$ coincides with ordinary inclusion $\le$ but when restricted instead to partial functions, $\sqsupseteq$ coincides with inclusion (note the reversal).

In either angelic or demonic setting, the unary operations of domain, range and antidomain are defined on ${{\,\mathrm{\mathsf{Rel}}\,}}(X)$ as follows: for all $a\in {{\,\mathrm{\mathsf{Rel}}\,}}(X)$,

$$\begin{aligned} D(a)&=\{\, (x,x)\in X\times X\mid x\in {{\,\mathrm{dom}\,}}(a)\, \},\\ R(a)&=\{\, (y,y)\in X\times X\mid y\in {{\,\mathrm{ran}\,}}(a)\, \}\\ Ant(a)&=\{\, (x, x)\in X\times X\mid x\not \in {{\,\mathrm{dom}\,}}(a)\, \}. \end{aligned}$$

These are obviously well defined on ${{\,\mathrm{\mathsf Par}\,}}(X)$ also (but Ant is not well defined over ${{\,\mathrm{\mathsf{Lt} }\,}}(X)$). Observe that demonic composition is definable from ordinary composition and antidomain by

$$\begin{aligned} a*b= Ant(a; Ant(b)); a; b. \end{aligned}$$

But in the other direction, it seems not possible to define ordinary composition from demonic composition plus any set of the other relation algebra operations considered here that excludes composition itself.

A final operation on ${{\,\mathrm{\mathsf{Rel}}\,}}(X)$, closely related to domain, is left restrictive multiplication $\circ$, defined as follows:

$$\begin{aligned} a\circ b&=\{\, (x, y)\in X\times X\mid x\in {{\,\mathrm{dom}\,}}(a)\wedge (x, y)\in b\, \}. \end{aligned}$$

So $a\circ b$ is the domain restriction of b to the domain of a, and indeed $a\circ b=D(a); b=D(a)*b$.

In the presence of left restrictive multiplication (hence in the presence of domain and either angelic or demonic composition), inclusion and $\sqsubseteq$ are inter-definable since for $a,b\in {{\,\mathrm{\mathsf{Rel}}\,}}(X)$,

$$\begin{aligned} a\le b&\iff (b\circ a=a) \wedge (a\sqsubseteq a\circ b), \end{aligned}$$

(1.1)

$$\begin{aligned} a\sqsubseteq b&\iff (a\circ b=b) \wedge (b\circ a\le b). \end{aligned}$$

(1.2)

In what follows, let S be a signature contained in

We let R(S) (respectively P(S), L(S)) denote the closure under isomorphism of the classes of binary relations (respectively partial functions, left-total relations) closed under the operations in S, so for example if $0\in S$ then the set of relations (partial functions, left-total relations) must include the empty set, if $+\in S$ then the set must be closed under union, and so on. If $\Sigma$ is a set of S-formulas and ${{\mathcal {K}}}$ is a class of S-structures we say that $\Sigma$ defines or axiomatises ${{\mathcal {K}}}$ if ${{\mathcal {K}}}$ is the class of all models of $\Sigma$.

Finite axiomatisations of classes of algebras of binary relations are unusual – for many relation algebra signatures the representation class is known to be non-finitely axiomatisable. For example, although $R({\le , ;})$ is finitely axiomatisable [20], $R({\le , 1', ;})$ is not finitely axiomatisable [7], and neither is R(D, ; ) [8].

Positive results are more common for P(S). Partial functions are not closed under union or complementation, so consider signatures

$$\begin{aligned} S\subseteq \{\, 0, \le , \wedge , 1', D, Ant, \circ , ;, *\, \}. \end{aligned}$$

P(S) is always finitely axiomatisable when composition is included in S and $S\subseteq \{\, 0, \wedge , 1', D, Ant, ;\, \}$ (see [14, Table 3.1] for attributions of these results). Note that for partial functions, the inclusion order is expressible in (D, ; ), since $s\le t$ when and only when $s=D(s); t$, and $s\circ t$ may be expressed by D(s); t, so P(S) is finitely axiomatisable for all signatures with composition or demonic composition, contained in $\{\, 0, \le , \wedge , 1', D, Ant, \circ , ;, *\, \}$. For example $P(\le , ;)$, P(D, ; ) and P(D, R, ; ) are shown to be finitely axiomatisable in [15] (see also [17, page 38]), Lemma 4.2, and [16], respectively. By contrast, in the relational case, as mentioned above there is no finite axiomatisation of R(D, ; ), or of R(D, R, ; ) [8]; indeed it was shown in [13] that there is no axiomatisation using only finitely many variables for these two relational cases.

In [20], Zareckiĭ showed that every ordered semigroup ${{\mathcal {A}}}$ is isomorphic to an ordered semigroup of binary relations: one represents an element $a\in {{\mathcal {A}}}$ of the ordered semigroup as the relation

$$\begin{aligned} \{\, (b, c)\mid b \in {{\mathcal {A}}}\cup \{\, e\, \}, c\in {{\mathcal {A}}}, b; a\ge c\, \}, \end{aligned}$$

where e is an additional identity element, included to ensure that the representation is faithful. We note that Zareckiĭ’s proof represents elements of an ordered semigroup as left total binary relations over ${{\mathcal {A}}}\cup \{\, e\, \}$. So his theorem states that the axioms of ordered semigroups define $R(\le , ;)$ but also shows that they define $L(\le , ;)$, so $R(\le , ;)=L(\le , ;)$. It is known that demonic refinement is a partial order and demonic composition is monotonic with respect to demonic refinement, so $({{\,\mathrm{\mathsf{Rel}}\,}}(X),*,\sqsubseteq )$ is an ordered semigroup (see [4] and [5] for example). For left-total relations, $*$ and ;  coincide, as do $\le$ and $\sqsubseteq$, and so the proof of Zareckiĭ’s theorem using left-total relations also shows that every ordered semigroup is isomorphic to an ordered semigroup of binary relations under $*$ and $\sqsubseteq$, and hence that the “demonic” representation class $R(\sqsubseteq , *)$ shares the same axioms as the “angelic” representation class $R(\le , ;)$, namely the axioms of ordered semigroups.

For the signature $S=(D,*)$, a finite axiomatisation for P(S) is known and is given by the laws for left restriction semigroups, given in Section 4. (Recall that for partial functions, $*$ and ;  coincide.) However, it is known that these same axioms are valid over R(S) and therefore must axiomatise it as well since $P(S)\subseteq R(S)$. Precisely the same comments apply to the signature $\{\, \circ ,*\, \}$, where the 1-stack axioms are known to axiomatise P(S), but are sound for R(S) and therefore axiomatise it too.

Given that finite axiomatisations exist for $R(\sqsubseteq , *), R(*,D)$ and $R(*,\circ )$, we consider signatures obtained by combining these, namely $R(\sqsubseteq ,*,D)$ and $R(\sqsubseteq ,*,\circ )$ (the combination $R(*, D, \circ )$ is essentially the same as $R(*, D)$ since $\circ$ is definable).

We show that $R(D, *, \sqsubseteq )$ and $R(D, *, \le )$ are not finitely axiomatisable. To do this, we first obtain a result for left total relations which has many other consequences. In [7] it was shown that $R(\le , 1', ;)$ is not finitely axiomatisable. We modify the proof and show that $L(\le , 1', ;)$ is also not finitely axiomatisable. From this, we obtain the negative result for $S=\{D, *, \sqsubseteq \}$, but also prove as consequences of our result for left total relations and some other results that R(S) is not finitely axiomatisable if (i) either D or $1'$ is in S, (ii) either inclusion $\le$ or demonic refinement $\sqsubseteq$ is in S and (iii) either composition ;  or demonic composition $*$ is in S, and

We also obtain some further negative results for related structures where the predicates $\le , \sqsubseteq$ are excluded and cannot be defined. In [8] it is shown that R(D, ; ) is not finitely axiomatisable. We modify that proof and show that there is no finite axiomatisation of R(S) if (i) either D or $\circ$ is in S and (ii) either ;  or $*$ is in S, and $S\subseteq \{\, 0,1', D, Ant, \circ , ;, *\, \}$.

On the positive side, our main result is that $R(\sqsubseteq ,*,\circ )$ is finitely axiomatised as the class of “ordered 1-stacks” (defined below); because of the interdefinability of $\sqsubseteq$ and $\le$ in the presence of $*$ and $\circ$, this gives a finite axiomatisation for $R(\le ,*,\circ )$ also. A special case then gives finite axiomatisations for $R(\sqsubseteq ,\circ )$ and $R(\le ,\circ )$.

2 Non-finite axiomatisability

It was shown in [7] that in contrast to $R(\le , ;)$, there is no finite axiomatisation for $R(1', \le , ;)$. This proof of non-finite axiomatisability requires a minor modification in order to work for left-total relations (see the appendix below). Note that $L(\le , 1', ;)$ does not share an axiomatisation with $R(\le , 1', ;)$, since the law $a\le 1'\implies a=1'$ holds in the former but not the latter.

Let ${{\mathcal {A}}}=(A, 1', ;, \le )$ be any structure with constant $1'$, binary operation ;  and binary relation $\le$. For any $S\subseteq A$ we write $S^\uparrow$ for $\{\, t\in A\mid \exists s\in S : s\le t\, \}$ and for a single element $a\in A$ we write $a^\uparrow$ for $\{\, a\, \}^\uparrow$.

Definition 2.1

An ${{\mathcal {A}}}$-network is a map $N:\mathsf{nodes}(N)\times \mathsf{nodes}(N)\rightarrow \wp ({{\mathcal {A}}})$ (the power set of ${{\mathcal {A}}}$) having range the set of upward closed subsets of ${{\mathcal {A}}}$, such that $1'\in N(x, y)$ if and only if $x=y$ and $N(x, y); N(y, z)\subseteq N(x, z)$, for $x, y, z\in \mathsf{nodes}(N)$. We say that an ${{\mathcal {A}}}$-network M is a refinement of N if $\mathsf{nodes}(M)\supseteq \mathsf{nodes}(N)$ and $M(x, y)\supseteq N(x, y)$. We say that M is an extension of N if $\mathsf{nodes}(M)\supseteq \mathsf{nodes}(N)$ and for $x, y\in \mathsf{nodes}(N)$ we have $M(x, y)=N(x, y)$. An element $a\in N(x, y)$ is called minimal if $N(x, y)=a^\uparrow$.

Let $k\le \omega$. In the initial round of the network game $\Gamma _k({{\mathcal {A}}})$ over ${{\mathcal {A}}}$ that tests representability by left-total relations k times, $\forall$ picks any $a_0\not \le b_0\in {{\mathcal {A}}}$ and $\exists$ responds with a network $N_0$ such that there are $x_0, y_0\in \mathsf{nodes}(N_0)$ (not necessarily distinct) such that $a_0\in N_0(x_0, y_0)$ but $b_0\not \in N_0(x_0, y_0)$. In a later round, if the current network is N then $\forall$ may either play

• a domain move (x, a) where $x\in \mathsf{nodes}(N)$ and $a\in {{\mathcal {A}}}$, or

• a composition move (x, y, a, b) where $x, y\in \mathsf{nodes}(N)$ and $a, b\in {{\mathcal {A}}}$ such that $a; b\in N(x, y)$.

In the latter case, provided minimal elements exist, we may assume that a, b are minimal subject to $a; b\in N(x, y)$. In each case, $\exists$ must play a refinement $N^+$ of N with some node $z\in \mathsf{nodes}(N^+)$, such that

• $a\in N^+(x, z)$ for a domain move (x, a) (for left-totality of a) and

• $a\in N^+(x, z)$, $b\in N^+(z, y)$ for a composition move (x, y, a, b) (for preservation of composition).

If she cannot find such a network or if $b_0\in N^+(x_0, y_0)$ she loses in that round. If she never loses then she wins the play of the game.

Lemma 2.2

If ${{\mathcal {A}}}$ is countable and $\exists$ has a winning strategy in $\Gamma _\omega ({{\mathcal {A}}})$ then ${{\mathcal {A}}}$ can be represented as left-total relations.

Proof

Let $N_{a_0, b_0}$ be the limit of a play in which $\forall$ plays $a_0\not \le b_0$ initially and schedules all possible subsequent moves. The map taking $a\in {{\mathcal {A}}}$ to the binary relation $\{\, (x, y)\mid a\in N_{a_0,b_0}(x, y)\, \}$ is a homomorphism from ${{\mathcal {A}}}$ to a structure of left-total binary relations over $\mathsf{nodes}(N_{a_0,b_0})$, distinguishing $a_0$ from $b_0$. By considering a disjoint union of networks $N_{a_0, b_0}$ as $a_0\not \le b_0\in {{\mathcal {A}}}$ ranges over all suitable pairs, we obtain a representation of ${{\mathcal {A}}}$.

Take a five character alphabet $\Sigma =\{\, f, {\bar{f}}, g, {\bar{g}}, b\, \}$, let $I=\{\, f, {\bar{f}}, g, {\bar{g}}\, \}\subseteq \Sigma$ (the invertible characters). For $s, t\in \Sigma ^*$, we write st for the concatenation of the two strings. For $s\in I^*$, say $s=(s_0s_1\dots s_{|s|-1})$, we write ${\overline{s}}$ for $(\bar{s}_{|s|-1}\dots {\bar{s}}_0)$ where $\bar{}$ toggles between c and ${\bar{c}}$. For $i, j\le |s|$ let

$$\begin{aligned} s[i, j] = {\left\{ \begin{array}{ll} (s_is_{i+1}\dots s_{j-1})&{} \text{ if } i\le j,\\ \overline{s[j, i]}&{} \text{ if } i>j. \end{array}\right. } \end{aligned}$$

Fix $1\le n<\omega$. We define a binary relation ${\le _0}$ over $\Sigma ^*$ as follows:

$$\begin{aligned} \Lambda&\le _0 f{\bar{f}} \le _0\Lambda ,&\Lambda&\le _0 {\bar{g}} g \le _0 \Lambda ,\\ \Lambda&\le _0 {\bar{f}} f,&\Lambda&\le _0g {\bar{g}},\\ b&\le _0(fg)^n. \end{aligned}$$

Let ${\le _1} = \{\, (\sigma u \tau , \sigma s \tau )\mid \sigma , u, s, \tau \in \Sigma ^*, u\le _0 s\, \}$ and let $\le$ be the reflexive, transitive closure of $\le _1$. Write $s\equiv t$ if $s\le t\wedge t\le s$.

For any string s, if we delete all substrings ${\bar{g}}g$ and $f\bar{f}$ we get ${{\,\mathrm{\mathsf{nf}}\,}}(s)\equiv s$ in normal form. It now follows routinely from the definition that for strings s and t, $s\equiv t$ if and only if ${{\,\mathrm{\mathsf{nf}}\,}}(s)={{\,\mathrm{\mathsf{nf}}\,}}(t)$. The ordering $\le$ is well-founded, over the strings in normal form. The following algebra is defined in [7, Definition 11].

Definition 2.3

Let $n\ge 1$. ${{\mathcal {A}}}_n$ is the $\{\, \le , 1',;\, \}$-structure having elements the normal form $\Sigma ^*$-strings, ordered by $\le$, where the identity is the empty string and where composition is given by

$$\begin{aligned} s; t={{\,\mathrm{\mathsf{nf}}\,}}(st). \end{aligned}$$

Clearly $\le$ is antisymmetric over ${{\mathcal {A}}}_n$ and the empty string is a two-sided identity for composition. Also note, for $v\in I^*$,

$$\begin{aligned} s; t\ge v \iff \exists s_0, t_0\in {{\mathcal {A}}}_n (v\equiv s_0t_0\wedge \exists u\in I^*(s_0u\le s\wedge {\bar{u}} t_0\le t)). \end{aligned}$$

(2.1)

Lemma 2.4

${{\mathcal {A}}}_n$ is not $(\le , 1', ;)$-representable (by any type of binary relations).

Proof

Suppose for contradiction that $\theta$ is a representation of ${{\mathcal {A}}}_n$. Note that $b\not \le b; ({\bar{g}}{\bar{f}})^n; b$. So there are x, y such that $(x, y)\in b^\theta \setminus (b; ({\bar{g}}{\bar{f}})^n; b)^\theta$. But since $(x, y)\in b^\theta \subseteq ((fg)^n)^\theta$, there must be a sequence $z_0, z_1, \dots , z_{2n}$ where ${z_0=x}, {z_{2n}=y}, (z_{2i}, z_{2i+1})\in f^\theta , (z_{2i+1}, z_{2i+2})\in g^\theta$, for $i<n$. For any w, z if $(w, z)\in g^\theta$ then since $(w, w)\in {1'}^\theta$ and $g; {\bar{g}}\ge 1'$, there is v such that $(w, v)\in g^\theta , (v, w)\in {{\bar{g}}}^\theta$, but then $(v, z)\in ({\bar{g}}; g)^\theta \subseteq {1'}^\theta$ (by w) so $v=z$ and $(z, w)\in {\bar{g}}^\theta$. Similarly for f. But then $(x, y)\in (b; ({\bar{g}}{\bar{f}})^n; b)^\theta$, a contradiction.

$\square$

The proof of the following lemma is based on the proof of [7, Theorem 19], but the representation game here includes domain moves, so our proof requires some modification (given in the appendix).

Lemma 2.5

Suppose $2^k<n<\omega$. $\exists$ has a winning strategy in the k round representation game over ${{\mathcal {A}}}_n$.

Since a winning strategy in a finite length game may be expressed by a first order formula, the lemma below follows, by Łoś’ Theorem.

Lemma 2.6

• (1) $\exists$ has a winning strategy in $\Gamma _\omega ({{\mathcal {A}}})$ where ${{\mathcal {A}}}$ is a non-principal ultraproduct of the ${{\mathcal {A}}}_n$,

• (2) $\exists$ has a winning strategy in $\Gamma _\omega ({{\mathcal {A}}}_0)$ for some countable elementary substructure ${{\mathcal {A}}}_0$ of ${{\mathcal {A}}}$.

Theorem 2.7

There is no finite axiomatisation of any class of representable $(\le , 1', ; )$-structures containing all algebras of left-total binary relations.

Proof

Suppose for contradiction that ${{\mathcal {K}}}$ is such a class, axiomatised by a single formula $\phi$. Since ${{\mathcal {A}}}_n$ is not representable we have ${{\mathcal {A}}}_n\not \models \phi$, for each $n<\omega$. But by Lemmas 2.5 and 2.6, ${{\mathcal {A}}}\in {{\mathcal {K}}}$ where ${{\mathcal {A}}}$ is a countable elementary subalgebra of $\prod _U{{\mathcal {A}}}_n$, so ${{\mathcal {A}}}\models \phi$ by Lemma 2.2, hence $\prod _U{{\mathcal {A}}}_n\models \phi$. This contradicts Łoś’ Theorem. $\square$

3 Extending the signature

So now we know that $R(\le , 1', ;)$ is not finitely axiomatisable nor, by [8], is R(D, ; ). In this section we extend those results to various signatures, possibly with ordinary inclusion and composition replaced by demonic variants.

We extend the signature $\{\, \le , 1', ; \, \}$ to in two stages. First we extend to the signature $\{\, \le , \sqsubseteq , 1', D, \circ , ; , *\, \}$. So letting ${{\mathcal {A}}}$ be a $(\le , 1', ; )$-structure, let ${{\mathcal {A}}}'=(A, \le , \sqsubseteq , 1', D, \circ , ; , *)$ be the expansion of ${{\mathcal {A}}}$ where $\{\, \sqsubseteq , *\, \}$ coincides with $\{\, \le , ; \, \}$, $D(a)=1'$ and $a\circ b=b$ for all $a, b\in A$.

The following is easily checked.

Lemma 3.1

If ${{\mathcal {A}}}\in L(\le , 1', ; )$ then ${{\mathcal {A}}}'\in L(\le , \sqsubseteq , 1', D, \circ , ; , *)$.

Next we extend to the signature by defining a structure ${{\mathcal {A}}}^\Downarrow$ over the set $A^\Downarrow$ of downward closed subsets of A and where the predicates and operations are defined as $\emptyset , Ant, \le$ (for the first three), where for all downwards closed sets $\alpha , \beta$ we have $\alpha \sqsubseteq \beta \iff (\beta =\emptyset \vee \alpha \le \beta )$, is the empty set if either $\alpha$ or $\beta$ is empty else it is $\alpha \cup \beta$, the identity is $\{\, 1'\, \}$ (note that this is downward closed as $1'$ is minimal in ${{\mathcal {A}}}\in L(\le , 1', ; )$), and the remaining operations are defined as follows:

$$\begin{aligned} D(\alpha )&={\left\{ \begin{array}{ll}\{\, 1'\, \}&{} \text{ if } \alpha \ne \emptyset \\ \emptyset &{} \text{ if } \alpha =\emptyset ,\end{array}\right. } \\ Ant(\alpha )&={\left\{ \begin{array}{ll}\emptyset &{} \text{ if } \alpha \ne \emptyset \\ \{\, 1'\, \}&{} \text{ if } \alpha =\emptyset ,\end{array}\right. }\\ \alpha \circ \beta&={\left\{ \begin{array}{ll}\beta &{} \text{ if } \alpha \ne \emptyset \\ \emptyset &{} \text{ if } \alpha =\emptyset ,\end{array}\right. }\\ \alpha ; \beta =\alpha *\beta&=\{\, a; b \mid a\in \alpha , b \in \beta \, \}^\downarrow . \end{aligned}$$

(Here, for $S\subseteq A$, we are defining $S^\downarrow =\{\, t\in A\mid \exists s\in S : s\ge t\, \}\in A^\Downarrow$.) The reader may easily verify that the map $a\mapsto a^\downarrow =\{\, b\in A\mid b\le a\, \}$ is an embedding of ${{\mathcal {A}}}$ into the $(\le , 1', ; )$-reduct of ${{\mathcal {A}}}^\Downarrow$.

Lemma 3.2

If ${{\mathcal {A}}}\in L(\le , 1', ; )$ then .

Proof

If $\theta$ is a left-total $(\le , 1', ; )$-representation of ${{\mathcal {A}}}$ over base set X then we may define $\theta ^+:A^\Downarrow \rightarrow \wp (X\times X)$ by

$$\begin{aligned} \alpha ^{\theta ^+}=\bigcup _{a\in \alpha }a^\theta . \end{aligned}$$

By definition, $\theta ^+$ respects sums (that is, unions), and each non-empty downset is interpreted as a left-total relation, hence all relations and operations are interpreted correctly and $\theta ^+$ is a representation of ${{\mathcal {A}}}^\Downarrow$ with the required signature: in . $\square$

Recall the $(\le , 1', ; )$-structures ${{\mathcal {A}}}_n$ of Definition 2.3. Each ${{\mathcal {A}}}_n$ is not in $R(\le , 1', ; )$ but a non-principal ultraproduct ${{\mathcal {A}}}=\prod _U{{\mathcal {A}}}_n$ belongs to $L(\le , 1', ; )$ as seen in the previous section. So .

Theorem 3.3

For any signature containing (i) either the identity $1'$ or D, (ii) $\le$ or $\sqsubseteq$ and (iii) ;  or $*$, there is no finite axiomatisation of R(S).

Proof

Let S be a signature as in the theorem. The proof of Lemma 2.4 requires only minor modification to show that the S-reduct of ${{\mathcal {A}}}^\Downarrow _n$ is not in R(S), for each finite n, but a non-principal ultraproduct $\prod _U({{\mathcal {A}}}_n^\Downarrow )$ embeds into $(\prod _U{{\mathcal {A}}}_n)^\Downarrow ={{\mathcal {A}}}^\Downarrow$ the S-reduct of which belongs to R(S) by Lemmas 2.6 and 3.2. The theorem follows, by Łoś’ Theorem. $\square$

For signatures without ordering, a different construction is used. In [8], for each n, a $(0, 1', D, Ant, ;)$-structure ${{\mathcal {B}}}_n$ is defined, the (D, ; )-reduct of which has no (D, ; )-representation but where a non-principal ultraproduct $\prod _U{{\mathcal {B}}}_n$ has a $(0, 1', D, Ant, ;)$-representation. For this construction, elements of the ultraproduct cannot typically be represented as left-total relations. The proof of non-representability of ${{\mathcal {B}}}_n$ is based on defining a binary relation $\preceq$ over ${{\mathcal {B}}}_n$ consisting of all pairs ((a; D(b); c), (a; c)).

In any (D, ; )-representation $\theta$, we have $a\preceq b\implies a^\theta \subseteq b^\theta$ (although $\le$ is not in the signature). By construction, ${{\mathcal {B}}}_n$ contains an n-cycle $c_0\prec c_1\prec \dots \prec c_{n-1}\prec c_0$ (but no $n-1$-cycle) [8, Lemma 3.8], hence it can have no faithful representation. We may expand these structures ${{\mathcal {B}}}_n$ to structures ${{\mathcal {B}}}_n'$ of the signature $\{\, 0, 1', D, Ant, \circ , ;, *\, \}$ by letting

$$\begin{aligned} a\circ b&=D(a); b,\\ a*b&=Ant(a; Ant(b)); a; b. \end{aligned}$$

Lemma 3.4

If S is a signature consisting of operations that can be defined from the operations $0, 1', D, Ant, ;$, and contains ;  and either D or $\circ$, then ${{\mathcal {B}}}_n'$ is not S-representable.

Proof

When $S\supseteq \{\, D, ;\, \}$ then ${{\mathcal {B}}}_n'$ has no S-representation [8]. If S does not include D then it includes $\circ$. We may define $\preceq '$ as follows:

$$\begin{aligned} {\preceq '}=\{\, ((a; (b\circ c)), (a; c))\mid a, b, c\in {{\mathcal {B}}}_n\, \}, \end{aligned}$$

and we still have $a\preceq 'b\implies a^\theta \subseteq b^\theta$ for any S-representation $\theta$, and a cycle $c_0\prec 'c_1\prec '\dots \prec 'c_{n-1}\prec 'c_0$. It follows that ${{\mathcal {B}}}_n'$ has no S-representation. $\square$

We note that the D-free case of this result was shown using essentially the same argument in Section 10.1 of [13].

Theorem 3.5

Let $S\subseteq \{\, 0, 1', D, Ant, \circ , ;, *\, \}$ contain ;  and either D or $\circ$. The representation class R(S) is not finitely axiomatisable.

Proof

The reduct of ${{\mathcal {B}}}'_n$ to S is not S-representable by Lemma 3.4. But a non-principal ultraproduct $\prod _U ({{\mathcal {B}}}_n')\cong (\prod _U{{\mathcal {B}}}_n)'$ has a $(0, 1', D, Ant, ;)$-representation $\theta$ which induces an S-representation of the S-reduct of $\prod _U {{\mathcal {B}}}_n'$. The theorem follows, by Łoś’ Theorem. $\square$

Remark 3.6

(i) This construction cannot be used to prove the non-finite axiomatisability of R(S) when S includes $*$ instead of ;  (indeed by Lemma 4.2, $R(D, *)$ is finitely axiomatised, as is $R(\circ , *)$). If we define $\preceq ^*$ by $\{\, ((a*D(b)*c), (a*c))\mid a, b, c, \in {{\mathcal {B}}}_n\, \}$ or $\{\, ((a*(b\circ c)), (a*c))\mid a, b, c\in {{\mathcal {B}}}_n\, \}$ then $c_i\preceq ^*c_{i+1}$ fails, so the proof of non-S-representability of ${{\mathcal {B}}}_n'$ fails.

(ii) Theorems 3.3 and 3.5 extend to signatures including range and anti-range (defined in the obvious way), similarly.

For signatures that do not include $1', D$ or Ant, additional negative results can be obtained from [1].

Proposition 3.7

For there is no finite axiomatisation of R(S).

Proof

The proof is entirely based on the non-finite axiomatisability of R(S), where $\{\, +, ;\, \}\subseteq S\subseteq \{\, 0, 1, +, 1', {}^{\smile }, ;\, \}$ [1, Theorem 31]. (Here ${}^{\smile }$ denotes relational converse.) Andréka constructs finite $(0, 1, +, 1', {}^{\smile }, ;)$-algebras ${{\mathcal {A}}}_n$ the reduct to $(+, ;)$ of which is not in $R(+, ;)$ but with a non-principal ultraproduct ${{\mathcal {A}}}=\prod _U{{\mathcal {A}}}_n\in R(0, 1, +, 1', {}^{\smile }, ;)$. Let $\theta$ be a $(0, 1, +, 1', {}^{\smile }, ;)$-representation of ${{\mathcal {A}}}$ over base set X say. Pick $z\not \in X$ and define a $(+, ;)$-representation $\theta '$ of ${{\mathcal {A}}}$ over base set $X\cup \{\, z\, \}$ by letting $a^{\theta '}=a^\theta \cup \{\, (x, z)\mid x\in X\cup \{\, z\, \}\, \}$, note that zero 0, the identity $1'$ and converse ${}^{{\smile }}$ are no longer represented correctly, but $\theta '$ is faithful and preserves $+$ and ; , and hence it is a $(+, ;)$-representation and each element is represented by $\theta '$ as a left-total relation over $X\cup \{\, z\, \}$.

In such a representation, coincides with $\{\, \le , \cup , ;\, \}$. So, we modify the algebra ${{\mathcal {A}}}_n$ by reducing to the signature $\{\, +, ;\, \}$, then expanding to a -structure ${{\mathcal {A}}}_n'$ by letting $a\le b\iff a+b=b$. We have and $s\circ t=t$ (all s, t), the $(+, ;)$-reduct of each ${{\mathcal {A}}}'_n$ is not $(+, ;)$-representable, but the non-principal ultraproduct $\prod _U({{\mathcal {A}}}_n') \cong (\prod _U{{\mathcal {A}}}_n)'$ is -representable. The proposition follows, by Łoś’ Theorem.

$\square$

4 Finite axiomatisations

We have seen that the axioms of ordered semigroups define $R(\le , ;)$ and also define $R(\sqsubseteq , *)$. Now consider signatures $\{\, D, ;\, \}$ and $\{\, D, *\, \}$. Although R(D, ; ) is known to be non-finitely axiomatisable, P(D, ; ) does have a finite axiomatisation.

Definition 4.1

A left restriction semigroup is an algebra $(A, D, \cdot )$ where $\cdot$ is associative and

$$\begin{aligned} D(a)\cdot a&=a,&D(a)\cdot D(b)&=D(b)\cdot D(a),&D(D(a)\cdot b)&=D(D(a)\cdot D(b)), \end{aligned}$$

(4.1)

(valid over binary relations with domain and composition) together with

$$\begin{aligned} a\cdot D(b)&=D(a\cdot b)\cdot a. \end{aligned}$$

(4.2)

Though not valid in general for binary relations with domain and composition, this last axiom is valid over algebras of partial functions under domain and composition. Curiously, as has been noted by several authors (again, see [4] for example), (4.1) and (4.2) are valid over binary relations with domain and demonic composition. Any left restriction semigroup ${{\mathcal {A}}}=(A, D, \cdot )$ has a representation $\theta$ to an algebra of partial functions on the base set A with domain and composition, where for each $a\in {{\mathcal {A}}}$, $a^\theta$ is the partial function over A given by

$$\begin{aligned} a^\theta (b)={\left\{ \begin{array}{ll}b\cdot a&{} \text{ if } b\cdot D(a)=b\\ \text{ undefined }&{} \text{ if } b\cdot D(a)\ne b.\end{array}\right. } \end{aligned}$$

(See [19] or [12], amongst others). So every left restriction semigroup is isomorphic to an algebra of partial functions with domain and composition, which coincides with an algebra of partial functions with domain and demonic composition, which is an algebra of binary relations with domain and demonic composition. Hence we obtain the following.

Lemma 4.2

$P(D, ;)=P(D, *)=R(D, *)$ is axiomatised by the laws of left restriction semigroups.

The following are now easily verified (since they are functionally valid).

Lemma 4.3

If $(A,D,*)$ is a left restriction semigroup, then for $a,b\in A$:

• (1) $D(a)*D(a)=D(a)$,

• (2) $D(a)*D(b)=D(b)*D(a)=D(D(a)*b)$,

• (3) $D(a*b)*D(a)=D(a*b)$,

• (4) $D(a*b)=D(a*D(b))$.

Moreover $D(A)=\{\, D(a)\mid a\in A\, \}$ is a semilattice under $*$, with associated partial order given by $D(a)\le D(b)$ if and only if $D(a)*D(b)=D(a)$.

A further case where R(S) is finitely axiomatisable is $S=(\le , D, {}^{\smile }, ;)$, where ${}^{\smile }$ is the unary operation that returns the converse of a relation. This result and a finite axiomatisation are due to Bredhikin [3], while Hirsch and Mikulas showed that if the algebra is finite then the base set of the representation can be chosen to be finite [9].

So we know that the representation class R(S) is finitely axiomatisable when $S=(\sqsubseteq , *)$ (ordered semigroups), or $S=(D, *)$ (left restriction semigroups). Similarly, the representation class P(S) is finitely axiomatised in each of these cases also. For the first case, it is the ordered semigroups satisfying one additional law as in [15] (see also [18]), which when expressed in terms of $\sqsubseteq$ (which is the opposite of inclusion on partial functions) is as follows:

$$\begin{aligned} (x*v \sqsubseteq z) \wedge (u*y\sqsubseteq z) \wedge (u\sqsubseteq x) \implies x*y\sqsubseteq z, \end{aligned}$$

where some or all of u, v, x, y, z may be formally replaced by a multiplicative identity element e. For the other case, $P(D, *)$ is defined by the same axioms (Definition 4.1) that define $R(D, *)$.

The remaining cases where we have finite axiomatisations of R(S) are cases where S includes the left restrictive multiplication operation $\circ$, which has some resemblance to D. Over R(S) and hence also over P(S), $\circ$ can be expressed in terms of D and composition as $a\circ b=D(a); b=D(a)*b$, but conversely D cannot be expressed in terms of $\circ$ and composition (or indeed $\circ$ and $*$) alone, unless an identity element $1'$ modelling the diagonal relation is included in the signature, in which case $D(a)=a\circ 1'$.

In Theorem 4.7, we saw that $R(\sqsubseteq , D, *)$ has no finite axiomatisation. Our ‘consolation prize’ is to obtain a finite axiomatisation for $R(\sqsubseteq ,\circ ,*)$. This is perhaps surprising, considering how close the two signatures are (and how similar the proofs of finite axiomatisability are in the partial function case). The order-free part of this axiomatisation defines $R(\circ , *)$. Recall that in the presence of $\circ$, inclusion and $\sqsubseteq$ are inter-definable, using (1.1), (1.2). These definitions allow us to derive a finite axiomatisation of $R(\le , \circ , *)$ from a finite axiomatisation of $R(\sqsubseteq , \circ , *)$.

Definition 4.4

A right normal band $(A, \circ )$ is a semigroup satisfying

$$\begin{aligned} a\circ a=a \text{ and } (a\circ b)\circ c=(b\circ a)\circ c. \end{aligned}$$

(4.3)

A 1-stack is a structure $(A, \circ , \cdot )$ where both operations are associative, $\circ$ satisfies (4.3) and for all $a, b, c \in A$,

• $a\circ (b\cdot c)=(a\circ b)\cdot c$,

• $a\cdot (b\circ c)=(a\cdot b)\circ (a\cdot c)$.

The 1-stack axioms above are given in [17], where it is noted that they axiomatise $P(;,\circ )$. In the functional case, the representability of 1-stacks and of left restriction semigroups run in close parallel. In a left restriction semigroup ${{\mathcal {A}}}=(A, D, \cdot )$ we may define $\circ$ by

$$\begin{aligned} a\circ b=D(a)\cdot b \end{aligned}$$

(4.4)

for all $a, b\in A$ and then $(A, \circ , \cdot )$ is a 1-stack (and hence is representable as partial functions), and so it follows that $R(D, \circ , ;)$ is axiomatised by the 1-stack laws together with (4.4).

A rather similar signature is $S=\{\, \sqsubseteq ,\circ ,*\, \}$. In the functional case, $\sqsubseteq$ is the converse of inclusion and can be expressed as

$$\begin{aligned} a\sqsubseteq b\iff b\circ a=b, \end{aligned}$$

(4.5)

and so the 1-stack axioms with (4.5) define $P(\sqsubseteq , \circ , *)$. But in the relational case (4.5) fails, and indeed $R(\sqsubseteq , D, *)$ is not finitely axiomatisable (Theorem 2.7).

Now we prove these results.

Lemma 4.5

Every 1-stack ${{\mathcal {A}}}=(A,\circ ,*)$ embeds in a left restriction semigroup ${{\mathcal {A}}}^+=(A^+,D,*)$, obtained from ${{\mathcal {A}}}$ by adding in only domain elements (so that $A^+=A\cup \{\, D(a)\mid a\in A\, \}$), in such a way that the restriction to A of the derived left restrictive multiplication in ${{\mathcal {A}}}^+$ coincides with the left restrictive multiplication operation in ${{\mathcal {A}}}$: for all $a,b\in A$, $D(a)*b$ computed in ${{\mathcal {A}}}^+$ is equal to $a\circ b$ computed in ${{\mathcal {A}}}$.

Proof

${{\mathcal {A}}}$ is isomorphic to a 1-stack of partial functions; identify A with this copy. Now just add in the domain D(s) of each $s\in A$ (if not already present) to give $A^+$. It is easy to see that $A^+$ is closed under domain and indeed composition: for all $s,t\in A$, $D(s)*t=s\circ t$, $s*D(t)=D(s*t)*s=(s*t)\circ s$, $D(s)*D(t)=D(D(s)*t)=D(s\circ t)$. So ${{\mathcal {A}}}^+$ is a left restriction semigroup. Clearly for $s,t\in A$, $s\circ t=D(s)*t$. $\square$

Definition 4.6

Let ${{\mathcal {A}}}$ be a 1-stack. We call any left restriction semigroup ${{\mathcal {A}}}^+$ such that $A^+=A\cup D(A^+)$ and $s\circ t=D(s)*t$ for all $s,t\in A$ an extension by domains of ${{\mathcal {A}}}$.

By Lemma 4.5, every 1-stack has an extension by domains. One can think of the elements D(a) in such an extension by domains as domain elements, with caution, noting that in a $(\circ , *)$-representation D(a) need not be a restriction of the identity. We will use an extension by domains ${{\mathcal {A}}}^+$ of ${{\mathcal {A}}}$ as the base set of a representation of ${{\mathcal {A}}}$.

But first we add an ordering and consider the signature $S=\{\, \sqsubseteq , \circ , *\,\}$. We will give a finite axiomatisation of $R(\sqsubseteq , \circ , *)$ and from this we will derive a finite axiomatisation of $R(\le , \circ , *)$.

For the signature $\{\, \sqsubseteq , \circ , *\, \}$, the ordered 1-stack laws $\Sigma _1$ consist of the 1-stack laws together with:

• (1) $\sqsubseteq$ is a partial order,

• (2) both $({{{\mathcal {A}}}},\sqsubseteq ,*)$ and $({{{\mathcal {A}}}},\sqsubseteq ,\circ )$ are ordered semigroups (associative, partially ordered, monotonic in both arguments),

• (3) for all $a, b \in {{{\mathcal {A}}}}$, $a\circ b\sqsupseteq b$.

Theorem 4.7

$R({\sqsubseteq , \circ , * })$ is axiomatised by the finite theory $\Sigma _1$.

Proof

It is easy to verify $R(\sqsubseteq , \circ , *)\models \Sigma _1$. To show completeness, we must represent an ordered 1-stack ${{{\mathcal {A}}}}=(A,\sqsubseteq ,\circ ,*)$ relationally.

First embed the 1-stack $(A, \circ , *)$ in an extension by domains ${{\mathcal {A}}}^+=(A^+, D, *)$, a left restriction semigroup. We shall embed ${{{\mathcal {A}}}}$ in ${{\,\mathrm{\mathsf{Rel}}\,}}(A^+)$, the set of binary relations on ${A^+}$ equipped with demonic composition, refinement and left restrictive multiplication. Throughout what follows we freely use the left restriction semigroup laws in ${{\mathcal {A}}}^+$, including those listed in Lemma 4.3, as well as the ordered 1-stack laws when dealing with elements of A.

Define the mapping $\theta :{{{\mathcal {A}}}}\rightarrow {{\,\mathrm{\mathsf{Rel}}\,}}({A^+})$ as follows. For $a\in {{\mathcal {A}}}$ and $x, y\in {{\mathcal {A}}}^+$ let

$$\begin{aligned} (x,y)\in a^\theta \iff (y\in A)\wedge (x*a\sqsupseteq y)\wedge (D(x*a)=D(x)=D(y)). \end{aligned}$$

(4.6)

Note that $x*a$ is evaluated in ${{\mathcal {A}}}^+$ but gives an element of ${{\mathcal {A}}}$, so $x*a\sqsupseteq y$ can be evaluated in ${{\mathcal {A}}}$. For $a\in {A}$, note that $x\in {{\,\mathrm{dom}\,}}(a^\theta )$ requires that $D(x*a)=D(x)$ and then $(x,x*a)\in a^\theta$. So

$$\begin{aligned} x\in {{\,\mathrm{dom}\,}}(a^\theta )\iff D(x*a)=D(x) \iff (x, x*a)\in a^\theta . \end{aligned}$$

Let $a, b\in A$. Next we show that $(a*b)^\theta =a^\theta *b^\theta$. First we show that $(a*b)^\theta$ and $a^\theta *b^\theta$ have the same domains. Consider $x\in {{\,\mathrm{dom}\,}}(a^{\theta }*b^{\theta })$. Then $D(x*a)=D(x)$, and since $(x,x*a)\in a^{\theta }$, it must be that $x*a\in {{\,\mathrm{dom}\,}}(b^{\theta })$, and so $D(x*a*b)=D(x*a)=D(x)$ and so $x\in {{\,\mathrm{dom}\,}}((a*b)^{\theta })$. Conversely, if $x\in {{\,\mathrm{dom}\,}}((a*b)^{\theta })$ then $D(x*a*b)=D(x)$ and so $D(x*a)=D(x)*D(x*a)=D(x*a*b)*D(x*a)=D(x*a*b)=D(x)$. Hence $x\in {{\,\mathrm{dom}\,}}(a^{\theta })$ and $x*a\in {{\,\mathrm{dom}\,}}(b^{\theta })$. So if $(x,y)\in a^{\theta }$ for some $y\in S$, then $y\sqsubseteq x*a$ with $D(y)=D(x*a)$ and so $D(y*b)\le D(y)=D(x*a*b)\le D(y*b)$ using the partial order of domain elements as in Lemma 4.3, so $D(y)=D(y*b)$ and so $y\in {{\,\mathrm{dom}\,}}(b^{\theta })$. Hence $x\in {{\,\mathrm{dom}\,}}(a^{\theta }* b^{\theta })$. So ${{\,\mathrm{dom}\,}}(a^{\theta }*b^{\theta })={{\,\mathrm{dom}\,}}((a*b)^{\theta })$.

If $(x,z)\in a^{\theta }*b^{\theta }$ then there is $y\in S$ such that $(x,y)\in a^{\theta }$ and $(y,z)\in b^{\theta }$, so $y\sqsubseteq x*a$ and $z\sqsubseteq y*b\sqsubseteq x*a*b$, and moreover $D(x)=D(x*a)=D(y)=D(y*b)=D(z)$ with $D(x)=D(x*a*b)$ as shown earlier for $x\in {{\,\mathrm{dom}\,}}(a^{\theta }*b^{\theta })$. Hence $(x,z)\in (a*b)^{\theta }$. So $a^{\theta }*b^{\theta }\subseteq (a*b)^{\theta }$.

If $(x,z)\in (a*b)^{\theta }$ then $z\sqsubseteq x*a*b$ and $D(z)=D(x)$, so letting $y=x*a$, we see that $(x,x*a)\in a^{\theta }$ as above, and $(x*a,z)\in b^{\theta }$ since $z\sqsubseteq x*a*b$ and $D(x*a)=D(x)=D(z)$. So since $x\in {{\,\mathrm{dom}\,}}(a^{\theta }*b^{\theta })$, $(x,z)\in a^{\theta }*b^{\theta }$. So $(a*b)^{\theta }=a^{\theta }*b^{\theta }$.

For preservation of $\sqsubseteq$, suppose $a\sqsubseteq b$. By the third ordered 1-stack law and monotonicity, we have $b\sqsubseteq a\circ b\sqsubseteq b\circ b=b$, so $b=a\circ b=D(a)*b$ in $A^+$. First we show that ${{\,\mathrm{dom}\,}}(b^\theta )\subseteq {{\,\mathrm{dom}\,}}(a^\theta )$. For this, let $x\in {{\,\mathrm{dom}\,}}(b^\theta )$. Then $D(x)=D(x*b)=D(x*D(a)*b)=D(D(x*a)*x*b)=D(x*a)*D(x*b)=D(x*a)*D(x)=D(x*a)$, and so $x\in {{\,\mathrm{dom}\,}}(a^\theta )$. This proves ${{\,\mathrm{dom}\,}}(b^\theta )\subseteq {{\,\mathrm{dom}\,}}(a^\theta )$. For $x\in {{\,\mathrm{dom}\,}}(b^\theta )$ suppose $(x, y)\in a^\theta$. Then $D(x)=D(x*b)$ and $x*a\sqsupseteq y$ implies $x*b\sqsupseteq x*a\sqsupseteq y$, so $(x, y)\in b^\theta$. This proves $a^\theta \sqsubseteq b^\theta$. Conversely, if $b^\theta \sqsupseteq a^\theta$, then ${{\,\mathrm{dom}\,}}(a^\theta )\supseteq {{\,\mathrm{dom}\,}}(b^\theta )$ and

$$\begin{aligned} \forall x\in {{\,\mathrm{dom}\,}}(b^\theta ) : \forall y\in X : ((x, y)\in a^\theta )\implies ((x, y)\in b^\theta ). \end{aligned}$$

Letting $x=D(b)$ and $y=a$ we get $(D(b), a)\in b^\theta$ so $D(b)*b = b \sqsupseteq a$. By preservation of $\not \sqsupseteq$, the map $\theta$ is injective.

Finally we check preservation of $\circ$ and show $a^\theta \circ b^\theta = (a\circ b)^\theta$. To show that the domains of the two sides are equal:

$$\begin{aligned} x\in {{\,\mathrm{dom}\,}}(a^\theta \circ b^\theta )&\iff x\in {{\,\mathrm{dom}\,}}(a^\theta )\cap {{\,\mathrm{dom}\,}}(b^\theta )\\&\iff D(x*a)=D(x*b)= D(x) \\&\iff D(x*a)*D(x*b)= D(x) \\&\iff D(D(x*a)*(x*b))= D(x) \\&\iff D((x*a)\circ (x*b))=D(x)\\&\iff D(x*(a\circ b))=D(x) \\&\iff x\in {{\,\mathrm{dom}\,}}((a\circ b)^\theta ). \end{aligned}$$

Suppose x is in this common domain, so $D(x)=D(x*(a\circ b))=D(x*a)=D(x*b)$. For all $y\in {{\mathcal {A}}}^+$,

$$\begin{aligned} (x, y)\in (a\circ b)^\theta&\iff (x*(a\circ b)\sqsupseteq y) \wedge (D(x)=D(y))\\&\iff ((x*a)\circ (x*b)\sqsupseteq y) \wedge (D(x)=D(y))\\&\iff (D(x*a)*(x*b)\sqsupseteq y) \wedge (D(x)=D(y))\\&\iff (D(x*b)*(x*b)\sqsupseteq y) \wedge (D(x)=D(y))\\&\iff (x*b\sqsupseteq y) \wedge (D(x)=D(y)) \\&\iff ((x, y)\in b^\theta ) \wedge (x\in {{\,\mathrm{dom}\,}}(a^\theta ))\\&\iff (x, y)\in a^\theta \circ b^\theta . \end{aligned}$$

$\square$

Corollary 4.8

$R(\le , \circ , *)$ is finitely axiomatisable.

Proof

Recall from (1.1), (1.2) that demonic refinement and ordinary containment can define each other using left restrictive multiplication. Take the finite axiomatisation $\Sigma _1$ of $R(\sqsubseteq , \circ , *)$, together with (1.1) itself. Then replace each atomic formula $s\sqsubseteq t$ by $t\circ s\le t\wedge s\circ t=t$ to obtain an axiomatisation of $R(\le , \circ , *)$.

The next corollary concerns partial functions. Recall that $\sqsupseteq$ coincides with $\le$ (note the reversal).

Corollary 4.9

$P({\sqsubseteq , \circ , *})$ is axiomatised by $\Sigma _1\cup \{\, a\sqsupseteq b\iff a=a\circ b\, \}$.

Proof

First observe that $a\sqsupseteq b\iff a=a\circ b$ is valid over partial functions. Conversely, let ${{\mathcal {A}}}=(A, \sqsubseteq , \circ , *) \models \Sigma _1\cup \{\, a\sqsupseteq b \iff a=a\circ b\, \}$. As before, let ${{{\mathcal {A}}}^+}=(A^+, D, \circ , *)$ be an extension by domains of $(A, \circ , *)$ and let $\theta$ be defined by (4.6). Then $(c, d)\in a^\theta \implies (c*a\sqsupseteq d)\wedge (D(c*a)=D(d)=D(c))$. By the new axiom, $c*a\sqsupseteq d$ implies $c*a=(c*a)\circ d=D(c*a)*d=D(d)*d=d$. Hence $a^\theta$ is single valued, hence a partial function. It follows that $\theta$ represents ${{\mathcal {A}}}$ as an algebra of partial functions over ${{\mathcal {A}}}^+$. $\square$

Definition 4.10

In the signature $\{\, \sqsubseteq , \circ \, \}$, the ordered band axioms (OB) consist of (i) the axioms for ordered semigroups, (ii) the axioms in (4.3) (Definition 4.4, right normal band axioms) and (iii) $a\circ b\sqsupseteq b$. For the signature $\{\, \le , \circ \, \}$ the dual ordered band axioms ($\hbox {OB}'$) consist of (i), (ii) and $\hbox {(iii)}'$: $a\circ b\le b$.

Corollary 4.11

$R(\sqsubseteq , \circ )$ is defined by OB, $R(\le , \circ )$ is defined by $\hbox {OB}'$.

Proof

Suppose ${{\mathcal {A}}}=(A, \sqsubseteq , \circ )$ satisfies (i), (ii) and (iii). Letting ${*}={\circ }$, it is routine to check that $(A, \sqsubseteq , \circ ,\circ )$ is an ordered 1-stack, since the 1-stack axioms of Definition 4.4 become $x\circ (y\circ z)=(x\circ y)\circ z$ and $x\circ (y\circ z)=(x\circ y)\circ (x\circ z)$, and both equations follow from Definition 4.10(ii). Represent as in Theorem 4.7, then simply ignore the second operation $\circ$ in the representation. The second part of the corollary is similar, using $\ge$ in place of $\sqsubseteq$. $\square$

Fig. 1

Finite axiomatisations of R(S)

5 5. Summary

Figure 1 summarises what we know about finite and non-finite axiomatisability results for various signatures S contained in

For such a signature S, we define its boolean and non-boolean parts to be the respective intersections

The horizontal axis specifies B(S) and the vertical axis specifies N(S). Negative results (marked by $\times$) extend to supersignatures as stated in the cited theorems. Negative results following from Theorem 3.3 extend to signatures including $+$ or . The entries SG, OSG, LRS, 1-St, Ord-1-St denote the finite sets of axioms for semigroups, ordered semigroups, left restriction semigroups, 1-stacks and ordered 1-stacks, respectively. OB and OB$'$ are from Definition 4.10. Reference [10] is a manuscript due to the two authors and S. Mikulas. Entries marked $\times$ have no finite axiomatisations. Under N(S) an entry $S^\uparrow$ can be any signature containing S and contained in $\{\, 1', D, Ant, \circ , ;, *\, \}$.

Axioms for signatures as above but also including intersection (in terms of which inclusion can be expressed) and/or range R are also of interest. Again, some results are known in the functional and angelic relational case. In [11], a finite equational axiomatisation for the variety generated by $R(D,R,*)$ was given, and the question of finite axiomatisability for $R(D,R,*)$ itself was posed there. Our observation (ii) after Theorem 3.5 comes close to resolving this case in the negative.

Appendix

Proof of Lemma 2.5. Recall from Definition 2.3 the $(\le , ;)$-structure ${{\mathcal {A}}}_n$.

Definition 5.1

An element $s\in {{\mathcal {A}}}_n$ is i-short if there are $\alpha _0, \alpha _1, \dots , \alpha _{i-1}\in \{\, {\bar{g}}, f\, \}^*$, $\beta _0, \beta _1, \dots , \beta _{i-1}\in \{\, g, {\bar{f}}\, \}^*$ such that $s\le \alpha _0\beta _0\dots \alpha _{i-1} \beta _{i-1}$. (For example, $b\le (fg)^n$ is n-short but not $n-1$-short.)

A label $s\in N(x, y)$ is witnessed in N if for all u, t where $s=ut$, $ut={{\,\mathrm{\mathsf{nf}}\,}}(ut)$ and u, t are minimal subject to $u; v\in N(x, y)$, there is $z\in \mathsf{nodes}(N)$ such that $u\in N(x, z)$, $t\in N(z, y)$. For $i<n$, an ${{\mathcal {A}}}_n$-network N is i-good if every i-short, minimal label is witnessed.

Lemma 5.2

Let $i, j<\omega$. If $s\in I^*$ and s is i-short then ${\bar{s}}$ is also i-short. If s is i-short and t is j-short and $u\le s; t$ then u is $(i+j)$-short. If s; t is i-short then either $s; t=\Lambda$ or s is i-short.

For the last statement, note that if $s; t=\Lambda$ then $s\in \{\, {\bar{g}}, f\, \}^*$ and $t={\bar{s}}$. Then s is 1-short and if it is non-empty it is not 0-short, but $s; t=\Lambda$ is 0-short. Suppose $s; t\ne \Lambda$. Since $s\in I^*$ we may write $s=\alpha _0\beta _0\dots \alpha _{j-1}\beta _{j-1}$ where $\alpha _k\in \{\, {\bar{f}}, g\, \}^*$, $\beta _k\in \{\, f, {\bar{g}}\, \}^*$ for some j and we may assume that none of the $\alpha _k$ or $\beta _k$ in the decomposition of s is empty except possibly $\alpha _0$ or $\beta _{j-1}$. If s is not i-short then $j>i$. When we multiply s on the right by $t\in I^*$ we might possibly cancel the final $\beta _{j-1}$ (in the case where $t=\overline{\beta _{j-1}}t_0$), but all the other parts of the decomposition of s will be unaffected, hence s; t is not i-short.

In the following, whenever we refer to i-short elements we have $j\le n$, so an i-short element will not involve b.

Lemma 5.3

In a play of $\Gamma _k({{\mathcal {A}}}_n)$, if the current network N is $2^i$-good, then for any move by $\forall$, there is an $2^{i-1}$-good extension $N^+$ of N that $\exists$ can play.

Proof

The proof differs from the proof of [7, Theorem 19] here, because domain moves and range moves are not treated there. Suppose $\forall$ makes a domain move (d, x, a). First suppose $a\in \Sigma$ is a one letter word. If there is $w\in \mathsf{nodes}(N)$ where $a\in N(x, w)$ then she lets $N^+=N$, otherwise she adds a single new node z to N, lets $N^+(z, z)=\Lambda ^\uparrow$ and

$$\begin{aligned} N^+(v, z)&=(N(v, x); a)^\uparrow ,&N^+(z, v)&={\left\{ \begin{array}{ll}\emptyset &{} \text{ if } a=b\\ ({\bar{a}}; N(x, v))^\uparrow &{} \text{ if } a\in I,\end{array}\right. } \end{aligned}$$

for $v\in \mathsf{nodes}(N)$. If $a=b$ then no new irreflexive label is $2^{i}$-short. If $a\in I$ (so a is 1-short), $s\in N(v, x)$ and $s; a\in N^+(v, z)$ is minimal and $2^{i}$-short then either $s; a=\Lambda$ or s is $2^i$-short, by Lemma 5.2. The former case is ruled out by our assumption that no suitable $w\in \mathsf{nodes}(N)$ exists. In the latter case, inductively, we have ${\bar{s}}\in N(x, v)$. Also, we must have $s; a =sa$ (as otherwise a suitable witness already exists in N). If $sa\le ut={{\,\mathrm{\mathsf{nf}}\,}}(ut)$ where $ut\in N(v, z)$ is minimal then $sa=ut$, $t=t_0a$ (some $t_0$) and $s= u t_0$ where $ut_0\in N(v, w)$ is minimal, hence inductively there is $w\in \mathsf{nodes}(N)$ where $u\in N(v, w)$ and $t_0\in N(w, x)$. It follows that $u\in N(v, w)$ and $t=t_0a\in N(w, z)$, so $N^+$ is a consistent, $2^i$-good extension of N. More generally for $a\in \Sigma ^*$ she computes her extension $N^+$ of N by iterating the previous extension |a| times, still $2^i$-good. Her response to a range move (r, x, a) is defined similarly.

Suppose $\forall$ plays a composition move (c, x, y, s, t), so we can assume that s, t are minimal subject to $s; t\in N(x, y)$, that is,

$$\begin{aligned} (s'\le s)\wedge (t'\le t)\wedge (s'; t'\in N(x, y))\implies (s'=s)\wedge (t'=t). \end{aligned}$$

If s, t are both $2^{i-1}$-short then $s; t\in N(x, y)$ is $2^i$-short by Lemma 5.2. By (2.1) and minimality of s, t, there are $s_0, t_0, u\in \{\, f, {\bar{f}}, g, {\bar{g}}\, \}^*$ such that $s=s_0u$, $t={\bar{u}} t_0$ and $s_0t_0\in N(x, y)$ is minimal. Since N is $2^i$-good there is $v\in \mathsf{nodes}(N)$ such that $N(x, v)=s_0$, $N(v, y)=t_0$. $\exists$ pretends (to herself) that $\forall$ played (d, v, u) to compute her extension $N^+$, as above, so $s=s_0; u\in N^+(x, z)$, $t={\bar{u}}; t_0\in N^+(z, y)$. Again, $N^+$ is a legal $2^i$-good (hence $2^{i-1}$-good) extension of N.

Suppose s is $2^{i-1}$-short but t is not. First suppose $s=c\in I$, a one letter word. If there is $v\in \mathsf{nodes}(N)$ such that $N(x, v)=c$, $N(v, y)\le t$ then $\exists$ may let $N^+=N$, if not $\exists$ adds a single new node z to the network and lets

$$\begin{aligned} N^+(v, z)&=(N(v, x); c)^\uparrow ,\\ N^+(z, z)&=\Lambda ^\uparrow ,\\ N^+(z, v)&=({\bar{c}}; N(x, v)\cup t; N(y, v))^\uparrow , \end{aligned}$$

for $v\in \mathsf{nodes}(N)$.

Since t is not $2^{i-1}$-short, the only new $2^{i-1}$-short labels have the form $u; c\in N^+(v, z)$ and ${\bar{c}}{\bar{u}}\in N^+(z,v)$, for $2^{i-1}$-short $u\in N(v, x)$, and since we are assuming that no witness for the composition exists in N we must have $uc={{\,\mathrm{\mathsf{nf}}\,}}(uc)$. As in the proof that her response to domain moves is $2^i$-good, a minimal label $uc={{\,\mathrm{\mathsf{nf}}\,}}(uc)\in N^+(v, z)$ is witnessed, where $u\in N(v, x)$ is $2^{i}$-short. Hence $N^+$ is $2^{i-1}$-good. More generally, in response to a move (c, x, y, s, t) where s is $2^{i-1}$-short but t is not, she computes her $2^{i-1}$-good response $N^+$ by iterating the preceeding 1-character case |s| times. The case where t is $2^{i-1}$-short but s is not is similar.

Finally, if neither s nor t is $2^{i-1}$-short then $\exists$ adds a single new node z and lets $N^+(v, z)=(N(v, x); s)^\uparrow$, $N^+(z, v)=(t; N(y, v))^\uparrow$, for $v\in \mathsf{nodes}(N)$ and of course $N^+(z, z)=\Lambda ^\uparrow$. No irreflexive edges incident with the new node z have $2^{i-1}$-short labels by Lemma 5.2, so $N^+$ is $2^{i-1}$-good. $\square$

We are now in a position to prove Lemma 2.5.

Proof

In the initial round, if $\forall$ plays $a\not \le c$ and a is not $2^k$-short then $\exists$ plays $N_0$ where $\mathsf{nodes}(N_0)=\{\, x, y\, \}$, $N_0(x, y)=a^\uparrow$, $N_0(x, x)=N_0(y, y)=\Lambda ^\uparrow$ and $N_0(y, x)=\emptyset$. If a is $2^k$-short then it is in $I^*$, say $a=a_0a_1\dots a_{|a|-1}$, then $N_0$ has $|a|+1$ nodes $x=x_0, x_1, \dots , x_{|a|}=y$ and $N_0(x_i, x_j)=a[i, j]^\uparrow$, for all $i, j\le |a|$. Observe that $N_0$ is $2^k$-good. By the previous lemma, $\exists$ can play a $2^{k-i}$-good extension network $N_i$ in each round. Since $N_i$ is an extension of $N_0$ we have $c\not \in N_i(x, y)=N_0(x, y)$, so $\exists$ wins the play. $\square$