2.1 Modal syntax and semantics

Let $\mathrm {A}$ be a finite set, an alphabet of modalities. Modal formulas over $\mathrm {A}$ , in symbols, are constructed from a countable set of variables using Boolean connectives $\bot ,\rightarrow $ and unary connectives $\lozenge \in \mathrm {A}$ . Other logical connectives are defined as abbreviations in the standard way, in particular $\Box \varphi $ denotes $\neg \lozenge \neg \varphi $ .

We define the following abbreviations: $\lozenge ^0 \varphi =\varphi $ , $\lozenge ^{i+1}\varphi =\lozenge ^i\lozenge \varphi $ , $\lozenge ^{\leq m} \varphi = \bigvee _{i\leq m} \lozenge ^i \varphi $ . We write $\lozenge _{\mathrm {A}}\varphi $ for $\bigvee _{\lozenge \in \mathrm {A}}\lozenge \varphi $ . Abbreviations such as $\lozenge _{\mathrm {A}}^i,\,\lozenge _{\mathrm {A}}^{\leq m}$ are defined likewise.

By an $\mathrm {A}$ -logic we mean a normal modal logic whose alphabet of modalities is $\mathrm {A}$ (see, e.g., [Reference Blackburn, de Rijke and Venema6]). The terms unimodal and bimodal refer to the cases $\mathrm {A}=\{\lozenge \}$ and $\mathrm {A} = \{\lozenge _1,\lozenge _2\}$ , respectively.

An $\mathrm {A}$ -frame is a pair $F = (X,\,(R_\lozenge )_{\lozenge \in \mathrm {A}})$ , where X is a non-empty set and $R_\lozenge \subseteq X\times X$ for any $\lozenge \in \mathrm {A}$ . We write $\mathop {\mathrm {dom}} F$ for X. By the cardinality $|F|$ of F we mean the cardinality of X. We put $R_F = \bigcup _{\lozenge \in \mathrm {A}} R_\lozenge .$ For $a\in X$ , $Y\subseteq X$ , we put $R_\lozenge (a)=\{b\mid aR_\lozenge b\}$ , $R_\lozenge [Y]=\bigcup _{a\in Y} R_\lozenge (a)$ .

A model on F is a pair $(F,\,\theta )$ , where , and $\mathcal {P}(X)$ is the powerset of X; $\theta $ is called a valuation in F. The truth-relation $(F,\theta ),a\vDash \varphi $ is defined in the standard way; in particular, $(F,\,\theta ),\,a\models \lozenge \varphi $ means that $(F,\theta ),b\models \varphi $ for some $b\in R_\lozenge (a)$ . We put

$$ \begin{align*}\bar{\theta}(\varphi)=\{a\mid (F,\theta),a\vDash\varphi\}.\end{align*} $$

A formula is valid in an $\mathrm {A}$ -frame F, in symbols $F\vDash \varphi $ , if $X=\bar {\theta }(\varphi )$ for every model $(F,\theta )$ on F. For a set of formulas , by $F\vDash \Gamma $ we mean that $F\vDash \varphi $ for all $\varphi \in \Gamma $ ; in this case F is said to be a $\Gamma $ -frame. For a class $\mathcal {F}$ of $\mathrm {A}$ -frames, $\mathcal {F}\vDash \Gamma $ means that $F\vDash \Gamma $ for all $F\in \mathcal {F}$ .

The set of $\mathrm {A}$ -formulas that are valid in F is denoted by $\mathop {\mathrm {Log}} F$ . For a class $\mathcal {F}$ of $\mathrm {A}$ -frames, $\mathop {\mathrm {Log}} \mathcal {F}$ is the set of all formulas over $\mathrm {A}$ that are valid in each $F\in \mathcal {F}$ ; this set is a logic [Reference Chagrov and Zakharyaschev9, Section 4.2] and is called the logic of $\mathcal {F}$ . Such logics are said to be Kripke complete.

Let us recall that is the smallest unimodal logic that contains $\lozenge \lozenge p \to \lozenge p$ , extends with $p\rightarrow \lozenge p$ , and extends with $p\rightarrow \Box \lozenge p$ . These logics are Kripke complete; $\lozenge \lozenge p \to \lozenge p$ expresses the transitivity, $p\rightarrow \lozenge p$ reflexivity, and $p\rightarrow \Box \lozenge p$ the symmetry of a binary relation (see, e.g., [Reference Blackburn, de Rijke and Venema6, Section 4.3] or [Reference Chagrov and Zakharyaschev9, Section 5.2]).

The notions of generated subframe and p-morphism (or bounded morphism) are defined in the standard way (see, e.g., [Reference Blackburn, de Rijke and Venema6, Section 3.3]). In particular, for frames $F = (X,\,(R_\lozenge )_{\lozenge \in \mathrm {A}})$ and $G = (Y,\,(S_\lozenge )_{\lozenge \in \mathrm {A}})$ , $f:\:X\to Y$ is a p-morphism from F to G, if

1. 1. f is a homomorphism: for any $a,\,b\in X$ and $\lozenge \in \mathrm {A},\, a R_\lozenge b$ implies $f(a) S_\lozenge f(b)$ , and

2. 2. f satisfies the back condition: for any $a\in X,\,u\in Y$ , and $\lozenge \in \mathrm {A},\, f(a) S_\lozenge u$ implies that there exists $b\in X$ such that $a R_\lozenge b$ and $f(b) = u.$

If f is surjective, we write $f:\:F\twoheadrightarrow G.$ If there exists a p-morphism from F onto $G,$ we write $F \twoheadrightarrow G;$ in this case, $\mathop {\mathrm {Log}}{F} \subseteq \mathop {\mathrm {Log}}{G}$ [Reference Blackburn, de Rijke and Venema6, Section 3.3].

For a frame $F = (X,\,(R_\lozenge )_{\lozenge \in A})$ and an equivalence $\approx $ on X, the quotient frame ${F}{/}{\approx }$ is the frame $({X}{/}{\approx },\,(R^\approx _\lozenge )_{\lozenge \in \mathrm {A}})$ , where for $[a],[b]\in {X}{/}{\approx }$ and $\lozenge \in \mathrm {A}$ ,

$$\begin{align*}[a] R^\approx_\lozenge [b] \text{ iff } \exists a'\in[a]\ \exists b'\in [b]\ \left(a' R_{\lozenge} b' \right). \end{align*}$$

2.2 Products

Let $\mathrm {A}$ and $\mathrm {B}$ be two disjoint finite sets. For an $\mathrm {A}$ -frame $F=\left (X,\,(R_\lozenge )_{\lozenge \in \mathrm {A}}\right )$ and $\mathrm {B}$ -frame $G = \left (Y,\,(R_\lozenge )_{\lozenge \in \mathrm {B}}\right )$ , the product frame $ F\times G$ is the frame $(X\times Y,\,(R^h_\lozenge )_{\lozenge \in \mathrm {A}}, (R^v_\lozenge )_{\lozenge \in \mathrm {B}})$ , where

