2 Preliminaries

Algebraically, our setting is varieties of Boolean algebras with an associative operator $\circ $ (associative BAOs), also known as Boolean semigroups: Boolean algebras equipped with an associative binary operator $\circ $ that distributes over all finite (including empty) joins. Logically, varieties of associative BAOs correspond to normal extensions of the least associative normal modal logic.

Formally, we define as follows.

Definition 2.1 (Logics)

Let $\mathbf {K}_2$ denote the least normal modal logic over the language $\mathcal {L}$ generated by the grammar

$$ \begin{align*} \varphi\mathrel{::=} p \mid \neg\varphi \mid \varphi \lor \varphi \mid \varphi \circ \varphi, \end{align*} $$

where $\circ $ is a binary diamond and $p\in \mathsf {Prop}$ for $\mathsf {Prop}$ a countable set of propositional variables. The connectives $\land $ , $\to $ , $\leftrightarrow $ and the constants $\bot , \top $ are defined as usual.

By $\mathbf {AK}_2$ we denote the least normal modal logic extending $\mathbf {K}_2$ that contains the associativity axiom for $\circ $ :

$$ \begin{align*}(p \circ q) \circ r \leftrightarrow p \circ (q \circ r).\end{align*} $$

That is,

$$ \begin{align*}\mathbf{AK}_2\mathrel{:=}\mathbf{K}_2 \oplus (p \circ q) \circ r \leftrightarrow p \circ (q \circ r).\end{align*} $$

We say that a normal modal logic $\mathbf {L}$ is associative if it contains the associativity axiom, that is, if $\mathbf {L}\supseteq \mathbf {AK}_2$ .

Terms $\mathsf {t}$ , equations (or identities) $\mathsf {t}\approx \mathsf {s}$ , and validity of an equation $\mathsf {t}\approx \mathsf {s}$ in a class $\mathsf {K}$ of associative BAOs, written $\mathsf {K}\vDash \mathsf {t}\approx \mathsf {s}$ , are defined in the standard way. Recall also that, by Birkhoff’s theorem, a class of algebras is a variety if and only if it is equationally definable. It follows that the class of all associative BAOs, $\mathsf {BSg}$ , is a variety.

By algebraic completeness, every associative normal modal logic $\mathbf {L}$ is sound and complete with respect to the variety $\mathsf {V}_{\mathbf {L}}$ of associative BAOs defined by

$$ \begin{align*}\mathsf{V}_{\mathbf{L}}\mathrel{:=}\{\mathfrak{A}\mid \mathfrak{A}\vDash \varphi\approx\top, \text{ for all }\varphi\in\mathbf{L}\}.\end{align*} $$

Moreover, the mapping $\mathbf {L}\mapsto \mathsf {V}_{\mathbf {L}}$ constitutes a dual isomorphism between the lattice of normal extensions of $\mathbf {AK}_2$ and the lattice of subvarieties of $\mathsf {BSg}$ , with inverse given by

$$ \begin{align*}\mathsf{V}\mapsto \mathbf{AK}_2\oplus \{\varphi\mid \mathsf{V}\vDash \varphi\approx\top\}.\end{align*} $$

For our purposes, we highlight the following.

Thus, we have the promised correspondence between (decidability of) associative normal modal logics and (decidability of equational theories of) varieties of associative BAOs.

To prove our undecidability results, we proceed via the dual Kripke-semantic perspective. We use that, by canonicity of the associativity axiom (as it is Sahlqvist), the variety of associative BAOs corresponds to the class of all associative Kripke frames. That is, $\mathbf {AK}_2=\mathbf {K}_2\oplus (p\circ q)\circ r\leftrightarrow p\circ (q\circ r)$ is sound and complete with respect to the class of associative Kripke frames, defined as follows.

Definition 2.4 (Frames and models)

An associative frame is a pair $\mathbb {F}=(X,R)$ where $R\subseteq X^3$ is an associative ternary relation, that is, for all $x,a,b,c\in X$ ,

$$ \begin{align*} Rx(ab)c \text{ iff } Rxa(bc). \end{align*} $$

Here, $Rx(ab)c$ means that there is $y \in X$ such that $Rxyc$ and $Ryab$ , and $Rxa(bc)$ means that there is $z \in X$ such that $Rxaz$ and $Rzbc$ .Footnote ² In addition to the prefix notation $Rxyz$ , we occasionally use the infix $xRyz$ for $(x,y,z)\in R$ .

A model is a triple $\mathbb {M}=(X,R, V)$ where $(X,R)$ is an associative frame, and V is a valuation on X, that is, a function $V:\mathsf {Prop} \to \mathcal {P}(X)$ .

Remark 2.5. Some authors define an associative frame as a pair $\mathbb {F}=(X,\cdot )$ where $\cdot :X\times X\to \mathcal {P}(X)$ is an associative binary operation, rather than a ternary relation. This formulation makes the use of the term associativity more transparent: associativity of $\cdot $ amounts to the equality

$$ \begin{align*} (x\cdot y)\cdot z=x\cdot (y\cdot z), \end{align*} $$

where $\cdot $ is lifted to sets $Y,Z\subseteq X$ by

$$ \begin{align*} Y\cdot Z\mathrel{:=}\{x\in X\mid \exists y\in Y, z\in Z:x\in y\cdot z\},\;\; Y\cdot z\mathrel{:=}Y\cdot\{z\},\;\; y\cdot Z\mathrel{:=}\{y\}\cdot Z. \end{align*} $$

On the other hand, an advantage of the ternary-relation presentation is that it aligns directly with modal logic.

In any case, the definitions are equivalent: a ternary relation $R\subseteq X^3$ induces a binary operation $\cdot :X^2\to \mathcal {P}(X)$ by letting $x\in y\cdot z$ iff $Rxyz$ . Conversely, a binary operation $\cdot :X^2\to \mathcal {P}(X)$ induces a ternary relation $R\subseteq X^3$ defined by $R\mathrel {:=}\{(x,y,z)\in X^3\mid x\in y\cdot z\}$ . The transformations are inverse to each other, and $R\subseteq X^3$ is associative if and only if the corresponding operation $\cdot :X^2\to \mathcal {P}(X)$ is.

Note that we have defined associativity from the perspective of the first coordinate; that is, $Rx(ab)c$ holds iff $Rxa(bc)$ does. This choice is also a matter of convention. It contrasts with, for example, the literature on relevant logic, where associativity is typically defined in terms of the third coordinate: $R(ab)cx$ iff $Ra(bc)x$ , but aligns with the usual Kripke semantics for unary diamonds and boxes, which will become clear as we now provide the Kripke-semantic clause for the binary diamond $\circ $ .

Definition 2.6 (Frame semantics)

Given a model $\mathbb {M}=(X,R, V)$ and an $x\in X$ , we say that a formula $\varphi \in \mathcal {L}$ is satisfied at x (in $\mathbb {M}$ ), and write $\mathbb {M}, x\Vdash \varphi $ or simply $x\Vdash \varphi $ , according to the following recursive clauses:

$$ \begin{align*} &\mathbb{M}, x\Vdash p && \textbf{iff} && x\in V(p),\\ &\mathbb{M}, x\Vdash \neg\varphi && \textbf{iff} && \mathbb{M}, x\nVdash \varphi,\\ &\mathbb{M}, x\Vdash \varphi\lor\psi && \textbf{iff} && \mathbb{M}, x\Vdash \varphi \text{ or } \mathbb{M}, x\Vdash \psi,\\ &\mathbb{M}, x\Vdash \varphi\circ\psi && \textbf{iff} && \text{there exist } y,z\in X \text{ such that } \mathbb{M}, y\Vdash \varphi; \\ & && &&\mathbb{M}, z\Vdash \psi; \text{ and } Rxyz. \end{align*} $$

We say that a formula $\varphi \in \mathcal {L}$ is valid in a frame $\mathbb {F}=(X,R)$ , and write $\mathbb {F}\Vdash \varphi $ , if for every model $\mathbb {M}=(X, R, V)$ based on $\mathbb {F}$ and every $x\in X$ , we have $\mathbb {M}, x\Vdash \varphi $ ; and that it is refuted by $\mathbb {F}$ if it is not valid in $\mathbb {F}$ . It is valid in a class of frames $\mathsf {C}$ , written $\mathsf {C}\Vdash \varphi $ , if it is valid in every frame $\mathbb {F}\in \mathsf {C}$ ; and we define the logic of a class of frames $\mathsf {C}$ , $\mathrm {Log}(\mathsf {C})$ , as the set of formulas valid in $\mathsf {C}$ , that is, $\mathrm {Log}(\mathsf {C})\mathrel {:=}\{\varphi \in \mathcal {L}\mid \mathsf {C}\Vdash \varphi \}$ .

