<p>The equational theory of the signature <span class="math-container">$S=\{\vee,\wedge,.,\epsilon,^\smile\}$</span> is decidable. See <a href="http://file:///home/doumane/T%C3%A9l%C3%A9chargements/Andr%C3%A9ka-Bredikhin1995_Article_TheEquationalTheoryOfUnion-fre%20(1).pdf" rel="nofollow noreferrer">this</a> paper by Andréka and Bredikhin.</p>
<p>The idea is to associate to every term <span class="math-container">$t$</span> over <span class="math-container">$S$</span> a graph <span class="math-container">$G_t$</span>. Then Andréka and Bredikhin show that two terms <span class="math-container">$t$</span> and <span class="math-container">$u$</span> are equivalent iff there is a graph homomorphism from <span class="math-container">$G_t$</span> to <span class="math-container">$G_u$</span> and a graph homomorphism from <span class="math-container">$G_u$</span> to <span class="math-container">$G_t$</span>. Testing graph homomorphism between finite graphs is decidable, hence the equational theory is also decidable.</p>
<p>The equational theory of <span class="math-container">$S$</span> is not finitely axiomatizable, due to the paper of Andréka and Mikulas you have cited. However, contrarily to what is claimed in this paper, the restrictions of the signature to, say, <span class="math-container">$\{., \cap, \epsilon\}$</span> is not finitely axiomatizable, as shown in <a href="https://hal.archives-ouvertes.fr/hal-02870687v2/document" rel="nofollow noreferrer">this</a> paper.</p>

CC BY-SA 4.0
2020-11-10T10:24:54.657Z
2020-11-10T10:24:54.657Z
A. D.
<p>I'm working on a more thorough algebraic treatment of <a href="http://www.mhelvens.net/professional/publications?view=publication&amp;task=show&amp;id=3" rel="nofollow">delta modeling</a>. Briefly, <em>deltas</em> are syntactic entities that can modify <em>products</em> (as in 'software products'). They actually represent <em>relations</em> on products, so that they could be both partially defined and non-deterministic.</p>

<p>I've been looking into <a href="http://en.wikipedia.org/wiki/Relation_algebra" rel="nofollow">relation algebras</a>. For obvious reasons they seemed like a good place to start.</p>

<p>A relation algebra is a structure $(S, \vee, \wedge, {}^-, \bot, \top, \cdot, \epsilon, {}^\smallsmile)$ with disjunction, conjunction, negation, an empty element, a complete element, composition, a neutral element and converse. Semantically they correspond to the relation operations $(2^{P^2}, \cup, \cap, {}^{\mathsf C}, \varnothing, P^2, \circ, \mathrm{id}_P, {}^{-1})$.</p>

