Implication Algebras and Implication Semigroups of Binary Relations

Abstract

Representable implication algebras are known to be axiomatised by a finite number of equations (making the representation and finite representation problems decidable here). We show that this also holds in the context of unary (and binary) relations and present a Stone-style representation theorem. We then show that the (finite) representation decision problem is undecidable for implication semigroups, in stark contrast with implication algebras.

This work was supported by the Engineering and Physical Sciences Research Council EP/S021566/1.

1 Introduction

The variety of implication algebras, so-named by Abbott [1] and studied by Rasiowa [12], Diego [2], and their students, forms the algebraic semantics of the implicational fragment of classical propositional logic. These are Boolean algebras restricted to one operation ($\rightarrow$) and a constant ($\top$ or 1). The variety of Relation algebras, alias residuated Boolean algebras with an additional involution operator ($x^\smile$ or ‘converse of x’, with x understood as a relation), forms the algebraic semantics of the calculus of relations. By a classical result of Korselt attributed in [10], the variety of relation algebras corresponds to the three-variable fragment of classical first-order logic, permitting a study of mathematical logic, particularly set theory [14], via a quantifier-free equational theory. Proofs in this theory consist of simple manipulations of identities, similar to proofs in abstract algebra. This situation contrasts with proofs of standard mathematical logic (or set theory) which can involve complex alternations of quantifiers. Meanwhile, implication algebras (having one operation, classical implication) yield an algebraic analysis of the entailment relation between propositions in classical logic. Although informed by different motivations, a certain elegance recommends the study of relation and implication algebras.

The present paper considers a fragment of the signature of relation algebras we call implication semigroups based on adjoining a semigroup operation (; ), i.e. relational composition, to the implication algebras of Abbott. When the carrier set of this structure is a set of binary relations, we obtain the fragment of relation algebras consisting of $(S, \rightarrow , ;)$, i.e. relation algebras with signature restricted to implication and composition. There are good reasons to examine this signature. For one, it has not been well-explored: practically speaking, most algebraic structures considered in algebraic logic are residuated lattices, groups, or at least monoids – this can be noticed already in a standard definition of relation algebras, as residuated lattices [9] – where the implication and monoidal operations interact via residuation. Algebras featuring implication and semigroup operations fall out of the mainstream substructural logic literature as the algebra at hand lacks the interdefinability present even in the case of a residuated monoid.

For algebraic logic (particularly relation algebras) the question of whether an algebra has a finite representation looms large. One typically asks whether a given logical system of interest is not just consistent but has finite models, i.e. models we can inspect within finite time or employing finitely many resources. The present paper demonstrates the (finite) representation problem for implication semigroups is undecidable. Our results are curious for two reasons. First, implication semigroups represent, in a sense, a limiting case of substructural logics of implication for which the question of decidability of finite representations, to our knowledge, has not been raised, and certainly not approached from the angle considered here. This suggests a track of further research in what one might call substructural relation algebras, exploring the effects of weakening the Boolean base in relation algebra into other algebras of residuation. This is already a current area of research by Peter Jipsen and Nikolaos Galatos [4, 5], and has been broached from another angle in [13], where the signature considered there bears two residuals and a semigroup operation and is in fact a model of the famed Lambek Calculus (thus connecting that algebra to the base system for infinitely many substructural logics). Second, our results contribute to a research programme seeking a better grasp of the consequences for relation algebras when operating in a restricted signature. We are particularly motivated to understand the effect on representability when moving to subsignatures of the standard presentation of a relation algebra [6].

2 Preliminaries

In this section we present the definitions of the algebraic structures and operators for binary relations. We begin by defining Abbott’s implication algebras.

Definition 1

An implication algebra¹ $\mathfrak {A}$ is a pair $(A, \rightarrow )$, with A a set and $\rightarrow$ a binary operation on A satisfying the following properties:

• (i) $(a \rightarrow b) \rightarrow a = a$ (Contraction)

• (ii) $(a \rightarrow b) \rightarrow b = (b \rightarrow a) \rightarrow a$ (Quasi-commutativity)

• (iii) $a \rightarrow (b \rightarrow c) = b \rightarrow (a \rightarrow c)$ (Exchange)

Trivially, because the class of implication algebras is equationally definable, it forms a variety. We shall refer to this class as $\textbf{IA}$. Abbott shows a neat property about these in [1].

Proposition 2

(Abbott). Let $\mathfrak {A}= (A,\rightarrow )$ be an implication algebra. We can implicitly define a constant 1 as $a \rightarrow a$ such that $b \rightarrow 1 = 1$ and $1 \rightarrow b = b$, for all $b \in A$.

This also gives us

Proposition 3

For an implication algebra $(A, \rightarrow )$, we can define a partial order as

$$a \le b \Leftrightarrow (a \rightarrow b) = 1$$