For completeness, denoting the class of associative frames by $\mathsf {A}$ , let us make explicit that $\mathbf {AK}_2=\mathrm {Log}(\mathsf {A})$ , which, as noted earlier, is a consequence of the canonicity of the associativity axiom.

Remark 2.7. If we present models $\mathbb {M}$ from the operational perspective, so ${\mathbb {M}=(X,\cdot , V)}$ , the $\circ $ -clause takes the form:

$$ \begin{align*} &\mathbb{M}, x\Vdash \varphi\circ\psi && \textbf{iff} && \text{there exist } y,z\in X \text{ such that } \mathbb{M}, y\Vdash \varphi; \\ & && &&\mathbb{M}, z\Vdash \psi; \text{ and } x\in y\cdot z. \end{align*} $$

When $\cdot :X^2\to \mathcal {P}(X)$ is functional (in that $y\cdot z$ is always a singleton), we may treat it as a map $\cdot :X^2\to X$ and write $x= y\cdot z$ instead of $x\in y\cdot z$ . The induced lifting to sets $\cdot : \mathcal {P}(X) \times \mathcal {P}(X) \to \mathcal {P}(X)$ , as defined in Remark 2.5 and called a complex operation, then becomes

$$\begin{align*}Y \cdot Z = \{y \cdot z \mid y \in Y, z \in Z\}. \end{align*}$$

Given an associative frame $\mathbb {F}=(X,R)$ , the complex algebra of $\mathbb {F}$ is defined as

$$\begin{align*}\mathbb{F}^+ = (\mathcal{P}(X), \cup, \cap, {^c}, \varnothing, X, \cdot), \end{align*}$$

where $\cdot :\mathcal {P}(X)\times \mathcal {P}(X) \to \mathcal {P}(X)$ is the induced lifting, the complex operation, given by

$$\begin{align*}Y \cdot Z := \{x \in X \mid \text{there are } y \in Y, z \in Z: Rxyz\}. \end{align*}$$

Observe that $\mathbb {F}^+$ is an associative BAO. For a class of frames $\mathsf {C}$ , we write $\mathsf {C}^+$ for the class of complex algebras of frames in $\mathsf {C}$ . We also note, for completeness, that for any class of associative frames $\mathsf {C}$ ,

$$\begin{align*}\mathsf{V}_{\mathrm{Log}(\mathsf{C})} = \mathsf{Var}(\mathsf{C}^+). \end{align*}$$

In particular, $\mathsf {V}_{\mathbf {AK}_2}=\mathsf {Var}(\mathsf {A}^+)=\mathsf {BSg}$ , that is, the variety of associative BAOs, $\mathsf {BSg}$ , is generated by the complex algebras of associative frames, $\mathsf {A}^+$ , and precisely contains the algebras validating $\varphi \approx \top $ for every $\varphi \in \mathbf {AK}_2$ .

With this, we conclude the preliminaries by setting out two central systems; additional systems will be presented alongside the undecidability results in the next section.

First, from the binary-operation perspective $(X, \cdot )$ , a natural subclass of associative frames is the class of semilattices, $\mathsf {SL}$ , where $\cdot $ is functional (i.e., $\cdot : X^2 \to X$ ) and associative, commutative, and idempotent. Note that on semilattices, a point x satisfies $\varphi \circ \psi $ if and only if it is the join (or meet) of points y and z satisfying $\varphi $ and $\psi $ , respectively. The variety generated by complex algebras of semilattices, $\mathsf {Var}(\mathsf {SL}^+)$ , is a variety of associative BAOs and has been studied by Bergman [Reference Bergman and Czelakowski8], who, among more, raises the question of its decidability (Problem 4.3)—a question also noted by Jipsen et al. [Reference Jipsen, Kurd-Misto, Wimberley, Madarász and Székely19]. From the logical perspective, the corresponding logic, $\mathrm {Log}(\mathsf {SL})$ , aptly described as the modal logic of semilattices, has been studied by the author in connection with modal information logic and truthmaker semantics [Reference Knudstorp22, Reference Knudstorp23] (more on this in the next section and again in the final section). There, the same decidability problem was raised, posed in logical terms as whether modal information logic over semilattices is decidable.

Second, the complex algebra of a Boolean algebra $(B, \lor , \land , \neg , \bot , \top )$ yields a structure

$$ \begin{align*}(\mathcal{P}(B), \cup, \cap, {^c}, \varnothing, B, \lor, \land, \neg, \bot, \top)\end{align*} $$

with two layers of operators: the (outer or external) Boolean operators $(\cup , \cap , {^c}, \varnothing , B)$ , as well as the (inner or internal) complex operators $(\lor , \land , \neg , \bot , \top )$ , where, for $X,Y\in \mathcal {P}(B)$ , we have

$$ \begin{align*}X\lor Y\mathrel{:=}\{x\lor y\mid x\in X, y\in Y\},\end{align*} $$

and similarly for the other operators. Observe that the reduct $(\mathcal {P}(B), \cup , \cap , {^c}, \varnothing , B, \lor )$ of a complex Boolean algebra is, in particular, an associative BAO; and similarly that, given a Boolean algebra $(B, \lor , \land , \neg , \bot , \top )$ , the join-reduct $(B, \lor )$ (or meet-reduct $(B, \land )$ ) is an associative frame, where, again, relative to a valuation, a point $x\in B$ satisfies $\varphi \circ \psi $ if and only if it is the join (meet) of points y and z satisfying $\varphi $ and $\psi $ , respectively. Also, note that $(B, \lor )^+=(\mathcal {P}(B), \cup , \cap , {^c}, \varnothing , B, \lor )$ .

Complex Boolean algebras, referred to as hyperboolean algebras by Goranko and Vakarelov [Reference Goranko and Vakarelov16], have a modal analogue in the logic termed hyperboolean modal logic, which treats Boolean algebras as Kripke frames and includes modalities corresponding to each Boolean operation, not only the join (or meet). The decidability of this logic was posed as an open problem already in [Reference Goranko and Vakarelov16] and has remained unresolved, with the question raised again by van Benthem [Reference van Benthem, Weiss and Birman6], who brought it to the author’s attention.

These are the systems and questions that initially motivated this line of undecidability research, the impact of which, however, reaches further.

3 Method and scope

To establish our undecidability results, we employ a reduction from the tiling problem, introduced by Wang [Reference Wang38] and shown to be undecidable by Berger [Reference Berger7]. The problem is formulated in terms of Wang tiles—unit squares with a colour on each edge—and asks whether, given a finite set of tiles $\mathcal {W}$ , it is possible to cover the quadrant $\mathbb {N}\times \mathbb {N}$ so that adjacent tiles match along their shared edges. The formal definition is as follows.

It was shown to be undecidable by Berger [Reference Berger7].

We reduce the tiling problem to our setting by computably constructing, for each $\mathcal {W}$ , a formula $\phi ^{}_{\mathcal {W}}\in \mathcal {L}$ such that $\phi ^{}_{\mathcal {W}}$ is valid if and only if $\mathcal {W}$ fails to tile the quadrant.

To extend this result across a range of systems, we divide this biimplication into two lemmas, each proving one direction. In the remainder of this section, we state these lemmas, show that they suffice for undecidability, and highlight their consequences. Proofs of these tiling lemmas, along with the definition of the tiling formulas $\phi ^{}_{\mathcal {W}}$ , are deferred to the next section.

Using these two lemmas, we can derive the following theorem, stated both in algebraic and logical terms. We remind the reader that the two formulations are equivalent, and that results in this section—whether stated algebraically or logically—admit an immediate translation via Proposition 2.3.

Proof. We prove the algebraic version; the logical version then follows by Proposition 2.3, although a direct proof is equally simple.

Let $\mathsf {V}$ be a class of algebras such that

$$\begin{align*}(\mathcal{P}(\mathbb{N}), \cup)^+\in \mathsf{V}\subseteq \mathsf{BSg}. \end{align*}$$

We claim that $\phi ^{}_{\mathcal {W}}\approx \top $ is valid in $\mathsf {V}$ iff $\mathcal {W}$ does not tile the quadrant. Indeed, the left-to-right direction follows from the latter tiling lemma, and right-to-left from the former.

Consequently, the undecidability of the tiling problem implies the undecidability of the equational theory of $\mathsf {V}$ .

We continue by highlighting the main consequences of this theorem. (The reader interested in the more technical part of the article may safely skip ahead to Section 4—the theorems in this section will all be direct consequences of Theorem 3.5, or slight adaptations thereof.) First, the promised solution to the problem posed in [Reference Goranko and Vakarelov16].