<p>But this is more expressiveness than I need. If I could just remove negation $^-$ and the complete element $\top$, the operations that remain have sensible interpretations for delta modeling. Moreover, it seems that in contrast to $^-$ and $\top$, the operations that remain are in a sense 'constructive' (though I'm not sure the term is apt here), since their meaning does not depend on the description of the full set of products $P$.</p>

<p>Has the structure $(S, \vee, \wedge, \bot, \cdot, \epsilon, {}^\smallsmile)$ been studied? Is there a complete axiomatization for it (with respect to the behavior of the corresponding relation operations)? Does it have a decidable theory?</p>

<hr>

<p><strong>Edit:</strong> I've discovered the work of Hajnal Andréka and Szabolcs Mikulás. In particular the article entitled <a href="http://link.springer.com/article/10.1007/s00012-011-0142-3" rel="nofollow">Axiomatizability of positive algebras of binary relations</a> (a PDF version can be found with Google).</p>

<p>This article seems to summarize some of the results I need. If I understand correctly, the exact structure I describe is not finitely axiomatizable, but it will be if I also remove either $\wedge$, $\cdot$ or ${}^\smallsmile$. Moreover, any signature without that combination, but with $\cdot$ and either $\vee$ or $\wedge$, is finitely axiomatizable.</p>

<p>However, I'm not well-versed enough yet in abstract algebra to write up a coherent answer myself. For example, I don't understand why the presence of $\vee$ or $\wedge$ is required. If I omit both, aren't we simply in monoid territory? And I also still don't know about a decidable theory.</p>

<p>So I would still appreciate it if someone with more experience could write up an answer, preferably one that is easier to understand for the layman than the above cited article.</p>

<algebra><relational-structures>
Complete axiomatization of relation algebras without ${}^-$ and $\top$
mhelvens
# Complete axiomatization of relation algebras without ${}^-$ and $\top$

(Asked by: username_0 on 2013-06-20)

I'm working on a more thorough algebraic treatment of [delta modeling](http://www.mhelvens.net/professional/publications?view=publication&task=show&id=3). Briefly, *deltas* are syntactic entities that can modify *products* (as in 'software products'). They actually represent *relations* on products, so that they could be both partially defined and non-deterministic.

I've been looking into [relation algebras](http://en.wikipedia.org/wiki/Relation_algebra). For obvious reasons they seemed like a good place to start.

A relation algebra is a structure $(S, \vee, \wedge, {}^-, \bot, \top, \cdot, \epsilon, {}^\smallsmile)$ with disjunction, conjunction, negation, an empty element, a complete element, composition, a neutral element and converse. Semantically they correspond to the relation operations $(2^{P^2}, \cup, \cap, {}^{\mathsf C}, \varnothing, P^2, \circ, \mathrm{id}\_P, {}^{-1})$.

But this is more expressiveness than I need. If I could just remove negation $^-$ and the complete element $\top$, the operations that remain have sensible interpretations for delta modeling. Moreover, it seems that in contrast to $^-$ and $\top$, the operations that remain are in a sense 'constructive' (though I'm not sure the term is apt here), since their meaning does not depend on the description of the full set of products $P$.

Has the structure $(S, \vee, \wedge, \bot, \cdot, \epsilon, {}^\smallsmile)$ been studied? Is there a complete axiomatization for it (with respect to the behavior of the corresponding relation operations)? Does it have a decidable theory?

---

**Edit:** I've discovered the work of Hajnal Andréka and Szabolcs Mikulás. In particular the article entitled [Axiomatizability of positive algebras of binary relations](http://link.springer.com/article/10.1007/s00012-011-0142-3) (a PDF version can be found with Google).

This article seems to summarize some of the results I need. If I understand correctly, the exact structure I describe is not finitely axiomatizable, but it will be if I also remove either $\wedge$, $\cdot$ or ${}^\smallsmile$. Moreover, any signature without that combination, but with $\cdot$ and either $\vee$ or $\wedge$, is finitely axiomatizable.

However, I'm not well-versed enough yet in abstract algebra to write up a coherent answer myself. For example, I don't understand why the presence of $\vee$ or $\wedge$ is required. If I omit both, aren't we simply in monoid territory? And I also still don't know about a decidable theory.

So I would still appreciate it if someone with more experience could write up an answer, preferably one that is easier to understand for the layman than the above cited article.

**Tags:** algebra, relational-structures

---

## 1 answers

### Answer by username_1 on 2020-11-10. Score: 2

The equational theory of the signature $S=\{\vee,\wedge,.,\epsilon,^\smile\}$ is decidable. See [this](http://file:///home/doumane/T%C3%A9l%C3%A9chargements/Andr%C3%A9ka-Bredikhin1995_Article_TheEquationalTheoryOfUnion-fre%20(1).pdf) paper by Andréka and Bredikhin.

The idea is to associate to every term $t$ over $S$ a graph $G\_t$. Then Andréka and Bredikhin show that two terms $t$ and $u$ are equivalent iff there is a graph homomorphism from $G\_t$ to $G\_u$ and a graph homomorphism from $G\_u$ to $G\_t$. Testing graph homomorphism between finite graphs is decidable, hence the equational theory is also decidable.

The equational theory of $S$ is not finitely axiomatizable, due to the paper of Andréka and Mikulas you have cited. However, contrarily to what is claimed in this paper, the restrictions of the signature to, say, $\{., \cap, \epsilon\}$ is not finitely axiomatizable, as shown in [this](https://hal.archives-ouvertes.fr/hal-02870687v2/document) paper.


---