Proof

Let $a+b = (a \rightarrow b) \rightarrow b$. It is commutative by quasi-commutativity, idempotent by contraction, has 1 as the top by Proposition 2, and can be shown associative (see [1][Theorem 12]). So $a+b=b$ forms a partial order. Observe that if $a+b=b$ then $a \rightarrow b = a \rightarrow ((a \rightarrow b) \rightarrow b) = (a \rightarrow b) \rightarrow (a \rightarrow b) = 1$. If $a \rightarrow b = 1$ then $(a \rightarrow b) \rightarrow b = 1 \rightarrow b = b$.    $\square$

Definition 4

Let $\top \subseteq X \times X$ be a binary relation. Define $\mathfrak {A}(\top ) = (\wp (\top ), \rightarrow )$ where $\rightarrow$ is interpreted as proper Boolean implication defined below

$$a \rightarrow b = (\top \setminus a) \cup b$$

One can check that $\mathfrak {A}(\top ) \in \textbf{IA}$. Although $\top$ is conventionally an arbitrary maximal relation, this is not the only possible interpretation of the $\rightarrow$ operation for binary relations. We say that the implication operator is absolute if we require $\top = X \times X$, else we say that it is relative.

We say that $\mathfrak {A}\in \textbf{IA}$ is representable if and only if it embeds into $\mathfrak {A}(\top )$ for some $\top \subseteq X \times X$. The embedding (usually denoted h) is called a representation. If $\mathfrak {A}$ embeds into $\mathfrak {A}(\top )$ and $\top$ is over a finite base X, then we say $\mathfrak {A}$ is also finitely representable.

Another standard presentation of implication algebras is $\mathfrak {A}= (A,\rightarrow ,1)$. However, the constant 1 can be defined as $a \rightarrow a$, for any a. Furthermore, the quasi-commutativity axiom is a consequence of the fact that $(a \rightarrow b) \rightarrow b$ is equivalent to the Boolean join of $a+b$.

Proposition 5

Let $\mathfrak {A}= (A,\rightarrow ) \in \textbf{IA}$ be representable via h. Then $h((a \rightarrow b) \rightarrow b) = h(a) \cup h(b)$ and $h(1) = h(a \rightarrow a) = \top$, for any $a,b \in A$.

Proof

Since $1 = a \rightarrow a$ and h is a representation we get $h(1) = h(a \rightarrow a) = h(a) \rightarrow h(a) = (\top \setminus h(a)) \cup h(a) = \top$.

By h being a representation, DeMorgan’s law, and $a \cap \top = a$ we also have $h((a \rightarrow b) \rightarrow b) = (h(a) \rightarrow h(b)) \rightarrow h(b) = \top \setminus ((\top \setminus h(a)) \cup b) \cup h(b) = (h(a) \cap (\top \setminus h(b))) \cup h(b) = (h(a) \cup h(b)) \cap ((\top \setminus h(b)) \cup h(b)) = (h(a) \cup h(b)) \cap \top = h(a) \cup h(b)$.

   $\square$

We now direct our attention to what happens when we add a semigroup operation (; ) to the signature.

Definition 6

An implication semigroup $\mathfrak {S}$ is a tuple $(S, \rightarrow , ;)$, with a carrier set S and $\rightarrow , ;$ binary operations on S where

• (i) $(S, \rightarrow )$ is an implication algebra

• (ii) (S, ; ) is a semigroup

• (iii) $((a \rightarrow b) \rightarrow b);c = (a;c \rightarrow b;c) \rightarrow b;c$ (Left quasi-additivity)

• (iv) $c;((a \rightarrow b) \rightarrow b) = (c;a \rightarrow c;b) \rightarrow c;b$ (Right quasi-additivity)

The class of implication semigroups will be called $\textbf{ISG}$. Similarly to $\textbf{IA}$ we also examine structures where the carrier set is a set of binary relations.

Definition 7

Let $\top \subseteq X \times X$ be a transitive binary relation. Define $\mathfrak {S}(\top ) = (\wp (\top ), \rightarrow , ;)$ where $\rightarrow$ is interpreted as proper Boolean implication and ;  as proper relational composition defined as

$$a ; b = \{(x,z) \mid \exists y \in X: (x,y)\in a, (y,z) \in b\} $$

Again checking $\mathfrak {S}(\top ) \in \textbf{ISG}$ is relatively straightforward, note that they are closed under composition due to the transitivity of $\top$. Similarly to $\textbf{IA}$, $\mathfrak {S}\in \textbf{ISG}$ is (finitely) representable if it embeds into $\mathfrak {S}(\top )$ for some transitive $\top$ (over a finite base).

3 Basic Theory, Stone Representation, and Decidability for Implication Algebras

