Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations

TL;DR

This paper demonstrates that certain modal product logics, specifically Diff x Diff and its square version, cannot be finitely axiomatised but can be characterized by infinite sets of canonical Sahlqvist axioms, revealing limits of finite axiomatisability.

Contribution

It provides the first examples of finitely axiomatisable modal logic products that are not finitely axiomatisable but can be axiomatized by infinite canonical axioms.

Findings

Diff x Diff is non-finitely axiomatisable but has an infinite Sahlqvist axiomatisation.

The square version of Diff x Diff is also non-finitely axiomatisable but admits an infinite Sahlqvist axiomatisation.

These are the first known examples of such non-finitely axiomatisable product logics with explicit infinite axiomatizations.

Abstract

Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic Diff x Diff is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its `square' version (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over Diff x Diff, but can be axiomatised by adding infinitely many Sahlqvist axioms. These are the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable, but axiomatisable by explicit infinite sets of canonical axioms.

Tables

Table 1. Table 1: Possible finite bi-clusters in a grid of bi-clusters.

type of $ℭ$					constraints on $x\times y$ size
					p-morphic preimage
(no1)	–	+	+	-	no such $x,y$
(no2)	+	–	+	-	no such $x,y$
(no3)	+	+	–	–	no such $x,y$
(no4)	+	+	+	–	no such $x,y$
(inf1)	–	+	+	+	$x={\aleph }_0,y={\aleph }_0$
(inf2)	+	–	+	+	$x={\aleph }_0,y={\aleph }_0$
(inf3)	+	+	–	+	$x={\aleph }_0,y={\aleph }_0$
(inf4)	+	+	+	+	$x={\aleph }_0,y={\aleph }_0$
(h2vsw)	–	+	–	+	$x\ge 2y,y\ge \text{v\_size}\left(ℭ\right)$
$x{\to }^{2}y$
(v2hsw)	–	–	+	+	$x\ge \text{h\_size}\left(ℭ\right),y\ge 2x$
$y{\to }^{2}x$
($=$sw)	+	–	–	+	$x\ge y,y\ge x$,
$x{\leftrightarrow }^{1}y$					$x\ge \text{h\_size}\left(ℭ\right),y\ge \text{v\_size}\left(ℭ\right)$
(hstrict)	–	–	+	–	$x=\text{h\_size}\left(ℭ\right)=\left|ℭ\right|$,
					$y\ge \text{v\_size}\left(ℭ\right)=2\cdot \left|ℭ\right|$
(vstrict)	–	+	–	–	$x\ge \text{h\_size}\left(ℭ\right)=2\cdot \left|ℭ\right|$,
					$y=\text{v\_size}\left(ℭ\right)=\left|ℭ\right|$
(hvstrict)	+	–	–	–	$x=\text{h\_size}\left(ℭ\right)=\left|ℭ\right|$,
					$y=\text{v\_size}\left(ℭ\right)=\left|ℭ\right|$
(free)	–	–	–	+	$x\ge \text{h\_size}\left(ℭ\right)=2\cdot \left|ℭ\right|$,
					$y\ge \text{v\_size}\left(ℭ\right)=2\cdot \left|ℭ\right|$

Equations

$$C_0^{\ne }(X)$$

$$C_1^{\ne }(X)$$

$$\varphi :=p\mid \top \mid \perp \mid \neg \varphi \mid {\varphi }_1\wedge {\varphi }_2\mid {\varphi }_1\vee {\varphi }_2\mid {\square }_{\mathbf{h}}\varphi \mid {\square }_{\mathbf{v}}\varphi \mid {◊}_{\mathbf{h}}\varphi \mid {◊}_{\mathbf{v}}\varphi ,$$

$${◊}_i^{+}\varphi :=\varphi \vee {◊}_i\varphi ,{\square }_i^{+}\varphi :=\varphi \wedge {\square }_i\varphi ,$$

$$F^{x}=\{y\in F:y\mbox{ is accessible from }x\mbox{ along the reflexive and transitive closure of $R_{\mathbf{h}}^{{\mathfrak{F}}}\cup R_{\mathbf{v}}^{{\mathfrak{F}}}$}\}.$$

$${\sf Logic\_of}\,\mathcal{C}=\{\phi:\phi\mbox{ is a bimodal formula valid in every member of $\mathcal{C}$}\}.$$

$${\sf Logic\_of}\,\mathcal{C}={\sf Logic\_of}\,\{\mbox{rooted frames in $\mathcal{C}$}\}.$$

$$\Box^{1}\Bigl{(}\psi_{1}\to\Box^{2}\bigl{(}\psi_{2}\to\dots\Box^{n}(\psi_{n}\to\Box^{0}p)\dots\bigr{)}\Bigr{)},$$

$$\mathbf{K}$$

$$S5$$

$$\mathbf{S5}={\sf Logic\_of}\,\bigl{\{}(W,\forall_{W}):\mbox{$W$ is a non-empty set}\bigr{\}}.$$

$$p\to \square ◊p,$$

$$◊◊p\to (p\vee ◊p).$$

$$\forall x,y,z\;\bigl{(}R(x,y)\land R(y,z)\to(x=z\lor R(x,z))\bigr{)}.$$

$$|U|\geq 2\cdot|\{w\in W:w\mbox{ is $R$-reflexive}\}|+|\{w\in W:w\mbox{ is $R$-irreflexive}\}|.$$

$$|U|\ge 2\cdot |W|$$

$$\forall \varphi :$$

$${◊}^{\ge 2}\varphi :$$

$${◊}^{=1}\varphi :$$

$${\mathfrak{F}}_{\mathbf{h}}\times {\mathfrak{F}}_{\mathbf{v}}=(W_{\mathbf{h}}\times W_{\mathbf{v}},{\overline{R}}_{\mathbf{h}},{\overline{R}}_{\mathbf{v}}),$$

$$(x,y){\overline{R}}_{\mathbf{h}}(x^{\prime },y^{\prime })\text{ iff }x{R}_{\mathbf{h}}{x}^{\prime }\text{mbox}andy=y^{\prime },$$

$$(x,y){\overline{R}}_{\mathbf{v}}(x^{\prime },y^{\prime })\text{ iff }y{R}_{\mathbf{v}}{y}^{\prime }\text{mbox}andx=x^{\prime }.$$

$$x_{\mathbf{h}}$$

$${\mathfrak{F}}_i$$

$${\mathfrak{F}}_{\mathbf{h}}\times {\mathfrak{F}}_{\mathbf{v}}$$

$${\sf Logic\_of}\,\bigl{\{}{\mathfrak{F}}_{\mathbf{h}}\!\times\!{\mathfrak{F}}_{\mathbf{v}}:\mbox{${\mathfrak{F}}_{i}$ is a frame for $L_{i}$, for $i=\mathbf{h},\mathbf{v}$}\bigr{\}}.$$

$$\mathbf{Diff}\times \mathbf{Diff}=Logic\_of\{\text{mbox}productsofdifferenceframes\}.$$

$$\mathbf{Diff}{\times }^{\text{sq}}\mathbf{Diff}=Logic\_of\{\text{mbox}squareproductsofdifferenceframes\}.$$

$$\mathbf{Diff}\times \mathbf{Diff}\subseteq \mathbf{Diff}{\times }^{\text{sq}}\mathbf{Diff}.$$

$$[\mathbf{Diff},\mathbf{Diff}]\subseteq \mathbf{Diff}\times \mathbf{Diff}.$$

$$\text{h\_size}(\mathfrak{C})$$

$$\text{v\_size}(\mathfrak{C})$$

$$u\sim v\text{mbox}iffu{R}_{\mathbf{h}}^{+}v\text{mbox}andu{R}_{\mathbf{v}}^{+}v.$$

$$X=\bigl{\{}[v]\in W^{\sim}:rR_{\mathbf{h}}^{+}v\bigr{\}}\quad\mbox{ and }\quad Y=\bigl{\{}[w]\in W^{\sim}:rR_{\mathbf{v}}^{+}w\bigr{\}},$$

$$g\bigl{(}[v],[w]\bigr{)}=[u]\quad\mbox{ iff }\quad vR_{\mathbf{v}}^{+}u\mbox{ and }wR_{\mathbf{h}}^{+}u.$$

Full text

1 Introduction

Ever since their introduction [38, 40, 9], products of modal logics—propositional multimodal logics determined by classes of product frames—have been extensively studied; see [8] for a comprehensive exposition and further references. In this paper we consider the problem of finding explicit infinite ‘nice’ axiomatisations for non-finitely axiomatisable two-dimensional modal product logics. By ‘nice’ here we mean formulas to which both the canonicity and first-order correspondence properties of Sahlqvist formulas apply.

Canonicity is an important tool for proving Kripke completeness of propositional multimodal logics [2, 12]. A modal logic is canonical if it is valid in all its canonical frames. The analogous algebraic notion of canonical extension is central in the theory of Boolean algebras with operators (BAOs) [26]. A variety of BAOs is canonical if it is closed under taking canonical extensions. A modal formula is canonical if the modal logic axiomatised by it is canonical. Though in general canonicity of a formula is an undecidable ‘semantical’ property [29], there exist known syntactical classes of canonical formulas, such as Sahlqvist formulas [37], and their generalisations by Goranko and Vakarelov [16].

While any set of canonical formulas always axiomatises a canonical logic, Hodkinson and Venema [24] show that there are canonical logics that are barely canonical in the sense that every axiomatisation for such logics must contain infinitely many non-canonical axioms. Further examples of barely canonical elementarily generated logics are given in [14, 3, 28]. Kikot [28] also obtained the following general dichotomy result: If a class of Kripke frames is definable by first-order formulas of the form $\displaystyle\forall x_{0}\exists x_{1}\dots\exists x_{n}\bigwedge R_{\lambda}(x_{i},x_{j})$, then the modal logic generated by such a class is either barely canonical or can be axiomatised by a single generalised Sahlqvist formula. In this paper we show some elementarily generated modal logics that are outside of the scope of this dichotomy.

It is well known that the two-dimensional (2D) modal product logic $\mathbf{S5}\!\times\!\mathbf{S5}$ has a finite axiomatisation with Sahlqvist axioms, describing two commuting $\mathbf{S5}$-modalities [18]. ($\mathbf{S5}\!\times\!\mathbf{S5}$ is the modal counterpart of the substitution and equality free fragment of two-variable first-order logic, where only relational atomic formulas of the form $R(x_{0},x_{1})$ are allowed.) On the other hand, for $n\geq 3$ the $n$-dimensional product logic $\mathbf{S5}^{n}$ is non-finitely axiomatisable [25] and barely canonical (even though it is canonical and recursively enumerable [18]). There are also known examples of recursively enumerable (even decidable) 2D products of finitely axiomatisable modal logics that are not finitely axiomatisable, such as ${\bf K4.3}\!\times\!\mathbf{S5}$ [32]. However, so far no canonical axiomatisations for non-finitely axiomatisable products of finitely axiomatisable logics have been known.

Instead of $\mathbf{S5}$ (the modal logic of all equivalence relations), here we consider modal products with the finitely axiomatisable [39] logic $\mathbf{Diff}$ of all non-equality frames $(W,\neq_{W})$. An arbitrary frame for $\mathbf{Diff}$ is a pseudo-equivalence relation: its equivalence classes might contain both reflexive and irreflexive points. (In particular, equivalence relations are frames for $\mathbf{Diff}$, and so $\mathbf{Diff}\subseteq\mathbf{S5}$.) It is easy to see that, unlike equivalence relations, the class of pseudo-equivalence relations is not Horn-definable. Therefore, the general theorem of Gabbay and Shehtman [9] on axiomatising 2D products of Horn-definable logics by their commutator does not apply to $\mathbf{Diff}\!\times\!\mathbf{Diff}$. However, as pseudo-equivalence relations form an elementary class, it does follow from general results [13, 31, 9] that $\mathbf{Diff}\!\times\!\mathbf{Diff}$ is canonical and recursively enumerable.

We show that the 2D product logic $\mathbf{Diff}\!\times\!\mathbf{Diff}$ is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its ‘square’ version $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over $\mathbf{Diff}\!\times\!\mathbf{Diff}$, but can be axiomatised by adding infinitely many axioms that are generalised Sahlqvist à la Goranko and Vakarelov [16]. This way we give the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable but axiomatisable by explicit infinite sets of canonical axioms. By the correspondence theorem for (generalised) Sahlqvist formulas it follows that the classes of all frames for both $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ are elementary (unlike the frames for $\mathbf{Diff}^{n}$ and $\mathbf{S5}^{n}$ whenever $n\geq 3$, see [22, 31]). As $\mathbf{Diff}$-modalities are ‘self-reversive’, it also follows [15] that $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ in fact can be axiomatised by infinitely many Sahlqvist axioms.

Our results can also be formulated in an algebraic logic setting. Given the full Boolean set algebra $\mathfrak{B}(U\times V)$ of all subsets of the Cartesian product $U\times V$ of some non-empty sets $U,V$, one can define two additional unary operations $C^{\neq}_{0}$, $C^{\neq}_{1}$ on it by taking, for every $X\subseteq U\times V$,

[TABLE]

Just like usual cylindrifications are algebraisations of the existential quantifier in first-order logic, these strict-cylindrifications algebraise the ‘there is a different’ first-order quantifier. We define $\mathsf{sRdf}_{2}$ as the variety generated by all set algebras of this kind, and $\mathsf{sRdf}_{2}^{\textit{sq}}$ as the variety generated by those ones where $U=V$ for the Boolean unit $U\times V$. Members of $\mathsf{sRdf}_{2}$ ($\mathsf{sRdf}_{2}^{\textit{sq}}$) might be referred to as two-dimensional rectangularly (square) representable diagonal-free strict-cylindric algebras. It follows from general considerations that both $\mathsf{sRdf}_{2}$ and $\mathsf{sRdf}_{2}^{\textit{sq}}$ are canonical varieties. We show the following:

• •

The equational theory of $\mathsf{sRdf}_{2}$ is non-finitely axiomatisable, but it has an infinite Sahlqvist axiomatisation.

• •

The equational theory of $\mathsf{sRdf}_{2}^{\textit{sq}}$ is non-finitely axiomatisable over that of $\mathsf{sRdf}_{2}$, but it has an infinite generalised Sahlqvist axiomatisation.

While our varieties are the first such among ‘full rectangular’ algebraisations of finite variable fragments of classical first-order logic, a similarly behaving ‘non-rectangular’ algebraisation has been known. Andréka and Németi [18, 5.5.12] showed that the equational theory of the variety $\mathsf{Crs}_{n}$ of $n$-dimensional relativised cylindric algebras is non-finitely axiomatisable whenever $n\geq 3$, while Resek and Thompson [36, 34] gave an infinite Sahlqvist axiomatisation for it, for any $n$.

2 Our results and proof methods

2.1 Non-finite axiomatisability

Theorem 1**.**

For any Kripke complete logic $L$ with $\mathbf{K}\subseteq L\subseteq\mathbf{S5}$, $L\!\times\!\mathbf{Diff}$ is not axiomatisable using finitely many propositional variables. Thus, $\mathbf{Diff}\!\times\!\mathbf{Diff}$ is not finitely axiomatisable.

Theorem 2**.**

$\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$* is not axiomatisable over $\mathbf{Diff}\!\times\!\mathbf{Diff}$ using finitely many propositional variables. *

After providing the necessary definitions in §3 and some general tools in §4, Theorems 1 and 2 are proved in §5. In our proofs, we will use the following pattern. We show that every axiomatisation of a logic $L$ must contain infinitely many propositonal variables by providing two infinite sequences of frames ${\mathfrak{F}}_{k}$ and ${\mathfrak{G}}_{k}$ such that

• •

every ${\mathfrak{F}}_{k}$ is a frame for $L$, while every ${\mathfrak{G}}_{k}$ is not,

• •

but if $k$ is sufficiently large compared to $m$, then we cannot distinguish between ${\mathfrak{F}}_{k}$ and ${\mathfrak{G}}_{k}$ using $m$ many propositional variables.

2.2 Infinite canonical axiomatisations

Theorem 3**.**

• (i)

There is an infinite axiomatisation for $\mathbf{Diff}\!\times\!\mathbf{Diff}$ consisting of Sahlqvist formulas.

• (ii)

The class of all frames for $\mathbf{Diff}\!\times\!\mathbf{Diff}$ is elementary.

• (iii)

For every countable rooted frame ${\mathfrak{F}}$, ${\mathfrak{F}}$ is a frame for $\mathbf{Diff}\!\times\!\mathbf{Diff}$ iff ${\mathfrak{F}}$ is the p-morphic image of some product of two difference frames.

Theorem 4**.**

• (i)

$\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$* can be axiomatised by adding infinitely many generalised Sahlqvist formulas to $\mathbf{Diff}\!\times\!\mathbf{Diff}$.*

• (ii)

The class of all frames for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ is elementary.

• (iii)

For every countable rooted frame ${\mathfrak{F}}$, ${\mathfrak{F}}$ is a frame for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ iff ${\mathfrak{F}}$ is the p-morphic image of some product of two difference frames of the same size.

As each generalised Sahlqvist formula is axiomatically equivalent to a Sahlqvist formula with inverse modalities [15, 16] and $\mathbf{Diff}$-modalities are ‘self-reversive’, we have the following (see §7.3 for more detail):

Corollary 5**.**

There is an infinite axiomatisation for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ consisting of Sahlqvist formulas.

Theorems 3 and 4 are proved in the respective §6 and §7. In our proofs, we will use the following pattern. In order to axiomatise ${\sf Logic\_of}\,\mathcal{C}$ for some class $\mathcal{C}$ of frames, we define a recursive set $\Sigma$ of (generalised) Sahlqvist formulas, and prove that the following hold:

• (ax1)

All formulas in $\Sigma$ are valid in every frame in $\mathcal{C}$.

• (ax2)

For every countable rooted frame ${\mathfrak{F}}$ that is not the p-morphic image of some frame in $\mathcal{C}$, there is some $\phi_{\mathfrak{F}}\in\Sigma$ such that $\phi_{\mathfrak{F}}$ is not valid in ${\mathfrak{F}}$.

Then it follows that ${\sf Logic\_of}\,\mathcal{C}$ is axiomatised by $\Sigma$. Indeed, let $L$ be the smallest bimodal logic containing $\Sigma$. Then we clearly have $L\subseteq{\sf Logic\_of}\,\mathcal{C}$ by (ax1). On the other hand, by the (generalised) Sahlqvist completeness theorem, $L$ is canonical, and so Kripke complete. By the (generalised) Sahlqvist correspondence theorem, the class of all frames for $L$ is an elementary class. Then it is easy to see by a Löwenheim–Skolem type argument (see e.g. [8, Thm. 1.6]) that $L$ is the logic of its countable frames, and so by a standard modal logic argument $L$ is the logic of its countable rooted frames. Now take some $\psi\notin L$. Then there is some countable rooted frame ${\mathfrak{F}}$ such that ${\mathfrak{F}}$ is a frame for $L$, but $\psi$ is not valid in ${\mathfrak{F}}$. By (ax2), ${\mathfrak{F}}$ is the p-morphic image of some frame in $\mathcal{C}$, and so $\psi\notin{\sf Logic\_of}\,\mathcal{C}$.

Now the following two statements clearly follow from the above:

• •

The class of all frames for ${\sf Logic\_of}\,\mathcal{C}$ is elementary.

• •

For every countable rooted frame ${\mathfrak{F}}$, ${\mathfrak{F}}$ is a frame for ${\sf Logic\_of}\,\mathcal{C}$ iff ${\mathfrak{F}}$ is the p-morphic image of some frame in $\mathcal{C}$.

3 Preliminaries and basic definitions

Our notation and terminology are mostly standard. We denote the cardinality of a set $S$ by $|S|$. Natural numbers are considered as finite cardinals, and we use the usual multiplication operation and ordering relations $<$ and $\leq$ among them and the infinite cardinal $\aleph_{0}=|\omega|$. We call $S$ countable if $|S|\leq\aleph_{0}$. We denote the set of natural numbers by $\mathbb{N}$ and its positive members by $\mathbb{N}^{+}$. We will also use the usual functions $\min(X)$, $\max(X)$ and $\sup(X)$ with respect to $<$, for $X\subseteq\mathbb{N}\cup\{\aleph_{0}\}$.

3.1 Digraphs

We assume that the reader is familiar with the basic notions about digraphs $\mathcal{G}=(N_{\mathcal{G}},\to)$ (see [1] for reference). Below we summarise the notions used in the paper. We call a node (vertex) in $N_{\mathcal{G}}$ an initial node if it has no incoming $\to$ edges, and a final node if it has no outgoing $\to$ edges. A digraph $\mathcal{G}^{-}$ is called a subgraph of $\mathcal{G}$ if its nodes and edges are subsets of the nodes and edges of $\mathcal{G}$, respectively. If the edges of a subgraph $\mathcal{G}^{-}$ consists of all the edges of $\mathcal{G}$ whose endpoints are nodes in $\mathcal{G}^{-}$, then $\mathcal{G}^{-}$ is called an induced subgraph of $\mathcal{G}$. Given two nodes $z,z^{\prime}$, a (directed) path in $\mathcal{G}$ from $z$ to $z^{\prime}$ is a finite sequence of subsequent edges, the first one starting in $z$ and the last one ending in $z^{\prime}$. The length of a path is the number of edges in it (we also consider paths of length [math]). We call a path simple if it does not contain the same edge twice. A cycle is a path starting and ending at the same node. $\mathcal{G}$ is called acyclic if it does not contain any cycles. A strongly connected component is a maximal subgraph $\mathcal{S}$ such that for all nodes $z$ and $z^{\prime}$ in $\mathcal{S}$ there is a path from $z$ to $z^{\prime}$. A finite sequence $z_{0},\dots,z_{m}$ of nodes is an undirected path between $z_{0}$ and $z_{m}$ in $\mathcal{G}$ if for every $i<m$, either $z_{i}\to z_{i+1}$ or $z_{i+1}\to z_{i}$ is an edge in $\mathcal{G}$.

An acyclic digraph $\mathcal{G}$ is called a directed rooted tree (or tree, for short) if there is some inital node $r$ (the root) such that for every node $z$ in $\mathcal{G}$ there is a unique path from $r$ to $z$. For each $z$, the length of this unique path is the height of $z$. If $z\to z^{\prime}$ is an edge in a tree, then $z^{\prime}$ is called a child of $z$. A leaf in a tree is a node without children, that is, a final node.

Given a finite digraph $\mathcal{G}$ and a node $r$ in it, the tree unravelling of $\mathcal{G}$ with root $r$ is the directed rooted tree $\mathcal{T}_{\mathcal{G},r}=(T_{\mathcal{G},r},\Rightarrow)$, where $T_{\mathcal{G},r}$ is the set of all paths in $\mathcal{G}$ starting at $r$ (with the length 0 path being the root of $\mathcal{T}_{\mathcal{G},r}$), and $P\Rightarrow P^{\prime}$ iff $P^{\prime}$ can be obtained from $P$ by adding an additional $\to$ edge to its endpoint. It is customary to identify each path $P\in T_{\mathcal{G},r}$ with a distinct copy of its endpoint, in particular, to identify the root of $\mathcal{T}_{\mathcal{G},r}$ with $r$.

3.2 Unimodal and bimodal logics

In what follows we assume that the reader is familiar with the basic notions in propositional multimodal logic and its possible world semantics (see [2, 4] for reference). Below we summarise the necessary notions and notation for the bimodal case only, but we will use them throughout for the unimodal case as well. We define bimodal formulas by the following grammar:

[TABLE]

where $p$ ranges over a countably infinite set of propositional variables. We use the usual abbreviations $\to$, $\leftrightarrow$, and also

[TABLE]

for $i=\mathbf{h},\mathbf{v}$. (The subscripts are indicative of the 2D intuition: $\mathbf{h}$ for ‘horizontal’ and $\mathbf{v}$ for ‘vertical’.) Bimodal formulas are evaluated in bimodal frames: relational structures of the form ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$, having two binary relations $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ on a non-empty set $W$. A (Kripke) model on ${\mathfrak{F}}$ is a function ${\mathfrak{M}}$ mapping propositional variables to subsets of $W$. (With a slight abuse of notation, we identify the pair $({\mathfrak{F}},{\mathfrak{M}})$ with ${\mathfrak{M}}$.) Given $m\in\mathbb{N}$, we call a Kripke model ${\mathfrak{M}}$ $m$-generated if there are at most $m$ different propositional variables $p$ such that ${\mathfrak{M}}(p)\neq\emptyset$. The truth relation ‘${\mathfrak{M}},w\models\phi$’, connecting points in models and formulas, is defined as usual by induction on $\phi$. If ${\mathfrak{M}},w\models\phi$ for some model ${\mathfrak{M}}$ on ${\mathfrak{F}}$ and some point $w$ in ${\mathfrak{M}}$, then we say that $\phi$ is satisfied in ${\mathfrak{M}}$, and satisfiable in ${\mathfrak{F}}$. Given a set $\Sigma$ of bimodal formulas, we write ${\mathfrak{M}}\models\Sigma$ if we have ${\mathfrak{M}},w\models\phi$, for every $\phi\in\Sigma$ and every $w\in W$. (We write just ${\mathfrak{M}}\models\phi$ for ${\mathfrak{M}}\models\{\phi\}$.) We say that $\phi$ is valid in ${\mathfrak{F}}$, if ${\mathfrak{M}}\models\phi$ for every model ${\mathfrak{M}}$ based on ${\mathfrak{F}}$. If every formula in a set $\Sigma$ is valid in ${\mathfrak{F}}$, then we say that ${\mathfrak{F}}$ is a frame for $\Sigma$.

The usual operations on unimodal frames and models can be defined on their bimodal counterparts as well. In particular, given two frames ${\mathfrak{F}}=(F,R_{\mathbf{h}}^{{\mathfrak{F}}},R_{\mathbf{v}}^{{\mathfrak{F}}})$ and ${\mathfrak{G}}=(G,R_{\mathbf{h}}^{{\mathfrak{G}}},R_{\mathbf{v}}^{{\mathfrak{G}}})$, a function $f:F\to G$ is called a p-morphism from ${\mathfrak{F}}$ to ${\mathfrak{G}}$ if it satisfies the following conditions, for all $u,v\in F$, $y\in G$, $i=\mathbf{h},\mathbf{v}$:

• •

uR_{i}^{{\mathfrak{F}}}v\ implies $f(u)R_{i}^{{\mathfrak{G}}}f(v)$ (that is, $f$ is a homomorphism),

• •

$f(u)R_{i}^{{\mathfrak{G}}}y$ implies that there is some $v\in F$ such that $f(v)=y$ and $uR_{i}^{{\mathfrak{F}}}v$ (the backward condition).

If $f$ is onto then we say that ${\mathfrak{G}}$ is a p-morphic image of ${\mathfrak{F}}$. Similarly to the unimodal case, validity of bimodal formulas in frames is preserved under taking p-morphic images. For any model ${\mathfrak{M}}$ on ${\mathfrak{F}}$ and model ${\mathfrak{N}}$ on ${\mathfrak{G}}$, a p-morphism from ${\mathfrak{F}}$ to ${\mathfrak{G}}$ is called a p-morphism from ${\mathfrak{M}}$ to ${\mathfrak{N}}$ whenever, for all propositional variables $p$ and points $x$ in ${\mathfrak{F}}$, $x\in{\mathfrak{M}}(p)$ iff $f(x)\in{\mathfrak{N}}(p)$. If $f$ is onto then we say that ${\mathfrak{N}}$ is a p-morphic image of ${\mathfrak{M}}$.

Given two frames ${\mathfrak{F}}=(F,R_{\mathbf{h}}^{{\mathfrak{F}}},R_{\mathbf{v}}^{{\mathfrak{F}}})$ and ${\mathfrak{G}}=(G,R_{\mathbf{h}}^{{\mathfrak{G}}},R_{\mathbf{v}}^{{\mathfrak{G}}})$, ${\mathfrak{F}}$ is a subframe of ${\mathfrak{G}}$ if $F\subseteq G$ and $R_{i}^{{\mathfrak{F}}}=R_{i}^{{\mathfrak{G}}}\cap(F\times F)$, for $i=\mathbf{h},\mathbf{v}$. Given some $x\in F$, the subframe ${\mathfrak{F}}^{x}$ of ${\mathfrak{F}}$ generated by point $x$ is the subframe of ${\mathfrak{F}}$ with the following set $F^{x}$ of points:

[TABLE]

We say that a frame ${\mathfrak{F}}$ is rooted if ${\mathfrak{F}}={\mathfrak{F}}^{r}$ for some point $r$. Such a point $r$ is called a root in ${\mathfrak{F}}$.

A set $L$ of bimodal formulas is called a (normal) bimodal logic (or logic, for short) if it contains all propositional tautologies and the formulas $\Box_{i}(p\to q)\to(\Box_{i}p\to\Box_{i}q)$, for $i=\mathbf{h},\mathbf{v}$, and is closed under the rules of Substitution, Modus Ponens and Necessitation $\varphi/\Box_{i}\varphi$, for $i=\mathbf{h},\mathbf{v}$. Given a class $\mathcal{C}$ of frames, we always obtain a logic by taking

[TABLE]

We say that ${\sf Logic\_of}\,\mathcal{C}$ is the logic of $\mathcal{C}$. It is well known that

[TABLE]

A logic $L$ is called Kripke complete if $L={\sf Logic\_of}\,\mathcal{C}$ for some class $\mathcal{C}$. Given a bimodal logic $L$ and a recursive set $\Sigma$ of bimodal formulas, we say that $\Sigma$ axiomatises $L$ if $L$ is the smallest bimodal logic containing $\Sigma$. A logic $L$ is called finitely axiomatisable whenever there is some finite $\Sigma$ axiomatising $L$.

3.2.1 Sahlqvist and generalised Sahlqvist formulas

Below we recall the definition of Sahlqvist formulas [37], and generalised (monadic) Sahlqvist formulas of Goranko and Vakarelov [16, Def.24] for our bimodal language.

A bimodal formula is positive (negative) if every occurrence of a propositional variable in it is under the scope of an even (odd) number of negations $\neg$. A boxed atom is a formula $\Box_{i_{1}}\dots\Box_{i_{n}}p$ where $n\in\mathbb{N}$, $i_{1},\dots,i_{n}\in\{\mathbf{h},\mathbf{v}\}$ and $p$ is a propositional variable. A Sahlqvist antecedent is a formula built up from $\top$, $\bot$, boxed atoms, and negative formulas, using $\lor$, $\land$, $\Diamond_{\mathbf{h}}$ and $\Diamond_{\mathbf{v}}$.

A boxed formula is a formula of the form

[TABLE]

where $n\in\mathbb{N}$, each $\Box^{i}$ is a finite (possibly empty) sequence of boxes $\Box_{\mathbf{h}}$ and $\Box_{\mathbf{v}}$, each $\psi_{i}$ is a positive formula, and $p$ is a propositional variable. The variable $p$ is called the head of the boxed formula, and all variables in any of the $\psi_{i}$ are called inessential variables. A potential generalised Sahlqvist antecedent is a formula $\phi$ built up from $\top$, $\bot$, boxed formulas, and negative formulas, using $\lor$, $\land$, $\Diamond_{\mathbf{h}}$ and $\Diamond_{\mathbf{v}}$. Given such a formula $\phi$, the dependency digraph of $\phi$ is a digraph $\mathcal{D}(\phi)=(N_{\phi},\Rrightarrow)$, where $N_{\phi}$ is the set of heads of the boxed formulas in $\phi$, and $q\Rrightarrow p$ iff $q$ is an inessential variable in a boxed formula with head $p$. If $\mathcal{D}(\phi)$ is acyclic, then $\phi$ is called a generalised Sahlqvist antecedent.

A (generalised) Sahlqvist implication is of the form $\phi\to\psi$, where $\phi$ is a (generalised) Sahlqvist antecedent and $\psi$ is a positive formula. A (generalised) Sahlqvist formula is a formula that is built up from (generalised) Sahlqvist implications by freely applying $\Box_{\mathbf{h}}$, $\Box_{\mathbf{v}}$ and $\land$, and by applying $\lor$ only between formulas that do not share any propositional variables.

The (generalised) Sahlqvist completeness theorem says that every logic axiomatised by (generalised) Sahlqvist formulas is canonical, and so Kripke complete. The (generalised) Sahlqvist correspondence theorem says that every (generalised) Sahlqvist formula has a first-order correspondent. (A first-order formula $A$ in the language having equality and binary predicate symbols $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ is called a correspondent of a bimodal formula $\phi$, whenever for every frame ${\mathfrak{F}}$, $A$ is valid in ${\mathfrak{F}}$ iff $\phi$ is valid in ${\mathfrak{F}}$.) Kracht [29] gives a syntactical description of first-order correspondents of Sahlqvist formulas. Kracht’s characterisation is extended to generalised Sahlqvist formulas by Kikot [27].

3.2.2 Some unimodal logics

The following well-known unimodal logics are mentioned in the paper:

[TABLE]

In order to avoid extensive use of $\times$, we denote the universal relation $W\times W$ on any non-empty set $W$ by $\forall_{W}$. By (1),

[TABLE]

Most of the paper is about two-dimensional modal product logics (see §3.2.3 below) where one or both component logics is the much-studied unimodal ‘logic of elsewhere’ $\mathbf{Diff}$ [6, 10, 11]. This logic was introduced by Von Wright [41] as the set of unimodal formulas that are valid in all difference frames, that is, in frames $(W,\neq_{W})$, where $\neq_{W}$ is the non-equality relation on some non-empty set $W$. Segerberg [39] axiomatised $\mathbf{Diff}$ by the Sahlqvist formulas

[TABLE]

So an arbitrary frame for $\mathbf{Diff}$ is a pseudo-equivalence relation, that is, it may contain both reflexive and irreflexive points, but it is always symmetric and pseudo-transitive:

[TABLE]

In particular, equivalence relations are frames for $\mathbf{Diff}$, and so $\mathbf{Diff}\subseteq\mathbf{S5}$. It is straightforward to see that every rooted frame $(W,R)$ for $\mathbf{Diff}$ is a p-morphic image of any difference frame $(U,\neq_{U})$ for which

[TABLE]

In particular,

[TABLE]

Note that one can express the universal, the at least two and the precisely one modalities with the help of a difference modality:

[TABLE]

3.2.3 Bimodal product frames and logics

Given unimodal frames ${\mathfrak{F}}_{\mathbf{h}}=(W_{\mathbf{h}},R_{\mathbf{h}})$ and ${\mathfrak{F}}_{\mathbf{v}}=(W_{\mathbf{v}},R_{\mathbf{v}})$, their (modal) product is defined to be the bimodal frame

[TABLE]

where $W_{\mathbf{h}}\!\times\!W_{\mathbf{v}}$ is the Cartesian product of $W_{\mathbf{h}}$ and $W_{\mathbf{v}}$ and, for all $x,x^{\prime}\in W_{\mathbf{h}}$, $y,y^{\prime}\in W_{\mathbf{v}}$,

[TABLE]

It is easy to see that both taking point-generated subframes and p-morphic images commute with the product construction:

[TABLE]

Given Kripke complete unimodal logics $L_{\mathbf{h}}$ and $L_{\mathbf{v}}$ in the respective unimodal languages having $\Diamond_{\mathbf{h}},\Box_{\mathbf{h}}$ and $\Diamond_{\mathbf{v}},\Box_{\mathbf{v}}$, their product is defined as the (Kripke complete) bimodal logic

[TABLE]

In particular, \mathbf{Diff}\!\times\!\mathbf{Diff}={\sf Logic\_of}\,\bigl{\{}{\mathfrak{F}}\!\times\!{\mathfrak{G}}:{\mathfrak{F}},{\mathfrak{G}}\mbox{ are frames for \mathbf{Diff}}\bigr{\}}. We call a frame of the form $(U,\neq_{U})\!\times\!(V,\neq_{V})$, for some non-empty sets $U,V$, a product of difference frames. Then, by (1), (6) and (7), we have that

[TABLE]

If $|U|=|V|>0$ then we call $(U,\neq_{U})\!\times\!(V,\neq_{V})$, a square product of difference frames. We define the ‘square’ version of $\mathbf{Diff}\!\times\!\mathbf{Diff}$ as

[TABLE]

Then by (8), we have

[TABLE]

As Theorem 2 shows, there is an infinite gap between these two logics. (Note that it is easy to reduce the validity problem of both $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ to that of two-variable first-order logic with counting, and so by the decidability of the latter [17], both $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ are decidable.)

It is easy to see that the classes of (isomorphic copies of) products of difference frames and of square products of difference frames are both closed under ultraproducts. Thus, by a general result of [13], both $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ are canonical logics. Note that while (isomorphic copies of) products of difference frames form a (finitely axiomatisable) elementary class by Corollary 7 below, it is not hard to show that the class of square products of difference frames is not closed under elementary equivalence, and so is not elementary (cf. [5, Thm. 4.1.12]).

Let $\mathsf{comm\_pse}$ be the conjunction of the Sahlqvist formulas $(\Box_{\mathbf{h}}\Box_{\mathbf{v}}p\leftrightarrow\Box_{\mathbf{v}}\Box_{\mathbf{h}}p)$ and (2)–(3) for both $\Box_{\mathbf{h}}$ and $\Box_{\mathbf{v}}$ (with the first-order correspondent saying that $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ are commuting pseudo-equivalence relations). Then the logic $[\mathbf{Diff},\mathbf{Diff}]$ axiomatised by $\mathsf{comm\_pse}$ is canonical, and so Kripke complete. It is straightforward to see that $\mathsf{comm\_pse}$ is valid in every product of difference frames, and so

[TABLE]

As Theorem 1 shows, there is an infinite gap between these two logics.

4 Rooted frames for $[\mathbf{Diff},\mathbf{Diff}]$

In this section, we have a closer look at rooted frames for $[\mathbf{Diff},\mathbf{Diff}]$, that is, rooted frames of the form ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$, where $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ are commuting pseudo-equivalence relations.

We begin with the simplest rooted frames of this kind. A frame $\mathfrak{C}=(C,R_{\mathbf{h}},R_{\mathbf{v}})$ is called a bi-cluster, if $\neq_{C}$ is a subset of $R_{j}$ for both $j=\mathbf{h},\mathbf{v}$. It is straightforward to see that a bi-cluster is a rooted frame for $[\mathbf{Diff},\mathbf{Diff}]$. For $j=\mathbf{h},\mathbf{v}$, a point $c$ in $\mathfrak{C}$ is called $R_{j}$-irreflexive ($R_{j}$-reflexive) if $c\neg R_{j}c$ ($cR_{j}c$) holds. So there can be four kinds of points in a bi-cluster: both $R_{\mathbf{h}}$- and $R_{\mathbf{v}}$-reflexive (denoted by ), $R_{\mathbf{h}}$-irreflexive and $R_{\mathbf{v}}$-reflexive ( ), $R_{\mathbf{h}}$-reflexive and $R_{\mathbf{v}}$-irreflexive ( ), and both $R_{\mathbf{h}}$- and $R_{\mathbf{v}}$-irreflexive ( ). We use   * to indicate when a point is $R_{\mathbf{h}}$-irreflexive and it does not matter whether it is $R_{\mathbf{v}}$-reflexive or $R_{\mathbf{v}}$-irreflexive. Similarly,   * will be used whenever a point is $R_{\mathbf{v}}$-irreflexive and it does not matter whether it is $R_{\mathbf{h}}$-reflexive or $R_{\mathbf{h}}$-irreflexive. (An example of a bi-cluster is depicted in Fig. 5.) In what follows we often identify a bi-cluster with its domain. In particular, for every bi-cluster $\mathfrak{C}=(C,R_{\mathbf{h}},R_{\mathbf{v}})$, we denote by $|\mathfrak{C}|$ the cardinality of its domain. We also let

[TABLE]

Next, let ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ be an arbitrary rooted frame for $[\mathbf{Diff},\mathbf{Diff}]$, and let $R_{\mathbf{h}}^{+}$ and $R_{\mathbf{v}}^{+}$ be the respective reflexive closures of $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$. It is easy to see that $R_{\mathbf{h}}^{+}$ and $R_{\mathbf{v}}^{+}$ are commuting equivalence relations. We define an equivalence relation $\sim$ on $W$ by taking, for all $u,v\in W$,

[TABLE]

For each $u\in W$, let $[u]$ denote its $\sim$-class, and let $W^{\sim}=\{[u]:u\in W\}$. We say (with a slight abuse of notation) that ${\mathfrak{F}}$ is (represented as) a grid of bi-clusters $(X,Y,g)$ whenever $g:X\!\times\!Y\to W^{\sim}$ is a bijection for some sets $X$, $Y$ such that the following hold for all $x\neq x^{\prime}\in X$ and $y\neq y^{\prime}\in Y$:

• (gc1)

$uR_{\mathbf{h}}v$ for all $u\in g(x,y)$ and $v\in g(x^{\prime},y)$;

• (gc2)

$uR_{\mathbf{v}}v$ for all $u\in g(x,y)$ and $v\in g(x,y^{\prime})$.

Observe that a single bi-cluster is a special case of a grid of bi-clusters when $|X|=|Y|=1$.

Given two grids of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ and ${\mathfrak{F}}^{\star}=(X^{\star},Y^{\star},g^{\star})$, we say that ${\mathfrak{F}}$ is a subgrid of ${\mathfrak{F}}^{\star}$ if $X\subseteq X^{\star}$, $Y\subseteq Y^{\star}$, and $g=g^{\star}|_{X\!\times\!Y}$. For each $(x,y)\in X\!\times\!Y$, we will denote by ${\mathfrak{F}}^{xy}$ the subgrid of \bigl{(}\{x\},\{y\},g|_{\{x\}\!\times\!\{y\}}\bigr{)} of ${\mathfrak{F}}$. Observe that ${\mathfrak{F}}^{xy}$ is always a bi-cluster. For any bi-cluster $\mathfrak{C}$, we say that ${\mathfrak{F}}$ contains $\mathfrak{C}$, if $\mathfrak{C}$ is isomorphic to ${\mathfrak{F}}^{xy}$ for some $x,y$.

Throughout, we draw grids of bi-clusters by depicting each bi-cluster as a rectangular box, depicting $X$ (and $R_{\mathbf{h}}$ between bi-clusters) horizontally and $Y$ (and $R_{\mathbf{v}}$ between bi-clusters) vertically; see, for example, Figs. 3 and 4.

Lemma** 6****.**

Every rooted frame ${\mathfrak{F}}$ for $[\mathbf{Diff},\mathbf{Diff}]$ is a grid of bi-clusters.

Proof.

Suppose ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is a rooted frame ${\mathfrak{F}}$ for $[\mathbf{Diff},\mathbf{Diff}]$, that is, $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ are commuting pseudo-equivalence relations. Take any $r\in W$. As $R_{\mathbf{h}}^{+}$ and $R_{\mathbf{v}}^{+}$ are commuting equivalence relations, it is easy to see that $r$ is a root in ${\mathfrak{F}}$, and for all $v,w\in W$, if $rR_{\mathbf{h}}^{+}v$ and $rR_{\mathbf{v}}^{+}w$ then there is $u$ with $vR_{\mathbf{v}}^{+}u$ and $wR_{\mathbf{h}}^{+}u$. So we let

[TABLE]

and define a function $g:X\times Y\to W^{\sim}$ by taking, for all $[v]\in X$, $[w]\in Y$,

[TABLE]

As both $R_{\mathbf{h}}^{+}$ and $R_{\mathbf{v}}^{+}$ are equivalence relations, for all $v$, $w$, $u$, $v^{\prime}$, $w^{\prime}$, $u^{\prime}$, if $v\sim v^{\prime}$, $w\sim w^{\prime}$, $vR_{\mathbf{v}}^{+}u$, $wR_{\mathbf{h}}^{+}u$, $v^{\prime}R_{\mathbf{v}}^{+}u^{\prime}$ and $w^{\prime}R_{\mathbf{h}}^{+}u^{\prime}$ then $u\sim u^{\prime}$ follows, and so $g$ is well-defined. It is easy to see that $g$ is injective and both (gc1) and (gc2) hold. Finally, we show that $g$ is surjective: Take some $[u]\in W^{\sim}$. Then there exist $n\in\mathbb{N}$ and $u_{0},\dots,u_{n}$ such that $u_{0}=r$, $u_{n}=u$ and for each $i<n$, either $u_{i}R_{\mathbf{h}}^{+}u_{i+1}$ or $u_{i}R_{\mathbf{v}}^{+}u_{i+1}$. As $R_{\mathbf{h}}^{+}$ and $R_{\mathbf{v}}^{+}$ are commuting equivalence relations, it follows that there are $v,w$ such that $rR_{\mathbf{h}}^{+}vR_{\mathbf{v}}^{+}u$ and $rR_{\mathbf{v}}^{+}wR_{\mathbf{h}}^{+}u$, and so $[v]\in X$, $[w]\in Y$ and g\bigl{(}[v],[w]\bigr{)}=[u], as required. ∎

Corollary 7**.**

For every frame ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$, ${\mathfrak{F}}$ is isomorphic to a product of difference frames iff $R_{\mathbf{h}}$ and $R_{\mathbf{v}}$ are commuting irreflexive pseudo-equivalence relations and all bi-clusters in ${\mathfrak{F}}$ are singletons.

Because of the proof-pattern described in §2.2, we are particularly interested in those countable grids of bi-clusters that are p-morphic images of some product of difference frames. The following lemma provides a general characterisation for them.

Lemma** 8****.**

A countable grid of bi-clusters ${\mathfrak{F}}$ is a p-morphic image of a product of two difference frames iff ${\mathfrak{F}}$ is such that

• •

each of its bi-clusters is the p-morphic image of a product of two difference frames, and

• •

the sizes of the product preimages for each bi-cluster ‘fit’.

More precisely, for any countable grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$, we have the following:

• (i)

If $h:(U,\neq_{U})\!\times\!(V,\neq_{V})\to{\mathfrak{F}}$ is an onto p-morphism, then there exists a function \xi_{h}:(X\cup Y)\to\bigl{(}\mathbb{N}^{+}\cup\{\aleph_{0}\}\bigr{)} such that for every $(x,y)\in X\times Y$, the bi-cluster ${\mathfrak{F}}^{xy}$ in ${\mathfrak{F}}$ is a p-morphic image of $(U_{x},\neq_{U_{x}})\!\times\!(V_{y},\neq_{V_{y}})$ for some sets $U_{x},V_{y}$ with $|U_{x}|=\xi_{h}(x)$ and $|V_{y}|=\xi_{h}(y)$.

• (ii)

If \xi:(X\cup Y)\to\bigl{(}\mathbb{N}^{+}\cup\{\aleph_{0}\}\bigr{)} is a function such that for every $(x,y)\in X\times Y$, the bi-cluster ${\mathfrak{F}}^{xy}$ in ${\mathfrak{F}}$ is a p-morphic image of $(U_{xy},\neq_{U_{xy}})\!\times\!(V_{xy},\neq_{V_{xy}})$ for some sets $U_{xy},V_{xy}$ with $|U_{xy}|=\xi(x)$ and $|V_{xy}|=\xi(y)$, then there is an onto p-morphism $h_{\xi}:(U,\neq_{U})\!\times\!(V,\neq_{V})\to{\mathfrak{F}}$ for some sets $U,V$ with $|U|=\sum_{x\in X}\xi(x)$ and $|V|=\sum_{y\in Y}\xi(y)$.

Proof.

(i): We let

[TABLE]

Then it is straightforward to see that, for every $(x,y)\in X\times Y$, the restriction of $h$ to $U_{x}\times V_{y}$ is a p-morphism onto ${\mathfrak{F}}^{xy}$. So we can define $\xi_{h}$ by taking $\xi_{h}(x)=|U_{x}|$, for $x\in X$, and $\xi_{h}(y)=|V_{y}|$, for $y\in Y$, as required.

(ii): For every $(x,y)\in X\times Y$, suppose that $h^{xy}:(U_{xy},\neq_{U_{xy}})\!\times\!(V_{xy},\neq_{V_{xy}})\to{\mathfrak{F}}^{xy}$ is an onto p-morphism. As for every $x\in X$, we have $|U_{xy}|=\xi(x)=|U_{xy^{\prime}}|$ for any $y,y^{\prime}\in Y$, we may assume that $U_{xy}$ and $U_{xy^{\prime}}$ are the same set $U_{x}$. Similarly, for every $y\in Y$, we may assume that $V_{xy}$ and $V_{x^{\prime}y}$ are the same set $V_{y}$. We may also assume that all these sets are disjoint. Now let $U=\bigcup_{x\in X}U_{x}$, $V=\bigcup_{y\in Y}V_{y}$, and let the function $h_{\xi}:U\times V\to{\mathfrak{F}}$ be defined by taking $h_{\xi}(u,v)=h^{xy}(u,v)$ whenever $u\in U_{x}$ and $v\in V_{y}$. Then it is straightforward to check that $h_{\xi}$ is a p-morphism from $(U,\neq_{U})\!\times\!(V,\neq_{V})$ onto ${\mathfrak{F}}$. ∎

4.1 ‘Good’ and ‘bad’ bi-clusters

By Lemma 8, if a grid of bi-clusters is not the p-morphic image of a product of difference frames, then it is because its bi-clusters are not p-morphic images of ‘fitting’ product preimages. In this subsection, we have a closer look at individual bi-clusters first: which of them can or cannot be obtained as the p-morphic image of some product of difference frames, and what size-restrictions we have on possible product preimages. We distinguish fifteen types of finite bi-clusters, depending on whether they contain $R_{i}$-reflexive points or not, for $i=\mathbf{h},\mathbf{v}$ (see Table 1). In particular, finite bi-clusters of types (no1)–(no4) will be called impossible bi-clusters throughout. Lemma 9 below claims that every countable bi-cluster that is not impossible can be obtained as the p-morphic image of any product of difference frames validating some constraints. (In §6.2 we will show that the converse of Lemma 9 also holds in the sense that whenever a countable bi-cluster $\mathfrak{C}$ is a p-morphic image of a product of difference frames, then $\mathfrak{C}$ is not impossible, and the described constraints hold for the preimage product frame, see Corollary 22.)

Lemma** 9****.**

• (i)

Every countably infinite bi-cluster $\mathfrak{C}$ is a p-morphic image of $(\omega,\neq_{\omega})\!\times\!(\omega,\neq_{\omega})$.

• (ii)

For every finite bi-cluster $\mathfrak{C}$, if $\mathfrak{C}$ is not an impossible bi-cluster, then $\mathfrak{C}$ is the p-morphic image of $(U,\neq_{U})\!\times\!(V,\neq_{V})$ for any countable sets $U$, $V$ such that the constraints of Table 1 hold for $x=|U|$ and $y=|V|$.

Proof.

We begin with a useful tool. Given a bi-cluster $\mathfrak{C}=(C,R_{\mathbf{h}},R_{\mathbf{v}})$, we define an $\mathfrak{C}$-network to be a homomorphism $f:(U,\neq_{U})\!\times\!(V,\neq_{V})\to\mathfrak{C}$, for some finite non-empty sets $U$ and $V$. Given $\mathfrak{C}$-networks $f_{1}:(U_{1},\neq_{U_{1}})\!\times\!(V_{1},\neq_{V_{1}})\to\mathfrak{C}$ and $f_{2}:(U_{2},\neq_{U_{2}})\!\times\!(V_{2},\neq_{V_{2}})\to\mathfrak{C}$, we write $f_{1}\subseteq f_{2}$ whenever $U_{1}\subseteq U_{2}$, $V_{1}\subseteq V_{2}$ and $f_{2}|_{U_{1}\!\times\!V_{1}}=f_{1}$. We define a game $\mathbb{G}(\mathfrak{C})$ between two players, $\forall$ and $\exists$. They build a countable sequence of $\mathfrak{C}$-networks $f_{0}\subseteq f_{1}\subseteq\dots\subseteq f_{k}\subseteq\dots.$ In round 0, $\forall$ picks any point $r$ in $\mathfrak{C}$, and $\exists$ responds with $U_{0}=\{u_{0}\}$, $V_{0}=\{v_{0}\}$, and $f_{0}(u_{0},v_{0})=r$. In round $k$ ($k\in\mathbb{N}^{+}$), some sequence $f_{0}\subseteq\dots\subseteq f_{k-1}$ of $\mathfrak{C}$-networks has already been built. $\forall$ picks a pair $(c^{\ast},z)$ where $c^{\ast}\in C$ and $z\in U_{k-1}\cup V_{k-1}$. There are two cases:

• •

$z\in V_{k-1}$. Then $\exists$ can respond in two ways: If either $c^{\ast}$ is $R_{\mathbf{h}}$-irreflexive and there is $u\in U_{k-1}$ with $f_{k-1}(u,z)=c^{\ast}$, or $c^{\ast}$ is $R_{\mathbf{h}}$-reflexive and there are $u,u^{\prime}\in U_{k-1}$, $u\neq u^{\prime}$ with $f_{k-1}(u,z)=f_{k-1}(u^{\prime},z)=c^{\ast}$, then she responds with $f_{k}=f_{k-1}$. Otherwise, she responds (if she can) with some $\mathfrak{C}$-network $f_{k}\supseteq f_{k-1}$ such that $V_{k}=V_{k-1}$, $U_{k}=U_{k-1}\cup\{u^{+}\}$ for some fresh point $u^{+}$, and $f_{k}(u^{+},z)=c^{\ast}$. In other words, she needs to find a sequence \bigl{(}c_{v}:v\in V_{k-1}-\{z\}\bigr{)} of points in $\mathfrak{C}$ such that, for every $v\in V_{k-1}-\{z\}$,

• –

$c_{v}R_{\mathbf{h}}f_{k-1}(u,v)$ for every $u\in U_{k-1}$,

• –

$c_{v}R_{\mathbf{v}}c^{\ast}$, and $c_{v}R_{\mathbf{v}}c_{v^{\prime}}$ for every $v^{\prime}\in V_{k-1}-\{z\}$, $v^{\prime}\neq v$.

• •

$z\in U_{k-1}$. Then again, $\exists$ can respond in two ways: If either $c^{\ast}$ is $R_{\mathbf{v}}$-irreflexive and there is $v\in V_{k-1}$ with $f_{k-1}(z,v)=c^{\ast}$, or $c^{\ast}$ is $R_{\mathbf{v}}$-reflexive and there are $v,v^{\prime}\in V_{k-1}$, $v\neq v^{\prime}$ with $f_{k-1}(z,v)=f_{k-1}(z,v^{\prime})=c^{\ast}$, then she responds with $f_{k}=f_{k-1}$. Otherwise, she responds (if she can) with some $\mathfrak{C}$-network $f_{k}\supseteq f_{k-1}$ such that $U_{k}=U_{k-1}$, $V_{k}=V_{k-1}\cup\{v^{+}\}$ for some fresh point $v^{+}$, and $f_{k}(z,v^{+})=c^{\ast}$. In other words, she needs to find a sequence \bigl{(}c_{u}:u\in U_{k-1}-\{z\}\bigr{)} of points in $\mathfrak{C}$ such that, for every $u\in U_{k-1}-\{z\}$,

• –

$c_{u}R_{\mathbf{v}}f_{k-1}(u,v)$ for every $v\in V_{k-1}$,

• –

$c_{u}R_{\mathbf{h}}c^{\ast}$, and $c_{u}R_{\mathbf{h}}c_{u^{\prime}}$ for every $u^{\prime}\in U_{k-1}-\{z\}$, $u^{\prime}\neq u$.

If $\exists$ can respond in each round $k$ for $k\in\mathbb{N}$ then she wins the play. We say that $\exists$ has a winning strategy in $\mathbb{G}(\mathfrak{C})$ if she can win all plays, whatever moves $\forall$ takes in the rounds.

Claim** 9.1****.**

For every countable bi-cluster $\mathfrak{C}$, player $\exists$ has a winning strategy in $\mathbb{G}(\mathfrak{C})$ iff $\mathfrak{C}$ is the p-morphic image of a product of two countable difference frames.

Proof.

On the one hand, it is easy to see that $\exists$ can use a p-morphism from a product of two difference frames onto $\mathfrak{C}$ to determine her winning strategy in $\mathbb{G}(\mathfrak{C})$.

For the other direction, consider a play of the game $\mathbb{G}(\mathfrak{C})$ with the following property: For all $k\in\mathbb{N}$, $(u,v)\in U_{k}\!\times\!V_{k}$, $c^{\ast}\in C$, there exist $\ell_{\mathbf{h}},\ell_{\mathbf{v}}\in\mathbb{N}$ such that $\ell_{\mathbf{h}},\ell_{\mathbf{v}}>k$, $\forall$ picks $(c^{\ast},u)$ in round $\ell_{\mathbf{h}}$, and $\forall$ picks $(c^{\ast},v)$ in round $\ell_{\mathbf{v}}$ (since $\mathfrak{C}$ is countable, he can do these). If $\exists$ uses her strategy, then the union $f:(U,\neq_{U})\!\times\!(V,\neq_{V})\to\mathfrak{C}$ of the constructed countable ascending chain of $\mathfrak{C}$-networks is a p-morphism. Indeed, take some $u^{\ast}\in U$, $v^{\ast}\in V$, $c^{\ast}\in C$ such that, say, $f(u^{\ast},v^{\ast})R_{\mathbf{h}}c^{\ast}$. We need to find some $u\in U$ such that $u\neq u^{\ast}$ and $f(u,v^{\ast})=c^{\ast}$. Let $k$ be such that $(u^{\ast},v^{\ast})\in U_{k}\!\times\!V_{k}$ and consider round $\ell>k$ when $\forall$ picks $(c^{\ast},v^{\ast})$. There are three cases: If $c^{\ast}$ is $R_{\mathbf{h}}$-irreflexive and there is $u\in U_{\ell-1}$ with $f_{\ell-1}(u,v^{\ast})=c^{\ast}$, then $f(u,v^{\ast})\neq f(u^{\ast},v^{\ast})$, and so $u\neq u^{\ast}$. If $c^{\ast}$ is $R_{\mathbf{h}}$-reflexive and there are $u,u^{\prime}\in U_{\ell-1}$ with $u\neq u^{\prime}$ and $f_{\ell-1}(u,v^{\ast})=f_{\ell-1}(u^{\prime},v^{\ast})=c^{\ast}$, then either $u\neq u^{\ast}$ or $u^{\prime}\neq u^{\ast}$. Otherwise, there is $u^{+}\in U_{\ell}-U_{\ell-1}$ with $f(u^{+},v^{\ast})=c^{\ast}$. As $u^{\ast}\in U_{\ell-1}$, it follows that $u^{+}\neq u^{\ast}$. ∎

Now we can complete the proof of Lemma 9.

Item (i): Consider the game $\mathbb{G}(\mathfrak{C})$. As $\mathfrak{C}$ is infinite and the constructed networks in each round of a play in the game have finite domains, $\exists$ can always respond according to the rules, and so she has a winning strategy in $\mathbb{G}(\mathfrak{C})$. So by Claim 9.1, $\mathfrak{C}$ is the p-morphic image of a product of two countable difference frames. As $\mathfrak{C}$ contains infinitely many points that are $R_{j}$-connected, for both $j=\mathbf{h}$ and $j=\mathbf{v}$, both components in the product preimage must be infinite.

Item (ii): Suppose first that $\mathfrak{C}$ is a finite infinity bi-cluster. Then $\mathfrak{C}$ contains at least one    point $a$. So in every round of a play in the game $\mathbb{G}(\mathfrak{C})$, $\exists$ can always use a full $a$-sequence as the sequence of points needed in her response, giving her a winning strategy in $\mathbb{G}(\mathfrak{C})$. So by Claim 9.1, there exists an onto p-morphism $f:(U,\neq_{U})\!\times\!(V,\neq_{V})\to\mathfrak{C}$, for some countable sets $U$ and $V$. We claim that

[TABLE]

Indeed, for (11), let $a$ be a    point in $\mathfrak{C}$. Then for every $v\in V$, there exist $u_{v},u_{v}^{\prime}\in U$, $u_{v}\neq u_{v}^{\prime}$ such that $f(u_{v},v)=f(u_{v}^{\prime},v)=a$. Also, if $v_{1}\neq v_{2}$ then $u_{v_{1}}$, $u_{v_{1}}^{\prime}$, $u_{v_{2}}$, $u_{v_{2}}^{\prime}$ must be four distint points, and so (11) follows. The proof of (12) is similar. For (13), let $b$ be a    point in $\mathfrak{C}$. Then for every $v\in V$, there exist $u_{v}\in U$ such that $f(u_{v},v)=b$. Also, if $v_{1}\neq v_{2}$ then $u_{v_{1}}\neq u_{v_{2}}$ must hold, and so $|U|\geq|V|$ follows. We can show $|V|\geq|U|$ similarly, and so we obtain (13). Now if $\mathfrak{C}$ is an infinity bi-cluster, then the infinity of both $U$ and $V$ follows from (11)–(13).

Suppose that $\mathfrak{C}$ is an $n$-element (hvstrict) bi-cluster, and take any $n$-element sets $U$ and $V$. Let $f:U\!\times\!V\to\mathfrak{C}$ be any function such that the $n\!\times\!n$-matrix \bigl{(}f(u,v)\bigr{)}_{(u,v)\in U\!\times\!V} is a Latin square over the elements of $\mathfrak{C}$ (that is, each element of $\mathfrak{C}$ occurs exactly once in each row and exactly once in each column). It is straightforward to check that such an $f$ is a p-morphism from $(U,\neq_{U})\!\times\!(V,\neq_{V})$ onto $\mathfrak{C}$.

Suppose that $\mathfrak{C}$ is an $n$-element (hstrict) bi-cluster, and take any $n$-element sets $U$ and $V^{-}$. Let $f:U\!\times\!V^{-}\to\mathfrak{C}$ be any function such that the $n\!\times\!n$-matrix \bigl{(}f(u,v)\bigr{)}_{(u,v)\in U\!\times\!V^{-}} is a Latin square over the elements of $\mathfrak{C}$. It is straightforward to check that such an $f$ is a p-morphism from $(U,\neq_{U})\!\times\!(V^{-},\forall_{V^{-}})$ onto $\mathfrak{C}$. Now take any set $V$ with $|V|\geq 2n$. By (5) and (7), we obtain that $\mathfrak{C}$ is the p-morphic image of $(U,\neq_{U})\!\times\!(V,\neq_{V})$. The proof for (vstrict) bi-clusters is similar.

The following claim will also be used in §5:

Claim** 9.2****.**

If $\mathfrak{C}$ is a (h2vsw) bi-cluster containing $n$    points and $m$    points, then for all sets $U^{\prime}$, $V$ with $|U^{\prime}|=|V|\geq n+2m$ there exists a p-morphism from $(U^{\prime},\forall_{U^{\prime}})\!\times\!(V,\neq_{V})$ onto $\mathfrak{C}$.

Proof.

Take any sets $U^{\prime}$, $V$ such that $|U^{\prime}|=|V|=N$ for some $N\geq n+2m$. Let $S$ be an $N$-element set that contains all the    points of $\mathfrak{C}$, and at least two distinct ‘copies’ of each    point in $\mathfrak{C}$. Then let $f:U^{\prime}\!\times\!V\to\mathfrak{C}$ be any function such that the $N\!\times\!N$-matrix \bigl{(}f(u,v)\bigr{)}_{(u,v)\in U^{\prime}\!\times\!V} is a Latin square over the elements of $S$. It is straightforward to check that such an $f$ is a p-morphism from $(U^{\prime},\forall_{U^{\prime}})\!\times\!(V,\neq_{V})$ onto $\mathfrak{C}$. ∎

Now suppose that $\mathfrak{C}$ is a (h2vsw) bi-cluster containing $n$    points and $m$    points, and take any sets $U,V$ with $|U|\geq 2\cdot|V|$ and $V\geq n+2m$. By (5), (7), and Claim 9.2, we obtain that $\mathfrak{C}$ is the p-morphic image of $(U,\neq_{U})\!\times\!(V,\neq_{V})$. The proof for (v2hsw) bi-clusters is similar.

Suppose that $\mathfrak{C}$ is a ($=$sw) bi-cluster containing $n$    points and $m$    points, and take any sets $U$, $V$ such that $|U|=|V|=N$ for some $N\geq n+2m$. Let $S$ be an $N$-element set that contains all the    points of $\mathfrak{C}$, and at least two distinct ‘copies’ of each    point in $\mathfrak{C}$. Then let $f:U\!\times\!V\to\mathfrak{C}$ be any function such that the $N\!\times\!N$-matrix \bigl{(}f(u,v)\bigr{)}_{(u,v)\in U\!\times\!V} is a Latin square over the elements of $S$. It is straightforward to check that such an $f$ is a p-morphism from $(U,\neq_{U})\!\times\!(V,\neq_{V})$ onto $\mathfrak{C}$.

Finally, suppose that $\mathfrak{C}$ is an $n$-element (free) bi-cluster, and take any $n$-element sets $U^{-}$ and $V^{-}$. Let $f:U^{-}\!\times\!V^{-}\to\mathfrak{C}$ be any function such that the $n\!\times\!n$-matrix \bigl{(}f(u,v)\bigr{)}_{(u,v)\in U^{-}\!\times\!V^{-}} is a Latin square over the elements of $\mathfrak{C}$. It is straightforward to check that such an $f$ is a p-morphism from $(U^{-},\forall_{U^{-}})\!\times\!(V^{-},\forall_{V^{-}})$ onto $\mathfrak{C}$. Now take any sets $U$, $V$ with $|U|\geq 2n$ and $|U|\geq 2n$. By (5) and (7), we obtain that $\mathfrak{C}$ is the p-morphic image of $(U,\neq_{U})\!\times\!(V,\neq_{V})$. ∎

5 Non-finite axiomatisability

In this section we prove Theorems 1 and 2, using the proof pattern described in §2.1. We will also use a result of [31, Cor. 2.5], saying that if $\mathcal{C}$ is closed under ultraproducts and point-generated subframes, then

[TABLE]

In order to prove Theorem 1, we show the following more general statement, which also generalises some results of [30]:

Theorem 10**.**

Let $L$ be any bimodal logic such that

• •

$L$* contains $\mathbf{K}\!\times\!\mathbf{Diff}$, and*

• •

for every $k\in\mathbb{N}^{+}$ there are $U$, $V$, such that $|V|\geq k$, $|U|\geq 2\cdot|V|$ and $(U,\forall_{U})\!\times\!(V,\neq_{V})$ is a frame for $L$.

Then $L$ is not axiomatisable using finitely many propositional variables.

Proof.

For every $k\in\mathbb{N}^{+}$, $k\geq 2$, take the grids of bi-clusters ${\mathfrak{F}}_{k}$ and ${\mathfrak{G}}_{k}$ depicted in Fig. 1.

Lemma** 10.1****.**

• (i)

${\mathfrak{F}}_{k}$* is not a frame for $\mathbf{K}\!\times\!\mathbf{Diff}$.*

• (ii)

${\mathfrak{G}}_{k}$* is a p-morphic image of $(U,\forall_{U})\!\times\!(V,\neq_{V})$, whenever $|V|\geq k$ and $|U|\geq 2\cdot|V|$.*

• (iii)

If $k,m\in\mathbb{N}$ and $k\geq 2^{m+1}$, then for every $m$-generated model ${\mathfrak{M}}$ over ${\mathfrak{F}}_{k}$ there is some model ${\mathfrak{N}}$ over ${\mathfrak{G}}_{k}$ that is a p-morphic image of ${\mathfrak{M}}$.

Proof.

(i): By definition, $\mathbf{K}\!\times\!\mathbf{Diff}={\sf Logic\_of}\,\mathcal{C}$, where

[TABLE]

Using (6) and the fact that the ultraproduct construction also commutes with the modal product construction, it is not hard to see that $\mathcal{C}$ is closed under point-generated subframes and ultraproducts. Therefore, by (14), it is enough to show that ${\mathfrak{F}}_{k}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is not the p-morphic image of any $(W_{\mathbf{h}},Q_{\mathbf{h}})\!\times\!(W_{\mathbf{v}},Q_{\mathbf{v}})$, where $Q_{\mathbf{v}}$ is a pseudo-equivalence relation. Suppose to the contrary that there is an onto p-morphism $f:(W_{\mathbf{h}},Q_{\mathbf{h}})\!\times\!(W_{\mathbf{v}},Q_{\mathbf{v}})\to{\mathfrak{F}}_{k}$. Take any point $a$ in the $k$-element bi-cluster $\mathfrak{C}_{1}(k)$, and any point $b$ in the $k+1$-element bi-cluster $\mathfrak{C}_{2}(k)$. As $aR_{\mathbf{h}}b$, there are $x_{0},x_{1}\in W_{\mathbf{h}}$, $y_{0}\in W_{\mathbf{v}}$ such that $x_{0}Q_{\mathbf{h}}x_{1}$, $f(x_{0},y_{0})=a$ and $f(x_{1},y_{0})=b$. As there are $k$ other points in $\mathfrak{C}_{2}(k)$, each of them is $R_{\mathbf{v}}$-related to $b$, there exist $y_{1},\dots,y_{k}\in W_{\mathbf{v}}$ such that $y_{0}Q_{\mathbf{v}}y_{i}$ for all $0<i\leq k$ and $y_{i}\neq y_{j}$ for all $i\neq j\leq k$. As $Q_{\mathbf{v}}$ is a pseudo-equivalence relation, it follows that $y_{i}Q_{\mathbf{v}}y_{j}$ for all $i\neq j\leq k$. Then $f(x_{0},y_{i})R_{\mathbf{v}}f(x_{0},y_{j})$ must hold, for all $i\neq j\leq k$. As every point in $\mathfrak{C}_{1}(k)$ is $R_{\mathbf{v}}$-irreflexive, this is not possible by the pigeonhole principle.

(ii): Take any sets $U$, $V$, with $|V|\geq k$ and $|U|\geq 2\cdot|V|$, and choose two disjoint subsets $U_{1}$ and $U_{2}$ of $U$ such that $|U_{1}|=|U_{2}|=|V|$. Observe that each of the two bi-clusters $\mathfrak{C}^{\prime}_{i}(k)$ in ${\mathfrak{G}}_{k}$ is a (h2vsw) bi-cluster, containing $k-2$    points and one    point (cf. Fig. 1 and Table 1). So by Claim 9.2, there exist onto p-morphisms $h_{i}:(U_{i},\forall_{U_{i}})\!\times\!(V,\neq_{V})\to\mathfrak{C}^{\prime}_{i}(k)$, for $i=1,2$. Let $U^{\prime}=U_{1}\cup U_{2}$, and define a function $h$ from $U^{\prime}\!\times\!V$ to ${\mathfrak{G}}_{k}$ by taking, for all $u\in U^{\prime}$, $v\in V$,

[TABLE]

Then it is easy to check that $h$ is a p-morphism from $(U^{\prime},\forall_{U^{\prime}})\!\times\!(V,\neq_{V})$ onto ${\mathfrak{G}}_{k}$. As $(U^{\prime},\forall_{U^{\prime}})$ is a p-morphic image of $(U,\forall_{U})$, it follows from (7) that ${\mathfrak{G}}_{k}$ is a p-morphic image of $(U,\forall_{U})\!\times\!(V,\neq_{V})$.

(iii): Let ${\mathfrak{M}}$ be a model over ${\mathfrak{F}}_{k}$ such that if ${\mathfrak{M}}(p)\neq\emptyset$ for some propositional variable $p$ then $p=p_{i}$ for some $i<m$. We define two equivalence relations $\sim_{1}$ and $\sim_{2}$ on $\mathfrak{C}_{1}(k)$ and on $\mathfrak{C}_{2}(k)$, respectively, by taking, for all $a,a^{\prime}$ in $\mathfrak{C}_{1}(k)$ and $b,b^{\prime}$ in $\mathfrak{C}_{2}(k)$,

[TABLE]

As $k\geq 2^{m+1}$, by the generalised pigeonhole principle, there is a $\sim_{1}$-class containing at least two points $a,a^{\prime}$, and there is a $\sim_{2}$-class containing at least three points $b,b^{\prime},b^{\prime\prime}$. Now define a function $h$ from ${\mathfrak{F}}_{k}$ onto ${\mathfrak{G}}_{k}$ by

• •

mapping $a$ and $a^{\prime}$ to the    point in $\mathfrak{C}^{\prime}_{1}(k)$,

• •

mapping the remaining $k-2$ points in $\mathfrak{C}_{1}(k)$ to the $k-2$ distinct    points in $\mathfrak{C}^{\prime}_{1}(k)$,

• •

mapping $b,b^{\prime}$ and $b^{\prime\prime}$ to the    point in $\mathfrak{C}^{\prime}_{2}(k)$,

• •

mapping the remaining $k-2$ points in $\mathfrak{C}_{2}(k)$ to the $k-2$ distinct    points in $\mathfrak{C}^{\prime}_{2}(k)$.

It is easy to check that $h$ is a p-morphism from ${\mathfrak{F}}_{k}$ onto ${\mathfrak{G}}_{k}$. Now define a model ${\mathfrak{N}}$ over ${\mathfrak{G}}_{k}$ by taking, for any propositional variable $p$, {\mathfrak{N}}(p)=\{c:h(a)=c\mbox{ for some a\in{\mathfrak{M}}(p)}\}. By the above, $h$ is a p-morphism from ${\mathfrak{M}}$ onto ${\mathfrak{N}}$. ∎

Now the proof of Theorem 10 can be completed as follows. Suppose to the contrary that $\Sigma$ axiomatises $L$ and $\Sigma$ contains only $m$ propositional variables, for some $m\in\mathbb{N}$. Let $k\geq 2^{m+1}$ and let ${\mathfrak{M}}$ be an arbitrary model over ${\mathfrak{F}}_{k}$. Let ${\mathfrak{M}}_{m}$ be another model over ${\mathfrak{F}}_{k}$ that is the same as ${\mathfrak{M}}$ on propositional variables occurring in $\Sigma$, and $\emptyset$ otherwise. Then ${\mathfrak{M}}_{m}$ is clearly $m$-generated and ${\mathfrak{M}}_{m}\models\Sigma$ iff ${\mathfrak{M}}\models\Sigma$. Also, by Lemma 10.1 (iii) there is a model ${\mathfrak{N}}$ over ${\mathfrak{G}}_{k}$ that is a p-morphic image of ${\mathfrak{M}}_{m}$. As there are $U$, $V$, such that $|V|\geq k$, $|U|\geq 4\cdot|V|$ and $(U,\forall_{U})\!\times\!(V,\neq_{V})$ is a frame for $L$, by Lemma 10.1 (ii) ${\mathfrak{G}}_{k}$ is a frame for $L$. Thus, ${\mathfrak{N}}\models L$, and so ${\mathfrak{M}}_{m}\models L$. As $\Sigma\subseteq L$, we obtain ${\mathfrak{M}}_{m}\models\Sigma$, and so ${\mathfrak{M}}\models\Sigma$. As this holds for any model ${\mathfrak{M}}$ over ${\mathfrak{F}}_{k}$, ${\mathfrak{F}}_{k}$ is a frame for $\Sigma$. Therefore, ${\sf Logic\_of}\,\{{\mathfrak{F}}_{k}\}$ is a bimodal logic containing $\Sigma$, and so we have that ${\mathfrak{F}}_{k}$ is a frame for $L$. As $L$ contains $\mathbf{K}\!\times\!\mathbf{Diff}$, this implies that ${\mathfrak{F}}_{k}$ is a frame for $\mathbf{K}\!\times\!\mathbf{Diff}$, contradicting Lemma 10.1 (i). ∎

Proof of Theorem 2

For every $k\in\mathbb{N}^{+}$, take the grids of bi-clusters ${\mathfrak{G}}_{k}$ and ${\mathfrak{H}}_{k}$ from Figs. 1 and 2, respectively.

Lemma** 10.2****.**

• (i)

${\mathfrak{H}}_{k}$* is not a frame for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$.*

• (ii)

${\mathfrak{G}}_{k}$* is a p-morphic image of $(\omega,\neq_{\omega})\!\times\!(\omega,\neq_{\omega})$.*

• (iii)

If $k,m\in\mathbb{N}$ and $k>2^{m}$, then for every $m$-generated model ${\mathfrak{M}}$ over ${\mathfrak{H}}_{k}$ there is some model ${\mathfrak{N}}$ over ${\mathfrak{G}}_{k}$ that is a p-morphic image of ${\mathfrak{M}}$.

Proof.

(i): By definition, $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}={\sf Logic\_of}\,\{$square products of difference frames$\}$. Using (6) and the fact that the ultraproduct construction also commutes with the modal product construction, it is not hard to see that the class of all square products of difference frames is closed under point-generated subframes and ultraproducts. Therefore, by (14), it is enough to show that ${\mathfrak{H}}_{k}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is not the p-morphic image of a square product $(U,\neq_{U})\!\times\!(V,\neq_{V})$ for any sets $U,V$ with $|U|=|V|>0$. Suppose indirectly that it is. As every point in ${\mathfrak{H}}_{k}$ is $R_{\mathbf{v}}$-irreflexive, $|V|=k$ must hold. On the other hand, as $R_{\mathbf{h}}$ is the universal relation in ${\mathfrak{H}}_{k}$, we must have $|U|\geq 2k$, contradicting $|U|=|V|>0$.

Item (ii) follows from Lemma 10.1 (ii), (5) and (7). The proof of item (iii) is similar to that of Lemma 10.1 (iii). ∎

Now the proof of Theorem 2 can be completed similarly to that of Theorem 10, using Lemma 10.2 in place of Lemma 10.1.

6 Infinite canonical axiomatisation for $\mathbf{Diff}\!\times\!\mathbf{Diff}$

In this section we prove Theorem 3 using the proof pattern described in §2.2 (for the class $\mathcal{C}$ of all products of difference frames). So we will define a recursive set $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ of Sahlqvist formulas, and prove that the following hold:

All formulas in $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ are valid in every product of difference frames. 2. 2.

For every countable rooted frame ${\mathfrak{F}}$ that is not the p-morphic image of some product of difference frames, there is some $\phi_{\mathfrak{F}}\in\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ such that $\phi_{\mathfrak{F}}$ is not valid in ${\mathfrak{F}}$.

To begin with, if ${\mathfrak{F}}$ is a countable rooted frame such that ${\mathfrak{F}}\not\models[\mathbf{Diff},\mathbf{Diff}]$, then ${\mathfrak{F}}\not\models\mathsf{comm\_pse}$, and so we let $\phi_{\mathfrak{F}}=\mathsf{comm\_pse}\in\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$. So from now on we assume that ${\mathfrak{F}}\models[\mathbf{Diff},\mathbf{Diff}]$, and so ${\mathfrak{F}}$ is a grid of bi-clusters by Lemma 6. We call a countable grid of bi-clusters ${\mathfrak{F}}$ bad if it is not the p-morphic image of a product of difference frames.

In §6.1 below we discuss two kinds of ‘finitary reasons’ for a countable grid of bi-clusters being bad, and prove that these are the only such reasons. Then in §6.2 we provide the Sahlqvist formulas in $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ ‘eliminating’ these reasons.

6.1 Bad grids of bi-clusters

The first reason for a countable grid of bi-clusters ${\mathfrak{F}}$ being bad is when ${\mathfrak{F}}$ contains a finite impossible bi-cluster. This reason will be ‘eliminated’ by a Sahlqvist formula in §6.2.1, where it is also shown that this is indeed a reason for ${\mathfrak{F}}$ being bad (see Corollary 18).

So suppose that ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is a countable rooted frame for $[\mathbf{Diff},\mathbf{Diff}]$ that is represented as a grid of bi-clusters as $(X,Y,g)$, and ${\mathfrak{F}}$ contains no impossible bi-clusters. We may assume that $X$ and $Y$ are disjoint, and consider the elements of $X\cup Y$ as distinct variables. We define a set $\Gamma^{{\mathfrak{F}}}$ of ‘constraints’ such that each constraint in $\Gamma^{{\mathfrak{F}}}$ is one of the forms $(z=n)$, $(z\geq k)$, or $(z\geq\lambda z^{\prime})$, for some $z,z^{\prime}\in X\cup Y$, $n\in\mathbb{N}^{+}\cup\{\aleph_{0}\}$, $k\in\mathbb{N}^{+}$, and $\lambda=1,2$. For all $x\in X$ and $y\in Y$,

[TABLE]

We assume that $(z\geq 1)\in\Gamma^{{\mathfrak{F}}}$ for every $z\in X\cup Y$. A solution of $\Gamma^{{\mathfrak{F}}}$ is a function

[TABLE]

validating all constraints in $\Gamma^{{\mathfrak{F}}}$. In other words, we are trying to solve a special kind of integer programming problem: $\Gamma^{{\mathfrak{F}}}$ is a (possibly infinite) set of linear equations and inequalities (where all coefficients are positive integers or $\aleph_{0}$), and we are looking for integer plus possibly (countably) infinite solutions of it. By Lemmas 8 (ii) and 9, it is easy to see the following:

Claim** 11****.**

*If ${\mathfrak{F}}$ is a countable grid of bi-clusters that contains no impossible bi-clusters and $\xi$ is a solution of $\Gamma^{{\mathfrak{F}}}$, then there is an onto p-morphism $h_{\xi}:(U,\neq_{U})\!\times\!(V,\neq_{V})\to{\mathfrak{F}}$ for some sets $U,V$ with $|U|=\sum_{x\in X}\xi(x)$ and $|V|=\sum_{y\in Y}\xi(y)$. *

(In §6.2 we will show that the converse of Claim 11 also holds in the sense that whenever a countable grid of bi-clusters ${\mathfrak{F}}$ is a p-morphic image of a product of difference frames, then ${\mathfrak{F}}$ contains no impossible bi-clusters, and $\Gamma^{{\mathfrak{F}}}$ has a solution; see Corollary 22.)

In order to characterise those countable ${\mathfrak{F}}$ for which $\Gamma^{{\mathfrak{F}}}$ has no solution, we first introduce some notions dealing with the one-variable constraints in $\Gamma^{{\mathfrak{F}}}$. For every $z\in X\cup Y$, we let

[TABLE]

Next, in order to deal with the two-variable constraints, we define a (finite or countably infinite) edge-labelled digraph $\mathcal{G}_{{\mathfrak{F}}}=(X\cup Y,E_{\mathfrak{F}})$ by taking, for any $z,z^{\prime}\in X\cup Y$,

[TABLE]

Observe that (i) all edges either go from some $x\in X$ to some $y\in Y$, or from some $y\in Y$ to some $x\in X$, (ii) edge-labels $\lambda$ can only be $1$ or $2$, and (iii) if $(z\to^{1}z^{\prime})\in E_{\mathfrak{F}}$ for some $z,z^{\prime}$ then $(z^{\prime}\to^{1}z)\in E_{\mathfrak{F}}$ as well. For some $m\in\mathbb{N}$, we call a path $z_{0}\to^{\lambda_{1}}z_{1}\to^{\lambda_{2}}\dots z_{m-1}\to^{\lambda_{m}}z_{m}$ in $\mathcal{G}_{{\mathfrak{F}}}$ bad, if $\textit{max}\,({z_{0}})<\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}\cdot\textit{min}\,({z_{m}})$. (Observe that when $m=0$ then $z_{0}$ is a bad path of length [math] whenever $\textit{max}\,({z_{0}})<\textit{min}\,({z_{0}})$. Note that a bad path is not necessarily simple: it may contain the same edge more than once.) Figs. 3 and 4 show two examples of grids of bi-clusters that are bad because their graphs contain some bad paths.

In §6.2.2 we will show that if a grid of bi-clusters ${\mathfrak{F}}$ is such that it does not contain impossible bi-clusters, but $\mathcal{G}_{{\mathfrak{F}}}$ contains a bad path, then there is a Sahlqvist formula ‘eliminating’ this reason (and ${\mathfrak{F}}$ is indeed bad). Here we show that we have found all reasons for $\Gamma^{{\mathfrak{F}}}$ not having a solution:

Lemma** 12****.**

Let ${\mathfrak{F}}=(X,Y,g)$ be a countable grid of bi-clusters such that

${\mathfrak{F}}$* contains no impossible bi-clusters, and* 2. 2.

there is no bad path in $\mathcal{G}_{{\mathfrak{F}}}$.

Then $\Gamma^{{\mathfrak{F}}}$ has a solution.

Proof.

Suppose ${\mathfrak{F}}$ contains no impossible bi-clusters, and there is no bad path in $\mathcal{G}_{{\mathfrak{F}}}$. We will define a ‘minimal’ solution $\xi_{\textit{min}}^{{\mathfrak{F}}}$ such that it takes the same value on variables belonging to the same strongly connected component of $\mathcal{G}_{{\mathfrak{F}}}$. To begin with, for every strongly connected component $\mathcal{S}$ in $\mathcal{G}_{{\mathfrak{F}}}$, we let (with a slight abuse of notation),

[TABLE]

Next, we define an acyclic digraph $\mathcal{G}_{{\mathfrak{F}}}^{+}$ as follows ($\mathcal{G}_{{\mathfrak{F}}}^{+}$ is what is called the condensation of $\mathcal{G}_{{\mathfrak{F}}}=(X\cup Y,E_{\mathfrak{F}})$): its nodes are the strongly connected components of $\mathcal{G}_{{\mathfrak{F}}}$, and we define the edges by taking

[TABLE]

For $n\in\mathbb{N}$, we call a path $\mathcal{S}_{0}\Rightarrow\mathcal{S}_{1}\Rightarrow\dots\mathcal{S}_{n-1}\Rightarrow\mathcal{S}_{n}$ in $\mathcal{G}_{{\mathfrak{F}}}^{+}$ bad, if $\textit{max}\,({\mathcal{S}_{0}})<2^{n}\cdot\textit{min}\,({\mathcal{S}_{n}})$.

Claim** 12.1****.**

There is no bad path in $\mathcal{G}_{{\mathfrak{F}}}^{+}$.

Proof.

Suppose indirectly that $\mathcal{S}_{0}\Rightarrow\mathcal{S}_{1}\Rightarrow\dots\mathcal{S}_{n-1}\Rightarrow\mathcal{S}_{n}$ is a bad path in $\mathcal{G}_{{\mathfrak{F}}}^{+}$, that is, $\textit{max}\,({\mathcal{S}_{0}})<2^{n}\cdot\textit{min}\,({\mathcal{S}_{n}})$. Then there exist $m\in\mathbb{N}$, $z_{0}\in\mathcal{S}_{0}$, $z_{n}\in\mathcal{S}_{n}$ and a path $P$ of the form $z_{0}\to^{\lambda_{1}}\dots\to^{\lambda_{m}}z_{n}$ in $\mathcal{G}_{{\mathfrak{F}}}$ such that $\textit{max}\,({\mathcal{S}_{0}})=\textit{max}\,({z_{0}})$ and $2^{n}\leq\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}$ whenever $m>0$. Now there are several cases:

• (a)

There is $z\in\mathcal{S}_{n}$ such that $\textit{min}\,({\mathcal{S}_{n}})=\textit{min}\,({z})$. Then take $P$ and continue it with any path from $z_{n}$ to $z$. The resulting path in $\mathcal{G}_{{\mathfrak{F}}}$ is bad, a contradiction.

• (b)

$\textit{min}\,({\mathcal{S}_{n}})=\aleph_{0}$ and there is a $\to^{2}$ edge within $\mathcal{S}_{n}$. Then take any path $Q$ from $z_{n}$ to $z_{n}$ containing this $\to^{2}$ edge. Suppose $Q$ is of the form $z_{n}\to^{\mu_{1}}\dots\to^{\mu_{i}}z_{n}$. Then $\mu_{1}\cdot$ $\dots$ $\cdot\mu_{i}\geq 2$, and so there is $r\in\mathbb{N}$ such that $\textit{max}\,({z_{0}})<2^{n}\cdot(\mu_{1}\cdot$ $\dots$ $\cdot\mu_{i})^{r}\cdot\textit{min}\,({z_{n}})$. Then the path in $\mathcal{G}_{{\mathfrak{F}}}$ obtained by starting with $P$ and then repeating $Q$ $r$ times is bad, a contradiction.

• (c)

$\textit{min}\,({\mathcal{S}_{n}})=\aleph_{0}$, there is no $\to^{2}$ edge within $\mathcal{S}_{n}$, but for every $i\in\mathbb{N}$ there is some $w_{i}\in\mathcal{S}_{n}$ with $\textit{min}\,({w_{i}})\geq i$. Then choose $i$ such that $i\cdot 2^{n}>\textit{max}\,({z_{0}})$. Then the path in $\mathcal{G}_{{\mathfrak{F}}}$ obtained by starting with $P$ and then continuing with any path from $z_{n}$ to $w_{i}$ is bad, a contradiction again,

proving Claim 12.1. ∎

Next, for every node $\mathcal{S}$ in $\mathcal{G}_{{\mathfrak{F}}}^{+}$, let

[TABLE]

We define a function $\nu_{\textit{min}}^{{\mathfrak{F}}}$ from the nodes of $\mathcal{G}_{{\mathfrak{F}}}^{+}$ to $\mathbb{N}^{+}\cup\{\aleph_{0}\}$ by induction on their rank  by taking, for every strongly connected component $\mathcal{S}$,

[TABLE]

(see Examples 14 and 32 below).

Claim** 12.2****.**

For all strongly connected components $\mathcal{S},\mathcal{S}^{\prime}$ in $\mathcal{G}_{{\mathfrak{F}}}$, all $n\in\mathbb{N}^{+}\cup\{\aleph_{0}\}$, $k\in\mathbb{N}^{+}$, and $\lambda\in\{1,2\}$, we have the following:

• (i)

If $(z=n)\in\Gamma^{{\mathfrak{F}}}$ for some $z\in\mathcal{S}$, then $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=n$.

• (ii)

If $(z\geq k)\in\Gamma^{{\mathfrak{F}}}$ for some $z\in\mathcal{S}$, then $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq k$.

• (iii)

If $(z\geq\lambda z^{\prime})\in\Gamma^{{\mathfrak{F}}}$ for some $z\in\mathcal{S}$, $z^{\prime}\in\mathcal{S}^{\prime}$, then $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq\lambda\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$.

Proof.

(i): If $n=\aleph_{0}$ then $\textit{min}\,({z})=\aleph_{0}$, and so $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\aleph_{0}$. So suppose that $n\in\mathbb{N}^{+}$. Then

[TABLE]

If any of the inequalities $\leq$ in (25) were $<$, then $\mathcal{S}$ would be a bad path of length [math] in $\mathcal{G}_{{\mathfrak{F}}}^{+}$, contradicting Claim 12.1. So we have $\textit{min}\,({\mathcal{S}})=\textit{max}\,({\mathcal{S}})=n$. We also have that $\textit{rank}\,(\mathcal{S})\in\mathbb{N}$. (Otherwise, there would exist a bad path of length $>n$ in $\mathcal{G}_{{\mathfrak{F}}}^{+}$ starting at $\mathcal{S}$.) If $\textit{rank}\,(\mathcal{S})=0$ then $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\textit{min}\,({\mathcal{S}})$ by definition, and so we have $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=n$. Now suppose that $\textit{rank}\,(\mathcal{S})>0$. By definition, $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq\textit{min}\,({\mathcal{S}})$ always holds. So suppose indirectly that $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})>\textit{min}\,({\mathcal{S}})$. We will construct a bad path in $\mathcal{G}_{{\mathfrak{F}}}^{+}$, contradicting Claim 12.1. To begin with, there is $\mathcal{S}_{1}$ such that $\mathcal{S}\Rightarrow\mathcal{S}_{1}$ and $2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})>\textit{min}\,({\mathcal{S}})=\textit{max}\,({\mathcal{S}})$. (Either because $\mathcal{S}_{1}$ is such that $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=2\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})$ or because $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\aleph_{0}$.) As $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})\geq\textit{min}\,({\mathcal{S}_{1}})$, there are two cases: (a) $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})=\textit{min}\,({\mathcal{S}_{1}})$. Then $2\cdot\textit{min}\,({\mathcal{S}_{1}})>\textit{min}\,({\mathcal{S}})=\textit{max}\,({\mathcal{S}})$, and so $\mathcal{S}\Rightarrow\mathcal{S}_{1}$ is a bad path in $\mathcal{G}_{{\mathfrak{F}}}^{+}$. (For example, this is the case when $\mathcal{S}_{1}$ is a final node in $\mathcal{G}_{{\mathfrak{F}}}^{+}$.) (b) $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})>\textit{min}\,({\mathcal{S}_{1}})$. Then there is $\mathcal{S}_{2}$ such that $\mathcal{S}_{1}\Rightarrow\mathcal{S}_{2}$ and $2^{2}\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{2})>\textit{max}\,({\mathcal{S}})$. (Either because $\mathcal{S}_{2}$ is such that $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})=2\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{2})$ or because $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{1})=\aleph_{0}$.) Again, there are two cases: (b.1) $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{2})=\textit{min}\,({\mathcal{S}_{2}})$. Then $\mathcal{S}\Rightarrow\mathcal{S}_{1}\Rightarrow\mathcal{S}_{2}$ is a bad path in $\mathcal{G}_{{\mathfrak{F}}}^{+}$. (b.2) $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}_{2})>\textit{min}\,({\mathcal{S}_{2}})$. Then again, there are two cases. And so on, sooner or later we reach a final node in $\mathcal{G}_{{\mathfrak{F}}}^{+}$, where we only have case (a).

(ii): If $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\aleph_{0}$ then the statement holds. If $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\in\mathbb{N}$ then $\textit{rank}\,(\mathcal{S})\in\mathbb{N}$, and so $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq\textit{min}\,({\mathcal{S}})\geq\textit{min}\,({z})\geq k$.

(iii): If $\lambda=1$ then $\mathcal{S}=\mathcal{S}^{\prime}$, and so $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$, as required. If $\lambda=2$ and $\mathcal{S}=\mathcal{S}^{\prime}$, then $\textit{min}\,({\mathcal{S}})=\textit{min}\,({\mathcal{S}^{\prime}})=\aleph_{0}$, and so $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})=\aleph_{0}$. Thus $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq 2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$ holds. If $\lambda=2$ and $\mathcal{S}\neq\mathcal{S}^{\prime}$, then $\mathcal{S}\Rightarrow\mathcal{S}^{\prime}$. If $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\aleph_{0}$, then $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq 2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$ holds. If $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\in\mathbb{N}$ then $\textit{rank}\,(\mathcal{S})\in\mathbb{N}$, and so again $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\geq 2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$ holds, as required. ∎

Now for every $\mathcal{S}$ in $\mathcal{G}_{{\mathfrak{F}}}^{+}$ and every $z$ in $\mathcal{S}$, we define

[TABLE]

By Claim 12.2, $\xi_{\textit{min}}^{{\mathfrak{F}}}$ is a solution of $\Gamma^{{\mathfrak{F}}}$, proving Lemma 12. ∎

Now by Claim 11 and Lemma 12 we obtain:

Corollary 13**.**

If a countable grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ is bad (that is, ${\mathfrak{F}}$ is not the p-morphic image of a product of difference frames), then at least one of the following two reasons holds:

either ${\mathfrak{F}}$ contains a finite impossible bi-cluster, 2. 2.

or there is a bad path in $\mathcal{G}_{{\mathfrak{F}}}$.

Example** 14****.**

Take the grid of bi-clusters ${\mathfrak{F}}$ in Fig. 8. We compute $\nu_{\textit{min}}^{{\mathfrak{F}}}$. To begin with, we have the following strongly connected components in $\mathcal{G}_{{\mathfrak{F}}}$: $\mathcal{S}_{1}=\{y_{1}\}$, $\mathcal{S}_{2}=\{x_{1}\}$, $\mathcal{S}_{3}=\{y_{3},x_{2},y_{2}\}$, $\mathcal{S}_{4}=\{y_{4}\}$, $\mathcal{S}_{5}=\{x_{4},y_{5},x_{5},x_{6}\}$, $\mathcal{S}_{6}=\{x_{3}\}$. Then the edges in $\mathcal{G}_{{\mathfrak{F}}}^{+}$ are $\mathcal{S}_{2}\Rightarrow\mathcal{S}_{3}$ and $\mathcal{S}_{4}\Rightarrow\mathcal{S}_{5}$. Therefore, we have:

[TABLE]

6.2 Sahlqvist formulas

In §6.2.1 and §6.2.2 below, we will eliminate each of the two kinds of reasons in Corollary 13 for a countable grid of bi-clusters ${\mathfrak{F}}$ being bad, using a Sahlqvist formula $\phi_{{\mathfrak{F}}}$ in each case.

6.2.1 Eliminating impossible bi-clusters

Recall from Table 1 that a finite bi-cluster is impossible, if it is one of the types (no1)–(no4). We define formulas for the cases of (no1), (no3) and (no4); the case of (no2) is similar and left to reader. So let $\mathfrak{C}=(C,R_{\mathbf{h}},R_{\mathbf{v}})$ be a bi-cluster consisting of $n=k+\ell$ points for some $k,\ell\in\mathbb{N}^{+}$, out of which $a_{1},\dots,a_{k}$ are $R_{\mathbf{v}}$-irreflexive, $a_{1}$ is $R_{\mathbf{h}}$-reflexive, $b_{1},\dots,b_{\ell}$ are $R_{\mathbf{h}}$-irreflexive; see Fig. 5. (It does not matter whether any of $a_{2},\dots,a_{k}$ are $R_{\mathbf{h}}$-reflexive or -irreflexive, or whether any of $b_{1},\dots,b_{\ell}$ are $R_{\mathbf{v}}$-reflexive or -irreflexive.)

We introduce fresh propositional variables $\mathsf{a}_{i}$ for $i=1,\dots k$, and $\mathsf{b}_{j}$ for $j=1,\dots,\ell$, and define

[TABLE]

It is straightforward to check that $\mathsf{impossible}_{\mathfrak{C}}$ is a Sahlqvist formula.

Lemma** 15****.**

It is decidable whether a bimodal formula is of the form $\mathsf{impossible}_{\mathfrak{C}}$ for some impossible bi-cluster $\mathfrak{C}$.

Proof.

Observe that $\mathsf{impossible}_{\mathfrak{C}}$ only depends on the numbers $k,\ell$ and the type of $\mathfrak{C}$. ∎

Lemma** 16****.**

$\mathsf{impossible}_{\mathfrak{C}}$* is not valid in any grid of bi-clusters that contains the bi-cluster $\mathfrak{C}$.*

Proof.

Suppose ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is a grid of bi-clusters containing $\mathfrak{C}$. We define a model ${\mathfrak{M}}$ on ${\mathfrak{F}}$ by taking

[TABLE]

It is straightforward to check that ${\mathfrak{M}},a_{1}\models\mathsf{clash}_{\mathfrak{C}}$. On the other hand, if $w\in W$ is such that ${\mathfrak{M}},w\models\bigwedge_{i=1}^{k}\mathsf{a}_{i}\land\bigwedge_{j=1}^{\ell}\mathsf{b}_{j}$, then $w$ must be in $\mathfrak{C}$ by the definition of ${\mathfrak{M}}$ and grids of bi-clusters. As all the $a_{i}$ are $R_{\mathbf{v}}$-irreflexive and all the $b_{j}$ are $R_{\mathbf{h}}$-irreflexive, $w$ should be different from all of them, a contradiction. ∎

Lemma** 17****.**

$\mathsf{impossible}_{\mathfrak{C}}$* is valid in every product of difference frames.*

Proof.

Let ${\mathfrak{M}}$ be a model over a product $(U,\neq_{U})\!\times\!(V,\neq_{V})$ of difference frames, and suppose that ${\mathfrak{M}},(u_{0},v_{1})\models\mathsf{clash}_{\mathfrak{C}}$. By (27)–(28), there are distinct points $u_{0},\dots,u_{n}$ in $U$ and distinct points $v_{1},\dots,v_{n}$ in $V$ such that

[TABLE]

(see Fig. 6).

We say that a pair $(u,v)\in U\!\times\!V$ is of $a$-type (or of $b$-type) if ${\mathfrak{M}},(u,v)\models\hat{\mathsf{a}}_{i}$ for some $i=1,\dots,k$ (or ${\mathfrak{M}},(u,v)\models\hat{\mathsf{b}}_{j}$ for some $j=1,\dots,\ell$). Take the subset $Z$ of $U\!\times\!V$ consisting of the pairs $(u_{i},v_{j})$ for $i=0,\dots,n$ and $j=1,\dots,n$. We claim that

[TABLE]

Indeed, suppose the contrary, that is, every pair in $Z$ is either $a$-type or $b$-type. For every $0\leq i\leq n$, there can be $\leq k$ many $a$-type pairs among $(u_{i},v_{1}),\dots,(u_{i},v_{n})$. So there have to be $\geq\ell$ many $b$-type pairs among them. So altogether in $Z$ there are $\geq(n+1)\cdot\ell$ many $b$-type pairs. Thus, by the generalised pigeonhole principle, there exists $1\leq s\leq n$ such that there are $>\ell$ many $b$-type points among $(u_{0},v_{s}),\dots,(u_{n},v_{s})$. But for every $1\leq j\leq n$, there can be $\leq\ell$ many $b$-type pairs among $(u_{0},v_{j}),\dots,(u_{n},v_{j})$, a contradiction, proving (33).

So suppose $(u,v)\in Z$ is neither $a$-type nor $b$-type. By (29)–(30), for every $1\leq i\leq k$ there is some $z_{i}\in V$ such that $z_{i}\neq v$ and ${\mathfrak{M}},(u,z_{i})\models\hat{\mathsf{a}}_{i}$, and so ${\mathfrak{M}},(u,v)\models\mathsf{a}_{i}$ by (27). Similarly, by (31)–(32), for every $1\leq j\leq\ell$ there is some $w_{j}\in U$ such that $w_{j}\neq u$ and ${\mathfrak{M}},(w_{j},v)\models\hat{\mathsf{b}}_{j}$, and so ${\mathfrak{M}},(u,v)\models\mathsf{b}_{j}$ by (28). Therefore, ${\mathfrak{M}},(u,v)\models\bigwedge_{i=1}^{k}\mathsf{a}_{i}\land\bigwedge_{j=1}^{\ell}\mathsf{b}_{j},$ as required. ∎

As a consequence of Lemmas 16 and 17 we also obtain:

Corollary 18**.**

For every countable grid of bi-clusters ${\mathfrak{F}}$, if ${\mathfrak{F}}$ is a p-morphic image of a product of difference frames, then ${\mathfrak{F}}$ contains no impossible bi-clusters.

6.2.2 Eliminating bad paths

Let ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ be a countable rooted frame for $[\mathbf{Diff},\mathbf{Diff}]$ that is represented as a grid of bi-clusters as $(X,Y,g)$. Suppose that ${\mathfrak{F}}$ contains no impossible bi-clusters, but $\mathcal{G}_{{\mathfrak{F}}}$ contains a bad path $P$ of the form

[TABLE]

such that $m\in\mathbb{N}$ and $\textit{max}\,({z_{0}})<\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}\cdot\textit{min}\,({z_{m}})$. Throughout this subsection, we assume that $z_{0},z_{m}\in Y$, and define a Sahlqvist formula $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ for this case. The other three cases are similar and left to the reader.

The antecedent of $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ will consists of two conjuncts: $\mathsf{small}_{{\mathfrak{F}}}^{P}$ (expressing the value of $\textit{max}\,({z_{0}})$), and $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{large}_{{\mathfrak{F}}}^{P}$ (expressing that the value of $\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}\cdot\textit{min}\,({z_{m}})$ is sufficiently large).

We begin with defining $\mathsf{small}_{{\mathfrak{F}}}^{P}$. As $\textit{max}\,({z_{0}})<\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}\cdot\textit{min}\,({z_{m}})$, we must have that $\textit{max}\,({z_{0}})=n_{P}$ for some $n_{P}\in\mathbb{N}^{+}$, and so $(z_{0}=n_{P})\in\Gamma^{{\mathfrak{F}}}$ by (18). As $z_{0}\in Y$,

[TABLE]

So, we introduce fresh propositional variables $\mathsf{a}$ and $\mathsf{a}_{i}$, for $i=1,\dots,n_{P}$, and define the formula

[TABLE]

In order to define $\mathsf{large}_{{\mathfrak{F}}}^{P}$, we first describe the path $P$ with a formula $\mathsf{path}_{{\mathfrak{F}}}^{P}$. To this end, we say that a bi-cluster $\mathfrak{C}$ corresponds to an edge $z\to^{\lambda}z^{\prime}$ in $\mathcal{G}_{{\mathfrak{F}}}$, if $\mathfrak{C}$ is (isomorphic to) ${\mathfrak{F}}^{zz^{\prime}}$ whenever $z\in X$, $z^{\prime}\in Y$, and $\mathfrak{C}$ is (isomorphic to) ${\mathfrak{F}}^{z^{\prime}z}$ whenever $z^{\prime}\in X$, $z\in Y$. Observe that only switch bi-clusters can correspond to some edge in $\mathcal{G}_{{\mathfrak{F}}}$. In particular, for every $x\in X$ and every $y\in Y$, we have the following:

• •

$x\to^{1}y$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$ iff $y\to^{1}x$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$ iff ${\mathfrak{F}}^{xy}$ is a type ($=$sw) bi-cluster.

• •

$x\to^{2}y$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$ iff ${\mathfrak{F}}^{xy}$ is a type (h2vsw) bi-cluster.

• •

$y\to^{2}x$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$ iff ${\mathfrak{F}}^{xy}$ is a type (v2hsw) bi-cluster.

If $m>0$ then let $\mathfrak{C}_{1},\dots\mathfrak{C}_{m}$ be the sequence of bi-clusters corresponding to the edges in $P$ (that is, $\mathfrak{C}_{j}$ corresponds to $z_{j-1}\to^{\lambda_{j}}z_{j}$). Observe that for each $j=1,\dots,m$,

• •

if $\mathfrak{C}_{j}$ is of type (v2hsw) then there is some    point $c_{j}$ in $\mathfrak{C}_{j}$;

• •

if $\mathfrak{C}_{j}$ is of type (h2vsw) then there is some    point $c_{j}$ in $\mathfrak{C}_{j}$; and

• •

if $\mathfrak{C}_{j}$ is of type ($=$sw) then there is some    point $c_{j}$ in $\mathfrak{C}_{j}$.

So, for $j=1,\dots,m$, we introduce fresh propositional variables $\mathsf{c}_{j}$, and define formulas

[TABLE]

We also introduce a fresh propositional variable $\mathsf{b}$, and define the formulas $\mathsf{path}_{0}$, $\mathsf{path}_{1}$, $\dots$, $\mathsf{path}_{m}=\mathsf{path}_{{\mathfrak{F}}}^{P}$ inductively as follows. Let $\mathsf{path}_{0}=\neg\mathsf{a}\land\Box_{\mathbf{h}}\mathsf{b}$ (where $\mathsf{a}$ is the same variable as in $\mathsf{small}_{{\mathfrak{F}}}^{P}$), and for $j=1,\dots,m$, let

[TABLE]

Now we are in a position to define $\mathsf{large}_{{\mathfrak{F}}}^{P}$, expressing that the value of $\lambda_{1}\cdot$ $\dots$ $\cdot\lambda_{m}\cdot\textit{min}\,({z_{m}})$ for the endpoint $z_{m}$ of $P$ is sufficiently large. Let $k_{P}\in\mathbb{N}^{+}$ be such that \textit{max}\,({z_{0}})<\mbox{\lambda_{1}\cdot$$\dots$$\cdot\lambda_{m}\cdot k_{P}} and $k_{P}\leq\textit{min}\,({z_{m}})$. We have two cases, depending on why $\textit{min}\,({z_{m}})$ is ‘too large’:

There is $x_{P}^{\prime}\in X$ such that $\textit{v\_size}({\mathfrak{F}}^{x_{P}^{\prime}z_{m}})\geq k_{P}$; 2. 2.

or there is $x_{P}^{\prime}\in X$ such that ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ is an infinity bi-cluster

(see (19), (15), and Table 1). We define a Sahlqvist formula $\mathsf{large}_{{\mathfrak{F}}}^{P}$ for each of these two cases.

Case 1. Then there are $R_{\mathbf{v}}$-reflexive points $b_{1}^{\circ},\dots,b_{r_{P}}^{\circ}$ and $R_{\mathbf{v}}$-irreflexive points $b_{1}^{\bullet},\dots,b_{i_{P}}^{\bullet}$ in ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ such that $2r_{P}+i_{P}\geq k_{P}$. We introduce fresh propositional variables $\mathsf{b}_{j}^{\circ}$ for $j=1,\dots,r_{P}$, and $\mathsf{b}_{s}^{\bullet}$ for $s=1,\dots,i_{P}$, and define the formulas

[TABLE]

Then we let

[TABLE]

Case 2. Now we cannot use that we have enough different points in ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ like in Case 1, but instead we need to ‘generate’ them. There are two cases: Either (a) ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ contains some    point $c$ and some   * point $d$ (this is when ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ is of type (inf1), (inf2) or (inf4)); or (b) ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ contains some   * point $c$ and some    point $d$ (this is when ${\mathfrak{F}}^{x_{P}^{\prime}z_{m}}$ is of type (inf1), (inf3) or (inf4)). In both cases, instead of the $\mathsf{b}_{j}^{\circ}$ and $\mathsf{b}_{j}^{\bullet}$ variables, we introduce fresh propositional variables $\mathsf{c}$ and $\mathsf{d}$, and define the formulas

[TABLE]

Then we define the formulas $\mathsf{large}_{1},\dots,\mathsf{large}_{k_{P}}=\mathsf{large}_{{\mathfrak{F}}}^{P}$ inductively as follows. Let

[TABLE]

and for $j=2,\dots,k_{P}$, let

[TABLE]

Finally, we define $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ by taking

[TABLE]

It is straightforward to check that $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ is a Sahlqvist formula.

Lemma** 19****.**

It is decidable whether a bimodal formula is of the form $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ for some grid of bi-clusters ${\mathfrak{F}}$ and bad path $P$ in $\mathcal{G}_{{\mathfrak{F}}}$.

Proof.

Observe that $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ only depends on the numbers $n_{P}$, $r_{P}$, $i_{P}$, $k_{P}$, and the types in the sequence of bi-clusters corresponding to the edges in $P$. ∎

Lemma** 20****.**

Suppose ${\mathfrak{F}}=(X,Y,g)$ is a grid of bi-clusters that contains no impossible bi-clusters. If $P$ is a bad path in $\mathcal{G}_{{\mathfrak{F}}}$, then $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ is not valid in ${\mathfrak{F}}$.

Proof.

We use the notation introduced in the definition of $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$. We define a model ${\mathfrak{M}}$ on ${\mathfrak{F}}$ by taking

[TABLE]

then in Case 1, take

[TABLE]

and in Case 2, take

[TABLE]

It is straightforward to check that ${\mathfrak{M}},a_{1}\models\mathsf{small}_{{\mathfrak{F}}}^{P}$. Further, it is easy to see that in Case 1, ${\mathfrak{M}},b_{j}^{\circ}\models\mathsf{path}_{{\mathfrak{F}}}^{P}$ for all $j=1,\dots,r_{P}$ and ${\mathfrak{M}},b_{s}^{\bullet}\models\mathsf{path}_{{\mathfrak{F}}}^{P}$ for all $s=1,\dots,i_{P}$, and in Case 2, ${\mathfrak{M}},c\models\mathsf{path}_{{\mathfrak{F}}}^{P}$. Using these, it is not hard to check that $\mathsf{large}_{{\mathfrak{F}}}^{P}$ is satisfied in ${\mathfrak{M}}$ in both cases.

On the other hand, suppose $w\in W$ is such that $a_{1}R_{\mathbf{v}}^{+}w$ and ${\mathfrak{M}},w\models\mathsf{b}$. We claim that $a_{1}R_{\mathbf{h}}^{+}w$ follows. Indeed, if $m=0$ then this is because we have some $w^{\prime}$ in ${\mathfrak{F}}^{x_{P}^{\prime}z_{0}}$ with $w^{\prime}R_{\mathbf{h}}^{+}a_{1}$ and $w^{\prime}R_{\mathbf{h}}w$, and if $m>0$ then because of $a_{1}R_{\mathbf{h}}c_{1}$ and $c_{1}R_{\mathbf{h}}w$. Thus, $w$ must be in ${\mathfrak{F}}^{x_{P}z_{0}}$ by the definition of grids of bi-clusters. If ${\mathfrak{M}},w\models\bigwedge_{i=1}^{n_{P}}\mathsf{a}_{i}$ held as well, then $w$ should be different from all the $a_{i}$, contradicting ${\mathfrak{F}}^{x_{P}z_{0}}=\{a_{1},\dots,a_{n_{P}}\}$. ∎

Lemma** 21****.**

$\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$* is valid in every product of difference frames.*

Proof.

Again, we use the notation introduced in the definition of $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$. Let ${\mathfrak{M}}$ be a model over a product $(U,\neq_{U})\!\times\!(V,\neq_{V})$ of difference frames, and suppose that ${\mathfrak{M}},(u,v)\models\mathsf{small}_{{\mathfrak{F}}}^{P}$ for some $u,v$. Then there are distinct points $v_{1},\dots,v_{n_{P}}$ in $V$ such that

[TABLE]

Claim** 21.1****.**

If $\mathsf{large}_{{\mathfrak{F}}}^{P}$ is satisfied in ${\mathfrak{M}}$, then there exist points $u_{1},\dots,u_{k_{P}}\in U$ and distinct points $w_{1},\dots,w_{k_{P}}\in V$ such that ${\mathfrak{M}},(u_{j},w_{j})\models\mathsf{path}_{{\mathfrak{F}}}^{P}$, for all $j=1,\dots,k_{P}$.

Proof.

In Case 1 this easily follows from $2r_{P}+i_{P}\geq k_{P}$ and (37)–(38). In Case 2(a): We show by induction that, for all $j=1,\dots,k_{P}$, if ${\mathfrak{M}},(a,b)\models\mathsf{large}_{j}$ for some $(a,b)$, then there are distinct points $u_{1},\dots,u_{j}$ in $U$ and distinct points $w_{1},\dots,w_{j}$ in $V$ such that

• •

$w_{j}=b$,

• •

$u_{s}\neq a$ for any $s$ with $1\leq s\leq j$,

• •

${\mathfrak{M}},(u_{s},w_{s})\models\hat{\mathsf{d}}\land\mathsf{path}_{{\mathfrak{F}}}^{P}$ for all $1\leq s\leq j$, and

• •

${\mathfrak{M}},(u_{s},w_{s-1})\models\hat{\mathsf{c}}$ for all $2\leq s\leq j$.

As $\mathsf{large}_{{\mathfrak{F}}}^{P}=\mathsf{large}_{k_{P}}$, Claim 21.1 will follow. To begin with, the $j=1$ case is obvious. So suppose inductively that the statement holds for some $j-1$, and suppose that ${\mathfrak{M}},(a,b)\models\mathsf{large}_{j}$. Then there are $a^{\prime}\in U$, $b_{1},b_{2}\in V$ such that $a^{\prime}\neq a$, $b,b_{1},b_{2}$ are all distinct, ${\mathfrak{M}},(a^{\prime},b)\models\hat{\mathsf{d}}\land\mathsf{path}_{{\mathfrak{F}}}^{P}$, and ${\mathfrak{M}},(a^{\prime},b_{i})\models\mathsf{large}_{j-1}$ for $i=1,2$. By the IH, for each $i=1,2$, there are distinct points $u_{1}^{i},\dots,u_{j-1}^{i}$ in $U$ and distinct points $w_{1}^{i},\dots,w_{j-1}^{i}$ in $V$ such that $w_{j-1}^{i}=b_{i}$, $u_{s}^{i}\neq a^{\prime}$ for any $s$, ${\mathfrak{M}},(u_{s}^{i},w_{s}^{i})\models\hat{\mathsf{d}}\land\mathsf{path}_{{\mathfrak{F}}}^{P}$ for all $1\leq s\leq j-1$, and ${\mathfrak{M}},(u_{s}^{i},w_{s-1}^{i})\models\hat{\mathsf{c}}$ for all $2\leq s\leq j-1$. Thus, for each $i=1,2$,

[TABLE]

As $w_{j-1}^{1}=b_{1}\neq b_{2}=w_{j-1}^{2}$, (40) and (41) imply that all the $u_{1}^{1},\dots,u_{j-1}^{1}$, $u_{1}^{2},\dots,u_{j-1}^{2}$ are distinct. Thus, either $a\notin\{u_{1}^{1},\dots,u_{j-1}^{1}\}$ or $a\notin\{u_{1}^{2},\dots,u_{j-1}^{2}\}$. Let $j$ be such that $a\notin\{u_{1}^{j},\dots,u_{j-1}^{j}\}$. Then the points $u_{s}=u_{s}^{j}$, $w_{s}=w_{s}^{j}$ for $s=1,\dots,j-1$, $u_{j}=a^{\prime}$, $w_{j}=b$ are as required.

Case 2(b) is similar. ∎

Claim** 21.2****.**

\displaystyle{\mathfrak{M}},(u,v)\models\Diamond_{\mathbf{v}}^{+}\Bigl{(}\mathsf{b}\land\bigwedge_{i=1}^{n_{P}}\mathsf{a}_{i}\Bigr{)}.

Proof.

We define sets $\textit{Gen}({z_{j}})$ and $\textit{Set}({z_{j}})$ inductively, for $j=m,\dots,0$, such that the following hold, for every $j\leq m$:

• (i)

$\textit{Gen}({z_{j}})\subseteq U\!\times\!V$;

• (ii)

${\mathfrak{M}},(a,b)\models\mathsf{path}_{j}$ for every $(a,b)\in\textit{Gen}({z_{j}})$;

• (iii)

if $j<m$ then ${\mathfrak{M}},(a,b)\models\hat{\mathsf{c}}_{j+1}$ for every $(a,b)\in\textit{Gen}({z_{j}})$;

• (iv)

\textit{Set}({z_{j}})=\left\{\begin{array}[]{ll}\{a\in U:(a,b)\in\textit{Gen}({z_{j}})\mbox{ for some b}\},&\mbox{ if z_{j}\in X},\\[3.0pt] \{b\in V:(a,b)\in\textit{Gen}({z_{j}})\mbox{ for some a}\},&\mbox{ if z_{j}\in Y};\end{array}\right.

• (v)

$|\textit{Set}({z_{m}})|=k_{P}$, and if $j<m$ then $|\textit{Set}({z_{j}})|=\lambda_{j+1}\cdot|\textit{Set}({z_{j+1}})|$.

To begin with, we take the points from Claim 21.1 and let

[TABLE]

Now suppose inductively that (i)–(v) hold for some $j$. There are several cases. Suppose first that $z_{j-1}\in X$, and $\textit{Set}({z_{j}})=\{b_{1},\dots,b_{s_{j}}\}$ for some $s_{j}$. Take some $a_{1},\dots,a_{s_{j}}\in U$ such that $(a_{i},b_{i})\in\textit{Gen}({z_{j}})$ for all $i=1,\dots,s_{j}$.

• •

If $\lambda_{j}=1$ (that is, $\mathfrak{C}_{j}$ is of type ($=$sw)), then $\mathsf{path}_{j}=\Diamond_{\mathbf{h}}(\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1})$ by (36). By (ii), there are $a^{\prime}_{1},\dots,a^{\prime}_{s_{j}}\in U$ such that ${\mathfrak{M}},(a^{\prime}_{i},b_{i})\models\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1}$, for all $i=1,\dots,s_{j}$. As $\hat{\mathsf{c}}_{j}=\neg\mathsf{c}_{j}\land\Box_{\mathbf{h}}\mathsf{c}_{j}\land\Box_{\mathbf{v}}\mathsf{c}_{j}$ by (35), all the $a^{\prime}_{i}$ are distinct. We let $\textit{Set}({z_{j-1}})=\{a^{\prime}_{1},\dots,a^{\prime}_{s_{j}}\}$.

• •

If $\lambda_{j}=2$ (that is, $\mathfrak{C}_{j}$ is of type (h2vsw)), then \mathsf{path}_{j}=\Diamond_{\mathbf{h}}\bigl{(}\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1}\land\Diamond_{\mathbf{h}}(\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1})\bigr{)} by (36). By (ii), there are $a^{\prime}_{1},\dots,a^{\prime}_{2s_{j}}\in U$ such that ${\mathfrak{M}},(a^{\prime}_{i},b_{i})\models\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1}$ and ${\mathfrak{M}},(a^{\prime}_{s_{j}+i},b_{i})\models\hat{\mathsf{c}}_{j}\land\mathsf{path}_{j-1}$, for all $i=1,\dots,s_{j}$. As $\hat{\mathsf{c}}_{j}=\neg\mathsf{c}_{j}\land\Box_{\mathbf{v}}\mathsf{c}_{j}$ by (35), all the $2s_{j}$ many $a^{\prime}_{i}$ are distinct. We let $\textit{Set}({z_{j-1}})=\{a^{\prime}_{1},\dots,a^{\prime}_{2s_{j}}\}$.

The cases when $z_{j-1}\in Y$ are similar.

So we have (i)–(v) for all $j=0,\dots,m$, and so $|\textit{Set}({z_{0}})|=k_{P}\cdot\lambda_{m}\cdot$ $\dots$ $\cdot\lambda_{1}$. As $P$ is a bad path, $|\textit{Set}({z_{0}})|>n_{P}$, and so by the pigeonhole principle, there is $w\in\textit{Set}({z_{0}})$ such that $w\neq v_{i}$ for any $1\leq i\leq n_{P}$. Therefore, ${\mathfrak{M}},(u,w)\models\bigwedge_{i=1}^{n_{P}}\mathsf{a}_{i}$ by (39). We claim that ${\mathfrak{M}},(u,w)\models\mathsf{b}$ also holds. Indeed, take any $a\in U$ such that $(a,w)\in\textit{Gen}({z_{0}})$. As $\mathsf{path}_{0}=\neg\mathsf{a}\land\Box_{\mathbf{h}}\mathsf{b}$, by (ii) we have ${\mathfrak{M}},(a,w)\models\neg\mathsf{a}\land\Box_{\mathbf{h}}\mathsf{b}$. Therefore, $a\neq u$ by (39), and so ${\mathfrak{M}},(u,w)\models\mathsf{b}$ follows, as required. ∎

As by Claim 21.2 the consequent of $\mathsf{bad\_path}_{{\mathfrak{F}}}^{P}$ holds at $(u,v)$ in ${\mathfrak{M}}$, the proof of Lemma 21 is completed. ∎

As a consequence of Corollary 18 and Lemmas 12, 20 and 21 we also obtain the following ‘converse’ of Lemma 9:

Corollary 22**.**

For every countable grid of bi-clusters ${\mathfrak{F}}$, if ${\mathfrak{F}}$ is a p-morphic image of a product of difference frames, then ${\mathfrak{F}}$ contains no impossible bi-clusters, and $\Gamma^{{\mathfrak{F}}}$ has a solution.

7 Infinite canonical axiomatisation for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$

In this section we prove Theorem 4 using the proof pattern described in §2.2 (for the class $\mathcal{C}$ of all square products of difference frames). So we will define a recursive set $\Sigma_{\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}}$ of generalised Sahlqvist formulas containing $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$, and prove that the following hold:

All formulas in $\Sigma_{\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}}$ are valid in every square product of difference frames. 2. 2.

For every countable rooted frame ${\mathfrak{F}}$ that is not the p-morphic image of some square product of difference frames, there is some $\phi_{\mathfrak{F}}\in\Sigma_{\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}}$ such that $\phi_{\mathfrak{F}}$ is not valid in ${\mathfrak{F}}$.

To begin with, if ${\mathfrak{F}}$ is a countable rooted frame such that it is not the p-morphic image of a product of difference frames at all, then there is some $\phi_{\mathfrak{F}}\in\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ such that $\phi_{\mathfrak{F}}$ is not valid in ${\mathfrak{F}}$. So from now on we assume that ${\mathfrak{F}}$ is the p-morphic image of a product of difference frames. In particular, ${\mathfrak{F}}\models[\mathbf{Diff},\mathbf{Diff}]$, and so ${\mathfrak{F}}$ is a grid of bi-clusters by Lemma 6. We call a countable grid of bi-clusters ${\mathfrak{F}}$ square-bad if it is the p-morphic image of a product of difference frames, but it is not the p-morphic image of a square product of difference frames.

In §7.1 below we classify square-bad grids of bi-clusters into several categories. Then in §7.2 we define the generalised Sahlqvist formulas in $\Sigma_{\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}}$, for each such category. Finally, in §7.3 we discuss Corollary 5, that is, why $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ is in fact Sahlqvist axiomatisable.

7.1 Good grids of bi-clusters that are not p-morphic images of squares

Throughout, we suppose that ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is square-bad and represented as a grid of bi-clusters as $(X,Y,g)$. By Corollary 22, ${\mathfrak{F}}$ contains no impossible bi-clusters, and the set $\Gamma^{{\mathfrak{F}}}$ of constraints (as defined in (15)) does have a solution. By Claim 11, we have $\sum_{y\in Y}\xi(y)\neq\sum_{x\in X}\xi(x)$ for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$ (see Figs. 7 and 8 for some examples). In particular,

[TABLE]

We begin with introducing some notions that will help us to deal with ‘upper bound’ constraints. For any $n\in\mathbb{N}^{+}$ and any $z\in X\cup Y$, we call $z$ $n$-strict if $(z=n)\in\Gamma^{{\mathfrak{F}}}$. We call $z$ strict if it is $n$-strict for some $n\in\mathbb{N}^{+}$. Now recall the digraph $\mathcal{G}_{{\mathfrak{F}}}$ from (20). We call a $z\in X\cup Y$ bounded if there is a path in $\mathcal{G}_{{\mathfrak{F}}}$ from some strict $z^{\prime}$ to $z$, and unbounded otherwise. (In particular, if $z$ is strict then $z$ is bounded.) Given a bounded $z$ and a path $P$ in $\mathcal{G}_{{\mathfrak{F}}}$ of the form $z_{0}\to^{\lambda_{1}}z_{1}\dots\to^{\lambda_{m}}z_{m}$ where $z_{m}=z$ and $z_{0}$ is $n$-strict for some $n\in\mathbb{N}^{+}$, we let

[TABLE]

Then for every bounded $z\in X\cup Y$, we let

[TABLE]

Note that since $\Gamma^{{\mathfrak{F}}}$ has a solution, $\textit{ub}^{{\mathfrak{F}}}({z})=n$ for any $n$-strict node $z$. Also, it is easy to see that

[TABLE]

For any bounded $z$, we choose a simple path $P_{\textit{ub}}^{{\mathfrak{F}}}({z})$ from $z$ to a strict node such that \textit{weight}\,\bigl{(}P_{\textit{ub}}^{{\mathfrak{F}}}({z})\bigr{)}=\textit{ub}^{{\mathfrak{F}}}({z}), and if $z$ is strict then $P_{\textit{ub}}^{{\mathfrak{F}}}({z})$ consists of just $z$.

Lemma** 23****.**

Suppose ${\mathfrak{F}}=(X,Y,g)$ is a grid of bi-clusters such that $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{y\in Y}\xi(y)\neq\sum_{x\in X}\xi(x)$ for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$. Then one of the following cases holds:

• (i)

$X\cup Y$* is finite, and every $z\in X\cup Y$ is bounded.*

• (ii)

$X\cup Y$* is finite, and either (a) every $x\in X$ is bounded, there is some unbounded $y^{\star}\in Y$, and $\sum_{x\in X}\xi(x)<\sum_{y\in Y}\xi(y)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$; or (b) every $y\in Y$ is bounded, there is some unbounded $x^{\star}\in X$, and $\sum_{y\in Y}\xi(y)<\sum_{x\in X}\xi(x)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$.*

• (iii)

Either (a) $X$ is finite, every $x\in X$ is bounded, $Y$ is infinite, and there is a finite subgrid ${\mathfrak{F}}^{-}=(X,Y^{-},g^{-})$ of ${\mathfrak{F}}$ such that $\sum_{x\in X}\xi(x)<\sum_{y\in Y^{-}}\xi(y)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}^{-}}$; or (b) $Y$ is finite, every $y\in Y$ is bounded, $X$ is infinite, and there is a finite subgrid ${\mathfrak{F}}^{-}=(X^{-},Y,g^{-})$ of ${\mathfrak{F}}$ such that $\sum_{y\in Y}\xi(y)<\sum_{x\in X^{-}}\xi(x)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}^{-}}$.

Proof.

Observe that since $\Gamma^{{\mathfrak{F}}}$ has a solution, at least one of $X$ and $Y$ must be finite by (42). So suppose, say, that $X$ is finite. Suppose also that there is some unbounded $x\in X$. Then by (44) and (42) we obtain that $Y$ is finite and every $y\in Y$ is bounded. So at least one of $X$ or $Y$ must be such that it is finite and all its members are bounded. Suppose, say, that $X$ is finite and every $x\in X$ is bounded. There are three cases:

If $Y$ is finite and every $y\in Y$ is bounded, then we have Case (i).

If $Y$ is finite and there is some unbounded $y^{\star}\in Y$, then (as every $x\in X$ is bounded) the only constraints about $y^{\star}$ in $\Gamma^{{\mathfrak{F}}}$ are of the form $(y^{\ast}\geq k)$ or $(y^{\ast}\geq\lambda x)$, for some $k\in\mathbb{N}^{+}$, $\lambda=1,2$ and $x\in X$. So for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$, if we keep $\xi(z)$ for all $z\neq y^{\ast}$, and increase $\xi(y^{\ast})$ arbitrarily, we obtain another solution. Therefore, we cannot have that $\sum_{x\in X}\xi(x)\geq\sum_{y\in Y}\xi(y)$ for any solution $\xi$, and so we have Case (ii).

Finally, suppose that $Y$ is infinite. Then let

[TABLE]

Clearly, $Y^{\prime}$ is finite. Now take any finite $Y^{-}\supseteq Y^{\prime}$ such that $|Y^{-}|>\sum_{x\in X}\textit{ub}^{{\mathfrak{F}}}({x})$, and let {\mathfrak{F}}^{-}=\bigl{(}X,Y^{-},g|_{X\!\times\!Y^{-}}\bigr{)}. By (43), for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}^{-}}$, we have

[TABLE]

and so we have Case (iii). ∎

7.2 Generalised Sahlqvist formulas

In this subsection, we will eliminate the reasons for a countable grid of bi-clusters ${\mathfrak{F}}$ being square-bad. For each of the cases described in Lemma 23, we use a different generalised Sahlqvist formula $\phi^{\textit{sq}}_{\mathfrak{F}}$. Throughout this subsection, we assume that ${\mathfrak{F}}=(W,R_{\mathbf{h}},R_{\mathbf{v}})$ is represented as a grid of bi-clusters as $(X,Y,g)$, $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{y\in Y}\xi(y)\neq\sum_{x\in X}\xi(x)$ for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$. In §7.2.1 and §7.2.2 we will discuss the cases when $X\cup Y$ is finite and infinite, respectively.

7.2.1 $X\cup Y$ is finite

If $X\cup Y$ is finite then, by Lemma 23, at least one of $X$ and $Y$ is such that all its members are bounded. Suppose, say, that every $x\in X$ is bounded, and let $Y^{\textit{b}}$ be the set of bounded members in $Y$. (The case when every $y\in Y$ is bounded is similar.)

We will define a formula $\mathsf{solution}_{{\mathfrak{F}}}$ that is satisfiable in ${\mathfrak{F}}$ (Lemma 27), and ‘forces’ a solution of $\Gamma^{{\mathfrak{F}}}$ when satisfied in a product of difference frames (Lemma 28). The formula $\mathsf{solution}_{{\mathfrak{F}}}$ will consist of three conjuncts: $\mathsf{upper\_bound}_{\mathfrak{F}}$ and $\mathsf{lower\_bound}_{\mathfrak{F}}$ will describe the respective upper and lower bound constraints on any possible solution, while $\mathsf{switch}_{\mathfrak{F}}$ will describe the interactions among switch bi-clusters in ${\mathfrak{F}}$. We also want $\mathsf{solution}_{{\mathfrak{F}}}$ to be a generalised Sahlqvist antecedent, and so it is a problem that the digraph $\mathcal{G}_{{\mathfrak{F}}}=(X\cup Y,E_{\mathfrak{F}})$ might contain cycles. The following claim says that we can always take a suitable acyclic subgraph of it:

Claim** 24****.**

If ${\mathfrak{F}}$ is finite and every $x\in X$ is bounded, then there is an acyclic subgraph $\mathcal{H}_{{\mathfrak{F}}}=(X\cup Y,E^{\textit{ub}}_{\mathfrak{F}})$ of $\mathcal{G}_{{\mathfrak{F}}}=(X\cup Y,E_{\mathfrak{F}})$ such that the following hold:

• (i)

Every initial node in $\mathcal{H}_{{\mathfrak{F}}}$ is either strict or belongs to $Y-Y^{\textit{b}}$.

• (ii)

$E^{\textit{ub}}_{\mathfrak{F}}$* contains all the $\to^{2}$-edges in $E_{\mathfrak{F}}$.*

• (iii)

For every edge $z\to^{1}z^{\prime}$ in $E_{\mathfrak{F}}$, there is an undirected path between $z$ and $z^{\prime}$ in $\mathcal{H}_{{\mathfrak{F}}}$ such that all edges in the path are $\to^{1}$ edges.

Proof.

Observe that by (42), (24) and (23), no strongly connected component $\mathcal{S}$ in $\mathcal{G}_{{\mathfrak{F}}}$ contain any $\to^{2}$ edge. So all cycles in $\mathcal{G}_{{\mathfrak{F}}}$ consists of $\to^{1}$ edges only. Observe also that if $y\in Y-Y^{\textit{b}}$, then (as all $x\in X$ are bounded) there are no edges in $E_{\mathfrak{F}}$ of the form $x\to^{\lambda}y$ for any $x\in X$. So either $y$ is an isolated node in $\mathcal{G}_{{\mathfrak{F}}}$, or there is an edge $y\to^{2}x$ in $E_{\mathfrak{F}}$ for some (maybe several) $x\in X$. In any case, the strongly connected component $y$ belongs to consists of just $y$ alone.

We give an algorithm for how to construct $E^{\textit{ub}}_{\mathfrak{F}}$ from $E_{\mathfrak{F}}$. For every strongly connected component $\mathcal{S}=(S,E_{\mathcal{S}})$ containing only bounded nodes, we define step-by-step a subset $E_{\mathcal{S}}^{-}$ of $E_{\mathcal{S}}$ such that $(S,E_{\mathcal{S}}^{-})$ is acyclic. First, we choose a node $z_{\mathcal{S}}$ in $\mathcal{S}$ as follows. If there is a strict node in $\mathcal{S}$, then let $z_{\mathcal{S}}$ be any of the strict nodes in $\mathcal{S}$. If there is no strict node in $\mathcal{S}$, then let $z_{\mathcal{S}}$ be any node in $\mathcal{S}$ such that there is a $\to^{2}$ edge in $\mathcal{G}_{{\mathfrak{F}}}$ starting at some bounded node and ending at $z_{\mathcal{S}}$. Let $X_{0}=\{z_{\mathcal{S}}\}$ and $E_{0}=\emptyset$. In the inductive step, take some $z\in S-X_{n}$, and consider any path $P$ within $\mathcal{S}$ from some node in $X_{n}$ to $z$ such that no other node in $P$ is in $X_{n}$. Let $E_{n+1}$ consist of the edges in $E_{n}$ plus the edges in $P$, and let $X_{n+1}$ be obtained from $X_{n}$ by adding all the nodes in $P$. Clearly, if $(X_{n},E_{n})$ is acyclic, then $(X_{n+1},E_{n+1})$ is acyclic as well. We do this until $X_{i}=\mathcal{S}$ for some $i$, and let $E_{\mathcal{S}}^{-}=E_{i}$.

Now let $E^{\textit{ub}}_{\mathfrak{F}}$ consist of the edges in $E_{\mathcal{S}}^{-}$ for each $\mathcal{S}$, plus all the $\to^{2}$-edges in $E_{\mathfrak{F}}$. It is easy to check that $\mathcal{H}_{{\mathfrak{F}}}$ is as required. ∎

The formula $\mathsf{upper\_bound}_{\mathfrak{F}}$

We will describe the ‘bounded’ part of $\mathcal{H}_{{\mathfrak{F}}}$, while also keeping track of the connections with the unbounded nodes in $Y-Y^{\textit{b}}$.

To begin with, we need to describe that the rows and columns of the grid-structure are pairwise disjoint. So for every $x\in X$ and every $y\in Y$, we introduce respective fresh propositional variables $\mathsf{x}$ and $\mathsf{y}$, and define the formulas

[TABLE]

Next, we need to describe strict nodes in $X\cup Y^{\textit{b}}$. Observe that, for every $n\in\mathbb{N}^{+}$ and every $n$-strict $x\in X$, there exist some $y^{\prime}\in Y$ and distinct $R_{\mathbf{h}}$-irreflexive points $a_{1}^{x},\dots,a_{n}^{x}$ in ${\mathfrak{F}}^{xy^{\prime}}$. Similarly, for every $n$-strict $y\in Y^{\textit{b}}$, there exist some $x^{\prime}\in X$ and distinct $R_{\mathbf{v}}$-irreflexive points $a_{1}^{y},\dots,a_{n}^{y}$ in ${\mathfrak{F}}^{x^{\prime}y}$. Thus, for every $n\in\mathbb{N}^{+}$ and every $n$-strict $z\in X\cup Y^{\textit{b}}$, we introduce fresh propositional variables $\mathsf{a}^{z}_{i}$ for $i=1,\dots,n$.

We also need to describe the switch bi-clusters in $\mathcal{H}_{{\mathfrak{F}}}$. To simplify notation, for all $z,z^{\prime}\in X\cup Y$, we will write

[TABLE]

and let

[TABLE]

Observe that for every $(x,y)\in\textit{Sw}_{{\mathfrak{F}}}$, ${\mathfrak{F}}^{xy}$ is a switch bi-cluster. Therefore, ${\mathfrak{F}}^{xy}$ contains a point $c^{xy}$ such that (i) $c^{xy}$ is    when ${\mathfrak{F}}^{xy}$ is of type (h2vsw) (that is, $x\to^{2}y$ is an edge in $\mathcal{H}_{{\mathfrak{F}}}$); (ii) $c^{xy}$ is    when ${\mathfrak{F}}^{xy}$ is of type (v2hsw) (that is, $y\to^{2}x$ is an edge in $\mathcal{H}_{{\mathfrak{F}}}$); and (iii) $c^{xy}$ is    when ${\mathfrak{F}}^{xy}$ is of type ($=$sw) (that is, either $x\to^{1}y$ or $y\to^{1}x$ is an edge in $\mathcal{H}_{{\mathfrak{F}}}$). Thus, for every $(x,y)\in\textit{Sw}_{{\mathfrak{F}}}$, we introduce a fresh propositional variable $\mathsf{c}^{{x}{y}}$, and define the formula

[TABLE]

Let $\mathcal{H}_{{\mathfrak{F}}}^{\textit{b}}$ be the induced subgraph of $\mathcal{H}_{{\mathfrak{F}}}$ on its bounded nodes, that is, on node set $X\cup Y^{\textit{b}}$. Starting at each strict node as root, we unravel $\mathcal{H}_{{\mathfrak{F}}}^{\textit{b}}$ into a forest (a disjoint union of directed rooted trees) $\mathcal{T}_{{\mathfrak{F}}}$, where each branch of each tree is continued until it reaches either a strict node different from the root or, if there is no such on the branch, a final node in $\mathcal{H}_{{\mathfrak{F}}}^{\textit{b}}$. So for each node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$ there is a unique $z\in X\cup Y^{\textit{b}}$ such that $q$ is a(n unravelled) copy of $z$. (Each $z\in X\cup Y^{\textit{b}}$ might have many different copies.) For every node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$, we let $\mathcal{T}_{{\mathfrak{F}}}({q})$ denote the set of its children in $\mathcal{T}_{{\mathfrak{F}}}$.

For every node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$, now we define a formula $\mathsf{tree}({q})$ by induction on the structure of $\mathcal{T}_{{\mathfrak{F}}}$ starting at its leaves:

• •

If $q$ is not a root in $\mathcal{T}_{{\mathfrak{F}}}$, then there is a unique $q^{\ast}$ with $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\ast}})$. There are two cases:

If $q$ is a copy of $x\in X$ and $q^{\ast}$ is a copy of $y^{\ast}\in Y^{\textit{b}}$, then let

[TABLE]

If $q$ is a copy of $y\in Y^{\textit{b}}$ and $q^{\ast}$ is a copy of $x^{\ast}\in X$, then let

[TABLE]

• •

If $q$ is a root in $\mathcal{T}_{{\mathfrak{F}}}$, then $q$ is a copy of some $n$-strict $z\in X\cup Y^{\textit{b}}$ for some $n\in\mathbb{N}^{+}$. Again, there are two cases:

If $z$ is some $x\in X$, then for each $i=1,\dots,n$, let

[TABLE]

and then let

[TABLE]

If $z$ is some $y\in Y^{\textit{b}}$, then for each $i=1,\dots,n$, let

[TABLE]

and then let

[TABLE]

Finally, let $\mathsf{upper\_bound}_{\mathfrak{F}}$ be the conjunction of $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{tree}({q})$ for all roots $q$ in the forest $\mathcal{T}_{{\mathfrak{F}}}$ (see Example 32 below).

The ‘interaction’ formula $\mathsf{switch}_{\mathfrak{F}}$

We use the variables introduced for the formula $\mathsf{upper\_bound}_{\mathfrak{F}}$. For every $x\in X$ and every $y\in Y^{\textit{b}}$, we define the respective formulas

[TABLE]

[TABLE]

and let $\mathsf{switch}_{\mathfrak{F}}$ be the conjunction of $\mathsf{switch}_{\mathfrak{F}}^{z}$, for all $z\in X\cup Y^{\textit{b}}$ (see Example 32 below).

The formula $\mathsf{lower\_bound}_{\mathfrak{F}}$

We use the $\mathsf{c}^{{x}{y}}$ variables introduced for $\mathsf{upper\_bound}_{\mathfrak{F}}$, and will also introduce some fresh variables.

Observe that by (19) and (42), for every $z\in X\cup Y$, we have $\textit{min}\,({z})\in\mathbb{N}^{+}$ and either \bigl{(}z=\textit{min}\,({z})\bigr{)}$$\in\Gamma^{{\mathfrak{F}}} or \bigl{(}z\geq\textit{min}\,({z})\bigr{)}\in\Gamma^{{\mathfrak{F}}}. So if $x\in X$, then there is $y_{x}\in Y$ such that \textit{h\_size}\bigl{(}{\mathfrak{F}}^{xy_{x}}\bigr{)}=\textit{min}\,({x}), and so there are $R_{\mathbf{h}}$-reflexive points $b_{1}^{\circ}(x)$, $\dots$, $b_{r_{x}}^{\circ}(x)$ and $R_{\mathbf{h}}$-irreflexive points $b_{1}^{\bullet}(x)$, $\dots$, $b_{i_{x}}^{\bullet}(x)$ in ${\mathfrak{F}}^{xy_{x}}$ such that $2r_{x}+i_{x}=\textit{min}\,({x})$. Similarly, if $y\in Y$, then there is $x_{y}\in X$ such that \textit{v\_size}\bigl{(}{\mathfrak{F}}^{x_{y}y}\bigr{)}=\textit{min}\,({y}), and so there are $R_{\mathbf{v}}$-reflexive points $b_{1}^{\circ}(y),\dots,b_{r_{y}}^{\circ}(y)$ and $R_{\mathbf{v}}$-irreflexive points $b_{1}^{\bullet}(y),\dots,b_{i_{y}}^{\bullet}(y)$ in ${\mathfrak{F}}^{x_{y}y}$ such that $2r_{y}+i_{y}=\textit{min}\,({y})$.

Now recall the function $\xi_{\textit{min}}^{{\mathfrak{F}}}$ from (26). As $\xi_{\textit{min}}^{{\mathfrak{F}}}$ is a solution of $\Gamma^{{\mathfrak{F}}}$ by Claim 12.2, it follows from (42) that $\xi_{\textit{min}}^{{\mathfrak{F}}}(z)\in\mathbb{N}^{+}$, for every $z\in X\cup Y$. We define

[TABLE]

For every $z\in X_{\textit{lb}}\cup Y_{\textit{lb}}\cup(Y-Y^{\textit{b}})$, we introduce fresh propositional variables $\mathsf{b}_{j}^{\circ}(z)$ for $j=1,\dots,r_{z}$, and $\mathsf{b}_{s}^{\bullet}(z)$ for $s=1,\dots,i_{z}$, and define the formulas

[TABLE]

For every $x\in X_{\textit{lb}}$, we define

[TABLE]

and for every $y\in Y_{\textit{lb}}\cup(Y-Y^{\textit{b}})$, we define

[TABLE]

Let $\mathsf{lower\_bound}_{\mathfrak{F}}$ be the conjunction of $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{lower\_bound}_{\mathfrak{F}}^{z}$, for all $z\in X_{\textit{lb}}\cup Y_{\textit{lb}}\cup(Y-Y^{\textit{b}})$ (see Example 32 below).

The formula $\mathsf{solution}_{{\mathfrak{F}}}$

We let

[TABLE]

Lemma** 25****.**

It is decidable whether a bimodal formula is of the form $\mathsf{solution}_{{\mathfrak{F}}}$ for some finite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ for which every $X\cup Y$ is bounded, $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{y\in Y}\xi(y)\neq\sum_{x\in X}\xi(x)$ for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$.

It is also decidable whether a bimodal formula is of the form $\mathsf{solution}_{{\mathfrak{F}}}$ for some finite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ for which every $x\in X$ is bounded, there is some unbounded $y^{\star}\in Y$, $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{x\in X}\xi(x)$ $<\sum_{y\in Y}\xi(y)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$.

Proof.

It is not hard to check that $\mathsf{solution}_{{\mathfrak{F}}}$ only depends on

• •

the finite acyclic digraph $\mathcal{H}_{{\mathfrak{F}}}$ and the types of bi-clusters corresponding to its edges,

• •

the values $\textit{min}\,({z})\in\mathbb{N}^{+}$ for all nodes $z$ in $\mathcal{H}_{{\mathfrak{F}}}$, and

• •

which nodes in $\mathcal{H}_{{\mathfrak{F}}}$ are strict.

An inspection of the proof of Claim 24 shows that it is decidable whether $\mathcal{H}_{{\mathfrak{F}}}$ is obtained from some finite edge-labelled digraph $\mathcal{G}$ with designated strict nodes and $\textit{min}\,({z})$ values. And it is clearly decidable whether such a $\mathcal{G}$ can be obtained as $\mathcal{G}_{{\mathfrak{F}}}$ for some finite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ as described. ∎

Lemma** 26****.**

$\mathsf{solution}_{{\mathfrak{F}}}$* is a generalised Sahlqvist antecedent.*

Proof.

It is straightforward to check that $\mathsf{solution}_{{\mathfrak{F}}}$ is a potential generalised Sahlqvist antecedent. We show that the dependency digraph $\mathcal{D}(\mathsf{solution}_{{\mathfrak{F}}})$ of $\mathsf{solution}_{{\mathfrak{F}}}$ is acyclic. To this end, observe that the nodes of $\mathcal{D}(\mathsf{solution}_{{\mathfrak{F}}})$ are among the $\mathsf{c}^{{x}{y}}$ variables occurring in $\mathsf{switch}_{\mathfrak{F}}$, and we have the following edges $\Rrightarrow$ in $\mathcal{D}(\mathsf{solution}_{{\mathfrak{F}}})$:

[TABLE]

We claim that if $Q$ is a path of length $>0$ in $\mathcal{D}(\mathsf{solution}_{{\mathfrak{F}}})$ from some $\mathsf{c}^{{x}{y}}$ to some $\mathsf{c}^{{x^{\prime}}{y^{\prime}}}$, then either there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $x$ to $x^{\prime}$, or there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $y$ to $y^{\prime}$. Indeed, we show this by induction on the length $\ell$ of $Q$. If $\ell=1$ then this follows from (55)–(56). So suppose $\ell>0$ and $Q$ is $Q^{-}$ followed by an edge of the form, say, $\mathsf{c}^{{x^{\prime}}{y^{\prime\prime}}}\Rrightarrow\mathsf{c}^{{x^{\prime}}{y^{\prime}}}$ for some $y^{\prime\prime}\in Y$. (The other case is similar.) By the IH, there are two cases: (i) either there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $x$ to $x^{\prime}$, in which case we are done, (ii) or there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $y$ to $y^{\prime\prime}$. As we also have $y^{\prime\prime}\to x^{\prime}\to y^{\prime}$ by (55), we have a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $y$ to $y^{\prime}$, as required.

Now suppose indirectly that there is a cycle in the dependency digraph of $\mathsf{solution}_{{\mathfrak{F}}}$. Choose an arbitrary edge in this cycle of the form, say, $\mathsf{c}^{{x}{y}}\Rrightarrow\mathsf{c}^{{x^{\prime}}{y}}$ for some $x,x^{\prime}\in X$, $y\in Y$. (The other case is similar.) Then $x\to y\to x^{\prime}$ holds by (56). Also, either there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $x^{\prime}$ to $x$, or there is a path of length $>0$ in $\mathcal{H}_{{\mathfrak{F}}}$ from $y$ to $y$. In both cases, we have a cycle in $\mathcal{H}_{{\mathfrak{F}}}$, contradicting that it is acyclic by Claim 24. ∎

Lemma** 27****.**

If a grid of bi-clusters ${\mathfrak{F}}_{1}=(X_{1},Y_{1},g_{1})$ contains ${\mathfrak{F}}$ as a subgrid, then $\mathsf{solution}_{{\mathfrak{F}}}$ is satisfiable in ${\mathfrak{F}}_{1}$.

Proof.

We use the notation introduced in the definition of $\mathsf{solution}_{{\mathfrak{F}}}$. We define a model ${\mathfrak{M}}$ on ${\mathfrak{F}}_{1}$ by taking

[TABLE]

It is not hard to check that $\mathsf{solution}_{{\mathfrak{F}}}$ is satisfied in ${\mathfrak{M}}$. ∎

Lemma** 28****.**

Suppose ${\mathfrak{M}},(u,v)\models\mathsf{solution}_{{\mathfrak{F}}}$ for some point $(u,v)$ in a model ${\mathfrak{M}}$ over a product frame $(U,\neq_{U})\!\times\!(V,\neq_{V})$. Then for every $x\in X$ there is a set $\textit{Set}({x})\subseteq U$, and for every $y\in Y$ there is a set $\textit{Set}({y})\subseteq V$ such that the following hold, for every $z\in X\cup Y$:

• (i)

$\textit{Set}({z})\cap\textit{Set}({z^{\prime}})=\emptyset$* whenever $z\neq z^{\prime}$; $z,z^{\prime}\in X$ or $z,z^{\prime}\in Y$.*

• (ii)

If $z\in X\cup Y^{\textit{b}}$ then we can ‘identify’ points outside $\textit{Set}({z})$ with a positive formula. In particular:

If $z=x\in X$ then for all $a\in U-\textit{Set}({x})$,

[TABLE]

If $z=y\in Y^{\textit{b}}$ then for all $b\in V-\textit{Set}({y})$,

[TABLE]

• (iii)

$\xi$* is a solution of $\Gamma^{{\mathfrak{F}}}$, where $\xi(z)=|\textit{Set}({z})|$, for $z\in X\cup Y$.*

Proof.

The argument uses a series of claims. To begin with, for every node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$ we will define, inductively on the height of $q$ in $\mathcal{T}_{{\mathfrak{F}}}$, a set $\textit{Gen}({q})\subseteq U\!\times\!V$ such that, for every $q$, and every $(a,b)\in\textit{Gen}({q})$,

[TABLE]

• •

If $q$ is a root and a copy of some $n$-strict $z\in X\cup Y^{\textit{b}}$, then $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{tree}({q})$ is a conjunct of $\mathsf{upper\_bound}_{\mathfrak{F}}$, and so there is $(a,b)$ with ${\mathfrak{M}},(a,b)\models\mathsf{tree}({q})$.

So if $z=x\in X$, then there are distinct $a_{1},\dots,a_{n}\in U$ such that ${\mathfrak{M}},(a_{i},b)\models\mathsf{tree}_{i}({q})$ for $i=1,\dots,n$. Let $\textit{Gen}({q})=\{(a_{1},b),\dots,(a_{n},b)\}$. Then (57) holds for every $(a,b)\in\textit{Gen}({q})$. Observe that

[TABLE]

Also,

[TABLE]

Similarly, if $z=y\in Y^{\textit{b}}$, then there are distinct $b_{1},\dots,b_{n}\in V$ such that ${\mathfrak{M}},(a,b_{i})\models\mathsf{tree}_{i}({u})$ for $i=1,\dots,n$. Let $\textit{Gen}({q})=\{(a,b_{1}),\dots,(a,b_{n})\}$. Then (58) holds for every $(a,b)\in\textit{Gen}({q})$.

• •

If $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\ast}})$, $q$ is a copy of some $x\in X$ and $q^{\ast}$ is a copy of some $y^{\ast}\in Y^{\textit{b}}$ then, by (58) of the IH, we have ${\mathfrak{M}},(a,b)\models\Diamond_{\mathbf{h}}\mathsf{tree}({q})$ for every $(a,b)\in\textit{Gen}({q^{\ast}})$. Thus, for every $(a,b)\in\textit{Gen}({q^{\ast}})$, there is some $a^{\prime}\in U$ with ${\mathfrak{M}},(a^{\prime},b)\models\mathsf{tree}({q})$. Let $\textit{Gen}({q})=\{(a^{\prime},b):(a,b)\in\textit{Gen}({q^{\ast}})\}$. Then (57) holds for every $(a,b)\in\textit{Gen}({q})$. Observe that

[TABLE]

Similarly, if $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\ast}})$, $q$ is a copy of some $y\in Y^{\textit{b}}$ and $q^{\ast}$ is a copy of some $x^{\ast}\in X$ then, by (57) of the IH, we have ${\mathfrak{M}},(a,b)\models\Diamond_{\mathbf{v}}\mathsf{tree}({q})$ for every $(a,b)\in\textit{Gen}({q^{\ast}})$. Thus, for every $(a,b)\in\textit{Gen}({q^{\ast}})$, there is some $b^{\prime}\in V$ with ${\mathfrak{M}},(a,b^{\prime})\models\mathsf{tree}({q})$. Let $\textit{Gen}({q})=\{(a,b^{\prime}):(a,b)\in\textit{Gen}({q^{\ast}})\}$. Then (58) holds for every $(a,b)\in\textit{Gen}({q})$.

Observe that

[TABLE]

Next, for every node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$ that is a copy of some $x\in X$, we let

[TABLE]

for every node $q$ that is a copy of some $y\in Y^{\textit{b}}$, we let

[TABLE]

Observe that

[TABLE]

Claim** 28.1****.**

For every node $q$ in $\mathcal{T}_{{\mathfrak{F}}}$, the following hold:

• (i)

If $q$ is a root and a copy of some $n$-strict $x\in X$, then ${\mathfrak{M}},(a^{\ast},v)\models\Diamond_{\mathbf{v}}^{+}\bigwedge_{i=1}^{n}\mathsf{a}^{x}_{i}$ for all $a^{\ast}\in U-\textit{Set}({q})$.

If $q$ is a root and a copy of some $n$-strict $y\in Y^{\textit{b}}$, then ${\mathfrak{M}},(u,b^{\ast})\models\Diamond_{\mathbf{h}}^{+}\bigwedge_{i=1}^{n}\mathsf{a}^{y}_{i}$ for all $b^{\ast}\in V-\textit{Set}({q})$.

• (ii)

If $q$ is a copy of some $x\in X$, $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime}})$, and $q^{\prime}$ is a copy of some $y^{\prime}\in Y^{\textit{b}}$, then ${\mathfrak{M}},(a^{\ast},v)\models\Box_{\mathbf{v}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ for all $a^{\ast}\in U-\textit{Set}({q})$.

If $q$ is a copy of some $y\in Y^{\textit{b}}$, $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime}})$, and $q^{\prime}$ is a copy of some $x^{\prime}\in X$, then ${\mathfrak{M}},(u,b^{\ast})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x^{\prime}}{y}}$ for all $b^{\ast}\in V-\textit{Set}({q})$.

Proof.

We prove the claim by induction on the height of $q$ in $\mathcal{T}_{{\mathfrak{F}}}$.

(i): Suppose $q$ is a root and a copy of some $n$-strict $x\in X$, and take some $a^{\ast}\in U-\textit{Set}({q})$. By (59), there is $b$ such that for every $1\leq i\leq n$ there is $(a_{i},b)\in\textit{Gen}({q})$ with ${\mathfrak{M}},(a_{i},b)\models\mathsf{tree}_{i}({q})$. As $\Box_{\mathbf{h}}\mathsf{a}^{x}_{i}$ is a conjunct of $\mathsf{tree}_{i}({q})$, we have ${\mathfrak{M}},(a_{i},b)\models\Box_{\mathbf{h}}\mathsf{a}^{x}_{i}$ for every $1\leq i\leq n$. As by (64) $a_{i}\in\textit{Set}({q})$ for every $1\leq i\leq n$, we have that $a^{\ast}\neq a_{i}$ for any $i$, and so ${\mathfrak{M}},(a^{\ast},b)\models\bigwedge_{i=1}^{n}\mathsf{a}^{x}_{i}$. The case when $q$ is a copy of some $n$-strict $y\in Y^{\textit{b}}$ is similar.

(ii): Suppose $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime}})$, $q$ is a copy of some $x\in X$, $q^{\prime}$ is a copy of some $y^{\prime}\in Y^{\textit{b}}$. (The case when $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime}})$, $q$ is a copy of some $y\in Y^{\textit{b}}$ and $q^{\prime}$ is a copy of some $x^{\prime}\in X$ is similar.) Suppose inductively that we have (i)–(ii) for $q^{\prime}$, and take some $a^{\ast}\in U-\textit{Set}({q})$. We claim that

[TABLE]

implying ${\mathfrak{M}},(a^{\ast},v)\models\Box_{\mathbf{v}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$, as required. Indeed, take some $b^{\ast}\in V$. There are two cases, either $b^{\ast}\in\textit{Set}({q^{\prime}})$ or $b^{\ast}\notin\textit{Set}({q^{\prime}})$. If $b^{\ast}\in\textit{Set}({q^{\prime}})$ then there is some $a$ such that $(a,b^{\ast})\in\textit{Gen}({q^{\prime}})$ by (65). Thus, there is $a^{\prime}$ such that $(a^{\prime},b^{\ast})\in\textit{Gen}({q})$ by (61), and so ${\mathfrak{M}},(a^{\prime},b^{\ast})\models\mathsf{tree}({q})$ by (63). As $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ is a conjunct of $\mathsf{tree}({q})$, we also have ${\mathfrak{M}},(a^{\prime},b^{\ast})\models\hat{\mathsf{c}}^{{x}{y^{\prime}}}$. As $q\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime}})$, we have $y^{\prime}\to x$. Thus, $\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}$ is a conjunct of $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$, and so ${\mathfrak{M}},(a^{\prime},b^{\ast})\models\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}$ as well. As $a^{\ast}\notin\textit{Set}({q})$ but $a^{\prime}\in\textit{Set}({q})$ by (64), it follows that $a^{\prime}\neq a^{\ast}$, and so (67) holds.

If $b^{\ast}\notin\textit{Set}({q^{\prime}})$ then suppose first that $q^{\prime}$ is a root, that is, $y^{\prime}$ is $n$-strict for some $n\in\mathbb{N}^{+}$. By item (i) of the IH, ${\mathfrak{M}},(u,b^{\ast})\models\Diamond_{\mathbf{h}}^{+}\bigwedge_{i=1}^{n}\mathsf{a}^{y^{\prime}}_{i}$. As $y^{\prime}\to x$ holds, ${\mathfrak{M}},(u,b^{\ast})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ follows by (52), and so (67) holds. Finally, suppose that $q^{\prime}$ is not a root. Let $q^{\prime\prime}$ be such that $q^{\prime}\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime\prime}})$, and suppose that $q^{\prime\prime}$ is a copy of some $x^{\prime\prime}\in X$. Then ${\mathfrak{M}},(u,b^{\ast})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x^{\prime\prime}}{y^{\prime}}}$ by item (ii) of the IH. As $x^{\prime\prime}\to y^{\prime}\to x$ holds, ${\mathfrak{M}},(u,b^{\ast})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ follows by (52). Thus, (67) holds in this case as well. ∎

Claim** 28.2****.**

For all nodes $q,q^{\prime}$ in $\mathcal{T}_{{\mathfrak{F}}}$, the following hold:

• (i)

If $q^{\prime}\to^{2}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$ then $|\textit{Set}({q^{\prime}})|\geq 2\cdot|\textit{Set}({q})|$.

• (ii)

If $q^{\prime}\to^{1}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$ then $|\textit{Set}({q})|=|\textit{Set}({q^{\prime}})|$.

Proof.

Suppose $q^{\prime}\to^{\lambda}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$ for some $\lambda$, $q$ is a copy of some $x\in X$, $q^{\prime}$ is a copy of some $y^{\prime}\in Y^{\textit{b}}$. (The case when $q$ is a copy of some $y\in Y^{\textit{b}}$ and $q^{\prime}$ is a copy of some $x\in X$ is similar.) By (64), for every $a\in\textit{Set}({q})$ there is $b_{a}$ with $(a,b_{a})\in\textit{Gen}({q})$. Then ${\mathfrak{M}},(a,b_{a})\models\mathsf{tree}({q})$ by (63). As $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ is a conjunct of $\mathsf{tree}({q})$, we also have ${\mathfrak{M}},(a,b_{a})\models\hat{\mathsf{c}}^{{x}{y^{\prime}}}$. By (65), we have

[TABLE]

(i): As $q^{\prime}\to^{2}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$, $y^{\prime}\to^{2}x$ is an edge in $\mathcal{H}_{{\mathfrak{F}}}$. Thus, $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ implies $\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}\land\Diamond_{\mathbf{v}}(\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}})$ (see (46)), and so ${\mathfrak{M}},(a,b_{a})\models\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}\land\Diamond_{\mathbf{v}}(\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}})$. So for every $a\in\textit{Set}({q})$, there is also a $b^{\prime}_{a}\neq b_{a}$ with ${\mathfrak{M}},(a,b^{\prime}_{a})\models\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}$. Therefore

[TABLE]

We claim that

[TABLE]

Indeed, suppose indirectly that $b^{\prime}_{a}\notin\textit{Set}({q^{\prime}})$ for some $a\in\textit{Set}({q})$. There are two cases: If $q^{\prime}$ is a root and $y^{\prime}$ is $n$-strict for some $n\in\mathbb{N}^{+}$, then ${\mathfrak{M}},(u,b^{\prime}_{a})\models\Diamond_{\mathbf{h}}^{+}\bigwedge_{i=1}^{n}\mathsf{a}^{y^{\prime}}_{i}$ by Claim 28.1 (i). As $y^{\prime}\to x$ holds, ${\mathfrak{M}},(u,b_{a}^{\prime})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ follows by (52), contradicting ${\mathfrak{M}},(a,b^{\prime}_{a})\models\neg\mathsf{c}^{{x}{y^{\prime}}}$. If $q^{\prime}\in\mathcal{T}_{{\mathfrak{F}}}({q^{\prime\prime}})$ for some $q^{\prime\prime}$ and $q^{\prime\prime}$ is a copy of some $x^{\prime\prime}\in X$, then by Claim 28.1 (ii) we have that ${\mathfrak{M}},(u,b^{\prime}_{a})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x^{\prime\prime}}{y^{\prime}}}$. As $x^{\prime\prime}\to y^{\prime}\to x$ holds, ${\mathfrak{M}},(u,b^{\prime}_{a})\models\Box_{\mathbf{h}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ follows by (52), a contradiction again, proving (70). Now $|\textit{Set}({q^{\prime}})|\geq 2\cdot|\textit{Set}({q})|$ follows by (68), (69) and (70).

(ii): As $q^{\prime}\to^{1}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$, $y^{\prime}\to^{1}x$ is an edge in $\mathcal{H}_{{\mathfrak{F}}}$. So $\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}$ is a conjunct of $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$, and so ${\mathfrak{M}},(a,b_{a})\models\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y^{\prime}}}$ as well. So if $a_{1}\neq a_{2}\in\textit{Set}({q})$ then $b_{a_{1}}\neq b_{a_{2}}$ must hold, and so $|\textit{Set}({q})|\leq|\textit{Set}({q^{\prime}})|$ by (68). On the other hand, by (65) and (64), for every $b\in\textit{Set}({q^{\prime}})$ there is $a_{b}\in\textit{Set}({q})$ such that $(a_{b},b)\in\textit{Gen}({q})$, and so ${\mathfrak{M}},(a_{b},b)\models\mathsf{tree}({q})$ by (63). As $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ is a conjunct of $\mathsf{tree}({q})$, we also have ${\mathfrak{M}},(a_{b},b)\models\hat{\mathsf{c}}^{{x}{y^{\prime}}}$. As $\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{v}}\mathsf{c}^{{x}{y^{\prime}}}$ is a conjunct of $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$, we have ${\mathfrak{M}},(a_{b},b)\models\neg\mathsf{c}^{{x}{y^{\prime}}}\land\Box_{\mathbf{v}}\mathsf{c}^{{x}{y^{\prime}}}$ as well. So if $b_{1}\neq b_{2}\in\textit{Set}({q^{\prime}})$ then $a_{b_{1}}\neq a_{b_{2}}$ must hold, and so $|\textit{Set}({q^{\prime}})|\leq|\textit{Set}({q})|$. ∎

Claim** 28.3****.**

For all nodes $q_{1},q_{2}$ in $\mathcal{T}_{{\mathfrak{F}}}$, if $q_{1}$ and $q_{2}$ are both copies of the same $z\in X\cup Y^{\textit{b}}$, then $\textit{Set}({q_{1}})=\textit{Set}({q_{2}})$.

Proof.

Clearly, it is enough to show that $\textit{Set}({q_{1}})\subseteq\textit{Set}({q_{2}})$. Suppose that $q_{1}\neq q_{2}$ are both copies of the same $x\in X$, and there is some $a\in\textit{Set}({q_{1}})-\textit{Set}({q_{2}})$. (The case when $q_{1}\neq q_{2}$ are both copies of the same $y\in Y^{\textit{b}}$ is similar.) As $a\in\textit{Set}({q_{1}})$, there is $b$ with $(a,b)\in\textit{Gen}({q_{1}})$ by (64). It cannot be that both $q_{1}$ and $q_{2}$ are roots in $\mathcal{T}_{{\mathfrak{F}}}$, so there are three cases:

If $q_{1}$ is a root and $q_{2}$ is not a root. Then suppose $x$ is $n$-strict for some $n\in\mathbb{N}^{+}$, $q_{2}\in\mathcal{T}_{{\mathfrak{F}}}({q_{2}^{\prime}})$, and $q_{2}^{\prime}$ is a copy of some $y^{\prime\prime}\in Y^{\textit{b}}$. So by (60) there exist $1\leq i\leq n$ such that ${\mathfrak{M}},(a,b)\models\mathsf{tree}_{i}({q_{1}})$. As $y^{\prime\prime}\to x$ holds, $\Diamond_{\mathbf{v}}\neg\mathsf{c}^{{x}{y^{\prime\prime}}}$ is a conjunct of $\mathsf{tree}_{i}({q_{1}})$, and so ${\mathfrak{M}},(a,b)\models\Diamond_{\mathbf{v}}\neg\mathsf{c}^{{x}{y^{\prime\prime}}}$. On the other hand, as $a\notin\textit{Set}({q_{2}})$, by Claim 28.1 (ii) we have $(a,v)\models\Box_{\mathbf{v}}^{+}\mathsf{c}^{{x}{y^{\prime\prime}}}$, a contradiction.

If $q_{2}$ is a root and $q_{1}$ is not a root. Again, suppose $x$ is $n$-strict for some $n\in\mathbb{N}^{+}$, $q_{1}\in\mathcal{T}_{{\mathfrak{F}}}({q_{1}^{\prime}})$, and $q_{1}^{\prime}$ is a copy of some $y^{\prime}\in Y^{\textit{b}}$. We have ${\mathfrak{M}},(a,b)\models\mathsf{tree}({q_{1}})$ by (63). As $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ is a conjunct of $\mathsf{tree}({q_{1}})$, we have ${\mathfrak{M}},(a,b)\models\hat{\mathsf{c}}^{{x}{y^{\prime}}}$. As $\neg\mathsf{c}^{{x}{y^{\prime}}}$ is a conjunct of $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$, we have ${\mathfrak{M}},(a,b)\models\neg\mathsf{c}^{{x}{y^{\prime}}}$. On the other hand, as $a\notin\textit{Set}({q_{2}})$, by Claim 28.1 (i) we have ${\mathfrak{M}},(a,v)\models\Diamond_{\mathbf{v}}^{+}\bigwedge_{i=1}^{n}\mathsf{a}^{x}_{i}$. As $y^{\prime}\to x$ holds, ${\mathfrak{M}},(a,v)\models\Box_{\mathbf{v}}^{+}\mathsf{c}^{{x}{y^{\prime}}}$ by (49), a contradiction.

If neither $q_{1}$ nor $q_{2}$ is a root. Then suppose $q_{1}\in\mathcal{T}_{{\mathfrak{F}}}({q_{1}^{\prime}})$, $q_{2}\in\mathcal{T}_{{\mathfrak{F}}}({q_{2}^{\prime}})$, $q_{1}^{\prime}$ is a copy of $y^{\prime}\in Y^{\textit{b}}$, and $q_{2}^{\prime}$ is a copy of $y^{\prime\prime}\in Y^{\textit{b}}$. We have ${\mathfrak{M}},(a,b)\models\mathsf{tree}({q_{1}})$ by (63). As $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$ is a conjunct of $\mathsf{tree}({q_{1}})$, we have ${\mathfrak{M}},(a,b)\models\hat{\mathsf{c}}^{{x}{y^{\prime}}}$. As $\neg\mathsf{c}^{{x}{y^{\prime}}}$ is a conjunct of $\hat{\mathsf{c}}^{{x}{y^{\prime}}}$, we have ${\mathfrak{M}},(a,b)\models\neg\mathsf{c}^{{x}{y^{\prime}}}$. On the other hand, as $a\notin\textit{Set}({q_{2}})$, by Claim 28.1 (ii) we have ${\mathfrak{M}},(a,v)\models\Box_{\mathbf{v}}^{+}\mathsf{c}^{{x}{y^{\prime\prime}}}$. If $y^{\prime}=y^{\prime\prime}$, this is a contradiction. If $y^{\prime}\neq y^{\prime\prime}$ then $\Diamond_{\mathbf{v}}\neg\mathsf{c}^{{x}{y^{\prime\prime}}}$ is a conjunct of $\mathsf{tree}({q_{1}})$, and so ${\mathfrak{M}},(a,b)\models\Diamond_{\mathbf{v}}\neg\mathsf{c}^{{x}{y^{\prime\prime}}}$, a contradiction again. ∎

Next, for every $z\in X\cup Y$, we will define $\textit{Set}({z})$. There are two cases:

• •

If $z\in X\cup Y^{\textit{b}}$, then let

[TABLE]

This is well-defined, as $\mathcal{T}_{{\mathfrak{F}}}$ contains some copy of every $z\in X\cup Y^{\textit{b}}$, and the definition does not depend on the choice of the particular copy by Claim 28.3.

• •

If $y\in Y-Y^{\textit{b}}$ then $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{lower\_bound}_{\mathfrak{F}}^{y}$ is a conjunct of $\mathsf{lower\_bound}_{\mathfrak{F}}$, and so there exist $a\in U$ and distinct $b_{1},\dots,b_{2r_{y}},b_{1}^{\prime},\dots,b_{i_{y}}^{\prime}\in V$ such that

[TABLE]

We let

[TABLE]

As $2r_{y}+i_{y}=\xi_{\textit{min}}^{{\mathfrak{F}}}(y)$, we have that

[TABLE]

Next, for each $x\in X$ such that $y\to^{2}x$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$, we will define a set $\textit{Set}^{x}({y})$ such that

[TABLE]

To this end, first we claim that

[TABLE]

Indeed, there are two cases. If $x$ is $n$-strict for some $n\in\mathbb{N}^{+}$, then choose a copy $q$ of $x$ that is a root in $\mathcal{T}_{{\mathfrak{F}}}$. Then by (59) and (60), there are distinct $a_{1},\dots,a_{k}\in U$ and $b\in V$ such that $(a_{i},b)\in\textit{Gen}({q})$, and so ${\mathfrak{M}},(a_{i},b)\models\mathsf{tree}_{i}({q})$, for all $1\leq i\leq n$. As $\Diamond_{\mathbf{v}}\hat{\mathsf{c}}^{{x}{y}}$ is a conjunct of $\mathsf{tree}_{i}({q})$ for every $1\leq i\leq n$, (77) follows. If $x$ is not strict, then choose a copy $q$ of $x$ that is not a root in $\mathcal{T}_{{\mathfrak{F}}}$. By (63), ${\mathfrak{M}},(a,b)\models\mathsf{tree}({q})$ for every $(a,b)\in\textit{Gen}({q})$. As $\Diamond_{\mathbf{v}}\hat{\mathsf{c}}^{{x}{y}}$ is a conjunct of $\mathsf{tree}({q})$, again we have (77).

As $y\to^{2}x$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$, $\hat{\mathsf{c}}^{{x}{y}}$ implies \Diamond_{\mathbf{v}}\bigl{(}\overline{\mathsf{y}}\land\neg\mathsf{c}^{{x}{y}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y}}\land\Diamond_{\mathbf{v}}(\overline{\mathsf{y}}\land\neg\mathsf{c}^{{x}{y}}\land\Box_{\mathbf{h}}\mathsf{c}^{{x}{y}})\bigr{)} (see (46)). So by (77), (64) and (71), for every $a\in\textit{Set}({x})$ there are $b_{a}\neq b_{a}^{\prime}\in V$ such that

[TABLE]

We let

[TABLE]

Clearly, if $a_{1},a_{2}\in\textit{Set}({x})$ and $a_{1}\neq a_{2}$, then $b_{a_{1}}$, $b_{a_{1}}^{\prime}$, $b_{a_{2}}$, and $b_{a_{2}}^{\prime}$ are four distinct points, and so (76) follows, as required.

Finally, let

[TABLE]

Thus, by (75) and (76), respectively, we obtain that

[TABLE]

Claim** 28.4****.**

For all $z,z^{\prime}\in X\cup Y$, the following hold:

• (i)

If $z$ is $n$-strict for some $n\in\mathbb{N}^{+}$, then $|\textit{Set}({z})|=n$.

• (ii)

If $z^{\prime}\to^{2}z$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$, then $|\textit{Set}({z^{\prime}})|\geq 2\cdot|\textit{Set}({z})|$.

• (iii)

If $z$ and $z^{\prime}$ are in the same strongly connected component of $\mathcal{G}_{{\mathfrak{F}}}$, then $|\textit{Set}({z})|=|\textit{Set}({z^{\prime}})|$.

• (iv)

$|\textit{Set}({z})|\geq\xi_{\textit{min}}^{{\mathfrak{F}}}(z)$.

Proof.

Item (i) is by (66).

(ii): If $z,z^{\prime}\in X\cup Y^{\textit{b}}$, then there are nodes $q$ and $q^{\prime}$ in $\mathcal{T}_{{\mathfrak{F}}}$ such that $q$ is a copy of $z$, $q^{\prime}$ is a copy of $z^{\prime}$, and $q^{\prime}\to^{2}q$ is an edge in $\mathcal{T}_{{\mathfrak{F}}}$. So $|\textit{Set}({z^{\prime}})|\geq 2\cdot|\textit{Set}({z})|$ follows by Claim 28.2 (i). If $z^{\prime}=y\in Y-Y^{\textit{b}}$ and $z=x\in X$, then $y\to^{2}x$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$. So $|\textit{Set}({y})|\geq 2\cdot|\textit{Set}({x})|$ follows by (81).

(iii): Suppose $z\neq z^{\prime}$. Then $z,z^{\prime}\in X\cup Y^{\textit{b}}$, and by Claim 24 (iii), there is an undirected path $P$ in $\mathcal{H}_{{\mathfrak{F}}}$ between $z$ and $z^{\prime}$ such that all edges in the path are $\to^{1}$ edges. We can break $P$ up to a union of directed paths in $\mathcal{H}_{{\mathfrak{F}}}$ (each of which has copies in the unravelling $\mathcal{T}_{{\mathfrak{F}}}$), and then $|\textit{Set}({z})|=|\textit{Set}({z^{\prime}})|$ follows by (possibly repeated applications of) Claim 28.2 (ii).

(iv): It is enough to show that for every strongly connected component $\mathcal{S}$ in $\mathcal{G}_{{\mathfrak{F}}}$,

[TABLE]

To this end, observe that for every $\mathcal{S}$, we have $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})\in\mathbb{N}^{+}$ by (42), (26) and Claim 12.2, and so by (24), (23) and (19),

[TABLE]

Therefore,

[TABLE]

Let $z^{\ast}\in\mathcal{S}$ be such that $\textit{min}\,({\mathcal{S}})=\textit{min}\,({z^{\ast}})$.

We prove (82) by induction on $\textit{rank}\,(\mathcal{S})$. Suppose $\textit{rank}\,(\mathcal{S})=0$. Then $\xi_{\textit{min}}^{{\mathfrak{F}}}(z^{\ast})=\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\textit{min}\,({\mathcal{S}})=\textit{min}\,({z^{\ast}})$. There are two cases:

• (a)

$z^{\ast}$ is $n$-strict for some $n$. As $\Gamma^{{\mathfrak{F}}}$ has a solution, $n=\textit{min}\,({z^{\ast}})$ must hold by (84). Thus, $|\textit{Set}({z^{\ast}})|=\textit{min}\,({z^{\ast}})$ by item (i), and so (82) follows by item (iii).

• (b)

$z^{\ast}$ is non-strict. If $z^{\ast}\in Y-Y^{\textit{b}}$ in $\mathcal{S}$, then $\mathcal{S}=\{z^{\ast}\}$ and so (82) follows by (80). If $z^{\ast}=x^{\ast}\in X_{\textit{lb}}$, then $y\to x^{\ast}$ holds for some $y\in Y^{\textit{b}}$. Also, $\Diamond_{\mathbf{h}}^{+}\Diamond_{\mathbf{v}}^{+}\mathsf{lower\_bound}_{\mathfrak{F}}^{x^{\ast}}$ is a conjunct of $\mathsf{lower\_bound}_{\mathfrak{F}}$, and so there exist $b\in V$ and distinct $a_{1},\dots,a_{\textit{min}\,({x^{\ast}})}\in U$ such that ${\mathfrak{M}},(a_{i},b)\models\Diamond_{\mathbf{v}}^{+}\neg\mathsf{c}^{{x}{y}}$ for every $1\leq i\leq\textit{min}\,({x^{\ast}})$. By Claim 28.1 (ii), $a_{i}\in\textit{Set}({x^{\ast}})$ for every $1\leq i\leq\textit{min}\,({x^{\ast}})$. Thus $|\textit{Set}({x^{\ast}})|\geq\textit{min}\,({x^{\ast}})=\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})$, and so (82) follows by item (iii). (The case when $z^{\ast}\in(Y_{\textit{lb}}\cap Y^{\textit{b}})$ is similar.)

Now take some $\mathcal{S}$ with $\textit{rank}\,(\mathcal{S})>0$, and suppose inductively that (82) holds for every $\mathcal{S}^{\prime}$ with $\textit{rank}\,(\mathcal{S}^{\prime})<\textit{rank}\,(\mathcal{S})$. There are two cases: If $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=\textit{min}\,({\mathcal{S}})$, then (82) can be shown as in (a)–(b) above, using $z^{\ast}\in\mathcal{S}$, Otherwise, by (83) there is $\mathcal{S}^{\prime}$ such that $\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})=2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})$ and $\mathcal{S}\Rightarrow\mathcal{S}^{\prime}$. Then there exist $z_{1}$ in $\mathcal{S}$ and $z_{2}$ in $\mathcal{S}^{\prime}$ such that $z_{1}^{\ast}\to^{2}z_{2}$ is an edge in $\mathcal{G}_{{\mathfrak{F}}}$. Therefore, by item (ii) and the IH, we have $|\textit{Set}({z_{1}})|\geq 2\cdot|\textit{Set}({z_{2}})|\geq 2\cdot\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S}^{\prime})=\nu_{\textit{min}}^{{\mathfrak{F}}}(\mathcal{S})$, and so (82) follows by item (iii). ∎

Finally, we can complete the proof of Lemma 28:

Item (i): We claim that

[TABLE]

Indeed, there are three cases. If $y\in Y^{\textit{b}}$, then $b\in\textit{Set}({q})$ for some copy $q$ of $y$ by (71). So there is $a$ such that $(a,b)\in\textit{Gen}({q})$ by (65), and so (85) follows by (58). If $y\in Y-Y^{\textit{b}}$ and $b\in\textit{Set}^{x}({y})$ for some $x$ with $y\to x$, then (85) follows by (78) and (79). If $y\in Y-Y^{\textit{b}}$ and $b\in\textit{Set}_{\textit{lb}}({y})$, then (85) follows from (72)–(74) and from the fact that $\overline{\mathsf{y}}$ is a conjunct of each $\hat{\mathsf{b}}_{j}^{\circ}(y)$ and $\hat{\mathsf{b}}_{s}^{\bullet}(y)$ (see (53)–(54)).

Now suppose indirectly that $y\neq y^{\prime}\in Y$ and there is some $b\in\textit{Set}({y})\cap\textit{Set}({y^{\prime}})$. By (85), there are $a$ and $a^{\prime}$ such that ${\mathfrak{M}},(a,b)\models\overline{\mathsf{y}}$ and ${\mathfrak{M}},(a^{\prime},b)\models\overline{\mathsf{y}}^{\prime}$, and so ${\mathfrak{M}},(a,b)\models\Box_{\mathbf{h}}^{+}\mathsf{y}$ and ${\mathfrak{M}},(a^{\prime},b)\models\neg\mathsf{y}$ by (45), a contradiction. (The case of $x,x^{\prime}\in X$ is similar, using the $\mathsf{x}$ variables.)

Item (ii) follows from Claim 28.1.

Item (iii): Constraints of the form $(z=n)\in\Gamma^{{\mathfrak{F}}}$ hold by Claim 28.4 (i). Constraints of the form $(z^{\prime}\geq 2z)\in\Gamma^{{\mathfrak{F}}}$ hold by Claim 28.4 (ii). Constraints of the form $(z^{\prime}\geq z)\in\Gamma^{{\mathfrak{F}}}$ hold by Claim 28.4 (iii). Finally, consider a constraint of the form $(z\geq k)\in\Gamma^{{\mathfrak{F}}}$, for some $k\in\mathbb{N}^{+}$. As $|\textit{Set}({z})|\geq\xi_{\textit{min}}^{{\mathfrak{F}}}(z)$ by Claim 28.4 (iv), we have $|\textit{Set}({z})|\geq k$ by (26) and Claim 12.2. ∎

The consequent $\mathsf{out}_{\mathfrak{F}}$ of the generalised Sahlqvist implication

We will use the positive formulas given in Lemma 28 (ii). For every $x\in X$, we let

[TABLE]

Similarly, for every $y\in Y^{\textit{b}}$, we let

[TABLE]

Then we let

[TABLE]

(see Example 32 below). Using Lemma 26, it is straightforward to check that $\mathsf{square\_bad}_{\mathfrak{F}}$ is a generalised Sahlqvist formula. Also, by Lemma 25, it is easy to see the following:

Lemma** 29****.**

It is decidable whether a bimodal formula is of the form $\mathsf{square\_bad}_{\mathfrak{F}}$ for some finite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ for which every $z\in X\cup Y$ is bounded, $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{y\in Y}\xi(y)\neq\sum_{x\in X}\xi(x)$ for any solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$.

It is also decidable whether a bimodal formula is of the form $\mathsf{square\_bad}_{\mathfrak{F}}$ for some finite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ for which every $x\in X$ is bounded, there is some unbounded $y^{\star}\in Y$, $\Gamma^{{\mathfrak{F}}}$ is defined and has a solution, but $\sum_{x\in X}\xi(x)<\sum_{y\in Y}\xi(y)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}}$.

Lemma** 30****.**

$\mathsf{square\_bad}_{\mathfrak{F}}$* is not valid in ${\mathfrak{F}}$.*

Proof.

Let ${\mathfrak{F}}_{1}={\mathfrak{F}}$ and take the model ${\mathfrak{M}}$ on ${\mathfrak{F}}_{1}$ from the proof of Lemma 27 satisfying $\mathsf{solution}_{{\mathfrak{F}}}$. It is easy to see that $\neg\mathsf{out}_{\mathfrak{F}}$ is satisfied in ${\mathfrak{M}}$ as well. ∎

Lemma** 31****.**

$\mathsf{square\_bad}_{\mathfrak{F}}$* is valid in every square product of difference frames.*

Proof.

Suppose ${\mathfrak{M}}$ is a model on $(U,\neq_{U})\!\times\!(V,\neq_{V})$ for some $U,V$ with $|U|=|V|>0$, and ${\mathfrak{M}},(u,v)\models\mathsf{solution}_{{\mathfrak{F}}}$. For every $z\in X\cup Y$, take the set $\textit{Set}({z})$ from Lemma 28. There are two cases:

• •

If $Y^{\textit{b}}=Y$, then Lemma 28 (i) and (iii) imply that $\sum_{x\in X}|\textit{Set}({x})|\neq\sum_{y\in Y}|\textit{Set}({y})|$. As $|U|=|V|$, either there is $a\in U-\bigcup_{x\in X}\textit{Set}({x})$, or there is $b\in V-\bigcup_{y\in Y}\textit{Set}({y})$.

• •

If $Y-Y^{\textit{b}}\neq\emptyset$, then Lemmas 23 and 28 (i),(iii) imply that $\sum_{x\in X}|\textit{Set}({x})|<\sum_{y\in Y}|\textit{Set}({y})|$. As $|U|=|V|$, there is $a\in U-\bigcup_{x\in X}\textit{Set}({x})$.

In both cases, ${\mathfrak{M}},(u,v)\models\mathsf{out}_{\mathfrak{F}}$ follows by Lemma 28 (ii). ∎

Note that when $X\cup Y$ is finite and every $z\in X\cup Y$ is bounded (cf. case (i) in Lemma 23), then it can happen that $\sum_{x\in X}\xi(x)\neq\sum_{y\in Y}\xi(y)$ for any solution of $\Gamma^{{\mathfrak{F}}}$, but there are solutions $\xi_{1}$ and $\xi_{2}$ of $\Gamma^{{\mathfrak{F}}}$ such that $\sum_{x\in X}\xi_{1}(x)<\sum_{y\in Y}\xi_{1}(y)$ and $\sum_{x\in X}\xi_{2}(x)>\sum_{y\in Y}\xi_{2}(y)$; see Fig. 8 for an example.

Example** 32****.**

Take the square-bad grid of bi-clusters ${\mathfrak{F}}$ in Fig. 7. We describe the formulas $\mathsf{upper\_bound}_{\mathfrak{F}}$, $\mathsf{switch}_{\mathfrak{F}}$, $\mathsf{lower\_bound}_{\mathfrak{F}}$, and $\mathsf{out}_{\mathfrak{F}}$.

To begin with, we have $X=\{x_{1},x_{2}\}$ and $Y^{\textit{b}}=\{y_{1}\}$ (so ${\mathfrak{F}}$ belongs to case (ii)(a) in Lemma 23). Also, $\mathcal{G}_{{\mathfrak{F}}}=\mathcal{H}_{{\mathfrak{F}}}$ has an isolated node $x_{2}$ and two edges: $y_{1}\to^{2}x_{1}$ and $y_{2}\to^{2}x_{1}$. Thus, the unravelling $\mathcal{T}_{{\mathfrak{F}}}$ of the bounded part $\mathcal{H}_{{\mathfrak{F}}}^{\textit{b}}$ of $\mathcal{H}_{{\mathfrak{F}}}$ has two roots, $y_{1}$ and $x_{2}$ (both are $6$-strict), and one edge: $y_{1}\to^{2}x_{1}$. Therefore, we have:

[TABLE]

where

[TABLE]

We also have

[TABLE]

Next, we compute the solution $\xi_{\textit{min}}^{{\mathfrak{F}}}$ of $\Gamma^{{\mathfrak{F}}}$. Note that all strongly connected components in $\mathcal{G}_{{\mathfrak{F}}}$ are singletons, and so \xi_{\textit{min}}^{{\mathfrak{F}}}(z)=\nu_{\textit{min}}^{{\mathfrak{F}}}\bigl{(}\{z\}\bigr{)} for all $z\in X\cup Y$. So we have:

[TABLE]

Thus, $X_{\textit{lb}}=\{x_{1}\}$, $Y_{\textit{lb}}=\emptyset$ and $Y_{\textit{lb}}\cup(Y-Y^{\textit{b}})=\{y_{2}\}$. We choose ${\mathfrak{F}}^{x_{1}y_{1}}$ and ${\mathfrak{F}}^{x_{2}y_{2}}$ to ‘witness’ that $\textit{min}\,({x_{1}})=3$ and $\textit{min}\,({y_{2}})=4$, respectively, and so we have $r_{x_{1}}=i_{x_{1}}=1$, $r_{y_{2}}=2$, $i_{y_{2}}=0$, and

[TABLE]

where

[TABLE]

Finally, we have:

[TABLE]

7.2.2 $X\cup Y$ is infinite

If $X\cup Y$ is infinite then, by Lemma 23 (iii), there are two cases. We suppose that $X$ is finite, every $x\in X$ is bounded, $Y$ is infinite, and there is a finite subgrid ${\mathfrak{F}}^{-}=(X,Y^{-},g^{-})$ of ${\mathfrak{F}}$ such that

[TABLE]

(The other case is similar.) By (87) and the finiteness of ${\mathfrak{F}}^{-}$, the formula $\mathsf{solution}_{{\mathfrak{F}}^{-}}$ is defined in §7.2.1. For every $x\in X$, take the formula $\mathsf{out}_{{\mathfrak{F}}}({x})$ from (86), and let

[TABLE]

Then $\mathsf{square\_bad}_{\mathfrak{F}}$ is clearly a generalised Sahlqvist formula. An inspection of the proof of Lemma 23 shows that by Lemma 29 we have the following:

Lemma** 33****.**

It is decidable whether a bimodal formula is of the form $\mathsf{square\_bad}_{\mathfrak{F}}$ for some infinite grid of bi-clusters ${\mathfrak{F}}=(X,Y,g)$ for which $X$ is finite, every $x\in X$ is bounded, and ${\mathfrak{F}}^{-}=(X,Y^{-},g^{-})$ is a finite subgrid of ${\mathfrak{F}}$ such that $\Gamma^{{\mathfrak{F}}^{-}}$ is defined and has a solution, but $\sum_{x\in X}\xi(x)<\sum_{y\in Y^{-}}\xi(y)$ for every solution $\xi$ of $\Gamma^{{\mathfrak{F}}^{-}}$.

Lemma** 34****.**

$\mathsf{square\_bad}_{\mathfrak{F}}$* is not valid in ${\mathfrak{F}}$.*

Proof.

As ${\mathfrak{F}}^{-}$ is a subgrid of ${\mathfrak{F}}$, the proof of Lemma 27 gives a model ${\mathfrak{M}}$ on ${\mathfrak{F}}$ satisfying $\mathsf{solution}_{{\mathfrak{F}}^{-}}$. As the ‘$X$-coordinates’ of both ${\mathfrak{F}}^{-}$ and ${\mathfrak{F}}$ are the same, it is easy to see that $\neg\Diamond_{\mathbf{h}}^{+}\bigwedge_{x\in X}\mathsf{out}_{{\mathfrak{F}}}({x})$ is satisfied in ${\mathfrak{M}}$ as well. ∎

Lemma** 35****.**

$\mathsf{square\_bad}_{\mathfrak{F}}$* is valid in every square product of difference frames.*

Proof.

Suppose ${\mathfrak{M}}$ is a model on $(U,\neq_{U})\!\times\!(V,\neq_{V})$ for some $U,V$ with $|U|=|V|>0$, and ${\mathfrak{M}},(u,v)\models\mathsf{solution}_{{\mathfrak{F}}^{-}}$. For every $z\in X\cup Y^{-}$, take the set $\textit{Set}({z})$ from Lemma 28. By Lemma 28 (i),(iii), we have $\sum_{x\in X}|\textit{Set}({x})|<\sum_{y\in Y^{-}}|\textit{Set}({y})|$. As $|U|=|V|$, there is $a\in U-\bigcup_{x\in X}\textit{Set}({x})$, and so ${\mathfrak{M}},(u,v)\models\mathsf{out}_{\mathfrak{F}}$ follows by Lemma 28 (ii). ∎

7.3 Infinite Sahlqvist axiomatisation for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$

Though in general generalised Sahlqvist formulas are more expressive than Sahlqvist formulas [16], there are special settings when their axiomatic powers coincide [15]. Our bimodal language only has two monadic modalities $\Diamond_{\mathbf{h}}$ and $\Diamond_{\mathbf{v}}$. So our generalised Sahlqvist formulas (as defined in §3.2.1 above) are special cases of the PCFs of [15] (and of the inductive formulas of [16]). The modalities $\Diamond_{\mathbf{h}}$ and $\Diamond_{\mathbf{v}}$ are self-reversive in the sense that the formulas $p\to\Box_{\mathbf{h}}\Diamond_{\mathbf{h}}p$ and $p\to\Box_{\mathbf{v}}\Diamond_{\mathbf{v}}p$ belong to $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ (by (2), (9) and (10)). Therefore, it follows from [15, Thm. 4.10] that there is an infinite axiomatisation for $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ consisting of Sahlqvist formulas. Moreover, the Sahlqvist axioms can be obtained algorithmically from the generalised Sahlqvist formulas they are axiomatically equivalent with.

8 Discussion

We have shown that the 2D product logic $\mathbf{Diff}\!\times\!\mathbf{Diff}$ is non-finitely axiomatisable, and also given an infinite set $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ of Sahlqvist formulas axiomatising $\mathbf{Diff}\!\times\!\mathbf{Diff}$. We have also proved that its ‘square’ version $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ (the modal counterpart of two-variable substitution and equality free first-order logic with counting to $2$) is non-finitely axiomatisable over $\mathbf{Diff}\!\times\!\mathbf{Diff}$, but can be axiomatised by adding infinitely many Sahlqvist axioms to $\mathbf{Diff}\!\times\!\mathbf{Diff}$. Here are some related issues and open problems:

The two-player p-morphism game we defined for bi-clusters in the proof of Lemma 9 can easily be generalised to arbitrary countable grids of bi-clusters ${\mathfrak{F}}$ such that the analogue of Claim 9.1 still holds for the game $\mathbb{G}({\mathfrak{F}})$. (Algebraically, this is the complete representation game à la Hirsch and Hodkinson [19], for subdirectly irreducible atomic diagonal-free strict-cylindric algebras.) So by Theorem 3, ${\mathfrak{F}}$ validates the Sahqvist axioms in $\Sigma_{\mathbf{Diff}\!\times\!\mathbf{Diff}}$ iff player $\exists$ has a winning strategy in $\mathbb{G}({\mathfrak{F}})$. However, the precise connection between particular plays of $\mathbb{G}({\mathfrak{F}})$ and the axioms is not clear. 2. 2.

One might also consider the ‘lopsided’ product logics $\mathbf{S5}\!\times\!\mathbf{Diff}$ and

[TABLE]

$\mathbf{S5}\!\times\!\mathbf{Diff}$ is not finitely axiomatisable by Theorem 10, and a proof very similar to that of Theorem 2 shows that $\mathbf{S5}\!\times^{\textit{sq}}\mathbf{Diff}$ is not finitely axiomatisable over $\mathbf{S5}\!\times\!\mathbf{Diff}$. Further, using the proof pattern in §2.2, it is easy to show that $\mathbf{S5}\!\times\!\mathbf{Diff}$ and $\mathbf{S5}\!\times^{\textit{sq}}\mathbf{Diff}$ are axiomatisable by adding the Sahlqvist axiom $\Box_{\mathbf{h}}p\to p$ (expressing that $R_{\mathbf{h}}$ is reflexive) to $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$, respectively.

However, much simpler axioms for these logics can be obtained by actually repeating the proofs of Theorems 3 and 4, and using that grids of bi-clusters are much simpler in these cases. In particular, it can be shown directly (without using the algorithm of [15]) that $\mathbf{S5}\!\times^{\textit{sq}}\mathbf{Diff}$ is Sahlqvist axiomatisable: In case of grids of bi-clusters ${\mathfrak{F}}$ with reflexive $R_{\mathbf{h}}$, there are only ‘local’ reasons for ${\mathfrak{F}}$ not being the p-morphic image of a product of a universal and a difference frame. Thus, switch bi-clusters play no role in an axiomatisation, and so there is no need for $\mathsf{switch}_{\mathfrak{F}}$-like conjuncts in the antecedents of the axioms. 3. 3.

Both $\mathbf{Diff}\!\times\!\mathbf{Diff}$ and $\mathbf{Diff}\!\times^{\textit{sq}}\mathbf{Diff}$ are elementarily generated modal logics (by Corollary 7 or Theorem 3, and Theorem 4, respectively). Hodkinson [23] ‘synthesises’ modal axioms for such logics from the first-order defining formulas via hybrid logic formulas. It would be interesting to consider the connections between our axioms and the axioms obtained in this way. Note that we did not use (or even compute) the first-order correspondents of our axioms. 4. 4.

Hirsch and Hodkinson [20, 21] give an explicit infinite axiomatisation for (the algebraic counterpart of) the $n$-dimensional product logic $\mathbf{S5}^{n}$, for any $n\in\mathbb{N}^{+}$. The axioms are obtained by first expressing ‘universally’ the winning strategy for $\exists$ in a two-player ‘representation’ game, and then turning these ‘universal expressions’ to modal formulas by using that there is a universal modality in $\mathbf{S5}^{n}$-frames. By the negative results of [24, 3], infinitely many of these axioms cannot be Sahlqvist/canonical whenever $n\geq 3$. It is easy to see that the method of [20] can also be used to give an explicit infinite axiomatisation for $\mathbf{Diff}^{n}$, for any $n\in\mathbb{N}^{+}$, so in particular for $\mathbf{Diff}\!\times\!\mathbf{Diff}$. As $\mathbf{S5}^{n}$ is finitely axiomatisable over $\mathbf{Diff}^{n}$ by [31, Thm. 2.14], infinitely many of the axioms obtained by the method of [20] cannot be Sahlqvist/canonical whenever $n\geq 3$. But what about the $n=2$ case? Are the axioms obtained for $\mathbf{Diff}\!\times\!\mathbf{Diff}$ this way Sahlqvist/canonical? 5. 5.

Our axiomatisations are connected to solutions of some special kinds of integer programming problems. It would be interesting to understand these connections further, and possibly use some known integer programming solver methods in order to find simpler axioms. Note that Pratt-Hartmann [35] also connects the type-structures of two-variable first-order logic with counting to integer programming. 6. 6.

Here we considered the axiomatisation problem for the modal counterpart of two-variable first-order logic with counting to $2$ only, and without equality and substitution/transposition of variables. It would be interesting to get closer to the full two-variable fragment with counting, and study richer languages that contain (some of the) modal operators ‘simulating’ these missing features (that is, cylindric and (quasi-) polyadic algebras with ‘graded’ cylindrifications corresponding to counting quantifiers); see [18, 38, 33, 7].

Acknowledgements

Sérgio Marcelino’s research was funded by FCT/MCTES through national funds and when applicable co-funded EU funds under the project UIDB/EEA/50008/2020. We thank the anonymous referees for their careful reading and expert criticism of the manuscript.