$$ \begin{align*} R^h_\lozenge&=\{((a,\,b),\,(a',\,b))\mid a,\,a'\in X \text{ and } b\in Y \text{ and } a R_\lozenge a'\} &\text{ for }\lozenge\in \mathrm{A};\\ R^v_\lozenge &= \{((a,\,b),\,(a,\,b'))\mid a\in X \text{ and } b,\,b'\in Y \text{ and } b R_\lozenge b'\} &\text{ for }\lozenge\in \mathrm{B}. \end{align*} $$

We say that relations $R^h_\lozenge $ are horizontal, and $R^v_\lozenge $ are vertical. For a class $\mathcal {F}$ of $\mathrm {A}$ -frames and a class $\mathcal {G}$ of $\mathrm {B}$ -frames, we put $ \mathcal {F} \times \mathcal {G} = \{F\times G \mid F\in \mathcal {F},\,G\in \mathcal {G}\}. $

For logics $L_1,L_2$ , the product logic $L_1\times L_2$ is defined as

$$\begin{align*}L_1\times L_2 = \mathop{\mathrm{Log}}\{F\times G \mid F\models L_1,\,G\models L_2\}. \end{align*}$$

If $L_1$ and $L_2$ are unimodal logics, we rename their modalities and follow the convention that the alphabet of $L_1\times L_2$ is $\{\lozenge _1,\lozenge _2\}$ . We write $L^2$ for $L\times L$ .

It is important to note that $\mathop {\mathrm {Log}} \mathcal {F} = \mathop {\mathrm {Log}} \mathcal {F}'$ and $\mathop {\mathrm {Log}} \mathcal {G} = \mathop {\mathrm {Log}} \mathcal {G}'$ do not imply that $\mathop {\mathrm {Log}} (\mathcal {F}\times \mathcal {G}) = \mathop {\mathrm {Log}} (\mathcal {F}'\times \mathcal {G}')$ . Moreover, $\mathop {\mathrm {Log}}\mathcal {F}\times \mathop {\mathrm {Log}} \mathcal {G}$ and $\mathop {\mathrm {Log}}(\mathcal {F}\times \mathcal {G})$ can be distinct. The reader may find examples of such logics in [Reference Gabbay, Kurucz, Wolter and Zakharyaschev11, Theorem 7.11].

2.3 Local tabularity and local finiteness

Let L be a logic over $\mathrm {A}$ . Formulas $\varphi $ and $\psi $ are said to be L-equivalent, if $\varphi \leftrightarrow \psi \in L$ . For a finite k, L is said to be k-finite, if there are only finitely many L-equivalence classes in the set of formulas over $\mathrm {A}$ in variables $p_i,\,i < k$ . Equivalently, L is k-finite, if the k-generated Lindenbaum (or free) algebra of L is finite. L is said to be locally tabular, if it is k-finite for all finite k.

In algebraic terms, local tabularity of a logic means that its countably generated Lindenbaum algebra is locally finite, which, in turn, means that the variety of its algebras is locally finite (see, e.g., [Reference Burris and Sankappanavar8, Chapter 2], [Reference Chagrov and Zakharyaschev9, Chapter 7] for corresponding notions).

The following fact is immediate.

A class $\mathcal {C}$ of algebras of a finite signature is said to be uniformly locally finite, if there exists a function $f:\omega \to \omega $ such that the cardinality of a subalgebra of any $B\in \mathcal {C}$ generated by $k<\omega $ elements does not exceed $f(k)$ .

2.4 Remark on infinite alphabets

As we mentioned, in this article we only consider finite modal alphabets. The current small remark is an exception.

If $\mathrm {B}$ is an infinite set of modalities, and a logic L over $\mathrm {B}$ is locally tabular (in fact, one-finite), then all but finitely many elements of $\mathrm {B}$ are just a “syntactic sugar.” Namely, let N be the number of L-equivalence classes of one-variable formulas over $\mathrm {B}$ . Choose their representatives $\{\psi _i(p)\}_{i<N}$ and let $\mathrm {A}$ be the set of all modalities occurring in them. Now consider the formulas $\{ \lozenge p\mid \lozenge \in \mathrm {B}\}$ . For each of them, for some $i<N$ , the logic L contains $\lozenge p \leftrightarrow \psi _i(p)$ . Hence, every formula over $\mathrm {B}$ is L-equivalent to a formula over the finite $\mathrm {A}$ .

2.5 Pretransitivity and finite height

For a binary relation R on X and a number $m < \omega $ , put $R^{\leq m}= \bigcup _{i \leq m} R^i$ , where $R^{i+1}=R\circ R^i$ , $\circ $ is the composition of relations, and $R^0$ is the diagonal relation $\{(x,x)\mid x\in X\}$ . The transitive reflexive closure $\bigcup _{i < \omega } R^i$ of R is denoted by $R^*$ .

A frame F is said to be m-transitive, if $R_F^{\leq m}=R_F^*$ .Footnote ¹ F is pretransitive, if it is m-transitive for some finite m. The following fact is standard.

For any $\mathrm {A}$ -frame F, we have the following equivalence [Reference Kracht19, Section 3.4]:

(1) $$ \begin{align} R_F\ \text{is} \ m\text{-transitive iff} \ F\vDash \lozenge_{\mathrm{A}}^{m+1} p \rightarrow \lozenge_{\mathrm{A}}^{\leq m} p. \end{align} $$

A logic L is said to be m-transitive, if L contains $\lozenge _{\mathrm {A}}^{m+1} p \rightarrow \lozenge _{\mathrm {A}}^{\leq m} p$ , and pretransitive, if it is m-transitive for some $m\geq 0$ . Let $\mathrm {tra}{(L)}$ be the least m such that L is m-transitive; m is called the pretransitivity index of L.

For a frame F, let $F^*$ be the preorder $(\mathop {\mathrm {dom}}{F},R_F^*)$ . For a class $\mathcal {F}$ of frames, $\mathcal {F}^*=\{F^*\mid F\in F\}$ .

The following fact is straightforward: for an m-transitive frame $F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$ , and any unimodal formula $\varphi $ , we have

(2) $$ \begin{align} F\vDash { [\varphi ]}^{m} \text{ iff } F^*\vDash \varphi, \end{align} $$

where ${ [\varphi ]}^{m}$ is the translation that is compatible with Boolean connectives (i.e., ${ [\bot ]}^{m}=\bot $ , ${ [p ]}^{m}=p$ for variables, ${ [\psi _1\rightarrow \psi _2 ]}^{m}={ [\psi _1 ]}^{m}\rightarrow { [\psi _2 ]}^{m}$ ) given by ${ [\lozenge \psi ]}^{m}= \lozenge _{\mathrm {A}}^{\leq m} { [\psi ]}^{m}$ .

For a frame $F = (X,\,(R_\lozenge )_{\lozenge \in \mathrm {A}}),$ let $\sim _F$ be the equivalence $R_F^*\cap (R_F^*)^{-1}$ on X, and $\mathop {\mathrm {Sk}} F={F^*}{/}{\sim _F}$ . The quotient frame $\mathop {\mathrm {Sk}} F$ is a poset; it is called the skeleton of F. Equivalence classes modulo $\sim _F$ are called clusters in F.

The height of a poset $(X,\leq )$ is defined as

