Ordered Monoids: Languages and Relations

TL;DR

This paper provides a finite set of axioms for the class of relational, integral ordered monoids and their language interpretations, advancing the algebraic understanding of these structures.

Contribution

It introduces a finite axiomatization for the variety generated by relational, integral ordered monoids and their language interpretations, which was previously unknown.

Findings

Finite axiomatization for relational, integral ordered monoids.

Finite axiomatization for their language interpretation.

Enhanced algebraic understanding of these structures.

Abstract

We give a finite axiomatization for the variety generated by relational, integral ordered monoids. As a corollary we get a finite axiomatization for the language interpretation as well.

Equations

$$a;b=\{st:s\in a\text{mbox}andt\in b\}$$

$$a;b$$

$$1^{\prime }$$

$$(x\cdot x^{\prime });(y\cdot y^{\prime })\le x;y$$

$$0$$

$$(1^{\prime }\cdot x);(1^{\prime }\cdot y)$$

$$(1^{\prime }\cdot x);(y\cdot z)$$

$$(x\cdot y);(1^{\prime }\cdot z)$$

$$1^{\prime }\cdot x;y$$

$$(1^{\prime }\cdot x);y$$

$$(x+y);z$$

$$x;(y+z)$$

$$x;y\cdot 1^{\prime }=(x\cdot 1^{\prime });(y\cdot 1^{\prime })$$

$$(e_1;x;e_2)\cdot (e_3;x;e_4)=(e_1\cdot e_3);x;(e_2\cdot e_4)$$

$$e;(x\cdot y)=e;x\cdot e;y=e;x\cdot y=x\cdot e;y$$

$$X;Y$$

$$\mathcal{E}(\tau ):$$

$$=\mathcal{F}(\{ϵ\le 1^{\prime }:\tau ;ϵ=\tau \})$$

$$=\mathcal{F}(\{ϵ\le 1^{\prime }:ϵ;\tau =\tau \})$$

$$\tau \le \sigma \text{mbox}implies\mathcal{E}(\sigma )\subseteq \mathcal{E}(\tau )$$

$${\ell }_0(u_0,v_0)$$

$${\ell }_0(u_0,u_0)$$

$$({ϵ}_0\cdot ϵ);\rho ;({ϵ}_0\cdot ϵ)\cdot \tau ;\sigma =({ϵ}_0\cdot ϵ);\rho ;({ϵ}_0\cdot ϵ)\cdot ({ϵ}_0\cdot ϵ);\tau ;({ϵ}_0\cdot ϵ);\sigma$$

$$1^{\prime }\in \mathcal{F}(\mathcal{E};\tau ;\mathcal{E})\text{mbox}implies\tau \in {\ell }_n(u,u)\text{mbox}and\sigma \in {\ell }_n(u,v)$$

$$ϵ;\rho ;ϵ$$

$$=(ϵ;\rho ;ϵ)\cdot (ϵ;\tau ;ϵ;\sigma )$$

$$\le \rho \cdot \sigma$$

$$\le \sigma$$

$$(ϵ;\tau ;ϵ);(ϵ;\rho ;ϵ)$$

$$=(ϵ;\tau ;ϵ);((ϵ;\tau ;ϵ;\sigma )\cdot ϵ;\rho ;ϵ)$$

$$=(ϵ;\tau ;ϵ;\sigma )\cdot (ϵ;\rho ;ϵ)$$

$$=(\tau ;\sigma )\cdot (ϵ;\rho ;ϵ)$$

$$=ϵ;\rho ;ϵ$$

$${\ell }_{n+1}(w,w)$$

$${\ell }_{n+1}(t,w)$$

$${\ell }_{n+1}(w,s)$$

$${\ell }_{n+1}(u,w)=\mathcal{F}(\mathcal{E};\tau ;\mathcal{E})\text{mbox}and{\ell }_{n+1}(w,v)=\mathcal{F}(\mathcal{E};\sigma ;\mathcal{E})$$

$${\ell }_{n+1}(t,w)$$

Full text

Keywords: finite axiomatizability, algebras of relations, language algebras

1. Introduction