Proof. Denote by $\mathsf {BA}_\lor $ , the class of join-reducts $(B,\lor )$ of Boolean algebras $(B, \lor , \land , \neg , \bot , \top )$ . Since the join of a Boolean algebra is associative, and powersets are Boolean algebras, we have $\mathsf {A}\supseteq \mathsf {BA}_\lor \ni (\mathcal {P}(\mathbb {N}), \cup )$ , where, we recall, $\mathsf {A}$ is the class of associative frames. Consequently,

$$\begin{align*}\mathbf{AK}_2\subseteq \mathrm{Log}(\mathsf{BA}_\lor)\subseteq \text{Log}(\mathcal{P}(\mathbb{N}), \cup), \end{align*}$$

hence $\mathrm {Log}(\mathsf {BA}_\lor )$ is undecidable by Theorem 3.5. It follows that hyperboolean modal logic is undecidable, as undecidability in a subsignature clearly implies undecidability in the full signature [ $\mathrm {Log}(\mathsf {BA}_\lor )$ is, by definition, the $\mathcal {L}$ -fragment of hyperboolean modal logic, where our ‘ $\circ $ ’ corresponds to [Reference Goranko and Vakarelov16]’s ‘ $\langle \lor \rangle $ ’-modality (or, alternatively, their ‘ $\langle \land \rangle $ ’-modality)].

Second, Theorem 3.5 also settles the mentioned problem posed in algebraic terms by Bergman [Reference Bergman and Czelakowski8] and Jipsen et al. [Reference Jipsen, Kurd-Misto, Wimberley, Madarász and Székely19], and in logical terminology by the author in [Reference Knudstorp22, Reference Knudstorp23].Footnote ³

The other main protagonist of [Reference Bergman and Czelakowski8, Reference Jipsen, Kurd-Misto, Wimberley, Madarász and Székely19], apart from $\mathsf {Var}(\mathsf {SL}^+)$ , is the variety $\mathsf {BSl}$ of Boolean semilattices—Boolean semigroups that are commutative ( $x\circ y\approx y\circ x$ ) and square-increasing ( $x\leq x\circ x$ ). From Theorem 3.5, we derive the undecidability of its equational theory, and equivalently of the logic

$$ \begin{align*}\mathbf{K}_2\oplus (p\circ q)\circ r\leftrightarrow p\circ (q\circ r)\oplus (p\circ q)\to(q\circ p)\oplus p\to(p\circ p).\end{align*} $$

Problem 4.4 of [Reference Bergman and Czelakowski8] asks whether $\mathsf {BSl}$ is generated by its finite members. Since it is finitely axiomatisable, if it were generated by its finite members, it would have a decidable equational theory.

Next, though not explicitly raised, we note that it follows from our result that logics recently explored by Wang and Wang [Reference Wang, Wang, Ciabattoni, Pimentel and Queiroz39, Reference Wang and Wang40] are undecidable.

We should also point out that our proof yields a new, and to the author’s knowledge the first tiling-based, proof of several known results. To begin, we have the following theorem.

Theorem 3.11 [Reference Kurucz, Némethi, Sain and Simon28, Reference Kurucz, Némethi, Sain and Simon29]

The least associative normal modal logic,

$$ \begin{align*}\mathbf{AK}_2=\mathbf{K}_2\oplus (p\circ q)\circ r\leftrightarrow p\circ (q\circ r),\end{align*} $$

is undecidable.

Next, let $\mathsf {Rel}$ and $\mathsf {CRel}$ denote the classes of algebras isomorphic to (commutative) algebras of binary relations closed under composition and the Boolean operations of intersection ( $\cap $ ), union ( $\cup $ ), and complementation ( $^c$ ). By a result of Jipsen [Reference Jipsen, Berghammer, Möller and Struth18, Theorem 1], we have $\mathsf {Rel}=\mathsf {Var}(\mathsf {Sg}^+)$ and $\mathsf {CRel}=\mathsf {Var}(\mathsf {CSg}^+)$ , where $\mathsf {(C)Sg}$ denotes the variety of (commutative) semigroups. We thus obtain the following theorem.

A final known result that merits emphasis and follows from ours concerns the undecidability of BBI. This was first proven in [Reference Kurucz, Némethi, Sain and Simon29, Corollary 8.1, stating that CRM is undecidable], thereby predating the formulation of BBI itself, with (intuitionistic) BI only introduced by O’Hearn and Pym in 1999 [Reference O’Hearn and Pym34]. The result remained unknown to the bunched implication community, and BBI’s decision problem was long considered open. It was eventually resolved independently by Brotherston and Kanovich [Reference Brotherston and Kanovich10, Reference Brotherston and Kanovich11], using Minsky machines, and by Larchey-Wendling and Galmiche [Reference Larchey-Wendling and Galmiche30, Reference Larchey-Wendling and Galmiche31], embedding an undecidable fragment of intuitionistic linear logic. All of these proofs use distinct approaches, and we supplement these with yet another: tiling.

We also mention that our proof implies the undecidability of several variants of BBI. The paper [Reference Larchey-Wendling and Galmiche30] considers three versions of BBI: $\mathbf {BBI}_{\text {ND}}$ , $\mathbf {BBI}_{\text {PD}}$ , and $\mathbf {BBI}_{\text {TD}}$ , with the first being BBI and the latter two stronger systems, and shows them all to be undecidable. These logics are defined as the sets of theorems, or the consequence relations, over classes of structures: non-deterministic (or relational) monoids, partial monoids, and total monoids, respectively.

A non-deterministic (or relational) monoid is a triple $(M, \cdot , \epsilon )$ , where $\cdot : M \times M \to \mathcal {P}(M)$ is associative and commutative ( $x \cdot y = y \cdot x$ ),Footnote ⁵ and $\epsilon \in M$ is a neutral element ( $\epsilon \cdot x=\{x\}$ ). A partial monoid is a non-deterministic monoid $(M, \cdot , \epsilon )$ in which $\cdot $ is partial functional, that is, $x \cdot y$ is either a singleton or empty. A total monoid is a partial monoid in which $\cdot $ is (total) functional. Theorem 3.5 shows that these three logics are undecidable.

Like [Reference Larchey-Wendling and Galmiche30], in addition to BBI, the paper [Reference Brotherston and Kanovich10] also addresses the decision problem for multiple of its variants. Among more, it considers:

• • The class of separation models, which are triples $(H, \cdot , E)$ , where $\cdot :H\times H\to \mathcal {P}(H)$ is partial functional, associative, commutative, and cancellative (if $z\cdot x=z\cdot y\neq \varnothing $ , then $x=y$ ), and $E\subseteq H$ is a set of units in that $E\cdot x=\{x\}$ .Footnote ⁶

• • The class of separation models with indivisible units, where a separation model $(H, \cdot , E)$ has indivisible units if $x\cdot y\in E$ implies $x\in E$ and $y\in E$ .

• • The class of CBI-models, which are quadruples $(H, \cdot , \{e\}, ^{-1})$ such that $(H, \cdot , \{e\})$ is a separation model and $^{-1}:H\to H$ satisfies $x\cdot x^{-1}=e\cdot e^{-1}=e^{-1}$ .

• • The class of CBI-models with indivisible unit.

• • The logic BBI $+$ eW, which extends BBI and is included in the logic of all separation models with indivisible units.

• • The logic CBI, which extends BBI.

• • The logic CBI $+$ eW, which extends CBI and is included in the logic of all CBI-models with indivisible unit.

As it stands, the undecidability of these is not an immediate consequence of our main result, since union is not cancellative. However, a simple adaptation of tiling lemma (Lemma 3.4) resolves this. Let $(\mathcal {P}(\mathbb {N}), \uplus )$ denote the associative frame where $\uplus $ is the partial disjoint-union operation, defined by $x=y\uplus z$ iff $x=y\cup z$ and $y\cap z=\varnothing $ .

As a concluding comment on propositional separation logics and BBI, observe that this not only offers a new proof of the above undecidability results, but also establishes a new result: the $\{\land , \lor , \neg , \ast \}$ -fragments of these logics are undecidable. In particular, the logics remain undecidable in the absence of the separating implication (or magic wand) ${\mathrel {-\mkern -6mu*}}$ .

On another note, our setting and result connect with Skvortsov’s logic of infinite problems [Reference Skvortsov35], an analogue of Medvedev’s logic of finite problems [Reference Medvedev32, Reference Medvedev33]. In their modal versions, these two logics are defined as the sets of theorems, or the consequence relations, in the basic modal language $\{\land , \lor , \neg , \Diamond \}$ , interpreted over the classes of Skvortsov and Medvedev frames, respectively.

A Skvortsov frame [resp. Medvedev frame] is a pair $(\mathcal {P}(X)\setminus \{\varnothing \}, \supseteq )$ , where X is a non-empty [finite] set and ‘ $\supseteq $ ’ denotes the superset relation on $\mathcal {P}(X)\setminus \{\varnothing \}$ . The decidability of either logic (whether in its modal or intuitionistic propositional version) remains a long-standing open question.