We now present the basic theory of implication algebras, the implicational fragment of the implication semigroups discussed in the previous section. We first consider the more general positive implication algebras, subsuming the implication algebras. This culminates in a representation theorem for implication algebras, informing our construction in Sect. 4.²

The axiomatics here are largely in [1] and [12] with some corrections and modifications. Their presentations of the implication algebras are quite different, Abbott preferring an equational presentation where Rasiowa utilises a quasiequational definition.

Definition 8

(Rasiowa 2). A positive implication algebra³ (Postive $\textbf{IA}$) is a pair $(A, \rightarrow , 1)$⁴, a set A and $\rightarrow$ satisfying:

• (P1) $a \rightarrow (b \rightarrow a) = 1$

• (P2) $(a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c)) = 1$

• (P3) if $a \rightarrow b = 1$ and $b \rightarrow a = 1$ then $a = b$

• (P4) $a \rightarrow 1 = 1$

Without proof, we state the following lemmas. For proofs, refer to [12].

Proposition 9

(Rasiowa 2(1)) In any positive implication algebra, the following condition is fulfilled: if $a \rightarrow b = 1$ and $a = 1$, then $b = 1$. Also, if $a = 1$, then $b \rightarrow a = 1$ for any $b \in A$.

Proposition 10

(Rasiowa 2.2). For any positive $\textbf{IA}$ $\mathfrak {A}$, for all $a, b \in A$, we can define a partial order $\le$ on A as

$$a \le b \Longleftrightarrow a \rightarrow b = 1$$

and $1 = c \rightarrow c$ for all maximal c in the poset $(A, \le )$.

Proposition 11

(Rasiowa 2.3). The following hold in any positive implication algebra:

• (1) If $a \le b \rightarrow c$ then $b \le a \rightarrow c$

• (2) $a \le (a \rightarrow b) \rightarrow b$

• (3) $1 \rightarrow a = a$

• (4) If $b \le c$, then $a \rightarrow b \le a \rightarrow c$

• (5) If $a \le b$ then $b \rightarrow c \le a \rightarrow c$

• (6) $a \rightarrow (b \rightarrow c) = b \rightarrow (a \rightarrow c)$

Proposition 12

(Distributivity). In any (positive) implication algebra $\mathfrak {A} = (A, \rightarrow , 1)$, we have $a \rightarrow (b \rightarrow c) = (a \rightarrow b) \rightarrow (a \rightarrow c)$

Proof

We have $b \le a \rightarrow b$ by (P1) and Proposition 10. Applying Proposition 11(5)(6), we get $(a \rightarrow b) \rightarrow (a \rightarrow c) \le b \rightarrow (a \rightarrow c) = a \rightarrow (b \rightarrow c)$. So, $a \rightarrow (b \rightarrow c) = (a \rightarrow b) \rightarrow (a \rightarrow c)$ follows from (P2) and Proposition 10.

The proof that distributivity holds in implication algebras is found in [1, Theorem 5].    $\square$

We now show that the class of implication algebras lies below the class of positive implication algebras. Although the following proposition is not in Abbott or Rasiowa, it is latent in the published results concerning implicative, positive implication, and implication algebras.

Proposition 13

Any implication algebra $(A, \rightarrow )$ is a positive implication algebra.

Proof

(P1) follows from the exchange axiom and Proposition 2, more specifically $a \rightarrow (b \rightarrow a) = b \rightarrow (a \rightarrow a) = b \rightarrow 1 = 1$. For (P2) follows from Proposition 12 and Proposition 2. For (P3) see that by Proposition 3 we have the anti-symmetry for the partial order in implication algebras. Finally (P4) follows directly from Proposition 2.    $\square$

Proposition 14

Any positive implication algebra $(A, \rightarrow )$ satisfying

$$(a\rightarrow b) \rightarrow a = a$$

for all $a,b \in A$ is an implication algebra.⁵

Proof

To show the other direction, let $(A, \rightarrow ,1)$ be a positive implication algebra satisfying $(a \rightarrow b) \rightarrow a = a$. The first axiom of implication algebras $(a \rightarrow b) \rightarrow a = a$ we have already assumed adjoined to the algebra, and the third axiom, $a \rightarrow (b \rightarrow c) = b \rightarrow (a \rightarrow c)$, is found in Proposition 11(6). To show the second axiom: $(a \rightarrow b) \rightarrow b = (b \rightarrow a) \rightarrow a$, we note $a \rightarrow b \le 1 = (b \rightarrow b) = (b \rightarrow a) \rightarrow (b \rightarrow b) = b \rightarrow ((b \rightarrow a) \rightarrow b)$ by Proposition 10 and Proposition 11(6). By Proposition 11(1) we have $b \le (a \rightarrow b) \rightarrow ((b \rightarrow a) \rightarrow b)$ and thus by Proposition 11(1) and (3) we get $(a \rightarrow b) \rightarrow b \le ((a \rightarrow b) \rightarrow (a \rightarrow b)) \rightarrow ((b \rightarrow a) \rightarrow b) = 1 \rightarrow ((b \rightarrow a) \rightarrow b) = ((b \rightarrow a) \rightarrow b)$. By a completely analogous argument, $(a \rightarrow b) \rightarrow b \le (b \rightarrow a) \rightarrow a$. Hence $(a \rightarrow b) \rightarrow b = (b \rightarrow a) \rightarrow a$ as desired.    $\square$