We will focus on algebras of similarity type $\Lambda\subseteq(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ where $\mathbin{+},\mathbin{\cdot\,},\mathbin{;}$ are binary operations and $0,{1^{\prime}}$ are constants. We will consider two types of representations: as families of binary relations and as families of languages. Our main concern is whether the varieties generated by these interpretations are finitely axiomatizable.

Definition 1.1**.**

[Language algebras] Let $\mathfrak{A}=(A,\Lambda)$ be an algebra of similarity type $\Lambda\subseteq(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. We say that $\mathfrak{A}$ is a language algebra if the following holds. There is an alphabet $\Sigma$ such that $A$ is a family of languages over $\Sigma$, i.e., $A\subseteq\wp(\Sigma^{*})$ where $\Sigma^{*}$ denotes the set of words (finite strings) over $\Sigma$, and the operations in $\Lambda$ are interpreted as follows: join $\mathbin{+}$ is union, meet $\mathbin{\cdot\,}$ is intersection, composition $\mathbin{;}$ is concatenation

[TABLE]

[math] is the empty language $\emptyset$ and ${1^{\prime}}$ is the singleton language consisting of the empty word.

We will denote the class of language algebras of similarity type $\Lambda$ by ${\sf L}(\Lambda)$.

Definition 1.2**.**

[Relation algebras] Let $\mathfrak{A}=(A,\Lambda)$ be an algebra of similarity type $\Lambda\subseteq(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. We say that $\mathfrak{A}$ is a relation algebra if the following holds. There is a set $U$, the base of $\mathfrak{A}$, such that $A$ is a family of binary relations on $U$, i.e., $A\subseteq\wp(U\times U)$, and the operations in $\Lambda$ are interpreted as follows: join $\mathbin{+}$ is union, meet $\cdot$ is intersection, composition $\mathbin{;}$ is relation composition

[TABLE]

and [math] is the empty relation $\emptyset$.

We will denote the class of relation algebras of similarity type $\Lambda$ by ${\sf R}(\Lambda)$.

In passing we note that the representation classes ${\sf L}(\Lambda)$ and ${\sf R}(\Lambda)$ are not finitely axiomatizable whenever $(\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})\subseteq\Lambda$. Indeed, the class of language algebras is not closed under products (see below), while the quasivariety ${\sf R}(\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})$ has no finite base [HM07]. This is one of the main reasons why we concentrate on the generated varieties below.

Assume that $0,{1^{\prime}}\in\Lambda$ and let $\mathfrak{A}$ be a $\Lambda$-algebra. We say that $\mathfrak{A}$ is integral if ${1^{\prime}}$ is an atom of $\mathfrak{A}$, i.e., ${1^{\prime}}$ is a minimal non-zero element. For a class ${\sf K}(\Lambda)$ of $\Lambda$-algebras, let ${\sf K}^{i}(\Lambda)$ denote the subclass of integral $\Lambda$-algebras. Observe that every language algebra is integral, ${\sf L}(\Lambda)={\sf L}^{i}(\Lambda)$, while there are non-integral relation algebras, ${\sf R}(\Lambda)\supset{\sf R}^{i}(\Lambda)$.

For a class ${\sf K}(\Lambda)$ of $\Lambda$-algebras, let ${\sf V}({\sf K}(\Lambda))$ denote the variety generated by ${\sf K}(\Lambda)$. Note that the variety ${\sf V}({\sf K}^{i}(\Lambda))$ generated by integral algebras may contain non-integral algebras, since neither products nor homomorphisms preserve the property that ${1^{\prime}}$ is an atom.

2. Main results

First we look at $\Lambda=(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. As usual $x\leq y$ is defined by $x\mathbin{\cdot\,}y=x$ and we assume that $\mathbin{;}$ binds closer than $\mathbin{\cdot\,}$, e.g., we write $x\mathbin{\cdot\,}y\mathbin{;}z$ for $x\mathbin{\cdot\,}(y\mathbin{;}z)$.

We define $\mbox{\rm Ax}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ as the collection of the following axioms.

• Semilattice axioms (for $\mathbin{\cdot\,}$)
• Monoid axioms (for $\mathbin{;}$ and ${1^{\prime}}$)
• Monotonicity:

[TABLE]

• Axioms for [math]:

[TABLE]

• Subidentity axioms:

[TABLE]

It is easily checked that all these axioms are valid in both relation and language algebras.

We will need additional axioms that are valid in language algebras and in integral relation algebras. We define $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ as $\mbox{\rm Ax}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ augmented with the integral axioms (7) and (8) below.

• “Integrality”:

[TABLE]

Note that ${1^{\prime}}\mathbin{\cdot\,}x\mathbin{;}y=0$ iff ${1^{\prime}}\mathbin{\cdot\,}y\mathbin{;}x=0$ in a relation algebra $\mathfrak{A}$. Hence, if $\mathfrak{A}$ is integral, then it follows that the two terms in (7) are either [math] or ${1^{\prime}}$ at the same time. Checking validity of the other integral axiom in integral algebras is similar. The set $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is not independent, e.g., we can derive (6) from (5) with the use of (8).

2.1. Axiomatizations for integral relation algebras

Theorem 2.1**.**

The variety ${\sf V}({\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ generated by ${\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is axiomatized by $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$.

Proof.

By the validity of the axioms in integral relation algebras we get that equations derivable using equational logic from $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ are valid in ${\sf V}({\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$. We will prove the other direction by showing that, for every non-derivable equation, there is an algebra in ${\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ witnessing that the equation is not valid, see Lemma 3.5. ∎

Next we include union into the signature. Define $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ as $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ augmented with the distributive lattice axioms (for $\mathbin{\cdot\,}$ and $\mathbin{+}$) and that the operation $\mathbin{;}$ is additive:

[TABLE]

for every $x,y,z$.

Theorem 2.2**.**

The variety ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ generated by ${\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is axiomatized by $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$.

Proof.

This follows from [Br93, Corollary 2] (see also [AM11, Proposition 4.4]), we just give a sketch here.

By the validity of the axioms we get that derivable equations are valid. For the other direction assume that ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))\models a=b$. Thus we have both ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))\models a\leq b$ and ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))\models b\leq a$, where $x\leq y$ is defined by $x\mathbin{\cdot\,}y=x$. Note that, using the additivity of the operations in relation algebras, we can rewrite every term as a join of join-free terms. Thus $a\leq b$ can be equivalently rewritten as $a_{1}\mathbin{+}\dots\mathbin{+}a_{n}\leq b_{1}\mathbin{+}\dots\mathbin{+}b_{m}$ where $a_{i}$ and $b_{j}$ do not contain $\mathbin{+}$. Furthermore, using the term graphs of [AB95] one can show that $a_{1}\mathbin{+}\dots\mathbin{+}a_{n}\leq b_{1}\mathbin{+}\dots\mathbin{+}b_{m}$ is valid in ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ iff, for every $i$, there is $j$ such that $a_{i}\leq b_{j}$ is valid in ${\sf V}({\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$. Thus ${\sf V}({\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))\models a_{i}\leq b_{j}$ (since $a_{i}$ and $b_{j}$ do not contain $\mathbin{+}$). By Theorem 2.1 we get $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash a_{i}\leq b_{j}$, whence $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash a_{i}\leq b_{j}$. Since the distributive lattice axioms ensure that the ordering $x\leq y$ can be equivalently defined by either $x\mathbin{\cdot\,}y=x$ or $x\mathbin{+}y=y$, we get $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash a_{i}\leq b_{1}\mathbin{+}\dots\mathbin{+}b_{m}$. Since this holds for every $i$, using the additivity axioms we get $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash a\leq b$. By an identical argument we get $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash b\leq a$ as well, whence $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash a=b$, as desired. ∎

2.2. Axiomatization for language algebras

Theorem 2.3**.**

The variety ${\sf V}({\sf L}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ generated by ${\sf L}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is axiomatized by

[TABLE]

together with $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$.

Proof.

In [AMN11] it is shown that the equational theory of ${\sf L}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is finitely axiomatizable over the equational theory of ${\sf R}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ by the equations (11) and (8). By a minimal and straightforward modification of the proof of [AMN11, Corollary 3.7] we get that the equational theory of ${\sf L}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ is finitely axiomatizable by (11) over the equational theory of ${\sf R}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$, which is axiomatized by $\mbox{\rm Ax}^{i}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. ∎

3. Relational representation of the free algebra

In this section we make the proof of Theorem 2.1 complete. We will need the following easy consequences of $\mbox{\rm Ax}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$:

[TABLE]

[TABLE]

where $e,e_{1},\ldots,e_{4}$ are subidentity terms (have the form $z\mathbin{\cdot\,}{1^{\prime}}$).

3.1. Step-by-step construction

Fix a countable set $X$ of variables. Let $T_{X}$ be the set of $(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$-terms using the variables from $X$ and ${\mathfrak{F}}_{X}=(F_{X},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ be the free algebra of the variety defined by $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ which is freely generated by $X$. That is, $\mathfrak{F}_{X}$ is given by factoring the absolutely free algebra by the congruence of derivability from $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ in equational logic. Thus ${\mathfrak{F}}_{X}\models\tau\leq\sigma$ (under the natural valuation of evaluating every variable to itself) iff $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\vdash\tau\leq\sigma$, where $\vdash$ denotes derivability in equational logic.

By a filter ${\mathcal{F}}$ of ${\mathfrak{F}}_{X}$ we mean a subset closed upward and under meet $\mathbin{\cdot\,}$, that is, $\tau,\sigma\in{\mathcal{F}}$ iff $\tau\mathbin{\cdot\,}\sigma\in{\mathcal{F}}$. For a $S\subseteq F_{X}$, let $\mathcal{F}(S)$ denote the filter generated by $S$. In particular, for a term $\tau$, $\mathcal{F}(\{\tau\})$ denotes the principal filter generated by $\{\tau\}$, i.e., the upward closure $\{\tau\}^{\uparrow}$ of the singleton set $\{\tau\}$. We extend the operation $\mathbin{;}$ to subsets of elements as follows:

[TABLE]

for subsets $X,Y$. When $X=\{x\}$ is a singleton, we will also use the notation $x\mathbin{;}Y=\{x\mathbin{;}y:y\in Y\}$, $\{x\}^{\uparrow}=x^{\uparrow}$, $\mathcal{F}(\{\tau\})=\mathcal{F}(\tau)$, etc.

For the whole rest of the section we fix a term $\theta$ such that $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\not\vdash\theta=0$.

Next we define special filters that are generated by some set of subidentity elements. We define

[TABLE]

for each element $\tau$. It is worth noting that

[TABLE]

since $\epsilon\mathbin{;}\tau=\epsilon\mathbin{;}(\tau\mathbin{\cdot\,}\sigma)=\tau\mathbin{\cdot\,}\epsilon\mathbin{;}\sigma\geq\tau\mathbin{\cdot\,}\sigma=\tau$ by (13) whenever $\epsilon\in\mathcal{E}(\sigma)$. We denote $\mathcal{E}:=\mathcal{E}(\theta)$ for our fixed term $\theta$. We say that the filter $\mathcal{F}$ is fundamental if the following holds: there is an element $\tau$ such that $\mathcal{F}=\mathcal{F}(\mathcal{E}\mathbin{;}\tau\mathbin{;}\mathcal{E})$. Observe that $\mathcal{E}=\mathcal{F}(\mathcal{E}\mathbin{;}{1^{\prime}}\mathbin{;}\mathcal{E})$ is fundamental, since for subidentity elements $\epsilon_{1},\epsilon_{2}$, we have $\epsilon_{1}\mathbin{;}{1^{\prime}}\mathbin{;}\epsilon_{2}=\epsilon_{1}\mathbin{;}\epsilon_{2}=\epsilon_{1}\mathbin{\cdot\,}\epsilon_{2}$ by (4). Also note that $\mathcal{F}(\mathcal{E}\mathbin{;}\tau\mathbin{;}\mathcal{E})=(\mathcal{E}\mathbin{;}\tau\mathbin{;}\mathcal{E})^{\uparrow}$, since $(\epsilon_{1}\mathbin{;}\tau\mathbin{;}\epsilon_{2})\mathbin{\cdot\,}(\epsilon_{3}\mathbin{;}\tau\mathbin{;}\epsilon_{4})=(\epsilon_{1}\mathbin{\cdot\,}\epsilon_{3})\mathbin{;}\tau\mathbin{;}(\epsilon_{2}\mathbin{\cdot\,}\epsilon_{4})$ by (12).

We will define a chain of labelled, directed graphs $G_{n}=(U_{n},\ell_{n},E_{n},W_{n})$ for $n\in\omega$, where

• •

$U_{n}$ is the set of nodes,

• •

$\ell_{n}\colon U_{n}\times U_{n}\to\wp(F_{X})$ is a labelling of edges,

• •

$E_{n}:=\{(u,v)\in U_{n}\times U_{n}:\ell_{n}(u,v)\neq\emptyset\}$ is the set of edges with non-empty labels,

• •

$W_{n}\subseteq E_{n}$ is a distinguished set of witness edges.

We will make sure that the following inductive conditions are maintained during the construction:

**RT: **

$E_{n}$ is reflexive and transitive.

**Gen: **

$W_{n}$ generates $E_{n}$ by closing under transitivity.

**Fun: **

for every $(u,v)\in E_{n}$, $\ell_{n}(u,v)$ is a proper, fundamental filter: there is $\tau$ such that $\ell_{n}(u,v)=\mathcal{F}(\mathcal{E}\mathbin{;}\tau\mathbin{;}\mathcal{E})$.

**DR: **

for every $(u,v)\in E_{n}$, $\mathcal{E}(\sigma)\subseteq\ell_{n}(u,u)=\ell_{n}(v,v)=\mathcal{E}$ for every $\sigma\in\ell_{n}(u,v)$.

**Comp: **

for every $(u,v),(u,w),(w,v)\in E_{n}$, we have $\ell_{n}(u,w)\mathbin{;}\ell_{n}(w,v)\subseteq\ell_{n}(u,v)$.

**Ide: **

for every $(u,v)\in E_{n}$, if ${1^{\prime}}\in\ell_{n}(u,v)$, then $u=v$.

Observe that DR implies ${1^{\prime}}\in\ell_{n}(u,u)=\ell_{n}(v,v)$ for every $u$ and $v$.

These conditions, with the exception of Ide, will be easily seen to be maintained during the construction. We will check that Ide holds for witness edges $(u,v)\in W_{n}$ as well, but we will establish the general case for Ide only at the end of the section.

The construction will terminate in $\omega$ steps, yielding $G_{\omega}=(U_{\omega},\ell_{\omega},E_{\omega},W_{\omega})$ where $U_{\omega}=\bigcup_{n}U_{n}$, $\ell_{\omega}=\bigcup_{n}\ell_{n}$, $E_{\omega}=\bigcup_{n}E_{n}$ and $W_{\omega}=\bigcup_{n}W_{n}$.

By the end of the construction we will achieve the following saturation condition:

**Sat: **

for every $(u,v)\in E_{\omega}$ and $\tau\mathbin{;}\sigma\in\ell_{\omega}(u,v)$, we have $\tau\in\ell_{\omega}(u,w)$ and $\sigma\in\ell_{\omega}(w,v)$ for some $w\in U_{\omega}$.

In the 0th step of the step-by-step construction we define $G_{0}$ by creating a witness edge for our fixed term $\theta$. We choose $u_{0},v_{0}\in\omega$ such that $u_{0}=v_{0}$ iff $\theta\leq{1^{\prime}}$ is derivable. We define

[TABLE]

and we label $(v_{0},u_{0})$ by $\emptyset$ in case $u_{0}\neq v_{0}$. Observe that $\ell_{0}$ is well defined. Indeed, in case $\theta\leq{1^{\prime}}$, we have that $\mathcal{E}=\theta^{\uparrow}=\mathcal{F}(\theta)$. All non-empty edges constructed so far will be witness edges: $W_{0}=E_{0}$.

It is easy to see that the inductive conditions are true. For Comp we note that, for every $\epsilon,\epsilon^{\prime}\in\ell_{0}(u_{0},u_{0})=\ell_{0}(v_{0},v_{0})=\mathcal{E}$, we have $\epsilon\mathbin{;}\epsilon^{\prime}=\epsilon\mathbin{\cdot\,}\epsilon^{\prime}\in\mathcal{E}$ by (4), and $\epsilon\mathbin{;}\theta\mathbin{;}\epsilon^{\prime}=\theta\in\ell_{0}(u_{0},v_{0})$ by the definition of $\mathcal{E}$. DR easily follows from (14). Note that $\theta^{\prime}\notin\ell_{0}(u_{0},v_{0})$ whenever $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\not\vdash\theta\leq\theta^{\prime}$, since $\theta^{\prime}\notin\mathcal{F}(\theta)=\theta^{\uparrow}$.

In the $(n+1)$th step we assume inductively that $G_{n}=(U_{n},\ell_{n},E_{n},W_{n})$ with $U_{n}\subset\omega$ and $W_{n}\subseteq E_{n}\subseteq U_{n}\times U_{n}$ has been constructed and that $G_{n}$ satisfies the inductive conditions. We also assume that there is a fair scheduling function $\Sigma\colon\omega\to\omega\times\omega\times F_{X}$, i.e., every element of $\omega\times\omega\times F_{X}$ appears infinitely often in the range of $\Sigma$.

Assume that $\Sigma(n+1)=(u,v,\tau\mathbin{;}\sigma)$, $(u,v)\in E_{n}$ and $\tau\mathbin{;}\sigma\in\ell_{n}(u,v)$, otherwise we define $G_{n+1}=G_{n}$. Recall that $\ell_{n}(u,u)=\ell_{n}(v,v)=\mathcal{E}$ by DR. Let $\rho$ be such that $\ell_{n}(u,v)=\mathcal{F}(\mathcal{E}\mathbin{;}\rho\mathbin{;}\mathcal{E})$, and $\rho^{\prime}$ be such that $\ell_{n}(v,u)=\mathcal{F}(\mathcal{E}\mathbin{;}\rho^{\prime}\mathbin{;}\mathcal{E})$ in case $(v,u)\in E_{n}$ as well. Thus $\epsilon_{0}\mathbin{;}\rho\mathbin{;}\epsilon_{0}\leq\tau\mathbin{;}\sigma$ for some subidentity $\epsilon_{0}\in\mathcal{E}$. Observe that, for any subidentity $\epsilon$,

[TABLE]

by using $\epsilon_{0}\mathbin{\cdot\,}\epsilon=(\epsilon_{0}\mathbin{\cdot\,}\epsilon)\mathbin{;}(\epsilon_{0}\mathbin{\cdot\,}\epsilon)$, (8) and (13).

We will assume that ${1^{\prime}}\notin\mathcal{F}(\mathcal{E}\mathbin{;}\tau\mathbin{;}\mathcal{E})$ and ${1^{\prime}}\notin\mathcal{F}(\mathcal{E}\mathbin{;}\sigma\mathbin{;}\mathcal{E})$, since we would have the required edges otherwise. Indeed, we have

[TABLE]

because of the following. Assume that $\epsilon^{\prime}\mathbin{;}\tau\mathbin{;}\epsilon^{\prime}\leq{1^{\prime}}$ for some subidentity $\epsilon^{\prime}\in\mathcal{E}$. Let $\epsilon=\epsilon_{0}\mathbin{\cdot\,}\epsilon^{\prime}$. Then $\epsilon\mathbin{;}\rho\mathbin{;}\epsilon\in\ell_{\omega}(u,v)$ and

[TABLE]

whence $\sigma\in\ell_{n}(u,v)$. Next we claim that $\epsilon\mathbin{;}\tau\mathbin{;}\epsilon\in\ell_{n}(u,u)$. Indeed, by using (15), (13) we get

[TABLE]

whence $\tau\geq\epsilon\mathbin{;}\tau\mathbin{;}\epsilon\in\ell_{n}(u,u)$ by DR. The case ${1^{\prime}}\in\mathcal{F}(\mathcal{E}\mathbin{;}\sigma\mathbin{;}\mathcal{E})$ is treated similarly.

Take a point $w\in\omega\smallsetminus U_{n}$ and define

[TABLE]

whenever $(t,u),(v,s)\in E_{n}$. In particular,

[TABLE]

since $\ell_{n}(u,u)=\ell_{n}(v,v)=\mathcal{E}$. By Fun and DR there are $\xi$ and $\chi$ such that $\ell_{n}(t,u)=\mathcal{F}(\mathcal{E}\mathbin{;}\xi\mathbin{;}\mathcal{E})$ and $\ell_{n}(v,s)=\mathcal{F}(\mathcal{E}\mathbin{;}\chi\mathbin{;}\mathcal{E})$. Then using (8)

[TABLE]

when $(v,u)\in E_{n}$. Thus the labels are fundamental filters. For all other edges, we let $\ell_{n+1}(x,y)=\ell_{n}(x,y)$ if $(x,y)\in E_{n}$, and $\ell_{n+1}(x,y)=\emptyset$ otherwise. The witness edges are those of $G_{n}$ (i.e., $W_{n}$) and $(u,w)$, $(w,v)$ and $(w,w)$. See Figure 1, where we show typical elements of the labels.

Observe that $E_{n+1}$ is reflexive, transitive and generated by $W_{n+1}$ (e.g., in case $(v,u)\in E_{n}$, the edge $(w,u)$ can be “decomposed” to $(w,v)\in W_{n+1}$ and $(v,u)$ which is generated by $W_{n}$ by the inductive condition). Ide holds for witness edges, since the new irreflexive witness edges $(u,w)$ and $(w,v)$ avoid ${1^{\prime}}$ by the assumption on $\tau$ and $\sigma$.

Next we check that Comp is maintained as well. Both $\ell_{n+1}(w,w)\mathbin{;}\ell_{n+1}(w,s)\subseteq\ell_{n+1}(w,s)$ and $\ell_{n+1}(t,w)\mathbin{;}\ell_{n+1}(w,w)\subseteq\ell_{n+1}(t,w)$ easily follow from the definition of the labels. Similarly we get $\ell_{n+1}(w,s)\mathbin{;}\ell_{n+1}(s,s)\subseteq\ell_{n+1}(w,s)$ and $\ell_{n+1}(t,t)\mathbin{;}\ell_{n+1}(t,w)\subseteq\ell_{n+1}(t,w)$ using that $G_{n}$ satisfies DR and Comp. If $(w,t),(t,w)\in E_{n+1}$, we need $\ell_{n+1}(w,t)\mathbin{;}\ell_{n+1}(t,w)\subseteq\ell_{n+1}(w,w)$ as well. Let $\chi\in\ell_{n+1}(v,t)$ and $\xi\in\ell_{n+1}(t,u)$ so that $\epsilon\mathbin{;}\sigma\mathbin{;}\chi\mathbin{;}\epsilon\in\ell_{n+1}(w,t)$ and $\epsilon\mathbin{;}\xi\mathbin{;}\tau\mathbin{;}\epsilon\in\ell_{n+1}(t,w)$ for some subidentity $\epsilon\in\mathcal{E}$. Then

[TABLE]

by (7) and Comp for $G_{n}$. Thus $\epsilon\mathbin{;}\sigma\mathbin{;}\chi\mathbin{;}\epsilon\mathbin{;}\xi\mathbin{;}\tau\mathbin{;}\epsilon\in\mathcal{E}=\ell_{n+1}(w,w)$ as desired. The proof of $\ell_{n+1}(t,w)\mathbin{;}\ell_{n+1}(w,t)\subseteq\ell_{n+1}(t,t)$ is similar. Next we show $\ell_{n+1}(t,w)\mathbin{;}\ell_{n+1}(w,s)\subseteq\ell_{n+1}(t,s)$. Indeed, we have

[TABLE]

by Comp for $G_{n}$. For $\ell_{n+1}(s,t)\mathbin{;}\ell_{n+1}(t,w)\subseteq\ell_{n+1}(s,w)$ we have

[TABLE]

by Comp for $G_{n}$, and similarly for $\ell_{n+1}(w,s)\mathbin{;}\ell_{n+1}(s,t)\subseteq\ell_{n+1}(w,t)$.

Finally we check DR. First let $\xi\in\ell_{n+1}(t,u)$ and $\epsilon\in\mathcal{E}$ so that $\xi\mathbin{;}\tau\mathbin{;}\epsilon\in\mathcal{F}(\ell_{n+1}(t,u)\mathbin{;}\tau\mathbin{;}\mathcal{E})=\ell_{n+1}(t,w)$, and assume that $\epsilon^{\prime}\leq{1^{\prime}}$ such that $\xi\mathbin{;}\tau\mathbin{;}\epsilon\mathbin{;}\epsilon^{\prime}=\xi\mathbin{;}\tau\mathbin{;}\epsilon$. We show that $\epsilon^{\prime}\in\mathcal{E}=\ell_{n+1}(w,w)$. We have $\xi\mathbin{;}\tau\mathbin{;}\sigma\mathbin{;}\epsilon\mathbin{;}\epsilon^{\prime}=\xi\mathbin{;}\tau\mathbin{;}\epsilon\mathbin{;}\epsilon^{\prime}\mathbin{;}\sigma=\xi\mathbin{;}\tau\mathbin{;}\epsilon\mathbin{;}\sigma=\xi\mathbin{;}\tau\mathbin{;}\sigma\mathbin{;}\epsilon\in\ell_{n}(t,v)$, whence $\epsilon^{\prime}\in\ell_{n}(v,v)=\mathcal{E}=\ell_{n+1}(w,w)$ by DR for $G_{n}$. That is, $\mathcal{E}(\xi\mathbin{;}\tau\mathbin{;}\epsilon)\subseteq\ell_{n+1}(w,w)$. A similar proof shows DR for $\ell_{n+1}(w,s)$.

This finishes the successor step yielding $G_{n+1}=(U_{n+1},\ell_{n+1},E_{n+1},W_{n+1})$. After the construction terminates we end up with a labelled structure $G_{\omega}=(U_{\omega},\ell_{\omega},E_{\omega},W_{\omega})$ such that $U_{\omega}=\bigcup_{n}U_{n}$, $\ell_{\omega}=\bigcup_{n}\ell_{n}$, $E_{\omega}=\bigcup_{n}E_{n}$ and $W_{\omega}=\bigcup_{n}W_{n}\subseteq E_{\omega}$. Observe that $G_{\omega}$ satisfies Sat, since the fair scheduling function $\Sigma$ ensures that every possible composition “defect” has been taken care of. But we have not showed yet that Ide is satisfied in general, we will do this shortly. $G_{\omega}$ satisfies the other inductive conditions (since so does every $G_{n}$).

3.2. Graphs and algebras

We define a valuation $\iota$ of variables on $U_{\omega}\times U_{\omega}$:

[TABLE]

for every variable $x\in X$. Let $\mathfrak{A}_{\theta}$ be the subalgebra of $(\wp(U_{\omega}\times U_{\omega}),\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ generated by $\{\iota(x):x\in X\}$. Next we show that $\mathfrak{A}_{\theta}\in{\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$.

Let $\mathfrak{A}_{\theta}(u,v)$ denote the set of those elements (a filter) that hold at $(u,v)$.

Lemma 3.1**.**

For every $u\in U_{\omega}$ and term $\tau$,

[TABLE]

Proof.

We will prove the lemma together with

[TABLE]

for every $(u,v)\in U_{\omega}\times U_{\omega}$. We will use simultaneous induction on the complexity of terms.

The base case, when $\tau$ is a variable, the identity constant ${1^{\prime}}$, or [math] is straightforward by the definition of the valuation $\iota$ and the fact that the labels are proper filters.

Next assume that $\tau=\sigma\mathbin{\cdot\,}\rho$. Recall that $\ell_{\omega}(u,v)$ is a filter, whence $\tau\in\ell_{\omega}(u,v)$ implies $\sigma,\rho\in\ell_{\omega}(u,v)$. First consider the statement (19). If $\tau\not\leq{1^{\prime}}$, then also $\sigma,\rho\not\leq{1^{\prime}}$, whence we can apply the induction hypothesis (IH) for (19), yielding $\sigma,\rho\in\mathfrak{A}_{\theta}(u,v)$ and $\sigma\mathbin{\cdot\,}\rho\in\mathfrak{A}_{\theta}(u,v)$, since $\mathfrak{A}_{\theta}(u,v)$ is a filter. The proof for (18) is analogous.

Finally assume that $\tau=\sigma\mathbin{;}\rho$. We start with showing (19). First assume that $\sigma\leq{1^{\prime}}$, whence $\rho\not\leq{1^{\prime}}$ (by $\tau\not\leq{1^{\prime}}$). Then using (16) we get that $\sigma\in\ell_{\omega}(u,u)$ and $\rho\in\ell_{\omega}(u,v)$. By the IH for (18) and (19) we have $\sigma\in\mathfrak{A}_{\theta}(u,u)$ and $\rho\in\mathfrak{A}_{\theta}(u,v)$. Thus $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(u,v)$. The case $\rho\leq{1^{\prime}}$ is treated similarly. The last case is when $\sigma,\rho\not\leq{1^{\prime}}$. By Sat we have $w$ such that $\sigma\in\ell_{\omega}(u,w)$ and $\rho\in\ell_{\omega}(w,v)$. Using the IH for (19) we get $\sigma\in\mathfrak{A}_{\theta}(u,w)$ and $\rho\in\mathfrak{A}_{\theta}(w,v)$, whence $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(u,v)$.

For (18) we argue as follows. First assume that $\sigma\leq{1^{\prime}}$. Using (16) we get that $\sigma,\rho\in\ell_{\omega}(u,u)$. By the IH for (18) we get $\sigma,\rho\in\mathfrak{A}_{\theta}(u,u)$, whence $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(u,u)$. The case for $\rho\leq{1^{\prime}}$ is similar. Finally, the case $\sigma,\rho\not\leq{1^{\prime}}$ is treated precisely like for (19) at the end of the previous paragraph. ∎

Lemma 3.2**.**

For every term $\tau$ and for every edge $(u,v)\in U_{\omega}\times U_{\omega}$,

[TABLE]

Proof.

This is an easy induction on the complexity of terms (using Comp for composition). ∎

Lemma 3.3**.**

$\mathfrak{A}_{\theta}\in{\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$.

Proof.

Clearly, $\mathfrak{A}_{\theta}$ is an algebra of relations. Recall that we have $\ell_{\omega}(u,u)=\mathcal{E}(\theta)=\mathcal{E}$ for every $u\in U_{\omega}$. Then by Lemma 3.1 and Lemma 3.2 we get

[TABLE]

Recall that $\mathfrak{A}_{\theta}$ is generated by $\{\iota(x):x\in X\}$, thus every element of $\mathfrak{A}_{\theta}$ is the interpretation of a term. Now assume indirectly that the interpretation of the identity constant ${1^{\prime}}$ in $\mathfrak{A}_{\theta}$ is not an atom, i.e., there is a term $\tau$ such that its interpretation is a proper, nonempty subset $T$ of $\{(u,u):u\in U_{\omega}\}$. Then $\tau\in\mathfrak{A}_{\theta}(u,u)$ iff $(u,u)\in T$, contradicting to (20). Thus $\mathfrak{A}_{\theta}$ is an integral algebra. ∎

Next we show that $\mathfrak{A}_{\theta}$ is a witness for the non-derivable equations of the form $\theta\leq\theta^{\prime}$ for our fixed $\theta$.

Lemma 3.4**.**

For every term $\tau$ and for every edge $(x,y)\in U_{\omega}\times U_{\omega}$,

[TABLE]

Proof.

We already showed the lemma for the case $x=y$ and for the general case with the restriction that $\tau\not\leq{1^{\prime}}$, see the proof of Lemma 3.1 above. Then it would suffice to show that ${1^{\prime}}$ cannot occur in the label of the edge $(x,y)$ whenever $x\neq y$. Indeed, our proof will show this (see (22) below), but we will go through all the cases for the sake of clarity.

We use induction over the “distance” between $x$ and $y$. To this end we define ${\rm path}(x,y)$ for $(x,y)\in E_{\omega}$ by recursion. For $(x,y)\in E_{0}$, we let ${\rm path}(x,y)=(x,y)$. Now assume that $(x,y)\in E_{n+1}\smallsetminus E_{n}$ and we already defined ${\rm path}$ for the elements of $E_{n}$. Assume that $U_{n+1}=U_{n}\cup\{w\}$ and that we expanded $U_{n}$ by $w$ because of some $\sigma\mathbin{;}\rho\in\ell_{n}(u,v)$. Again we let ${\rm path}(x,y)=(x,y)$ for $x,y\in\{u,w,v\}$. Now assume that $t\neq u$, $(t,u)\in E_{n}$ and ${\rm path}(t,u)=(t,z_{0},\dots,z_{k},u)$. Then we let

[TABLE]

and define ${\rm path}(w,s)$ for $(v,s)\in E_{n}$ analogously. Finally, $d(x,y)$ is defined as the length of ${\rm path}(x,y)$.

The base case is when $(x,y)\in W_{\omega}$ is a witness edge: $d(x,y)=1$. The base case will be established by induction on terms. The case of a variable is straightforward by the definition (17) of the valuation $\iota$. The case of [math] follows from the fact that we used proper filters as labels. Next assume that $\tau$ is the constant ${1^{\prime}}$. Observe that ${1^{\prime}}\in\ell_{\omega}(x,y)$ implies $x=y$, since irreflexive witness edges avoid ${1^{\prime}}$. Then ${1^{\prime}}\in\mathfrak{A}_{\theta}(x,x)$, since $\mathfrak{A}_{\theta}$ is representable. The case for $\mathbin{\cdot\,}$ follows from the fact that we used filters as labels. For the case of $\mathbin{;}$ assume that $\tau$ is $\sigma\mathbin{;}\rho$ and that $\sigma\mathbin{;}\rho\in\ell_{\omega}(x,y)$. Recall that we had either $\sigma\in\ell_{\omega}(x,x)$ and $\rho\in\ell_{\omega}(x,y)$, or $\sigma\in\ell_{\omega}(x,y)$ and $\rho\in\ell_{\omega}(y,y)$, or we constructed witness edges $(x,z)$ and $(z,y)$ such that $\sigma\in\ell_{\omega}(x,z)$ and $\rho\in\ell_{\omega}(z,y)$. Thus $\sigma\in\mathfrak{A}_{\theta}(x,z)$ and $\rho\in\mathfrak{A}_{\theta}(z,y)$ by the IH, whence $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(x,y)$ as desired.

For the inductive case assume that $d(x,y)=k+1>1$. Again we use induction on terms. The cases for variables and [math] are as in the base step $(x,y)\in W_{\omega}$. For the case of ${1^{\prime}}$ we show that $G_{\omega}$ in fact satisfies Ide:

[TABLE]

Assume that $(x,y)$ was created in the $(n+1)$th step of the construction. Recall that during the construction we defined $\ell_{n+1}(x,y)$ as $\mathcal{F}(\ell_{n+1}(x,z)\mathbin{;}\ell_{n+1}(z,y))$ for some $z$ such that either $(x,z)\in E_{n}$ and $(z,y)\in W_{n+1}$, or $(x,z)\in W_{n+1}$ and $(z,y)\in E_{n}$. Wlog assume the former. Then, using the notation in Figure 1, we have $x=t$, $y=w$ and $z=u$. Recall that ${\rm path}(t,w)$ is defined by adding the step $(u,w)$ at the end of ${\rm path}(t,u)$, see (21). Hence $d(x,z)=d(t,u)<d(t,w)=d(x,y)$.

Let $\ell_{n+1}(x,z)=\mathcal{F}(\mathcal{E}\mathbin{;}\rho_{1}\mathbin{;}\mathcal{E})$ and $\ell_{n+1}(z,y)=\mathcal{F}(\mathcal{E}\mathbin{;}\rho_{2}\mathbin{;}\mathcal{E})$, whence $\ell_{n+1}(x,y)=\mathcal{F}(\mathcal{E}\mathbin{;}\rho_{1}\mathbin{;}\rho_{2}\mathbin{;}\mathcal{E})$ by the construction. Since $d(x,z)<d(x,y)$ and $(z,y)\in W_{n+1}$, we can apply the induction hypothesis: $\epsilon\mathbin{;}\rho_{1}\mathbin{;}\epsilon\in\mathfrak{A}_{\theta}(x,z)$ and $\epsilon\mathbin{;}\rho_{2}\mathbin{;}\epsilon\in\mathfrak{A}_{\theta}(z,y)$ for every $\epsilon\in\mathcal{E}$. Thus we get $\epsilon\mathbin{;}\rho_{1}\mathbin{;}\rho_{2}\mathbin{;}\epsilon\in\mathfrak{A}_{\theta}(x,y)\not\ni{1^{\prime}}$. Assume, for a contradiction, that ${1^{\prime}}\in\ell_{n+1}(x,y)$. Then $\epsilon\mathbin{;}\rho_{1}\mathbin{;}\rho_{2}\mathbin{;}\epsilon\leq{1^{\prime}}$ is derivable from $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ for some $\epsilon\in\mathcal{E}$. But $\epsilon\mathbin{;}\rho_{1}\mathbin{;}\rho_{2}\mathbin{;}\epsilon\leq{1^{\prime}}$ is not valid in ${\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$ as witnessed by $\mathfrak{A}_{\theta}$, a contradiction. Hence (22) holds. Thus we have that ${1^{\prime}}\in\ell_{\omega}(x,y)$ only if $x=y$, and then ${1^{\prime}}\in\mathfrak{A}_{\theta}(x,y)$ as required.

The case of $\mathbin{\cdot\,}$ follows as above. Finally assume that $\tau=\sigma\mathbin{;}\rho$ and $\sigma\mathbin{;}\rho\in\ell_{n}(x,y)$. We have to consider three cases. The first is when $\sigma\in\ell_{n}(x,x)$ and $\rho\in\ell_{n}(x,y)$. Then $\sigma\in\mathfrak{A}_{\theta}(x,x)$ (since $(x,x)\in W_{\omega}$) and $\rho\in\mathfrak{A}_{\theta}(x,y)$ (since $\rho$ is a simpler term than $\sigma\mathbin{;}\rho$). Thus $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(x,y)$. The case $\sigma\in\ell_{n}(x,y)$ and $\rho\in\ell_{n}(y,y)$ is similar. Finally, if neither of the above cases apply, then we created witness edges $(x,z)$ and $(z,y)$ such that $\sigma\in\ell_{\omega}(x,z)$ and $\rho\in\ell_{\omega}(z,y)$. By the base case we get $\sigma\in\mathfrak{A}_{\theta}(x,z)$ and $\rho\in\mathfrak{A}_{\theta}(z,y)$, whence $\sigma\mathbin{;}\rho\in\mathfrak{A}_{\theta}(x,y)$ as desired. ∎

Lemma 3.5**.**

For every $\theta^{\prime}$ such that $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\not\vdash\theta\leq\theta^{\prime}$, we have ${\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})\not\models\theta\leq\theta^{\prime}$.

Proof.

By Lemma 3.3 we have $\mathfrak{A}_{\theta}\in{\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. By the initial step of the step-by-step construction we have $\theta\in\ell_{\omega}(u_{0},v_{0})=\mathcal{F}(\theta)$ and $\theta^{\prime}\notin\ell_{\omega}(u_{0},v_{0})$. So by Lemma 3.4 we get $\theta\in\mathfrak{A}_{\theta}(u_{0},v_{0})$ and by Lemma 3.2 we have $\theta^{\prime}\notin\mathfrak{A}_{\theta}(u_{0},v_{0})$. ∎

Remark 3.6**.**

[Representing the free algebra] In the above construction we fixed a term $\theta$ and constructed an algebra $\mathfrak{A}_{\theta}\in{\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. We can repeat the same construction for every non-zero element $\theta$ of the free algebra $\mathfrak{F}_{X}$, resulting in $\mathfrak{A}_{\theta}\in{\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. It is not difficult to show that $\mathfrak{F}_{X}$ can be embedded into $\prod_{\theta\neq 0}\mathfrak{A}_{\theta}\in{\sf V}({\sf R}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$.

4. Conclusions

The varieties ${\sf V}({\sf R}(\Lambda))$ generated by algebras of binary relations of the similarity types $\Lambda=(\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})$ and $\Lambda=(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})$ were stated to be finitely axiomatizable in [AM11] (Theorem 4.3 and Theorem 4.1(1), respectively), but their proofs relied on false lemmas. See [AM14].

In more detail, the third case of Definition 4.6 is ambiguous, and Lemmas 4.7 and 4.8 are not true. These lemmas are used in the proof of Theorem 4.3. As a consequence, the proof of Theorem 4.3 breaks down for the equation ${1^{\prime}}\mathbin{\cdot\,}x\mathbin{;}y\leq x\mathbin{;}({1^{\prime}}\mathbin{\cdot\,}y\mathbin{;}x)\mathbin{;}y$. This equation is easily seen to be valid, but so far we did not manage to derive it from the axioms of Theorem 4.3. In fact, we conjecture that this equation does not follow from the axioms presented in [AM11]. Theorem 4.3 is used in the proof of Theorem 4.1(1).

Since the main results of this paper, Theorem 2.1 and 2.2, give only a solution for the special case of integral algebras, we state the following as an open problem.

Problem 4.1**.**

Are the varieties generated by algebras of binary relations of the similarity types $(\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})$ and $(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},{1^{\prime}})$ finitely axiomatizable?

In [AMN11], we stated that ${\sf V}({\sf L}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;}0,{1^{\prime}}))$ is finitely axiomatizable by a certain set of axioms, Corollary 3.7. The proof was based on the theorems of [AM11] mentioned above, hence it is not correct. Luckily Theorem 2.3 above provides a satisfactory solution in this case.

Finally we mention a corollary related to commutative algebras. Let ${\sf R}^{c}(\Lambda)$ denote the class of relation algebras of signature $\Lambda$ that satisfy the commutativity axiom

[TABLE]

for every $x$ and $y$. It is easy to see that ${\sf V}({\sf R}^{c}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ satisfies $\mbox{\rm Ax}^{i}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$. Thus our construction can be applied in this case as well.

Corollary 4.2**.**

The varieties ${\sf V}({\sf R}^{c}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$, ${\sf V}({\sf R}^{c}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}}))$ are finitely axiomatized by commutativity (23) and $\mbox{\rm Ax}(\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$, $\mbox{\rm Ax}(\mathbin{+},\mathbin{\cdot\,},\mathbin{;},0,{1^{\prime}})$, respectively.

Acknowledgements

The author is grateful to Hajnal Andréka, Robin Hirsch and István Németi for helpful comments.