By considering the union operation on $\mathcal {P}(X)\setminus \{\varnothing \}$ , we obtain associative frames $(\mathcal {P}(X)\setminus \{\varnothing \}, \cup )$ , where, given a model $\mathbb {M}=(\mathcal {P}(X)\setminus \{\varnothing \}, \cup , V)$ , the semantics of $\circ $ becomes

$$ \begin{align*} &\mathbb{M}, x\Vdash \varphi\circ\psi && \text{iff} && \text{there exist } y,z\in \mathcal{P}(X)\setminus\{\varnothing\} \text{ such that } \mathbb{M}, y\Vdash \varphi; \\ & && &&\mathbb{M}, z\Vdash \psi; \text{ and } x=y\cup z. \end{align*} $$

In particular, it is readily verified that

$$ \begin{align*} &\mathbb{M}, x\Vdash \varphi\circ\top && \text{iff} && \text{there exist } y\in \mathcal{P}(X)\setminus\{\varnothing\} \text{ such that } x\supseteq y \text{ and } \mathbb{M}, y\Vdash \varphi. \end{align*} $$

That is, $\Diamond $ is definable in our language $\mathcal {L}$ . Hence, the logic

$$ \begin{align*}\text{Log}\big(\{(\mathcal{P}(X)\setminus\{\varnothing\}, \cup)\mid X\neq \varnothing\}\big)\end{align*} $$

in the language $\mathcal {L}$ is a conservative extension of Skvortsov’s modal logic.Footnote ⁷

A slight adjustment of tiling lemma (Lemma 3.4) yields the undecidability of this extension.

Theorem 3.20. The conservative extension of Skvortsov’s modal logic,

$$\begin{align*}\text{Log}\big(\big\{(\mathcal{P}(X)\setminus\{\varnothing\}, \cup)\mid X\neq \varnothing\big\}\big), \end{align*}$$

is undecidable.

Lastly, leveraging one impossibility result to prove another, we answer a somewhat different open question. Van Benthem [Reference van Benthem4, Reference van Benthem5] shows that truthmaker semantics can be faithfully translated into modal information logic over semilattices (see also [Reference Knudstorp23] for further work), and in [Reference van Benthem4], he poses the question of whether a converse translational embedding exists—a question reiterated in [Reference van Benthem, Weiss and Birman6]. We answer this in the negative.

4 Proofs of the tiling lemmas

We now define the tiling formula $\phi ^{}_{\mathcal {W}}$ for a given set of Wang tiles $\mathcal {W}$ and prove the tiling lemmas, Lemmas 3.3 and 3.4. This forms the core of the article implying the undecidability results discussed above.

We begin with a few preliminary definitions and observations that will come in handy. As the tiling lemmas will be proved working frame-theoretically, the following remarks are formulated in that setting, though they may be translated into essentially equivalent algebraic terminology.

Remark 4.1 (Associativity and tiling)

Let $(X,R)$ be an associative frame. For $z\in X$ , define two binary relations

$$\begin{align*}{_zR}\mathrel{:=}\{(a,b)\in X^2\mid Razb \}\quad \text{and} \quad R_z\mathrel{:=}\{(a,b)\in X^2\mid Rabz\} \end{align*}$$

for ‘composition’ on the left and right, respectively. If $(a,b)\in {_zR}$ , we draw an arrow from a to b: . Likewise if $(a,b)\in {R_z}$ . Associativity becomes

and, vice versa,

As the diagrams illustrate, to encode the quadrant $\mathbb {N}^2$ , it suffices to construct an infinite staircase by alternately taking steps along the first axis (via ${_xR}$ ) and the second axis (via ${R_y}$ ). The remaining points in the quadrant $\mathbb {N}^2$ are then generated by applying associativity. This idea forms a key component in our definition of the tiling formulas $\phi ^{}_{\mathcal {W}}$ as well as in our proof of Lemma 3.3.

Remark 4.2. We abbreviate

$$\begin{align*}\varphi\hookrightarrow\psi\mathrel{:=}\neg(\varphi\circ\neg\psi), \end{align*}$$

and

$$\begin{align*}\psi\hookleftarrow\varphi\mathrel{:=}\neg(\neg\psi\circ\varphi). \end{align*}$$

It is then readily verified that, given a model $\mathbb {M}=(X,R,V)$ , the semantics of ‘ $\hookrightarrow $ ’ and ‘ $\hookleftarrow $ ’ come down to the following:

$$ \begin{align*} &\mathbb{M}, x\Vdash \varphi\hookrightarrow\psi && \text{iff} && \text{for all } y,z\in X \text{ such that } Rxyz: &&\text{if } \mathbb{M}, y\Vdash \varphi, \\ & && && &&\text{then }\mathbb{M}, z\Vdash \psi. \end{align*} $$

$$ \begin{align*} &\mathbb{M}, x\Vdash \psi\hookleftarrow\varphi && \text{iff} && \text{for all } y,z\in X \text{ such that } Rxyz: &&\text{if } \mathbb{M}, z\Vdash \varphi, \\ & && && &&\text{then }\mathbb{M}, y \Vdash \psi. \end{align*} $$

Additionally, we define a unary operator ‘ $\Box $ ’ as

$$ \begin{align*} \Box\varphi\mathrel{:=} (\top\hookrightarrow \varphi)\land (\varphi\hookleftarrow\top)\land ([\top\hookrightarrow\varphi]\hookleftarrow\top), \end{align*} $$

and write $Sxy$ , or $xS y$ , if there are $a,b$ such that

• • $Rxay$ ; or

• • $Rxya$ ; or

• • $Rx(ay)b$ .Footnote ⁸

Observe that

$$ \begin{align*} &\mathbb{M}, x\Vdash \Box\varphi && \text{iff} && \text{for all } y\in X \text{ such that } xS y: \mathbb{M}, y\Vdash \varphi, \end{align*} $$

and note that, due to associativity, the relation S is transitive: if $xS yS z$ , then $xS z$ .

For intuition, consider the case where $(X,R)$ is a semilattice; that is, $Rxyz$ iff $x=y\cdot z$ for $\cdot :X\times X\to X$ a function that is

• • commutative: $x\cdot y=y\cdot x$ ;

• • associative: $(x\cdot y)\cdot z=x\cdot (y\cdot z)$ ;

• • idempotent: $x\cdot x=x$ .

Then $S\subseteq X^2$ is simply the partial order $\geq $ on X defined by the semilattice operation,

$$ \begin{align*} &x\geq y && \text{:iff} && x=x\cdot y, \end{align*} $$

andFootnote ⁹ $\Box $ the ‘past-looking’ boxed modality

$$ \begin{align*} &\mathbb{M}, x\Vdash \Box\varphi&& \text{iff}&& \text{for all } y\leq x: \mathbb{M}, y\Vdash \varphi. \end{align*} $$

With this, we now define the tiling formulas.

Definition 4.3 (Tiling formulas)

Let $\mathcal {W}$ be a finite set of tiles. Recall, cf. Definition 3.1, that for a tile t, its edge colours are denoted by $ t_u $ (up), $ t_d $ (down), $ t_l $ (left), and $ t_r $ (right). Given a tile $t\in \mathcal {W}$ , denote the sets of tiles that match to the right and upward, respectively, by

$$\begin{align*}R(t)=\{t'\in \mathcal{W}\mid t_r=t'_l\}\quad \text{and} \quad U(t)=\{t'\in \mathcal{W}\mid t_u=t'_d\}. \end{align*}$$

For each tile $t\in \mathcal {W}$ , we introduce a propositional letter $\mathtt {t}$ and, by an abuse of notation, identify the tile $t\in \mathcal {W}$ with the conjunction of literals

(1) $$ \begin{align} t\mathrel{:=}\mathtt{t}\land \bigwedge_{t\neq t'\in \mathcal{W}}\neg \mathtt{t'}. \end{align} $$

By a further abuse, we define formulas corresponding to the sets of tiles that match to the right and upward, respectively, by