$$ \begin{align*}\sup\{|\Sigma|\mid \Sigma\ \text{is a finite chain in}\ (X,\leq)\}.\end{align*} $$

The height of a frame F, in symbols $h(F)$ , is the height of its skeleton.

Consider unimodal formulas

$$\begin{align*}B_0 = \bot,\quad B_{i+1} = p_{i+1}\rightarrow \Box \left (\lozenge p_{i+1} \lor B_i\right). \end{align*}$$

For a unimodal frame $G=(X,R)$ with a transitive R, we have [Reference Segerberg26]

$$ \begin{align*}G\vDash B_h \text{ iff } h(G)\leq h.\end{align*} $$

Consequently, if F is an m-transitive $\mathrm {A}$ -frame, then $F\models { [B_h ]}^{m}$ iff $h(F)\le h$ . Formulas $B_h$ and their polymodal pretransitive generalizations ${ [B_h ]}^{m}$ are called formulas of finite height. For an m-transitive logic L, we define the height of L, denoted by $h(L),$ as the smallest $h < \omega $ such that $L \vdash [B_h]^m$ ; if there is no such h, we put $h(L)=\omega $ . Observe that for any m such that L is m-transitive this condition defines the same $h(L)$ .

In [Reference Shapirovsky and Shehtman33], this fact was stated for the unimodal case; its polymodal generalization is straightforward, details can be found in [Reference Shapirovsky32].

2.6 Local tabularity and tuned partitions

A partition $\mathcal {V}$ of a set X is a family of non-empty pairwise disjoint sets such that $X=\bigcup \mathcal {V}$ . For $x\in X$ , $[x]_{\mathcal {V}}$ denotes $V\in \mathcal {V}$ that contains x. A partition of X induced by $h :X\to Y$ is the set of non-empty sets $h^{-1}(y)$ , $y\in Y$ . A partition $\mathcal {U}$ refines $\mathcal {V}$ , if each element of $\mathcal {V}$ is the union of some elements of $\mathcal {U}$ .

Definition 2.5. Let R be a binary relation on X. A partition $\mathcal {U}$ of X is said to be R-tuned, if for every $U,V\in \mathcal {U}$ ,

(3) $$ \begin{align} \exists a\in U \exists b\in V \, (aR b) \,\text{ implies }\, \forall a\in U \exists b\in V \, (aR b). \end{align} $$

Let $F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$ be an $\mathrm {A}$ -frame. A partition $\mathcal {U}$ of X is said to be tuned in F, if it is $R_\lozenge $ -tuned for every $\lozenge \in \mathrm {A}$ . In other terms, the condition (3) means that the map $x\mapsto [x]_{\mathcal {U}}$ is a p-morphism $F\twoheadrightarrow {F}{/}{\sim }$ , where $\mathcal {U}={X}{/}{\sim }$ , see, e.g., [Reference Blok7, Proposition 3.2] for details.Footnote ²

A class $\mathcal {F}$ of $\mathrm {A}$ -frames is said to be f-tunable for a function $f:\omega \to \omega $ , if for every $F\in \mathcal {F}$ , for every finite partition $\mathcal {V}$ of F there exists a refinement $\mathcal {U}$ of $\mathcal {V}$ such that $|\mathcal {U}|\leq f(|\mathcal {V}|)$ and $\mathcal {U}$ is tuned in F. A class $\mathcal {F}$ is uniformly tunable, if it is f-tunable for some $f:\omega \to \omega $ .

The following theorem is a Kripke-style version of Mal’cev’s criterion (Theorem 2.2).

This characterization makes many properties of locally tabular logics visible.

For a frame $F = (X,\,(R_\lozenge )_{\lozenge \in \mathrm {A}})$ and $Y \subseteq X$ , put $F{\upharpoonright } Y = (Y,\,(R_\lozenge {\upharpoonright } Y)_{\lozenge \in \mathrm {A}})$ , where $R_\lozenge {\upharpoonright } Y= R_\lozenge \cap (Y\times Y)$ . For a class $\mathcal {F}$ of frames, put

$$ \begin{align*}\mathop{\mathrm{Sub}}{\mathcal{F}}=\{F{\upharpoonright} Y\mid F\in \mathcal{F} \text{ and } \varnothing\neq Y\subseteq \mathop{\mathrm{dom}}{F}\}.\end{align*} $$

A frame F is a cluster, if $a R_F^* b$ for all $a,b$ in F. For a class $\mathcal {F}$ of frames, $Cl{(\mathcal {F})}$ is the class of cluster frames which are restrictions on clusters (as sets) occurring in frames in $\mathcal {F}$ :

$$ \begin{align*}Cl{(\mathcal{F})}=\{F{\upharpoonright} C\mid C \text{ is a cluster in } F\in\mathcal{F}\}. \end{align*} $$

A class $\mathcal {F}$ is of uniformly finite height, if for some finite h, for every $F\in \mathcal {F}$ , we have $h(F)\leq h$ .

The following characterization is one of the main technical tools for our study.

Remark. In [Reference Shapirovsky and Shehtman33], Theorems 2.6 and 2.9 were stated for the unimodal case. Their polymodal generalizations are straightforward. For Theorem 2.6, details are given in [Reference Shapirovsky32]. The polymodal version of Theorem 2.9 was not considered before; for the sake of rigor, we prove it in the Appendix.

3.1 Reducible path property

For $m<\omega $ , consider the following first-order property $\mathrm {RP}_m$ :

$$ \begin{align*} \forall x_0,\ldots, x_{m+1} \; (x_0Rx_1R\ldots R x_{m+1}\rightarrow \bigvee\limits_{i<j\leq m+1} x_i = x_j \vee \bigvee\limits_{i< j\leq m} x_i R x_{j+1}). \end{align*} $$

We say that a class of $\mathcal {F}$ of frames has the reducible path property (for short, rpp), if for some fixed m, for every $F\in \mathcal {F}$ , $\mathrm {RP}_m$ holds in $(\mathop {\mathrm {dom}} F,R_F)$ . Notice that $\mathrm {RP}_m$ is stronger than m-transitivity. This property is another necessary condition for local tabularity.

Let $\mathrm {rp}_m(\lozenge )$ be the modal formula

$$ \begin{align*}p_0\wedge \lozenge(p_1\wedge \lozenge(p_2\wedge \dots \wedge \lozenge p_{m+1})\dots)\rightarrow \bigvee\limits_{i<j\leq m+1} \lozenge^i (p_i \wedge p_j) \vee \bigvee\limits_{i< j\leq m} \lozenge^i(p_i \wedge \lozenge p_{j+1}). \end{align*} $$

Since every locally tabular logic L is the logic of a uniformly tunable class, L contains $\mathrm {rp}_m(\lozenge _{\mathrm {A}})$ for some m.

Whether the reducible path property is sufficient for local tabularity in a class of clusters was left as an open question in [Reference Shapirovsky and Shehtman33, Problem 8.1]. Below we give a very simple example that shows that it is not sufficient; at the same time, in the next section we show that a variant of the reducible path property is sufficient for local tabularity of products.

3.2 Bounded cluster property

Recall that $Cl{(\mathcal {F})}$ denotes the class of clusters occurring in frames of a class $\mathcal {F}$ . We say that $\mathcal {F}$ has the bounded cluster property, if for some $n<\omega $ ,

