The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {∧, ∨, ¬, -*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then -* splits into two divisions ⧵, ∕). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

We show that every locally integral involutive partially ordered semigroup (ipo-semigroup) $\mathbf A = (A,\le, \cdot, \sim,-)$, and in particular every locally integral involutive semiring, decomposes in a unique way into a family $\{\mathbf A_p : p\in A^+\}$ of integral ipo-monoids, which we call its integral components. In the semiring case, the integral components are unital semirings. Moreover, we show that there is a family of monoid homomorphisms $Φ= \{φ_{pq}: \mathbf A_p\to \mathbf A_q : p\le q\}$, indexed over the positive cone $(A^+,\le)$, so that the structure of $\mathbf A$ can be recovered as a glueing $\int_Φ\mathbf A_p$ of its integral components along $Φ$. Reciprocally, we give necessary and sufficient conditions so that the Płonka sum of any family of integral ipo-monoids $\{\mathbf A_p : p\in D\}$, indexed over a join-semilattice $(D,\lor)$ along a family of monoid homomorphisms $Φ$ is an ipo-semigroup.

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 $\mathsf p,\mathsf q$. We obtain simple conditions on $\mathsf p,\mathsf q$ such that $x{\cdot} y=(\mathsf px\wedge y)\vee(x\wedge \mathsf 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. We find all subdirectly irreducible algebras up to cardinality eight in which $\mathsf p=\mathsf q$ is a closure operator, as well as all finite unary-determined bunched implication chains and map out the poset of join-irreducible varieties generated by them.

In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [ 34 ] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi \(\mathrm{D.LE}\) associated with the basic normal LE-logics and their axiomatic extensions with analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus \(\mathrm{D.LE}\) , as well as for its extensions with analytic structural rules satisfying certain additional properties.

Abstract It is shown that Tarski’s set of ten axioms for the calculus of relations is independent in the sense that no axiom can be derived from the remaining axioms. It is also shown that by modifying one of Tarski’s axioms slightly, and in fact by replacing the right-hand distributive law for relative multiplication with its left-hand version, we arrive at an equivalent set of axioms which is redundant in the sense that one of the axioms, namely the second involution law, is derivable from the other axioms. The set of remaining axioms is independent. Finally, it is shown that if both the left-hand and right-hand distributive laws for relative multiplication are included in the set of axioms, then two of Tarski’s other axioms become redundant, namely the second involution law and the distributive law for converse. The set of remaining axioms is independent and equivalent to Tarski’s axiom system.