(2) $$ \begin{align} \mathtt{R}(t)\mathrel{:=}\bigvee_{t'\in R(t)}t' \quad \text{and} \quad \mathtt{U}(t)\mathrel{:=}\bigvee_{t'\in U(t)}t'. \end{align} $$

We also introduce propositional letters to encode the quadrant $\mathbb {N}^2$ as well as properties of the coordinate components in pairs $(m,n) \in \mathbb {N}^2$ :

• • $\mathtt {x_e}$ , to encode that the first component m is even, that is, $m=2m'$ .

• • $\mathtt {x_o}$ , to encode that the first component m is odd, that is, $m=2m'+1$ .

• • $\mathtt {y_e}$ , to encode that the second component n is even, that is, $n=2n'$ .

• • $\mathtt {y_o}$ , to encode that the second component n is odd, that is, $n=2n'+1$ .

• • $\mathtt {x'}$ , used in encoding that the first component m is the successor of $m-1$ .

• • $\mathtt {y'}$ , used in encoding that the second component n is the successor of $n-1$ .

Using these propositional letters, we define the formulas:

$$ \begin{align*} &(\alpha_1) && \Box\left(\mathtt{x_e}\to [\mathtt{x'}\circ \mathtt{x_o}]\right)\\ &(\alpha_2) && \Box\left(\mathtt{x_o}\to [\mathtt{x'}\circ \mathtt{x_e}]\right)\\ &(\alpha_3) && \Box\left(\mathtt{y_e}\to [\mathtt{y_o}\circ \mathtt{y'}]\right)\\ &(\alpha_4) && \Box\left(\mathtt{y_o}\to [\mathtt{y_e}\circ \mathtt{y'}]\right)\\ &(\beta_1) && \Box\left( \Biggl[\bigvee_{\mathtt{a},\mathtt{b}\in \{\mathtt{e},\mathtt{o}\}} \mathtt{x_a} \circ \mathtt{y_b}\Biggr]\to \bigvee_{t\in \mathcal{W}}t\right)\\ &(\beta_2) && \Box\bigwedge_{\mathtt{a},\mathtt{b}\in \{\mathtt{e},\mathtt{o}\}}\Biggl( \mathtt{x_a} \circ \mathtt{y_b}\to \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{a},\mathtt{b})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}})\Biggr)\\ &(\gamma_1^h) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_e}\circ \mathtt{y_e}\land t\Bigr] \to\Bigl[ \mathtt{x'} \hookrightarrow \bigl(\mathtt{x_e}\circ \mathtt{y_e}\lor[\mathtt{x_o}\circ \mathtt{y_e}\land \mathtt{R}(t)]\bigr)\Bigr]\biggr)\\ &(\gamma_1^v) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_e}\circ \mathtt{y_e}\land t\Bigr] \to\Bigl[ \bigl(\mathtt{x_e}\circ \mathtt{y_e}\lor[\mathtt{x_e}\circ \mathtt{y_o}\land \mathtt{U}(t)]\bigr) \hookleftarrow \mathtt{y'} \Bigr]\biggr)\\ &(\gamma_2^h) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_e}\circ \mathtt{y_o}\land t\Bigr] \to\Bigl[ \mathtt{x'} \hookrightarrow \bigl(\mathtt{x_e}\circ \mathtt{y_o}\lor[\mathtt{x_o}\circ \mathtt{y_o}\land \mathtt{R}(t)]\bigr)\Bigr]\biggr)\\ &(\gamma_2^v) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_e}\circ \mathtt{y_o}\land t\Bigr] \to\Bigl[ \bigl(\mathtt{x_e}\circ \mathtt{y_o}\lor[\mathtt{x_e}\circ \mathtt{y_e}\land \mathtt{U}(t)]\bigr) \hookleftarrow \mathtt{y'} \Bigr]\biggr)\\ &(\gamma_3^h) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_o}\circ \mathtt{y_e}\land t\Bigr] \to\Bigl[ \mathtt{x'} \hookrightarrow \bigl(\mathtt{x_o}\circ \mathtt{y_e}\lor[\mathtt{x_e}\circ \mathtt{y_e}\land \mathtt{R}(t)]\bigr)\Bigr]\biggr)\\ &(\gamma_3^v) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_o}\circ \mathtt{y_e}\land t\Bigr] \to\Bigl[ \bigl(\mathtt{x_o}\circ \mathtt{y_e}\lor[\mathtt{x_o}\circ \mathtt{y_o}\land \mathtt{U}(t)]\bigr) \hookleftarrow \mathtt{y'} \Bigr]\biggr)\\ &(\gamma_4^h) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_o}\circ \mathtt{y_o}\land t\Bigr] \to\Bigl[ \mathtt{x'} \hookrightarrow \bigl(\mathtt{x_o}\circ \mathtt{y_o}\lor[\mathtt{x_e}\circ \mathtt{y_o}\land \mathtt{R}(t)]\bigr)\Bigr]\biggr)\\ &(\gamma_4^v) && \Box\bigwedge_{t\in \mathcal{W}}\biggl(\Bigl[\mathtt{x_o}\circ \mathtt{y_o}\land t\Bigr] \to\Bigl[ \bigl(\mathtt{x_o}\circ \mathtt{y_o}\lor[\mathtt{x_o}\circ \mathtt{y_e}\land \mathtt{U}(t)]\bigr) \hookleftarrow \mathtt{y'} \Bigr]\biggr) \end{align*} $$

Finally, we let

$$\begin{align*}\phi^{}_{\mathcal{W}} \mathrel{:=} \neg\left(\mathtt{x_e}\circ \mathtt{y_e}\land \bigwedge\alpha_i\land \bigwedge\beta_i\land \bigwedge(\gamma_i^h\land \gamma_i^v)\right). \end{align*}$$

Clearly, the construction of the tiling formula $\phi ^{}_{\mathcal {W}}$ from a finite set of tiles $\mathcal {W}$ is computable. It therefore only remains to prove the tiling lemmas, Lemmas 3.3 and 3.4, which we now proceed to do. For convenience we restate the lemmas.

Proof of Lemma 3.3

By contraposition, suppose that $\phi ^{}_{\mathcal {W}}$ is not valid in the least associative normal modal logic, that is, $\phi ^{}_{\mathcal {W}}\notin \mathbf {AK}_2$ (or algebraically, $\mathsf {BSg}\nvDash \phi ^{}_{\mathcal {W}}\approx \top $ ). We are then to show that $\mathcal {W}$ tiles $\mathbb {N}^2$ .

By canonicity it follows that there is some associative model $\mathbb {M}=(X,R,V)$ and point $z\in X$ such that

$$\begin{align*}\mathbb{M}, z\nVdash \phi^{}_{\mathcal{W}}, \end{align*}$$

that is,

$$\begin{align*}\mathbb{M}, z\Vdash \mathtt{x_e}\circ \mathtt{y_e}\land \bigwedge\alpha_i\land \bigwedge\beta_i\land \bigwedge(\gamma_i^h\land \gamma_i^v). \end{align*}$$

Using this, we prove that $\mathcal {W}$ tiles $\mathbb {N}^2$ . Before proceeding, we outline the structure of the proof.

Outline

We will begin by identifying elements of $\mathbb {M}$

$$\begin{align*}x_0,x_{1}, x_{2}, \ldots;\quad y_0,y_{1}, y_{2}, \ldots;\quad x_{1}', x_{2}', \ldots; \quad y_{1}', y_{2}', \ldots, \end{align*}$$

which we, in turn, will use to identify what we will call staircase points:

$$\begin{align*}p_{1,1}, p_{2,1}, p_{2,2}, p_{3,2}\ldots, p_{k,k}, p_{k+1,k}, \ldots \end{align*}$$

These are so named because they form a staircase in that they will satisfyFootnote ¹⁰ :

$$\begin{align*}p_{k,k}\,{R}\, x_{k}\, y_{k} \quad \text{and}\quad p_{k+1,k}\,{R} \,x_{k+1} \,y_{k}, \end{align*}$$

along with

$$\begin{align*}p_{k,k}\,{R} \,x_{k+1}' \,p_{k+1,k} \quad \text{and} \quad p_{k+1,k}\,{R} \,p_{k+1,k+1} \,y_{k+1}'. \end{align*}$$

From the staircase, we find a full grid of elements $p_{m,n} \in \mathbb {M}$ for all $(m,n) \in \mathbb {N}\times \mathbb {N}$ . Lastly, by associating each point in the quadrant $(m,n) \in \mathbb {N}\times \mathbb {N}$ with the corresponding grid point $p_{m,n} \in \mathbb {M}$ , we can define the tiling $\tau :\mathbb {N}\times \mathbb {N}\to \mathcal {W}$ according to which tile formula $t \in \mathcal {W}$ is satisfied at $p_{m,n}$ , that is, $\mathbb {M}, p_{m,n} \Vdash t$ .

Returning to the proof, we begin by locating the points $(x_i)_{i\geq 0},(y_i)_{i\geq 0}$ within $\mathbb {M}$ —which, loosely speaking, may be thought of as the first and second axis—along with auxiliary points $(x_i')_{i> 0}, (y_i')_{i>0}$ encoding how $x_{i+1}$ and $y_{i+1}$ are successors of $x_{i}$ and $y_{i}$ , respectively. Specifically, we use that $z \Vdash \mathtt {x_e}\circ \mathtt {y_e}\land \bigwedge \alpha _i$ and show by induction that for all $i\geq 0$ :