(4) $$ \begin{align} |C| \le n \text{ for all }C\in Cl{(\mathcal{F})}. \end{align} $$

The bounded cluster property in a class of frames is neither necessary nor sufficient for the local tabularity of its logic, even in the unimodal case. As examples, consider the class of all equivalence relations and the class of all posets.

The condition (4) is not modally definable in general. Indeed, by the bulldozer theorem (see [Reference Chagrov and Zakharyaschev9, Theorem 3.20]), the countable cluster $(\omega ,\omega \times \omega )$ is a p-morphic image of some strictly partially ordered frame, which satisfies (4) for $n = 1$ . However, as we show below, it is definable in classes of m-transitive frames of finite height, and in particular, in the class of frames of any locally tabular logic.

Let $F=(X,R)$ be a preorder whose skeleton is converse well-founded. Observe that F has no clusters of size greater than n iff $F{\upharpoonright } Y\twoheadrightarrow \boldsymbol {n+1}$ for no $Y\subseteq \mathop {\mathrm {dom}} F$ . It follows from [Reference Chagrov and Zakharyaschev9, Theorem 9.39(ii)] that in the class of converse well-founded preorders, (4) is definable by a modal formula $\mathrm {bc}_n$ .

The formulas $\mathrm {bc}_n$ can be defined explicitly in the following way.Footnote ³ Namely, let $\mathrm {bc}_n$ be

$$\begin{align*}\lnot ( \chi_0 \land \Box (\chi_0 \to \lozenge \varphi_n)), \end{align*}$$

where $\chi _k$ is $p_k \land \bigwedge _{i < k} \lnot p_i$ , $\varphi _0$ is $\chi _0$ , and $\varphi _{k+1}$ is $\chi _{k+1} \land \lozenge \varphi _k$ .

For example, $\mathrm {bc}_3$ is

$$\begin{align*}\lnot ( \chi_0 \land \Box (\chi_0 \to \lozenge (\chi_3 \land \lozenge(\chi_2 \land \lozenge(\chi_1\land \lozenge \chi_0))))). \end{align*}$$

This proposition allows to characterize the bounded cluster property for the case of finite height (over an arbitrary finite alphabet) as follows.

We call ${ [\mathrm {bc}_n ]}^{m}$ the bounded cluster formulas.

3.3 Path-bounded frames

Now we consider the combination of local tabularity and the bounded cluster property. This situation can be visualized via several equivalent conditions.Footnote ⁴

A logic is called tabular, if it is the logic of a single finite frame. It is trivial that tabularity implies local tabularity.

We call a class of frames $\mathcal {F}$ path-bounded, if for some $n < \omega $ , any path (i.e., a subset $\{a_0, \ldots , a_l\} \subseteq \mathop {\mathrm {dom}} F$ satisfying $a_0 R_F \ldots R_F a_l$ ) in any frame $F\in \mathcal {F}$ contains at most n distinct points. The logic of a path-bounded class of frames is said to be strongly locally tabular. The latter definition is justified by the following proposition.

4.1 Products of locally tabular logics

In the product $L_1\times L_2$ of two Kripke complete consistent logics, local tabularity of the factors is a necessary condition for local tabularity of $L_1\times L_2$ : the product is conservative over the factors in this case. However, it is not sufficient: it is known that the product of two locally tabular logics can be not locally tabular. The simplest example is the logic : that is locally tabular is well known (e.g., one can observe that in the class of point-generated frames of this Kripke complete logic every partition is tuned); at the same time is not locally tabular [Reference Henkin, Monk and Tarski18, Theorem 2.1.11]. We provide extra conditions which give criteria of local tabularity of the product of locally tabular logics.

The following classical fact about is important for our goals. For a set X, let ${\boldsymbol X}$ be the frame $(X,X\times X)$ . For sets $X,\,Y$ , the product frame $\boldsymbol X \times \boldsymbol Y$ is called a rectangle.

4.2 Products of pretransitive logics

Proof. Consider a chain $[a_1] < [a_2] < \cdots < [a_{h_1}]$ in $\mathop {\mathrm {Sk}} F$ and a chain $[b_1]< [b_2] < \cdots < [b_{h_2}]$ in $\mathop {\mathrm {Sk}} G.$ Then there is a chain of $h_1 + h_2 - 1$ elements in $\mathop {\mathrm {Sk}} (F\times G)$ :

$$\begin{align*}[(a_1,\,b_1)] < [(a_2,\,b_1)] < \cdots < [(a_{h_1},\,b_1)] < [(a_{h_1},\,b_2)] < \cdots < [(a_{h_1},\,b_{h_2})]. \end{align*}$$

Hence, $h(F\times G) \geq h_1 + h_2 -1$ .

For the converse direction, we prove by induction that for any chain $[(a_1,b_1)] < \cdots < [(a_l,b_l)]$ in $\mathop {\mathrm {Sk}}(F\times G)$ there exists a chain $[c_1] < \cdots < [c_m]$ in $\mathop {\mathrm {Sk}} F$ and a chain $[d_1] < \cdots < [d_n]$ in $\mathop {\mathrm {Sk}} G$ such that $a_1 = c_1,\,a_l = c_m,\,b_1 = d_1,\,b_l = d_n, $ and $m + n \ge l + 1.$ The base case is trivial. For the induction step, consider a chain $[(a_1,b_1)] < \cdots < [(a_{l+1},b_{l+1})]$ in $\mathop {\mathrm {Sk}}(F\times G)$ . The induction hypothesis holds for $\{[(a_i,b_i)]\}_{1 \le i \le l}$ , so let $\{c_i\}_{1 \le i \le m}$ and $\{d_i\}_{1 \le i \le n}$ be the corresponding chains in $\mathop {\mathrm {Sk}} F$ and $\mathop {\mathrm {Sk}} G$ , respectively. Then $[a_{l+1}] \ge [c_m]$ in $\mathop {\mathrm {Sk}} F$ and $[b_{l+1}] \ge [d_n]$ in $\mathop {\mathrm {Sk}} G$ . Moreover, at least one of these inequalities is strict, since otherwise $[(a_{l+1},b_{l+1})] = [(c_m,d_n)] = [(a_l,b_l)]$ . It follows that $[c_1],\,\dots ,\,[c_m],\,[a_{l+1}]$ is a strict chain in $\mathop {\mathrm {Sk}} F$ or $[d_1],\,\dots ,\,[d_n],\,[b_{l+1}]$ is a strict chain in $\mathop {\mathrm {Sk}} G$ , and the induction statement follows. Since $m\leq h_1$ and $n \leq h_2$ , we obtain $l\leq h_1+h_2 - 1$ .

For a formula $\varphi $ in the alphabet $\{\lozenge _1,\lozenge _2\}$ , we define the translation as follows. Let ${ [\varphi ]}^{m,n}$ be compatible with Boolean connectives, and let ${ [\lozenge _1 \psi ]}^{m,n}= \lozenge _{\mathrm {A}}^{\leq m} { [\psi ]}^{m,n}$ , ${ [\lozenge _2 \psi ]}^{m,n}= \lozenge _{\mathrm {B}}^{\leq n} { [\psi ]}^{m,n}$ . The following is straightforward.

