Decidability of equational theories for subsignatures of relation algebra

Abstract

Let S be a subset of the signature of relation algebra. Let R(S) be the closure under isomorphism of the class of proper S-structures and let F(S) be the closure under isomorphism of the class of proper S-structures over finite bases. Based on previous work, we prove that membership of R(S) is undecidable when (Formula presented), and for any of these signatures S if converse is excluded from S then membership of F(S) is also undecidable, for finite S-structures. We prove that the equational theories of F(S) and R(S) are undecidable when S includes composition and the signature of boolean algebra. If all operators in S are positive and it does not include negation, or if it can define neither domain, range nor composition, then the equational theory of either class is decidable. Open cases for decidability of the equational theory of R(S) are when S can define negation but not meet (or join) and either domain, range or composition. Open cases for the decidability of the equational theory of F(S) are (i) when S can define negation, converse and either domain, range or composition, and (ii) when S contains negation but not meet (or join) and either domain, range or composition.