1. 1. $z\,{R}\,x_0\,y_0$ ;

2. 2. $x_i\,{R}\,x_{i+1}'\, x_{i+1}$ ;

3. 3. $y_i\,{R} \,y_{i+1} \,y_{i+1}'$ ;

4. 4. $x_{i+1}'\Vdash \mathtt {x'}$ and $y_{i+1}'\Vdash \mathtt {y'}$ ;

5. 5. $zSx_i,\; zSy_i,\; zSx_{i+1}',\; zSy_{i+1}'$ ;

6. 6. if i is even: $x_i\Vdash \mathtt {x_e}$ and $y_i\Vdash \mathtt {y_e}$ ;

7. 7. if i is odd: $x_i\Vdash \mathtt {x_o}$ and $y_i\Vdash \mathtt {y_o}$ .

For the base case, since $z\Vdash \mathtt {x_e}\circ \mathtt {y_e}$ , there exist points $x_0,y_0\in \mathbb {M}$ such that $zRx_0y_0$ , $x_0\Vdash \mathtt {x_e}$ , and $y_0\Vdash \mathtt {y_e}$ .

For the induction step, suppose the induction hypothesis holds for some $n\geq 0$ . We treat the case of n even; the case where n is odd is analogous. By induction hypothesis, we have $x_n\Vdash \mathtt {x_e}$ , $y_n\Vdash \mathtt {y_e}$ , $zSx_n,$ and $zSy_n$ . Hence, since $z\Vdash \alpha _1\land \alpha _3$ , there exist points $x_{n+1}', x_{n+1}, y_{n+1}, y_{n+1}'\in \mathbb {M}$ such that

$$\begin{align*}x_n{R} x_{n+1}' x_{n+1}\quad \text{and}\quad y_n{R} y_{n+1} y_{n+1}' \end{align*}$$

as well as

$$\begin{align*}x_{n+1}'\Vdash \mathtt{x'}, \qquad x_{n+1}\Vdash \mathtt{x_o}, \qquad y_{n+1}\Vdash \mathtt{y_o}, \qquad y_{n+1}'\Vdash \mathtt{y'}. \end{align*}$$

Thus, items 1–4 and 6–7 are met. For item 5, simply recall that S is transitive in the presence of associativity (cf. Remark 4.2), thereby completing the induction.

Next, also by an induction, we show that there are staircase points

$$\begin{align*}p_{1,1}, p_{2, 1}, \ldots, p_{k,k}, p_{k+1,k}, \ldots \end{align*}$$

such that

$$ \begin{align*} &p_{1,1}\,{R} \,x_{2}' \,p_{2,1}, && p_{2,1}\,{R} \, p_{2,2} \,y_{2}', && p_{2,2}\,{R} \,x_{3}' \,p_{3,2}, && p_{3,2}\,{R} \, p_{3,3} \,y_{3}',\ldots \\ &p_{k,k}\,{R} \,x_{k+1}' \,p_{k+1,k}, && p_{k+1,k}\,{R} \, p_{k+1,k+1} \,y_{k+1}', &&\ldots, \end{align*} $$

while also demonstrating that for all $k\geq 1$ ,

(3) $$ \begin{align} &p_{k,k}\,{R} \, x_{k} \, y_{k} \quad \text{and} \quad p_{k+1,k}\,{R} \,x_{k+1}\, y_{k}, \end{align} $$

(4) $$ \begin{align} &z\,S\,p_{k,k} \quad \text{and} \quad z\,S\,p_{k+1,k}. \end{align} $$

For the base case, using that $zRx_0y_0$ , $x_0Rx_{1}'x_{1}$ , and $y_0Ry_{1} y_{1}'$ , it follows by associativity that there is a point $p_{1,1}$ such that

$$\begin{align*}z\,{R}\, (x_{1}' \,p_{1,1})\,y_{1}' \quad \text{ so }\quad z\,S\,p_{1,1}, \quad \text{and}\quad p_{1,1}\,{R}\,x_{1}\,y_{1}. \end{align*}$$

Further, $x_1$ witnesses $p_{1,1}R(x_{2}' x_{2})y_1$ because $x_{1}R x_{2}'x_{2}$ , hence, by associativity,

$$\begin{align*}p_{1,1}\,R\,x_{2}' \,(x_{2}\,y_1), \end{align*}$$

which means that there is a point $p_{2,1}$ such that

$$\begin{align*}p_{1,1}\,R\, x_2' \, p_{2,1} \quad \text{and}\quad p_{2,1}\,R\, x_2 \,y_1, \end{align*}$$

As we have already shown that $z\,S\,p_{1,1}$ and the former implies that $p_{1,1}\,S\,p_{2,1}$ , transitivity of S gives us $z\,S\,p_{2,1}$ , completing the base case.

The inductive step has two cases depending on whether we assume the claim up to $p_{k,k}\,{R} \,x_{k+1}' \,p_{k+1,k}$ or up to $p_{k+1,k}\,{R} \, p_{k+1,k+1} \,y_{k+1}'$ . We treat the former. That is, we must show that there is some $p_{k+1,k+1}$ such that

$$\begin{align*}p_{k+1,k}\,{R} \, p_{k+1,k+1} \,y_{k+1}',\quad p_{k+1,k+1}\,{R} \, x_{k+1} \, y_{k+1}, \quad \text{and}\quad z\,S\,p_{k+1,k+1}. \end{align*}$$

By assumption, we have $p_{k+1,k}\, R\,x_{k+1}\,y_k$ , so $y_k$ witnesses $p_{k+1,k}\,R\,x_{k+1} (y_{k+1}y_{k+1}')$ because $y_{k}R y_{k+1}y_{k+1}'$ , so by associativity,

$$\begin{align*}p_{k+1,k}\,R\,(x_{k+1}\, y_{k+1})\,y_{k+1}'. \end{align*}$$

This means that there is a point $p_{k+1,k+1}$ such that

$$\begin{align*}p_{k+1,k}\,R\, p_{k+1,k+1} \, y_{k+1}' \quad \text{and}\quad p_{k+1,k+1}\,R\, x_{k+1}\, y_{k+1}, \end{align*}$$

which—since $z\,S\,p_{k+1,k}\,S\,p_{k+1,k+1}$ implies $z\,S\,p_{k+1,k+1}$ —completes the induction and establishes the staircase.

To generate the full grid, we need points $p_{m,n}\in \mathbb {M}$ for all $m,n\geq 1$ such that

(5) $$ \begin{align} z\, S\, p_{m,n}, \quad p_{m,n}\, R\, x_{m+1}'\, p_{m+1, n}, \quad p_{m,n}\, R\, p_{m, n+1}\, y_{n+1}'. \end{align} $$

We already have these points along the staircase, hence, by repeatedly applying associativity as noted in Remark 4.1, we get the remaining points as illustrated in Figure 1. To be more precise, the construction can be formalised as a recursion on $\omega $ : at stage $k\in \omega $ , we construct all points $p_{m,n}\in \mathbb {M}$ with $|m-n|=k$ . For $k=0$ , these are the diagonal points $p_{m,m}$ , which are already given. For $k=1$ , the points with $m=n+1$ are staircase points as well; to construct the points with $n=m+1$ , we use that $p_{m,m}\,{R} \,x_{n}' \,p_{n,m}$ and $ p_{n,m}\,{R} \, p_{n,n} \,y_{n}'$ , whence $p_{m,m}\,R\,x_{n}'\, (p_{n,n}\,y_{n}')$ , and so by associativity,

$$\begin{align*}p_{m,m}\,R\,(x_{n}'\, p_{n,n})\,y_{n}'. \end{align*}$$

Thus there exists a point $p_{m,n}$ such that

$$\begin{align*}p_{m,m}\,R\, p_{m,n} \, y_{n}' \quad \text{and}\quad p_{m,n}\,R\, x_{n}'\, p_{n,n}, \end{align*}$$

for which we also have $z\, S\, p_{m,n}$ , as $z\,S\,p_{m,m}\,S\,p_{m,n}$ . This completes the case where $k=1$ . The cases where $k>1$ follow analogously, using the other direction of associativity for when $m>n$ .

Figure 1

Generating $\mathbb {N}^2$ from the staircase: $p_{1,1}, p_{2,1}, p_{2,2}, p_{3,2}, p_{3,3},\ldots $ .

As a consequence of $zSp_{m,n}$ along with $z\Vdash \beta _1$ and the identification in (1) of $t\in \mathcal {W}$ with the conjunction of literals, we have that $\tau :\mathbb {N}^2\to \mathcal {W}$ defined by

$$\begin{align*}(m,n)\mapsto t\in \mathcal{W} \text{ such that }p_{m, n} \Vdash t \end{align*}$$

is well-defined as a function, provided that all $p_{m,n}\Vdash \bigvee _{\mathtt {a},\mathtt {b}\in \{\mathtt {e},\mathtt {o}\}} \mathtt {x_a} \circ \mathtt {y_b}$ . In fact, to show that $\tau $ defines a tiling, we will need something stronger than this proviso, namely that for all $p_{m,n}$ ,

$$ \begin{align*} &\text{If } m \text{ and } n \text{ are even: } && p_{m,n}\Vdash \mathtt{x_e}\circ \mathtt{y_e}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{e},\mathtt{e})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}).\\&\text{If } m \text{ is even and } n \text{ is odd: } && p_{m,n} \Vdash \mathtt{x_e}\circ \mathtt{y_o}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{e},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}).\\&\text{If } m \text{ is odd and } n \text{ is even: } && p_{m,n} \Vdash \mathtt{x_o}\circ \mathtt{y_e}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{o},\mathtt{e})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}).\\&\text{If } m \text{ and } n \text{ are odd: } && p_{m,n} \Vdash \mathtt{x_o}\circ \mathtt{y_o}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{o},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}). \end{align*} $$