Proposition 4.9. Let $\mathcal {F}$ and $\mathcal {G}$ be classes of m- and n-transitive clusters, respectively. If $\sup \{|F| \mid F\in \mathcal {F}\}$ and $\sup \{|G | \mid G\in \mathcal {G}\}$ are infinite, then

4.3 Bounded cluster property

Recall that for a class $\mathcal {F}$ , $Cl{(\mathcal {F})}$ denotes the class of clusters occurring in frames in $\mathcal {F}$ , and that $\mathcal {F}$ has the bounded cluster property, if for some $n<\omega $ , $|C| \le n$ for all $C\in Cl{(\mathcal {F})}$ .

Proof. Let $\mathcal {V}$ be a finite partition of $F\times G$ , $n=|\mathcal {V}|$ .

Define $\alpha :\:\mathop {\mathrm {dom}} F \to \mathcal {V}^{\mathop {\mathrm {dom}} G}$ by

$$\begin{align*}\alpha(a) = ([(a,\,b)]_{\mathcal{V}})_{b\in\mathop{\mathrm{dom}} G},\quad a\in \mathop{\mathrm{dom}} F. \end{align*}$$

Then $\alpha $ induces a partition of F of cardinality at most $n^{|G|}.$ Since F is f-tunable, there is a refinement $\mathcal {U}$ of this partition such that $|\mathcal {U}|\le f\left (n^{|G|}\right )$ and $\mathcal {U}$ is tuned in F.

For $(a,b)$ in $F\times G$ , put $\beta (a,b) = ([a]_{\mathcal {U}},\,b)$ . Then $\beta $ induces a refinement $\mathcal {S}$ of $\mathcal {V}$ of cardinality at most $f\left (n^{|G|}\right )| G|.$ We show that $\mathcal {S}$ is tuned in $F\times G$ .

Let $R_\lozenge $ be a relation of $F,$ and suppose $(a_1,b) R_\lozenge ^h (a_2,b)$ in $F\times G$ . Then $a_1 R_\lozenge a_2.$ Let $(a_1',b')\in [(a_1,b)]_{\mathcal {S}}.$ Then $b'=b$ and $[a_1']_{\mathcal {U}} = [a_1]_{\mathcal {U}}$ . We have $a_1' R_\lozenge a_2'$ for some $a_2'\in [a_2]_{\mathcal {U}}$ , since $\mathcal {U}$ is tuned in F. Then $(a_1',b') R_\lozenge ^h (a_2',b)$ and $(a_2',b)\in [(a_2,b)]_{\mathcal {S}}$ .

Now let $(a,b_1) R_\lozenge ^v (a,b_2)$ , where $R_\lozenge $ is a relation of $G.$ Let $(a',b_1') \in [(a,b_1)]_{\mathcal {S}}.$ Then $b_1' = b_1 $ , so $b_1' R_\lozenge b_2.$ Moreover, $[a']_{\mathcal {U}}$ = $[a]_{\mathcal {U}}$ , so $\beta (a',b_2) = \beta (a,b_2)$ . Hence, we have $(a',b_1') R_\lozenge ^v (a',b_2)$ and $(a',b_2)\in [(a,b_2)]_{\mathcal {S}}$ .

4.4 Product reducible path property

Proof. For the sake of contradiction, assume that for all $l<\omega $ there are $F\in \mathcal {F}$ and $G\in \mathcal {G}$ , a cluster C in F and a cluster D in G such that $|C|,|D|>l$ . Let $H=F^*\times G^*$ . Pick distinct $x_0,\ldots , x_l\in C$ and distinct $y_0,\ldots ,y_l\in D$ and consider $a_0,\ldots , a_{2l}$ in H, where $a_{2i}=(x_i,y_i)$ , and $a_{2i+1}=(x_i,y_{i+1})$ . Then the zigzag path

$$ \begin{align*}a_0R_H a_1 R_H a_2 R_H \ldots R_H a_{2l} \end{align*} $$

falsifies $\mathrm {RP}_{2l-1}$ in H. It follows that $\mathrm {RP}_m$ holds in $\mathcal {F}^*\times \mathcal {G}^*$ for no m, and so $\mathcal {F}^*\times \mathcal {G}^*$ lacks the rpp.

From Theorem 4.12 and Proposition 4.13, we obtain the following corollary.

Let $\mathrm {rp}_m(k,n)$ denote the formula $\mathrm {rp}_m(\bar {\lozenge })$ , where $\bar {\lozenge }\varphi $ abbreviates $\lozenge _{\mathrm {A}}^{\leq k}\varphi \vee \lozenge _{\mathrm {B}}^{\leq n}\varphi $ . These formulas are called product rpp formulas.

It follows from Theorem 3.1 that these formulas are necessary for local tabularity. Indeed, consider a locally tabular logic L over $\mathrm {A}\cup \mathrm {B}$ . For a formula , let $t(\varphi )$ be the translation of $\varphi $ that is compatible with Boolean connectives and satisfies $t(\lozenge \varphi ) = \lozenge ^{\leq k}_{\mathrm {A}} t(\varphi ) \lor \lozenge _{\mathrm {B}}^{\leq n} t(\varphi ).$ Let Then $L_0$ is a normal unimodal logic, and it is locally tabular since L is. So $L_0$ contains $\mathrm {rp}_m(\lozenge )$ for some m. Hence, L contains $\mathrm {rp}_m(k,n) = t(\mathrm {rp}_m(\lozenge )).$ So we have the following proposition.

Note that if $\mathrm {A} = \{\lozenge _1,\,\lozenge _2\}$ , $F = (X, R_1, R_2)$ , and both $R_1$ and $R_2$ are preorders, then the following are equivalent:

1. 1. $F \models \mathrm {rp}_m(1,1)$ ;

2. 2. $(X, R_1\cup R_2)$ satisfies $\mathrm {RP}_m$ ;

3. 3. $(X, R_F)$ satisfies $\mathrm {RP}_m$ ;

4. 4. $F \models \mathrm {rp}_m(\lozenge _{\mathrm {A}}).$

Hence, in the case of two preorders, rpp and product rpp are equivalent. This equivalence does not hold in general.

4.5 $1$ -finiteness

It is known that above , 1-finiteness is sufficient for local tabularity [Reference Maksimova22]. In general, there are 1-finite logics that are not locally tabular [Reference Shapirovsky31, Reference Shapirovsky32]. We show that for products of locally tabular logics, $1$ -finiteness guarantees local tabularity.

Proof. Assume that $\mathop {\mathrm {Log}}\mathcal {F}$ and $\mathop {\mathrm {Log}}\mathcal {G}$ are locally tabular. Let $\mathcal {C}_1=Cl{(\mathcal {F})}$ , $\mathcal {C}_2=Cl{(\mathcal {G})}$ , and let $\mathcal {I}$ be the class of rectangles $\boldsymbol X_1 \times \boldsymbol X_2$ such that $X_j$ is the domain of $C_j\in \mathcal {C}_j$ , $j=1,2$ .

For the sake of contradiction, assume that $\mathop {\mathrm {Log}}(\mathcal {F}\times \mathcal {G})$ is not locally tabular. Then according to Theorems 4.1 and 4.12. It is known that is not 1-finite [Reference Henkin, Monk and Tarski18, Theorem 2.1.11(i)]. Hence, for each l, there is a model $M=(I,\theta )$ on $I\in \mathcal {I}$ and formulas $\psi _1, \ldots , \psi _l$ in the single variable p such that all sets $\bar {\theta }(\psi _i)$ are pairwise distinct (Mal’cev’s criterion, Theorem 2.2). Consider the frames F in $\mathcal {F}$ and G in $\mathcal {G}$ with clusters $C_1$ in F and $C_2$ in G that form the rectangle I. Let H be the subframe of $F\times G$ generated by a point in $C_1\times C_2$ . Consider a model $M'=(H,\theta ')$ with $\theta '(p)=\theta (p)$ .

