Have action/predicate systems (or similar) been considered in the literature?

Question

Question. Has the following concept, or anything similar, been considered in the literature?

Definition. An action/predicate system consists of sets $A$ (the actions) and $X$ (the predicates) such that the following hold.

1. $A$ forms a monoid
2. $X$ forms a Boolean lattice
3. There is a monoid action $A \times X \rightarrow X$ denoted $ax$, such that for all $a \in A$ we have that the function $x \in X \mapsto ax \in X$ is an endomorphism of $X$. Intuitively, $ax$ means "the predicate that returns $\mathtt{True}$ in precisely those states where $a$ brings about $x$."

4. There is a function $\sim \,: A \times A \rightarrow X$ subject to the following axioms. Intuitively, $a \sim b$ means "the predicate that returns $\mathtt{True}$ in precisely those states where $a$ has the same effect as $b$."

   • Reflexivity. $\forall a \in A : \top \leq (a \sim a)$
   • Symmetry. $\forall a,b \in A : (a \sim b) \leq (b \sim a)$
   • Transitivity. $\forall a,b,c \in A : (a \sim b) \wedge (b \sim c) \leq (a \sim c)$
   • Compatibility I. $$\forall a,b,c \in A : (a \sim b) \leq (ac \sim bc),\quad \forall a,b,c \in A : (a \sim b) \leq (ca \sim cb)$$
   • Compatibility II. $\forall a,b \in A,\;\forall x \in X : (a \sim b) \leq (ax \leftrightarrow bx)$

Reiteration of Question. Has this been considered in the literature? And if so, what is the correct terminology for such structures, and where can I learn more?

Intuition. Firstly, we can think of actions as being "commands" in a programming language; they move the machine to a new state, depending on its current state. The unit $1 \in A$ is the command that does nothing; furthermore, if $a$ and $b$ are commands, then $ab$ is the result of first performing $a$, then $b$.

Secondly, we can think of predicates as being... well, predicates; in the sense of returning true/false depending on the current state of the machine. Furthermore, if $a$ is an action and $x$ is a predicate, then $ax$ can be thought of as the predicate that returns $\mathtt{true}$ for precisely those states in which the action $a$, if performed, would bring about $x$. Thus we may read "$ax"$ as "$a$ brings about $x$."

Thirdly, the stipulation that the aforementioned action be a homomorphism of boolean algebras can be motivated by the observation that the following statements ought to be equivalent.

1. We're in a state such that performing $a$ would bring about $x \vee y$.
2. We're in a state such that either performing $a$ would bring about $x$, or performing $a$ would bring about $y$.

This corresponds to the axiom $a(x \vee y) = ax \vee ay$. Similar linguistic reasoning can motivate the remainder of the homomorphism stipulation.

Fourthly and finally, the function $\sim : A \times A \rightarrow X$ can be given the following interpretation. If $a,b \in A$ are actions, then $a \sim b$ is the predicate that returns $\mathtt{true}$ for precisely those states in which enacting $a$ would change the machine to the same state as would enacting $b$. The axioms associated with $\sim$ are motivated on this basis.

A bit more motivation. Here's some basic stuff that we can express in this language.

• In any state where $x$ holds, we have that $a$ brings about $y$.

$$x \leq ay$$

• In general, the action $a$ brings about that $x$ implies $y$.

$$\top \leq a(x \rightarrow y)$$

• In any state where $x$ holds, $a$ has the same effect as $b$.

$$x \leq (a \sim b)$$

Answer 1

The first three conditions indeed correspond to the action of a monoid on a Boolean algebra, but the fourth condition is of a different nature. Let me introduce another function $d: A \times A \to X$ by setting $d(a, b) = (a \sim b)'$. Rewriting the four axioms gives

1. For all $a \in A$, $d(a,a) = 0$ ($0$ stands for $\bot$, but seems more appropriate in this context).
2. For all $a,b \in A$, $d(a,b) = d(b,a)$.
3. For all $a,b, c \in A$, $d(a,c) \leqslant d(a,b) \vee d(b,c)$
4. For all $a,b \in A$, and $x \in X$, $ax\ \Delta\ bx \leqslant d(a,b)$ where $x\ \Delta\ y$ is the symmetric difference of $x$ and $y$.

Now, the first three axioms are reminiscent of the definition of a Boolean metric. The missing bit is $d(a, b) = 0$ implies $a = b$, but we are very close to it. Indeed if $d(a, b) = 0$, then by (4) $ax\ \Delta\ bx = 0$, whence $ax = bx$ for all $x$.

The notion of a Boolean metric space dates back at least from the fifties. You can easily find references on the web. I found this early one, but unfortunately I do not have access to this paper.

Blumenthal, L. M. Boolean Geometry I. Rend. Circ. Mat. Palermo. 1952, 1, 343-360.