In anticipation of the Stone-style representation theorem, we define some required notions like that of an implicative filter.

Definition 15

(Abbott). An implicative filter of a (positive) implication algebra $\mathfrak {A} = (A,\rightarrow )$ is a subset $F \subseteq A$ such that:

• (i) $1 \in F$

• (ii) if $a \in F$ and $a \rightarrow b \in F$ then $b \in F$

Definition 16

We say that an implicative filter F is proper if $F \ne A$. We say that a proper implicative filter is irreducible if it is not the intersection of two proper implicative filters distinct from it, or formally: F is irreducible if for any two proper implicative filters $F_{1}$, $F_{2}$ such that $F = F_{1} \cap F_{2}$, either $F = F_{1}$ or $F = F_{2}$. Finally, a proper implicative filter F is said to be prime if $a + b \in F$ (or equivalently $(a \rightarrow b) \rightarrow b \in F$) implies that either $a \in F$ or $b \in F$, for all $a,b \in A$.

The proof of the Stone-like Representation theorem follows the following steps. For proofs, refer to [12].

Proposition 17

(Rasiowa 1.8).⁶ If in any (positive) implication algebra $\mathfrak {A} = (A, \rightarrow )$ one of the following conditions is satisfied for all $a, b, c \in A$:

• (F1) $(a \rightarrow (b \rightarrow c)) \rightarrow a \rightarrow b) \rightarrow (a \rightarrow c)) = 1$

• (F2) $(a \rightarrow b) \rightarrow (a \rightarrow (b \rightarrow c)) \rightarrow (a \rightarrow c)) = 1$

then for every implicative filter F in $\mathfrak {A}$ and for every $a \in A$, the set $F_a* = \{x \in A: a \rightarrow x \in F\}$ is an implicative filter. If, moreover, for all $a,b \in A: a \rightarrow (b \rightarrow a) = 1$, then $F_a*$ is the least implicative filter containing F and a.

Proposition 18

(Rasiowa 3.4). If $(A, \rightarrow )$ is a (positive) implication algebra, then for every implicative filter F and for every element $a \in A$ the set $F_a* = \{x \in A : a \rightarrow x \in F \}$ is the least implicative filter containing F and a.

Proposition 19

(Rasiowa 6.1). An implicative filter in an implication algebra is prime if and only if it is irreducible.

Lemma 20

(Rasiowa 1.4). If $F_{0}$ is an implicative filter in an implicative algebra $\mathfrak {A}$ such that $a_{0} \notin F_{0}$ for some $a_{0} \in \mathfrak {A}$ then there exists an irreducible implicative filter G such that $F_{0} \subset G$ and $a_{0} \notin G$.

Immediately, by Lemma 20 and Proposition 19 we have:

Corollary 21

If F is an implicative filter in an implicative algebra $\mathfrak {A}$ such that $a \notin F$ for some $a \in \mathfrak {A}$ then there exists a prime implicative filter G such that $F \subset G$ and $a \notin G$.

This next corollary we prove, as it is not found in any of the literature cited above and is required for the representation theorem.

Corollary 22

Let F be an implicative filter of an implication algebra $\mathfrak {A} = (A, \rightarrow )$ such that $a \rightarrow b \notin F$ for some $a, b \in A$. Then there exists a prime implicative filter $G : F \subseteq G$ such that $a \in G$ and $b \notin G$.

Proof

Let $F_a*$ be the implicative filter generated by the filter F and a. Suppose that $a \rightarrow b \notin F$. If $b \in F_a*$, then we have $a \rightarrow b \in F$ by the definition of $F_a*$. This contradicts our assumption that $a \rightarrow b \notin F$; hence $b \notin F_a*$, and applying Corollary 21 for $F_a*$ and b we have a prime filter G such that $F_a* \subseteq G$ and $b \notin G$. Clearly, $a \in G$ and $F \subseteq G$.    $\square$

We have then, as an immediate corollary from Corollary 22 and Proposition 19, the following:

Corollary 23

Let F be an implicative filter of an implication algebra $\mathfrak {A} = (A, \rightarrow )$ such that $a \rightarrow b \notin F$ for some $a, b \in A$. Then there exists an irreducible implicative filter $G : F \subseteq G$ such that $a \in G$ and $b \notin G$.

