Unary-Determined Distributive $\ell$-magmas and Bunched Implication Algebras

Abstract

A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge ,\vee ,\cdot )$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee ,\cdot )$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is unary-determined if $x{\cdot } y=(x{\cdot }\top \wedge y)$ $\vee (x\wedge \top {\cdot }y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations p, q. We obtain simple conditions on p, q such that $x{\cdot } y=(px\wedge y)\vee (x\wedge qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models.