Assume that $l>2$ . Then $\theta (p)\neq \varnothing $ : otherwise, every formula in the single variable p is equivalent to either $\bot $ or $\top $ on M. By Theorem 2.4, for some $m,n$ , every frame in $\mathcal {F}$ is m-transitive and every frame in $\mathcal {G}$ is n-transitive. Let $\bar {\lozenge } p$ abbreviate $\lozenge _{\mathrm {A}}^{\leq m} \lozenge _{\mathrm {B}}^{\leq n} p$ . By Proposition 4.3, we have

$$ \begin{align*}M',a\vDash \bar{\lozenge} p \ \text{iff} \ a \ \text{belongs to } C_1\times C_2. \end{align*} $$

For bimodal formulas $\varphi $ in the single variable p, we define $t(\bot )=\bot $ , $t(p)=p$ , $t(\psi _1\rightarrow \psi _2)=\bar {\lozenge } p\wedge ( t(\psi _1)\rightarrow t(\psi _2))$ , and $t(\lozenge _1 \psi )=\bar {\lozenge } p \wedge \lozenge _{\mathrm {A}}^{\leq m} t(\psi )$ , $t(\lozenge _2 \psi )=\bar {\lozenge } p\wedge \lozenge _{\mathrm {B}}^{\leq n} t(\psi )$ . Then we have

$$ \begin{align*} M',a\vDash t(\varphi) \ \text{iff} \ (a \ \text{is} \ \text{in} \ M \text{and} \ M,a\vDash \varphi). \end{align*} $$

So formulas $t(\psi _1), \ldots , t(\psi _l)$ are pairwise non-equivalent in $M'$ . It follows that $\mathop {\mathrm {Log}}(\mathcal {F}\times \mathcal {G})$ is not 1-finite.

4.6 Main results

We combine our earlier results in the form of the following two criteria.

Recall that for a pretransitive logic L, its pretransitivity index $\mathrm {tra}{(L)}$ is the least k such that L is k-transitive. By Theorem 2.4, $\mathrm {tra}{(L)}$ is defined for every locally tabular logic.

6.1 Product fmp fails for a locally tabular product logic

We define the saw frame $F_S = (W,S,S_l,S_r)$ for the alphabet $\mathrm {A} = \{\lozenge ,\,\lozenge _l,\,\lozenge _r\}$ as follows:

$$ \begin{gather*} W = \{u\} \sqcup \{v_i\}_{i < \omega} \sqcup \{w_i\}_{i < \omega}; \\ S = \{u\} \times \{v_i\}_{i < \omega}; \\ S_l = \{(v_i,w_i)\}_{i < \omega}; \\ S_r = \{(v_i,w_{i+1})\}_{i < \omega}. \end{gather*} $$

The saw frame is shown in Figure 1.

Figure 1

The saw frame $F_S$ .

Let The next proposition follows from simple semantic observations.

Proposition 6.1. The following formulas are theorems of :

(5) $$ \begin{align} &\Box_{\mathrm{A}}^3 \bot; \end{align} $$

(6) $$ \begin{align} \lozenge \lozenge_r &p \to \lozenge \lozenge_l p. \end{align} $$

We define the formula as $\varphi = \varphi _1 \land \varphi _2 \land \varphi _3,$ where

Proof. Let be valid in a rooted frame $F = (X,R,R_l,R_r)$ with a root r and let $G = (Y,Y\times Y).$ Assuming that $\varphi $ is true at $F\times G,\theta ,(r,s)$ for some valuation $\theta $ and a point $s \in Y,$ we will show that X is infinite.

Let us show by induction that there exist sequences $\{m_i\}_{i < \omega },\,\{a_i\}_{i < \omega } \subseteq X$ and $\{b_i\}_{i < \omega }\subseteq Y$ such that the following are true for all $i < \omega $ :

(7) $$ \begin{align} &r R m_i R_l a_i; \end{align} $$

(8) $$ \begin{align} \text{for any } k < j \le i,\ &(a_k,b_k) \not\models p \text{ and }(a_j,b_k)\models p. \end{align} $$

By the assumption $\varphi _1$ is true at $(r,s),$ so $(r,s) R^h (m_0,s) R^h_l (a_0,s)$ for some $m_0,\,a_0 \in X.$ Then in the base case (7) holds, and (8) holds vacuously.

For the induction step, we assume that $\{m_j\}_{j \le i},\,\{a_j\}_{j \le i},$ and $\{b_j\}_{j < i}$ satisfying (7) and (8) are already constructed. Let us define $b_i$ , $m_{i+1},$ and $a_{i+1}$ . Since $\varphi _2$ is true at $(r,s)$ and $(r,s) R^h (m_i,s)$ , there exists $b_i \in Y$ such that p is false in $R_l^h(m_i,b_i)$ and true at some point $(a_{i+1},b_i)\in R^h_r(m_i,b_i).$ Then $m_i R_r a_{i+1}$ and therefore $a_{i+1} \in R\circ R_r(r)$ . The frame condition of (6) holds in F by Proposition 6.1, which means that $R \circ R_r \subseteq R \circ R_l$ . Then there exists $m_{i+1}$ such that $r R m_{i+1} R_l a_{i+1}$ , so (7) holds for $i + 1$ .

To complete the induction, it remains to prove (8) for $k < j \le i + 1.$ The induction hypothesis implies this condition for $k < j \le i$ , so we only need to show it for $j = i + 1$ and $k < j$ . The point $b_i$ was defined in such a way that p is true at $(a_{i+1}, b_i)$ . For all $k < i$ , p is also true at $(a_i, b_k)$ by the induction hypothesis, so $\varphi _3$ forces that $(a_{i+1}, b_k)$ satisfies p since $(m_i, b_k) R_l^h (a_i, b_k)$ and $(m_i,b_k) R_r^h (a_{i+1}, b_k)$ . Finally, recall that p is false in $R^h_l(m_i,b_i)$ . Since $m_i R_l a_i$ by the induction hypothesis, p is false at $(a_i,b_i)$ . Thus we proved the step.

Now (8) implies that $\{a_i\}_{i < \omega }$ is infinite. Indeed, for any $k < i < \omega $ we have $(a_k,b_k)\not \models p$ and $(a_i,b_k) \models p$ by (8), so $a_i \ne a_k$ . Thus $a_i$ are pairwise distinct for $i < \omega $ . It follows that X is infinite.