Finally, the culminating representation theorem. Rasiowa presents this for irreducible implicative filters [12], which given her equivalence result, one can also state using prime implicative filters, or maximal implicative filters.

Theorem 24

(Rasiowa 7.1). For any implication algebra $\mathfrak {A} = (A, \rightarrow )$, there is a monomorphism h from $\mathfrak {A}$ to $(\wp (X), \rightarrow )$ of an arbitrary space X with $|X| \ge A$.

From this it follows that every implication algebra is isomorphic to an implication algebra of sets. Since the focus of the present paper is on representations, we note a corollary from this last result [1, 2, 12]:

Corollary 25

For any implication algebra $\mathfrak {A}$, if A is finite, then $\mathfrak {A}$ has a finite representation.

Proof

Let $\mathfrak {A}$ be a finite implication algebra. Then by Theorem 24 $\mathfrak {A}$ is monomorphic to the algebra $\mathfrak {A}\prime$ under h, where $\mathfrak {A}\prime = (\wp (X), \rightarrow )$ , an implication algebra of sets. Now if $|X| = A$ then $|\wp (X)| = 2^{|A|}$, and thus finite. That means $h(\mathfrak {A})$, the subalgebra of $\mathfrak {A}\prime$ under h, is finite. So we have $h(\mathfrak {A})$ is a finite implication algebra (induced by h and $\mathfrak {A}$), and hence h is a finite representation of $\mathfrak {A}$.    $\square$

Now, the focus of the rest of the paper revolves around the (finite) representation decision problem for implication semigroups. In the case of $\textbf{IA}$, this is defined as follows:

Definition 26

The (finite) representation decision problem for implication algebras is a decision problem that takes an implication algebra with a (finite) carrier set as input. The algebra is a yes instance if and only if it is (finitely) representable.

Closing this section, we note:

Corollary 27

$\textbf{IA}$ is finitely axiomatisable.

Corollary 28

The (finite) representation problem for $\textbf{IA}$ is decidable.

4 Undecidability Results for Implication Semigroups

In this section we build on results from [7, 8, 11] to show undecidability of some decision problems for. We begin by defining the representation and the finite representation decision problems.

Definition 29

The (finite) representation decision problem for implication semigroups is a decision problem that takes an implication semigroup with a finite carrier set as input. The semigroup is a yes instance if and only if it is (finitely) representable.

As we mention in Sect. 2, whether a structure is representable, also depends on our interpretation of the constant 1. Here we show that the (finite) decision problem is undecidable in both cases.

4.1 Representation Problem with Absolute Implication

We begin by examining the case with absolute implication, i.e. we require $\top = X \times X$ for some (finite) base X.

Definition 30