We show this by an induction, using the staircase as our base case. For the staircase points, this follows immediately: (3), together with items 6 and 7, imply the first conjunct; the second then follows from (4) and that $z\Vdash \beta _2$ .

For the inductive step, we show that if the claim holds for both $p_{m',n'}$ and $p_{m'+1,n'+1}$ , then it also holds for $p_{m',n'+1}$ and $p_{m'+1,n'}$ . As noted, this will, in particular, entail that $\tau $ is well-defined as a function. To complete the proof, as part of the same argument, we also show that $\tau $ satisfies the tiling conditions:

$$\begin{align*}\tau(m',n')_r = \tau(m'+1,n')_l \quad \text{and} \quad \tau(m',n')_u = \tau(m',n'+1)_d. \end{align*}$$

By our definition of $\tau $ and the formulas $t, \mathtt {R}(t),$ and $\mathtt {U}(t)$ (cf. (1) and (2)), this means showing that

$$\begin{align*}\text{if }p_{m',n'}\Vdash t \text{ then } p_{m'+1,n'}\Vdash \mathtt{R}(t), \quad \text{and} \quad \text{if }p_{m',n'}\Vdash t \text{ then } p_{m',n'+1}\Vdash \mathtt{U}(t). \end{align*}$$

There are four cases to consider, corresponding to the parities of $m'$ and $n'$ . Since the cases are analogous, we only cover the case where $m'$ and $n'$ are even and show that the claim follows for $p_{m',n'+1}$ . Assume, then, that the claim holds for $m'=2m$ and $n'=2n$ ; that is,

$$\begin{align*}p_{2m,2n}\Vdash \mathtt{x_e}\circ \mathtt{y_e}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{e},\mathtt{e})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}) \end{align*}$$

and

$$\begin{align*}p_{2m+1,2n+1}\Vdash \mathtt{x_o}\circ \mathtt{y_o}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{o},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}). \end{align*}$$

Then, as mentioned, $zSp_{2m,2n}$ , $p_{2m,2n}\Vdash \mathtt {x_e}\circ \mathtt {y_e}$ , and $z\Vdash \beta _1$ , jointly imply that $p_{2m,2n}\Vdash t$ for some $t\in \mathcal {W}$ . So to complete the proof of this tiling lemma, we show that not only

$$\begin{align*}p_{2m,2n+1} \Vdash \mathtt{x_e}\circ \mathtt{y_o}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{e},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}) \end{align*}$$

but also

$$\begin{align*}p_{2m,2n+1} \Vdash\mathtt{U}(t). \end{align*}$$

Since we have (a) $z\Vdash \gamma _1^v$ , (b) $zSp_{2m,2n}$ , (c) $p_{2m,2n}\Vdash \mathtt {x_e}\circ \mathtt {y_e}\land t$ , (d) $p_{2m,2n}\,R \,p_{2m, 2n+1}$ $y_{2n+1}'$ (by (5)), and (e) $y_{2n+1}'\Vdash \mathtt {y'}$ (by item 4), we get that

$$\begin{align*}p_{2m, 2n+1}\Vdash \mathtt{x_e}\circ \mathtt{y_e}\lor[\mathtt{x_e}\circ \mathtt{y_o}\land \mathtt{U}(t)]. \end{align*}$$

It follows that $p_{2m, 2n+1}\Vdash t'$ for some $t'\in \mathcal {W}$ . Hence, if we had $p_{2m, 2n+1}\Vdash \mathtt {x_e}\circ \mathtt {y_e}$ , then (a’) $z\Vdash \gamma _1^h$ , (b’) $zSp_{2m,2n+1}$ , (c’) $p_{2m,2n+1}\Vdash \mathtt {x_e}\circ \mathtt {y_e}\land t'$ , (d’) $p_{2m,2n+1}\,R \,x_{2m+1}'\,p_{2m+1, 2n+1}$ , and (e’) $x_{2m+1}'\Vdash \mathtt {x'}$ , would jointly imply that

$$\begin{align*}p_{2m+1, 2n+1}\Vdash \mathtt{x_e}\circ \mathtt{y_e}\lor \mathtt{x_o}\circ \mathtt{y_e}, \end{align*}$$

which is a contradiction, as we have by assumption that

$$\begin{align*}p_{2m+1,2n+1}\Vdash \mathtt{x_o}\circ \mathtt{y_o}\land \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{o},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}). \end{align*}$$

Thus, $p_{2m, 2n+1}\nVdash \mathtt {x_e}\circ \mathtt {y_e}$ , so $p_{2m, 2n+1}\Vdash \mathtt {x_e}\circ \mathtt {y_o}\land \mathtt {U}(t)$ , whence the remaining

$$\begin{align*}p_{2m, 2n+1} \Vdash \bigwedge_{(\mathtt{a'},\mathtt{b'})\neq (\mathtt{e},\mathtt{o})}\neg ( \mathtt{x_{a'}}\circ \mathtt{y_{b'}}) \end{align*}$$

follows from $z\Vdash \beta _2$ and $zSp_{2m, 2n+1}$ , finalizing our proof.

We continue with the proof of the other tiling lemma.

Lemma 3.4 (Restated)

If $\phi ^{}_{\mathcal {W}}$ is valid in $(\mathcal {P}(\mathbb {N}), \cup )$ (i.e., $(\mathcal {P}(\mathbb {N}), \cup )^+\vDash \phi ^{}_{\mathcal {W}}\approx \top $ ), then $\mathcal {W}$ does not tile $\mathbb {N}^2$ .

Proof of Lemma 3.4

Suppose, contrapositively, that $\tau :\mathbb {N}^2\to \mathcal {W}$ is a tiling. We have to show that $\phi ^{}_{\mathcal {W}}$ is refuted by $(\mathcal {P}(\mathbb {N}), \cup )$ , that is, $\phi ^{}_{\mathcal {W}}\notin \mathrm {Log}(\mathcal {P}(\mathbb {N}),\cup )$ (or algebraically, $(\mathcal {P}(\mathbb {N}), \cup )^+\nvDash \phi ^{}_{\mathcal {W}}\approx \top $ ).

To this end, write $2\mathbb {N}=\{2n\mid n\in \mathbb {N}\}$ for the even numbers and $2\mathbb {N}+1=\{2n+1\mid n\in \mathbb {N}\}$ for the odd numbers, and define a valuation V as follows:

$$ \begin{align*} V(\mathtt{x_e})&=\{X\subseteq 2\mathbb{N}\mid |2\mathbb{N}\setminus X| \text{ is even}\},\\ V(\mathtt{x_o})&=\{X\subseteq 2\mathbb{N}\mid |2\mathbb{N}\setminus X| \text{ is odd}\},\\ V(\mathtt{y_e})&=\{X\subseteq 2\mathbb{N}+1\mid |(2\mathbb{N}+1)\setminus X| \text{ is even}\},\\ V(\mathtt{y_o})&=\{X\subseteq 2\mathbb{N}+1\mid |(2\mathbb{N}+1)\setminus X| \text{ is odd}\},\\ V(\mathtt{x'})&=\{\{n\}\mid n\in 2\mathbb{N}\},\\ V(\mathtt{y'})&=\{\{n\}\mid n\in (2\mathbb{N}+1)\},\\ V(\mathtt{t})&=\{X\cup Y\mid X\in (V(\mathtt{x_e})\cup V(\mathtt{x_o})), Y\in (V(\mathtt{y_e})\cup V(\mathtt{y_o})),\\ &\qquad\qquad\qquad\tau(|2\mathbb{N}\setminus X|,|(2\mathbb{N}+1)\setminus Y|)=t\}. \end{align*} $$