6.2 Product fmp and products of small height

As follows from Theorem 2.4 and Corollary 4.22, it is necessary for any locally tabular product of two logics that both have a finite height and one of them contains a bounded cluster formula. We will discuss how the product fmp depends on the height of $L_1$ and $L_2.$ For this section, we will assume that $L_1$ and $L_2$ are locally tabular, and that $L_1 \vdash [\mathrm {bc}_n]^{\mathrm {tra}{(L_1)}}$ for some $n < \omega $ .

By Theorem 6.5, the product fmp can fail even when $h(L_2) = 1$ . Thus we will focus on the height of $L_1.$

If $L_1$ has unit height, then the product fmp follows from the following result.

The logic $L_1$ is complete with respect to the class of its finite rooted frames by Proposition 2.1. Every such frame has unit height, so it consists of one cluster, which has size at most n by the frame condition of $[\mathrm {bc}_n]^{\mathrm {tra}{(L_1)}}$ . Then $L_1$ is tabular, so the product fmp for $L_1\times L_2$ follows by Proposition 6.6.

Proposition 6.4 shows that the product fmp can fail when $h(L_1)=3.$ The tabularity of $L_1$ or $L_2$ is a sufficient condition for the product fmp in this case, as well as for greater $h(L_1)$ . Describing weaker sufficient conditions is an open problem.

Finally, the case when $L_1$ has height $2$ is the most intriguing. Neither a proof, nor a counterexample for the product fmp of such logics is known yet.

7.1 Preliminaries: Commutators of logics

Let $L_1$ be an $\mathrm {A}$ -logic and $L_2$ be a $\mathrm {B}$ -logic. The fusion $L_1*L_2$ is the smallest $(\mathrm {A}\cup \mathrm {B})$ -logic that contains $L_1 \cup L_2.$ The commutator $\left [L_1,L_2\right ]$ is the smallest logic that contains $L_1*L_2$ and the formulas $ \lozenge _a \lozenge _b p \leftrightarrow \lozenge _b \lozenge _a p,\, \lozenge _a \Box _b p \to \Box _b \lozenge _a p $ for all $\lozenge _a\in \mathrm {A}$ and $\lozenge _b\in \mathrm {B}.$

In an $(\mathrm {A}\cup \mathrm {B})$ -frame, these formulas express commutativity $R_a\circ R_b = R_b \circ R_a$ and the Church–Rosser property

$$ \begin{align*} \forall x\,\forall y\,\forall z\,(x R_a y\,\&\,x R_b z \to \exists u\,(y R_b u\,\&\,z R_a u)). \end{align*} $$

For any $L_1$ and $L_2,$ the product logic $L_1\times L_2$ is a normal extension of $\left [L_1,L_2\right ]$ [Reference Gabbay, Kurucz, Wolter and Zakharyaschev11, Section 5.1].

7.2 The product rpp criterion

Recall that a logic is tabular, if it is characterized by a single finite frame. A non-tabular logic is pretabular, if all of its proper extensions are tabular. There are exactly five pretabular logics above (see [Reference Esakia and Meskhi10, Reference Maksimova21] or [Reference Chagrov and Zakharyaschev9, Section 12.3]). One of them is the logic . Another is the logic defined below.

An important fact about was established in [Reference Bezhanishvili5]: this logic is prelocally tabular, that is, the following theorem holds.

In this section we observe that for another pretabular logic , despite its similarities with , the product is not prelocally tabular. Then we give an axiomatic criterion of local tabularity for a family of logics, which in particular contains and its extensions.

The (one-dimensional) tack frame is the ordered sum $(\omega +1,R)$ of a countable cluster and a singleton, that is, $\alpha R \beta $ iff $\alpha <\omega $ or $\beta =\omega $ . Let be the logic of its frame.

The description of locally tabular extensions of (and, in fact, of a weaker logic) can be obtained via the product rpp formulas. We say that the product rpp criterion holds for a logic L above , if for any normal extension $L'$ of L, we have:

$$ \begin{align*} L' \text{ contains a product rpp formula } \mathrm {rp}_m(1,1) \text{ iff } L' \text{ is locally tabular}. \end{align*} $$

Recall that $L[h]$ denotes the extension of L with the axiom $B_h$ of finite height.

The unimodal logic is the extension of with the axiom $\Box \lozenge p\rightarrow \lozenge \Box p$ . In transitive frames, $\Box \lozenge p\rightarrow \lozenge \Box p$ defines the first-order property

(9) $$ \begin{align} \forall x\,\exists y\,\left(xRy \land \forall z \left(yRz \to z = y\right)\right), \end{align} $$

see, e.g., [Reference Blackburn, de Rijke and Venema6, Section 3.7].

Hence, in our notation, the unimodal logic is the extension of with the axioms $\Box \lozenge p\rightarrow \lozenge \Box p$ and $B_2$ . In particular, the tack frame T has this property; since it is transitive and has height .

We are going to show that the product rpp criterion holds for .

We say that a bimodal frame $(X,R,\approx )$ is simple, if $\approx $ is $X\times X$ .

7.3 Two-dimensional tack

A prelocally tabular logic has height $1$ . In this section, we give another example of a prelocally tabular logic above , which has height $2$ .

We define the semi-ordered sum $F \oplus G$ of disjoint bimodal frames $F = (X,R_1,R_2)$ and $G = (Y,S_1,S_2)$ as $(X\cup Y, R_1 \cup S_1 \cup (X \times Y), R_2 \cup S_2).$ Let $\circ $ denote the reflexive, with respect to both relations, singleton $(\{0\},R,S)$ with $R = S = \{(0,0)\}.$

Let . The two-dimensional tack is the frame . Let We show that is canonical, has the finite model property, and is prelocally tabular.

Firstly, we identify some axioms of , study its abstract frames, and then give a complete axiomatization.

Notice that the composition of relations $R=R_1\circ R_2$ in is a preorder. Let $\lozenge $ denote the compound modality $\lozenge _1\lozenge _2$ .

Observe that the skeleton of is a two-element chain. Hence, contains the axiom of height two for the compound modality $\lozenge $ . Moreover, the height of the first relation in is 2, so the fragment of in the first modality contains . Clearly, its fragment in the second modality is .

Moreover, our observation about the skeleton being the two-element chain implies the following modally definable properties. Clearly, the composition $R_1\circ R_2$ in satisfies the Church–Rosser property, and hence, the formula $\lozenge \Box p\rightarrow \Box \lozenge p$ , which is an abbreviation for

(10) $$ \begin{align} \lozenge_1\lozenge_2 \Box_1\Box_2 p\rightarrow\Box_1\Box_2 \lozenge_1\lozenge_2 p, \end{align} $$

is a valid principle of . In the combination with height 2, it follows that in every rooted -frame, there is a top cluster (i.e., the greatest in the skeleton). Next, observe that R satisfies the condition (9). It follows that the formula $\Box \lozenge p\rightarrow \lozenge \Box p$ , which is an abbreviation for