An implication monoid $\mathfrak {M}= (M, 1', \rightarrow , ;)$ is an algebra where $(M,\rightarrow ,;)$ is an implication semigroup and $1'$ is the monoidal identity for ; . For some transitive and reflexive $\top \subseteq X \times X$, we define $\mathfrak {M}(\top ) = (\wp (\top ), 1', \rightarrow , ;)$ where $\rightarrow ,;$ are proper relational implication and composition respectively and $1'$ is the proper relational identity for X defined as $1' = \{(x,x) \mid x \in X\}$.

In [8, Section 4] a construction of a Boolean monoid from a square cancellative partial group $\mathfrak {G}$ is given. Its implication monoid reduct is denoted $\mathfrak {M}(\mathfrak {G}) = (M,1',\rightarrow ,;)$. By [8, Proposition 5.1, Example 6.2] $\mathfrak {M}(\mathfrak {G})$ is representable (over a finite base) if and only if $\mathfrak {G}$ embeds into a (finite) group.

From the fact that both the group and the finite group embedding problems are undecidable [3] for finite structures it follows that the (finite) representation decision problem is undecidable. Thus if we prove that the $\textbf{ISG}$ reduct of $\mathfrak {M}(\mathfrak {G})$ is (finitely) representable if and only if $\mathfrak {M}(\mathfrak {G})$ is representable, we have shown that the (finite) representability is undecidable. The right to left implication is trivial. But we must examine the case where we relax the requirement where we represent $1'$ as the true relational identity, and show that this is still sufficient for the structure to remain (finitely) representable with $1'$ taken as the true relational identity.

Suppose we have an embedding h from $\mathfrak {M}(\mathfrak {G})$ to $\mathfrak {S}(\top )$, i.e. an injective mapping that preserves $\rightarrow , ;$, but not necessarily $1'$.

Lemma 31

If $(x,y) \in h(1')$ then $(y,x) \in h(1')$.

Proof

Suppose $(y,x) \not \in h(1')$. That means that $(y,x) \in h(1' \rightarrow 0) = h(\overline{1'})$. By composition of $(x,y) \in h(1')$ and $(y,x) \in h(\overline{1'})$ we get that $(x,x) \in h(\overline{1'})$ and by composing that with $(x,y) \in h(1')$ we have that $(x,y) \in h(\overline{1'})$. As $(x,y) \in h(1')$ and $(x,y) \in h(\overline{1'}) = h(1' \rightarrow 0)$, we also have $(x,y) \in h(0)$. By a series of compositions we also get that $(y,x) \in h(0)$ and because $0 \le 1'$ we also get $(y,x) \in h(1')$ and we’ve reached a contradiction.    $\square$

Lemma 32

$h(1')$ is an equivalence relation.

Proof

By Lemma 31 we have that $h(1')$ is symmetric. Furthermore, since all $(x,x) \in h(\top )$ there must exist a z witnessing $1';\top = \top$. Thus $(x,z) \in h(1')$ and $(z,x) \in h(1')$ and we compose that to get $(x,x) \in h(1')$, so $h(1')$ is reflexive. Finally, as $1' = 1';1'$ we also have that $h(1')$ is transitive.    $\square$

Lemma 33

For all $x,x',y,y' \in X$ where $(x',x),(y,y') \in h(1')$ we have for all $a \in \mathfrak {M}(\mathfrak {G})$ that $(x,y) \in h(a) \Leftrightarrow (x',y') \in h(a)$.

Proof

If $(x,y) \in h(a)$ we have $(x,y') \in h(a)$ by $(x',x),(y,y') \in h(1')$ and the composition of $1';a;1'=a$. By Lemma 31, we also have $(x,x'),(y',y) \in h(1')$ so similarly if $(x,y') \in h(a)$ then $(x,y) \in h(a)$.    $\square$

Theorem 34

The (finite) representation decision problem for $\textbf{ISG}$ is undecidable when $\rightarrow$ is interpreted as absolute implication.

Proof

As $h(1')$ is an equivalence relation by Lemma 32, so we can define $h': \mathfrak {M}(\mathfrak {G}) \rightarrow X/h(1')$ where

$$h'(a) = \{([x]_{h(1')}, [y]_{h(1')}) \mid (x,y) \in h(a)\}$$

and show that $h'$ is indeed an embedding of $\mathfrak {M}(\mathfrak {G})$ into $\mathfrak {M}(X \times X)$.

By Lemma 33, we know that if $(x,y) \in h(a)$ then for any $x' \in [x]_{h(1')}, y' \in [y]_{h(1')}$ we have $(x',y') \in h(a)$.

Take any $a \le b$. Then there exists $(x,y) \in h(a)\setminus h(b)$. From this follows $([x]_{h(1')}, [y]_{h(1')}) \in h'(a)$ and if it were the case that $([x]_{h(1')}, [y]_{h(1')}) \in h'(b)$ that would mean that there exist some $(x',y') \in h(b)$ with $(x,x') \in h(1')$ and $(y',y)\in h(1')$ and that would also means that $(x,y) \in h(b)$. Thus $h'$ is injective.

Every composition is witnessed by the equivalence class of the witness for the composition in h and if $(x,y) \in h(a)$ and $(y',z) \in h(b)$ with $y' \in [y]_{h(1')}$ we also have $(y,y') \in h(1')$ and thus we have the composition $(x,z) \in h(a;1';b) = h(a;b)$. Thus $h'$ represents ;  correctly. Finally $1'$ is represented correctly as a pair of equivalence classes is in $h'(1')$ if and only if they are the same equivalence class.

Thus we have shown that if we have an embedding of $\mathfrak {M}(\mathfrak {G})$ into $\mathfrak {S}(X \times X)$ then we also have an embedding of $\mathfrak {M}(G)$ into $\mathfrak {M}(X' \times X')$ where $X' = X/h(1')$. Furthermore if X is finite, so is $X'$. Trivially if $\mathfrak {M}(G)$ embeds into $\mathfrak {M}(X\times X)$ it also embeds into $\mathfrak {S}(X\times X)$ via the same embedding. This, together with the results presented in [8] shows that the (finite) representation decision problem for $\textbf{ISG}$ is undecidable.    $\square$

4.2 Representation Problem with Relative Implication

Now we show the same result for relative implication.

Definition 35

A Boolean semigroup is a tuple $\mathfrak {B}= (B,0,1,-,+,;)$ is an algebraic structure where S is a carrier set

• (i) $(B,0,1,-,+)$ is a Boolean algebra

• (ii) (B, ; ) is a semigroup

• (iii) ;  is additive over $+$

• (iv) $0;a = a;0 = 0$

Similarly to $\textbf{ISG}$, we denote the class of Boolean semigroups $\textbf{BSG}$ and we say that a Boolean semigroup is representable if and only for some transitive $\top \subseteq X \times X$ it embeds into $\mathfrak {B}(\top ) = (\wp (X\times X), \emptyset , \top , -, +, ;)$ where $-a$ is interpreted as proper Boolean negation $\top \setminus a$, $+$ is interpreted as proper Boolean join $\cup$ and ;  is interpreted as proper relational composition.

The (finite) representation problem for Boolean semigroups is defined analogous to that for implication semigroups. [7, Theorem 11.2] shows that the representation problem for Boolean semigroups is undecidable and [11, Theorem 2.5] shows that the finite representation problem for Boolean semigroups is undecidable. From this we show that the (finite) representation problem for implication semigroups is also undecidable.

Note that the above results require an operation $\cdot$ to be defined in the signature, but much like $\top$ in $\textbf{IA}$, $\cdot$ is term definable for $\textbf{BSG}$ as $a \cdot b = -(-a + -b)$.

Lemma 36

Let $\mathfrak {S}= (S, \rightarrow , ;)$ be an implication semigroup that contains some element 0 such that for all $a \in S$ we have $0 \le a$ and $0;a=a;0=0$. If $\mathfrak {S}$ is representable via some representation h then there exists a representation $h'$ of $\mathfrak {S}$ where $h'(0) = \emptyset$. If h is defined over a finite base, so is $h'$.

Proof

Let $h(\mathfrak {S})$ be the proper structure defined by h for some $\top \subseteq X \times X$. As h is a representation, there exists for every pair $a \not \le b \in S$ a discriminator pair $(\iota ,o) \in \top$ such that $(\iota ,o) \in h(a) \setminus h(b)$.

Define $X^{\iota ,o}$ as

$$X^{\iota ,o} = \bigg \{x \in X \mid \Big (x = \iota \vee (\iota ,x) \in \top \Big ) \wedge \Big (y = o \vee (y,o) \in \top \Big ) \bigg \}$$

$\top ^{\iota ,o}$ as $\top \cap (X^{\iota ,o} \times X^{\iota ,o})$, and a mapping $h^{\iota ,o}: \mathfrak {S}\rightarrow \mathfrak {S}(\top ^{\iota ,o})$ where $h^{\iota ,o}(a) = h(a) \cap \top ^{\iota ,o}$.

First observe that $h^{\iota ,o}(0) = \emptyset$. Suppose that there was a pair $(x,y) \in h^{\iota ,o}(0)$. If $x=\iota$, we have $(\iota ,y) \in h^{\iota ,o}(0)$, else $(\iota ,x) \in h(1) = \top$ and thus $(\iota , y) \in h(0)$ since $1;0=0$ and h preserves composition. Similarly if $y = o$ we get $(\iota , o) \in h(0)$, else by composing $(\iota ,y) \in h(0)$ with $(y,z) \in h(1)$ we get $(\iota ,o) \in h(0)$. Since $b \ge 0$ that would mean $(\iota , o) \in h(b)$ that contradicts the fact that $(\iota ,o)$ is a discriminator pair for $a \not \le b$.

Now let us check that $h^{\iota ,o}$ preserves composition. Suppose $(x,y) \in h^{\iota ,o}(a;b)$. This means that there exists $z \in X$ such that $(x,z) \in h(a)$ and $(y,z) \in h(b)$. If $x=\iota$, we trivially have $(x,\iota ) \in h(1) = \top$. Else, by composing $(\iota ,x) \in h(1)$ and $(x,y) \in h(a)$ we get $(\iota ,y) \in h(1) = \top$ as $1;a \le 1$. Similarly $(y,o) \in \top$ and thus $y \in X^{\iota ,o}$. Thus we have $(x,z) \in h^{\iota ,o}(a), (y,z) \in h^{\iota ,o}(b)$ and we have shown $h^{\iota ,o}(a;b) \subseteq h^{\iota ,o}(a);h^{\iota ,o}(b)$. The fact that $h^{\iota ,o}(a;b) \supseteq h^{\iota ,o}(a);h^{\iota ,o}(b)$ follows from $(x,y),(y,z) \in \top ^{\iota ,o}$ then $x,z \in X^{\iota ,o}$ and we have $(x,z) \in \top ^{\iota ,o}$. Thus $h^{\iota ,o}$ preserves composition.

We have $h^{\iota ,o}(a) \ne h^{\iota ,o}(b)$ as $(\iota ,o) \in \top ^{\iota ,o}$. The operation $\rightarrow$ is preserved by $h^{\iota ,o}$ as for all $(x,y) \in \top ^{\iota ,o}$ it holds $(x,y) \in h(a) \Longleftrightarrow (x,y) \in h^{\iota ,o}(a)$. Finally, $|X^{\iota ,o}| \le |X|$. Thus we conclude that $h^\{\iota ,o\}$ is a homomorphism for $\mathfrak {S}$ that discriminates the pair $a \not \le b$.

Now let us pick for every $a \not \le b$ a $\delta (a,b) = (\iota ,o)$ such that $(\iota ,o) \in \top$ is a discriminator pair for $a \not \le b$ and let $\dot{\cup }$ denote a disjoint union. A mapping

$$\begin{aligned}&h': S \rightarrow \wp \left( \dot{\bigcup }_{a \not \le b \in S}\top ^{\delta (a,b)} \right) \\&\qquad h'(c) = \dot{\bigcup }_{a \not \le b \in S}h^{\delta (a,b)}(c) \end{aligned}$$

still represents $;, \rightarrow$ correctly, discriminates all pairs $a \not \le b$ (i.e. is injective), which makes it a representation. Furthermore, $h'(0) = \emptyset$ and the size of its base is bounded by $|S|^2|X|$.    $\square$

Theorem 37

The (finite) representation decision problem for implication semigroups is undecidable.

Proof

We show this by proving that $\mathfrak {B}\in \textbf{BSG}$ is representable if and only if its $\langle \rightarrow , ; \rangle$-reduct $\mathfrak {S}$ is representable. The left to right implication is trivial as $a \rightarrow b \in S$ is term-definable as $(-a) + b \in B$. For the right to left implication, $+, 1$ are term-definable in $\langle \rightarrow , ;\rangle$ (see Proposition 5). By Lemma 36 the $\langle \rightarrow , ; \rangle$-reduct of $\mathfrak {B}$ is representable if and only if it has a representation where $h(0) = \emptyset$. See how in that representation $a \rightarrow 0$ (corresponding to $-a + 0 = -a$ in the Boolean semigroup) is represented as $\top \setminus a \cup \emptyset = \top \setminus a$.

As the (finite) representation decision problem is undecidable for Boolean semigroups, we conclude the same for implication semigroups.    $\square$

5 Problems

In this section we outline some open problems. It follows from the results in Sect. 4 that the class of representable implication semigroups is not finitely axiomatisable, nor does it have the finite representation property, i.e. not every finite representable structure in the class is finitely representable. However, another decision problem of interest is posed below.

Problem 38

Is membership in the equational theory generated by the class of representable implication semigroups decidable?

The reader can see that if we add the bottom element 0 to the signature, the undecidability follows from the undecidability of the equational theory of the Boolean semigroups as described in [7]. This is because all negations of terms $-t$ can be rewritten as $t \rightarrow 0$ and all joins $t+t'$ as $(t \rightarrow t') \rightarrow t'$ where $t,t'$ are terms.

The problem remains open for the class of representable implication semigroups without the bottom element. One of the possible ways to prove undecidability is by using discriminator terms, defined below.

Definition 39

A discriminator term d(a, b, c) is a term defined in terms of elements of algebra a, b, c such that for all representable algebras $d(a,b,c) = c$ if $a=b$ and a otherwise.

Although the existence of discriminator terms is not a guarantee for the undecidability of the equational theory membership decision problem, it is an interesting open question in its own right.

Problem 40

Is it possible to define a discriminator term in the language of implication semigroups?

It is well known that subreducts of representable relation algebras form quasivarieties. As such, the class of implication semigroups can be characterised by quasiequations. However, some open questions about the equational theory generated by the class of representable implication semigroups are listed below.

Problem 41

Is the class of representable implication semigroups a variety?

Problem 42

Is the equational theory generated by the class of representable implication semigroups finitely axiomatisable?

We continue by looking at the alternative interpretations of $\rightarrow$ operation for binary relations. An interesting example, as mentioned in the introduction section is that of a weakening relation defined below.

Definition 43

Let $\textbf{P} = (X, \le )$ be a poset. $R \subseteq X\times X$ is a weakening relation if and only if ${\le };R;{\le } \subseteq R$.

In the context of the weakening relation algebras as described in [4], the $\rightarrow$ operation can be given in first order terms as

$$R \rightarrow S = \{(x,y) \mid \forall x',y': ((x' \le x \wedge y \le y' \wedge (x',y') \in R) \Rightarrow (x',y') \in S) \}$$

where R, S are weakening relations over a poset $\textbf{P} = (X,\le )$.

This interpretation of the $\rightarrow$ operation gives rise to the class of representable weakening implication semigroups, for which the following properties remain open.

Problem 44

Is the (finite) representation decision problem decidable for the class of representable weakening implication semigroups? Is the class finitely axiomatisable and does it have the finite representation property?

Problem 45

Is the class of representable weakening implication semigroups a (discriminator) variety? Is the equational theory generated by the class finitely axiomatisable/decidable?

Finally, we note that it can be checked that all results presented in this paper can be generalised to the dual operation $\leftarrow$ by presenting dual axioms for the class of implication algebras and defining negation as $0 \leftarrow a$.