We proceed showing that

$$ \begin{align*} (\mathcal{P}(\mathbb{N}), \cup, V), \mathbb{N}\nVdash \phi^{}_{\mathcal{W}}, \end{align*} $$

that is,

$$ \begin{align*} (\mathcal{P}(\mathbb{N}), \cup, V), \mathbb{N}\Vdash \mathtt{x_e}\circ \mathtt{y_e}\land \bigwedge\alpha_i\land \bigwedge\beta_i\land \bigwedge(\gamma_i^h\land \gamma_i^v). \end{align*} $$

First off, observe that $2\mathbb {N}\Vdash \mathtt {x_e}$ and $2\mathbb {N}+1\Vdash \mathtt {y_e}$ , hence

$$\begin{align*}\mathbb{N}=2\mathbb{N}\cup (2\mathbb{N}+1)\Vdash \mathtt{x_e}\circ \mathtt{y_e}. \end{align*}$$

Alphas ( $\boldsymbol {\alpha _i}$ ). Second, to see that $\mathbb {N}$ also satisfies the $\alpha $ ’s, note that if some $X\Vdash \mathtt {x_e}$ , then by definition $X\subseteq 2\mathbb {N}$ such that $|2\mathbb {N}\setminus X|$ is even. In particular, there are even numbers $2n\in X$ , and for these, we have $\{2n\}\Vdash \mathtt {x'}$ and $|2\mathbb {N}\setminus (X\setminus \{2n\})|$ is odd, hence

$$ \begin{align*} X=\{2n\}\cup (X\setminus \{2n\}) \Vdash \mathtt{x'}\circ \mathtt{x_o}, \end{align*} $$

as required. A fortiori, $\mathbb {N}\Vdash \alpha _1$ . $\mathbb {N}\Vdash \alpha _2\land \alpha _3\land \alpha _4$ is proven analogously.

Betas ( $\boldsymbol {\beta _i}$ ). Note that the decomposition of a $Z\subseteq \mathbb {N}$ into $X\cup Y=Z$ for $X\in (V(\mathtt {x_e})\cup V(\mathtt {x_o})), Y\in (V(\mathtt {y_e})\cup V(\mathtt {y_o}))$ is unique when it exists. So since $\tau :\mathbb {N}^2\to \mathcal {W}$ in particular is a function, we get that $\mathbb {N}\Vdash \beta _1$ ; and since $V(\mathtt {x_e}), V(\mathtt {x_o}), V(\mathtt {y_e}), V(\mathtt {y_o})$ are pairwise disjoint, we also have $\mathbb {N}\Vdash \beta _2$ .

Gammas ( $\boldsymbol {\gamma _i}$ ). In proving that $\mathbb {N}\Vdash \gamma _1^h\land \gamma _1^v\land \cdots \land \gamma _4^h\land \gamma _4^v$ , we only cover the first conjunct, as the others are proven analogously. Accordingly, suppose $Z\Vdash \mathtt {x_e}\circ \mathtt {y_e}\land t$ for some tile t, and let $Z'\subseteq \mathbb {N}$ and $n\in 2\mathbb {N}$ be arbitrary such that $Z= \{n\}\cup Z'$ . For the purpose of demonstrating that $\mathbb {N}\Vdash \gamma _1^h$ , we must show that

$$\begin{align*}Z'\Vdash \mathtt{x_e}\circ \mathtt{y_e}\lor[\mathtt{x_o}\circ \mathtt{y_e}\land \mathtt{R}(t)]. \end{align*}$$

If $n\in Z'$ , then $Z'=Z\Vdash \mathtt {x_e}\circ \mathtt {y_e}$ , as required.

If $n\notin Z'$ , we use that $Z\Vdash \mathtt {x_e}\circ \mathtt {y_e}$ implies that $Z=X\cup Y$ for some $X\in V(\mathtt {x_e})$ and $Y\in V(\mathtt {y_e})$ . Since $Z\ni n$ is even, it follows that $n\in X$ , whence

$$\begin{align*}Z'=(X\setminus \{n\})\cup Y\Vdash \mathtt{x_o}\circ \mathtt{y_e}. \end{align*}$$

Further, using that $Z\Vdash t$ , so $X\cup Y=Z\Vdash \mathtt {t}$ , which means that $ \tau (|2\mathbb {N}\setminus X|, |(2\mathbb {N}+1)\setminus Y|)=t$ , we get that

$$ \begin{align*} \tau(|2\mathbb{N}\setminus (X\setminus\{n\})|, |(2\mathbb{N}+1)\setminus Y|)=\tau(|2\mathbb{N}\setminus X|+1, |(2\mathbb{N}+1)\setminus Y|)\in R(t), \end{align*} $$

since $\tau $ is a tiling. Consequently,

$$ \begin{align*} Z'=(X\setminus \{n\})\cup Y\Vdash \mathtt{R}(t), \end{align*} $$

as desired, completing the proof of $\mathbb {N}\Vdash \gamma _1^h$ , and thereby of the lemma.

5 Features of the (un)decidable

With the proofs completed, we conclude by turning to a broader aim of this line of research: to better understand the boundary between the solvable and the unsolvable. To this end, we contrast our undecidability results with known decidability results, accentuating features that appear to separate the decidable from the undecidable.

First, the undecidability of the modal logic of semilattices, $\mathrm {Log}(\mathsf {SL})$ (Theorem 3.7), contrasts with two established decidability results. As shown in [Reference Knudstorp24], if we expand the class of structures from semilattices to posets (so we do not require existence of all binary suprema), the resulting logic, typically referred to as modal information logic, is both decidable and finitely axiomatisable.Footnote ¹¹ At first glance, this may appear surprising: why should restricting to semilattices—that is, posets with all binary suprema (or infima)—a seemingly more benign subclass, lead to undecidability? But, as noted by van Benthem [Reference van Benthem, Weiss and Birman6], interpreting ‘ $\circ $ ’ via supremum (or infimum) over semilattices rather than posets yields an important distinction: only over the former is the associativity axiom validated (recall Remark 4.1 on the role of associativity).

Second, by [Reference Knudstorp23, Corollary 2] (building on [Reference van Benthem4, Reference van Benthem5]), truthmaker consequence can be identified with the $\{\lor , \circ \}$ -fragment of $\mathrm {Log}(\mathsf {SL})$ . This is significant because truthmaker consequence, unlike $\mathrm {Log}(\mathsf {SL})$ , is decidable [Reference Fine and Jago14, Reference Knudstorp23]. In fact, as observed in [Reference Knudstorp22, Remark B.3.8], the decidability proof in [Reference Knudstorp23] extends to the language that includes conjunction. Thus, although $\mathrm {Log}(\mathsf {SL})$ is undecidable, its $\{\land ,\lor , \circ \}$ -fragment, that is, the negation-free fragment, is decidable.

This inspires the following research question: how much, or how strong a, negation is needed for undecidability? One algebraically formulated precisification of this is whether the equational theory of the variety of Heyting semigroups—Heyting algebras with an associative operator distributing over finite joins—is decidable. In unpublished work with Peter Jipsen [Reference Jipsen and Knudstorp20], this was answered affirmatively. Thus, we find a sharp dividing line: unlike the variety of Boolean semigroups, $\mathsf {BSg}$ , the variety of Heyting semigroups is decidable. That is, for undecidability, not even intuitionistic negation suffices; classical negation seems necessary.

Having considered the impact on decidability of altering the language or the frames, we end with a note on the effect of restricting the valuations. As mentioned, [Reference Engström and Olsson13] conceives hyperboolean modal logic as a unifying framework for propositional team logics and studies it under the name LT. This connection is intriguing because propositional team logics are decidable, yet LT is not (Theorem 3.6). The key difference being that valuations in team semantics are principal ideals, while in LT they need not be.

To sharpen this contrast, let $\mathsf {Pow}_\cup $ denote the class of associative frames of the form $(\mathcal {P}(X), \cup )$ . By Theorem 3.5, $\mathrm {Log}(\mathsf {Pow}_\cup )$ is undecidable. However, if we only consider models $(\mathcal {P}(X), \cup , V)$ where V is a principal ideal—in that $V:\mathsf {Prop}\to \{\mathcal {P}(Y)\mid Y\subseteq X\}$ —instead of allowing arbitrary valuations $V:\mathsf {Prop}\to \mathcal {P}\mathcal {P}(X)$ , we achieve a sound and complete semantics for propositional team logic, which, contra $\mathrm {Log}(\mathsf {Pow}_\cup )$ , is decidable.Footnote ¹²