(11) $$ \begin{align} \Box_1\Box_2\lozenge_1\lozenge_2 p\rightarrow\lozenge_1\lozenge_2\Box_1\Box_2 p, \end{align} $$

belongs to the logic . In particular, it follows that in every rooted -frame, the top cluster is a singleton.

Our next step aims to express the symmetry property in the bottom cluster of an arbitrary rooted -frame (notice that in clusters of -frames, the symmetry of the first relation is not guaranteed). Consider the following relativized version of the symmetry axiom:

(12) $$ \begin{align} \lozenge_1\Box_1 q \wedge \neg q\wedge p\rightarrow \Box_1 (\neg q\rightarrow \lozenge_1 p). \end{align} $$

Readily, this formula is valid in . Let F be a point-generated -frame of height 2. We claim that its rooted cluster C, considered as a frame-restriction, validates . Given the axiomatization of from Proposition 7.1, it suffices to show the symmetry of $R_1$ . Indeed, assume that $x,y\in C$ are connected by the first relation $R_1$ . Then consider a valuation $\theta $ in F with $\theta (q)$ being the top cluster, and $\theta (p)=\{x\}$ . The validity of (12) implies that $yR_1 x$ , which proves the claim.

Let L be the extension of the commutator with the axioms (10)–(12). Putting our observations together, we obtain the following lemma.

Our next goal is to prove completeness.

It follows from Lemma 7.7 that has an analog of the product fmp:

Proof. Let L be the mentioned axiomatic extension of .

Firstly, we show that L is canonical. The axioms of are known to be canonical, in particular, canonicity of the finite height formula is given in [Reference Segerberg26, Theorem 6.4]. It is immediate that (12) is equivalent to the Sahlqvist formula

$$ \begin{align*}\lozenge_1\Box_1 q \wedge p\rightarrow \Box_1( q \vee \lozenge_1 p)\vee q, \end{align*} $$

and so is canonical. The formula $\lozenge \Box p \rightarrow \Box \lozenge p$ is also Sahlqvist.

The formula $\Box \lozenge p \rightarrow \lozenge \Box p$ is not a Sahlqvist formula. However, it is well-known that it is canonical in the transitive case, which, in our setting, pertains to the composition $R_1\circ R_2$ . Hence, we have a singleton cluster above every point in the canonical frame of L.

It follows that L is canonical.

Let us show that . Since L is canonical, it is Kripke complete, and so, in view of Lemma 7.6, L is included in the logic of the class

It is straightforward that $\mathcal {F}\vDash L$ , so $L=\mathop {\mathrm {Log}}(\mathcal {F})$ . From Lemma 7.7, the logic of $\mathcal {F}$ is .

Proof. Let L be an extension of . Let $F_k$ denote the k-generated canonical frame of L. For a set $\Psi $ of formulas, let $\Psi {\upharpoonright }{k}$ denote the set of all k-formulas in $\Psi $ .

Consider two cases.

First, assume that for each finite k, each point-generated subframe in $F_k$ is finite. It is straightforward that in this case $\mathop {\mathrm {Log}}(F_k){\upharpoonright }{k}=L{\upharpoonright }{k}$ . In particular, it follows that $L=\bigcap _{k<\omega }\mathop {\mathrm {Log}}(F_k)$ , and so L is Kripke complete. By Lemma 7.11, if L is a proper extension of , it is locally tabular.

Now assume that for some finite k, there is an infinite point-generated subframe in $F_k$ . We show that in this case .

Let us list some properties of $F_k$ . Since is canonical (Theorem 7.9), and L contains , $F_k$ is a -frame. The top clusters in $F_k$ are singletons. Let $\mathcal {C}$ be the family of non-top clusters in $F_k$ . In view of Lemma 7.6, $\mathcal {C}$ consists of -frames. We also have:

(13) $$ \begin{align} \text{For} \ C\in \mathcal{C}, \text{ there is a unique cluster} \ D \ \text{above} \ C, \text{ and} \ D\ \text{is a singleton.} \end{align} $$

It follows that there is an infinite cluster C in $\mathcal {C}$ . Let D be the cluster above C. Put $X=C\cup D$ . By (13), the restriction $F_k{\upharpoonright } X$ is a generated subframe of $F_k$ .

Consider the extension of with the axiom of height 1, which makes the composite relation $R_1\circ R_2$ an equivalence. Clearly, is locally tabular (even tabular, since this is the logic of the singleton $\circ $ ). It follows that the set T of points in top clusters in $F_k$ is definable [Reference Shapirovsky31, Theorem 5.1]: there exists a formula $\psi _T$ such that

(14) $$ \begin{align} \psi_T\in x \text{ iff } x\in T. \end{align} $$

Hence, for every x in X,

(15) $$ \begin{align} x\in C \text{ iff } \psi_T\notin x. \end{align} $$

Let $\Psi $ be the set of all bimodal formulas in k variables. For a formula $\psi \in \Psi $ , let $\theta (\psi )=\{x \in X \mid \psi \in x\}$ and $\eta (\psi )=\{x \in C \mid \psi \in x\}$ .

Let A denote the powerset modal algebra of the cluster-frame $F_k{\upharpoonright } C$ , and let B be its subalgebra generated by the sets $\eta (p_i)$ , $i<k$ .

By a straightforward induction on the structure of formulas, we have:

(16) $$ \begin{align} \text{For every} \ b\in B, \text{there is} \ \psi\in\Psi \ \text{such that} \ b=\eta(\psi). \end{align} $$

Since C is infinite, B is infinite as well: any two distinct points in C are separable by some formula. Hence, B is a finitely generated infinite -algebra. The logic of B is not locally tabular, thus it is by Theorem 7.2.

Let G be the general frame on $F_k{\upharpoonright } C$ , whose admissible subsets are elements of B. Since its logic is (the logic of B), for each finite m there is a p-morphism $f_m: F_k{\upharpoonright } C \twoheadrightarrow \boldsymbol m \times \boldsymbol m$ such that preimages of subsets of $\boldsymbol m \times \boldsymbol m$ are in B: it follows from the standard technique using Jankov–Fine formulas $\chi _m$ of the squares $\boldsymbol m \times \boldsymbol m$ . Namely, since the logic of G is , every $\chi _n$ is satisfiable in G, encoding a p-morphism from a point-generated subframe of G onto $\boldsymbol m \times \boldsymbol m$ . It remains to notice that every point-generated subframe of G is G.

Let be the extension of $f_m$ that maps the top to the top. Clearly, $g_m$ is a p-morphism (of Kripke frames). For any subset V of $\boldsymbol m \times \boldsymbol m$ , its preimage $g_m^{-1}(V)$ is defined in $F_k{\upharpoonright } X$ by $\psi \land \lnot \psi _T$ , where $\psi $ defines $g_m^{-1}(V)$ in G according to (16), and the preimage of the top singleton is defined by $\psi _T$ . Therefore validates the logic of the general frame $(F_k{\upharpoonright } X,U)$ , where ${U = \{\theta (\psi )\mid \psi \in \Psi \}}$ . Then, since $(F_k{\upharpoonright } X,U)$ is a generated subframe of the k-canonical general frame of L, we have Since m was arbitrary, , where the intersection equals by Corollary 7.8. Consequently, .