1 Introduction↩︎

 

It is well-known that the operation of product of modal logics does not preserve the finite model property of the factors, see, e.g., [1],[2], or the monography [3]. In this paper we describe new families of modal products which have the finite model property and, in fact, satisfy a stronger property of local tabularity.

A logic is locally tabular, if each of its finite-variable fragments contains only a finite number of pairwise nonequivalent formulas. In particular, every locally tabular logic has the finite model property. It is well known that for unimodal logics above \({\mathrm{\small K4}}\), local tabularity is equivalent to finite height [4],[5]. In the non-transitive unimodal, and in the polymodal case, no axiomatic criterion of local tabularity is known.

It follows from [6] that the product of a locally tabular logic with a tabular one is locally tabular. However, these cases are not exhaustive: other families of locally tabular modal products were identified in [7], see also [8]. For close systems, intuitionistic modal logics and expanding products, locally tabular families were identified in [9], [10], [11], and a recent manuscript [12].

In the product \(L_1\times L_2\) of two Kripke complete consistent logics, local tabularity of \(L_1\) and \(L_2\) is necessary for local tabularity of \(L_1\times L_2\). However, it is not sufficient: the product of two locally tabular logics can be not locally tabular. The simplest example is the logic \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) [13]. We provide extra semantic (Theorem 26) and axiomatic (Corollary 3) conditions which give criteria of local tabularity of the product of two locally tabular logics: bounded cluster property of one of the factors; a condition we call product reducible path property; finiteness of the one-variable fragment of the product.

In Section 4, we apply the criteria to identify new families of locally tabular products. In particular, we generalize some results from [7], [8].

In Section 5, we discuss the product finite model property in the locally tabular case. A modal logic \(L\) has the product fmp, if \(L\) is the logic of a class of finite product frames. The product fmp is stronger than the fmp: for example, \({\mathrm{\small K4}}\times {\mathrm{\small S5}}\) has the fmp [14], but lacks the product fmp [3]. It is perhaps surprising that the local tabularity of a product logic does not imply the product fmp even in the case of height 3, as we discovered in Theorem 31.

In Section 6, we discuss local tabularity and prelocal tabularity in extensions of \({\mathrm{\small S4}}\times{\mathrm{\small S5}}\). The logic \({\mathrm{\small S5}}\) is known to be one of the five pretabular logics above \({\mathrm{\small S4}}\) [15], [16]. We observe that for another pretabular logic \({\mathrm{\small Tack}}\), the logic of the ordered sum of a countable cluster and a singleton, the product \({\mathrm{\small Tack}}\times {\mathrm{\small S5}}\) is not prelocally tabular. Then we consider a weaker than \({\mathrm{\small Tack}}\) logic \({\mathrm{\small S4}}.1 [ 2 ]\), the extension of \({\mathrm{\small S4.1}}\) with the axiom of height 2, and give an axiomatic criterion of local tabularity for all normal extensions of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\). Finally, we discuss prelocal tabularity. It is known that \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) is prelocally tabular [17]. We construct a frame of height two, which we call two-dimensional tack, and show that its logic is another example of a prelocally tabular logic above \({\mathrm{\small S4}}\times {\mathrm{\small S5}}\).

2 Preliminaries↩︎

For basic notions in modal logic, see, e.g., [18] or [19].

2.1 Modal syntax and semantics.↩︎

Let \(\mathrm{A}\) be a finite set, an alphabet of modalities. Modal formulas over \(\mathrm{A}\), \({\mathrm{\small ML}}(\mathrm{A})\) in symbols, are constructed from a countable set of variables \({\mathrm{\small PV}}=\{p_0,p_1,\ldots\}\) 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\), \(\Box^{\leq m} \varphi=\neg \lozenge^{\leq m} \neg \varphi\). We write \(\lozenge_\mathrm{A}\varphi\) for \(\bigvee_{\lozenge\in\mathrm{A}}\lozenge\varphi\).

By an \(\mathrm{A}\)-logic we mean a normal modal logic whose alphabet of modalities is \(\mathrm{A}\), see, e.g. [19]. The terms unimodal and bimodal refers 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 \(\theta:\:PV \to \mathcal{P}(X)\), 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, for \(\lozenge\in \mathrm{A}\), \((F,\,\theta),\,a\models \lozenge\varphi\) means that \((F,\,\theta),\,b\models \varphi\text{ for some }b\in R_\lozenge(a)\). We put \[\bar{\theta}(\varphi)=\{a\mid (F,\theta),a\vDash\varphi\}.\] A formula \(\varphi\in {\mathrm{\small ML}}(\mathrm{A})\) 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 \(\Gamma\subseteq {\mathrm{\small ML}}(\mathrm{A})\), \(F\vDash\Gamma\) means 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}\), \(\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}=\bigcap\{\mathop{\mathrm{Log}}F \mid F\in \mathcal{F}\}\); this set is a logic [19] and is called the logic of \(\mathcal{F}\). Such logics are said to be Kripke complete.

Let us recall that \({\mathrm{\small K4}}\) is the smallest unimodal logic that contains \(\lozenge\lozenge p \to \lozenge p\), \({\mathrm{\small S4}}\) extends \({\mathrm{\small K4}}\) with \(p\rightarrow\lozenge p\), and \({\mathrm{\small S5}}\) extends \({\mathrm{\small S4}}\) 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., [19] or [18].

The notions of generated subframe and p-morphism (or bounded morphism) are defined in the standard way, see, e.g., [19]. 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. \(f\) is a homomorphism, that is for any \(a,\,b\in X\) and \(\lozenge\in \mathrm{A},\) \(a R_\lozenge b\) implies \(f(a) S_\lozenge f(b)\), and

2. \(f\) satisfies the back condition, that is 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}\) [19].

For a frame \(F = (X,\,(R_\lozenge)_{\lozenge\in A})\) and an equivalence \(\approx\) on \(F\), 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}\), \[[a] R^\approx_\lozenge[b] \text{ iff }\exists a'\in[a]\;\exists b'\in [b]\;\left(a' R_{\lozenge} b' \right).\]

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,\,b\in Y,\,a R_\lozenge a'\} &\text{ for }\lozenge\in \mathrm{A};\\ R^v_\lozenge&= \{((a,\,b),\,(a,\,b'))\mid a\in X,\,b,\,b'\in Y,\,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 \[L_1\times L_2 = \mathop{\mathrm{Log}}\{F\times G \mid F\models L_1,\,G\models L_2\}.\] 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\).

2.3 Local tabularity and local finiteness.↩︎

For finite \(k\), a logic \(L\) is \(k\)-finite, if \(L\) contains only a finite number of pairwise nonequivalent formulas in variables \(p_i\), \(i<k\). \(L\) is said to be locally tabular, if it is \(k\)-finite for all finite \(k\). The following fact is well known, see, e.g., [18].

In algebraic terms, local tabularity of a logic means that its Lindenbaum algebra is locally finite, which, in turn, means that the variety of its algebras is locally finite (see, e.g., [20], [18] for corresponding notions).

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 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, \(R^0\) is the diagonal relation on \(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^*\).¹ \(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 [22]: \[\label{pretr:sem} \text{ R_F is m-transitive iff F\vDash\lozenge_\mathrm{A}^{m+1} p \rightarrow\lozenge_\mathrm{A}^{\leq m} p. }\tag{1}\] 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\).

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 \[\label{eq:pretrans} F\vDash{ [\varphi ]}^{m} \text{ iff } F^*\vDash\varphi.\tag{2}\] where \({ [\varphi ]}^{m}\) is the translation that is compatible with Boolean connectives (that is, \({ [\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\).

We say that \(F\) has a finite height \(h\), in symbols \(h(F)=h\), if \(\mathop{\mathrm{Sk}}F\) contains a chain of \(h\) elements and no chains of more than \(h\) elements. Consider unimodal formulas \[B_0 = \bot,\quad B_{i+1} = p_{i+1}\rightarrow\Box \left (\lozenge p_{i+1} \lor B_i\right).\] For a unimodal frame \(G=(X,R)\) with a transitive \(R\), we have [4]: \[G\vDash B_h \text{ iff }h(G)\leq h.\] 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.\)

In [23], this fact was stated for the unimodal case; its polymodal generalization is straightforward, details can be found in [24].

2.5 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}\).

The following theorem is a Kripke-style version of Malcev criterion:

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 \[\mathop{\mathrm{Sub}}{\mathcal{F}}=\{F{\upharpoonright}Y\mid F\in \mathcal{F}\text{ and } \varnothing\neq Y\subseteq \mathop{\mathrm{dom}}{F}\}.\]

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}\): \[Cl{(\mathcal{F})}=\{F{\upharpoonright}C\mid C \text{ is a cluster in } F\in\mathcal{F}\}.\] 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 [23], Theorems 5 and 7 were stated for the unimodal case. Their polymodal generalizations are straightforward. For Theorem 5, details are given in [24]. The polymodal version of Theorem 7 was not considered before; for the sake of rigor, we prove it in Appendix.

3 Criteria↩︎

Throughout this section, \(\mathrm{A}\) and \(\mathrm{B}\) are finite disjoint alphabets, \(L_1\) is an \(\mathrm{A}\)-logic, \(L_2\) is a \(\mathrm{B}\)-logic, \(\mathcal{F}\) and \(\mathcal{G}\) are classes of \(\mathrm{A}\)- and \(\mathrm{B}\)-frames, respectively.

3.1 Products of locally tabluar logics↩︎

In the product \(L_1\times L_2\) of two Kripke complete consistent logic, 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 \({\mathrm{\small S5}}^2\): that \({\mathrm{\small S5}}\) is locally tabular is well known (for example, one can observe that in the class of frames of this Kripke complete logic every partition is tuned); at the same time \({\mathrm{\small S5}}^2\) is not locally tabular [13]. We provide extra conditions which give criteria of local tabularity of the product of locally tabular logics.

The following classical fact about \({\mathrm{\small S5}}^2\) 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.

3.2 Products of pretransitive logics↩︎

For a formula \(\varphi\) in the alphabet \(\{\lozenge_1,\lozenge_2\}\), we define a the translation \({ [\varphi ]}^{m,n}\in {\mathrm{\small ML}}(\mathrm{A}\cup\mathrm{B})\). 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:

3.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}\). We say that \(\mathcal{F}\) has the bounded cluster property, if for some \(m<\omega\), \(|C|<m\) for all \(C\in Cl{(\mathcal{F})}\).

3.4 Reducible path property↩︎

For \(m<\omega\), consider the following first-order property \(\mathrm{RP}_m\): \[\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}).\] 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 \((X,R_F)\).

Notice that \(\mathrm{RP}_m\) is stronger than \(m\)-transitivity. This property is another nesessary condition for local tabularity:

Let \(\mathrm{rp}_m(\lozenge)\) be the modal formula \[p_0\wedge\lozenge(p_1\wedge\lozenge(p_2\wedge\ldots \wedge\lozenge p_{m+1})\ldots )\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}).\]

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\).

If reducible path property is sufficient for local tabularity was left as an open question (in view of Theorem 7, it is enough to consider clusters, that is frames of height 1). Below we give a very simple example that shows that it is not sufficient; at the same time, we show that a special form of rpp is sufficient in the case of products.

From Theorem 16 and Proposition 20, we obtain

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. They give another necessary axiomatic condition for local tabularity. We illustrate it for the bimodal transitive case, while the case of more modalities and pretransitive logics is a straightforward generalization. For a formula \(\varphi\in {\mathrm{\small ML}}(\lozenge)\), let \(t(\varphi)\) be the translation of \(\varphi\) that is compatible with Boolean connectives and satisfies \(t(\lozenge\varphi) = \lozenge_1 \varphi \lor \lozenge_2 \varphi.\) Let \(L_0 = \{\varphi \mid t(\varphi) \in L\}.\) Then \(L_0\) is a normal logic, and it is locally tabular. So it contains an \(\mathrm{rp}_m(\lozenge)\) formula. Hence, \(L\) contains \(\mathrm{rp}_m(1,1) = t(\mathrm{rp}_m(\lozenge)) \in L.\) So we have

3.5 \(1\)-finiteness↩︎

It is known that above \({\mathrm{\small S4}}\), 1-finiteness is sufficient for local tabularity [30]. In general, there are 1-finite logics that are not locally tabular [24], [31]. We show that for products of locally tabular logics, \(1\)-finiteness guarantees local tabularity.

3.6 Criteria↩︎

We combine our previous observations in the following criteria.

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\). The latter property is modally definable [18]. It follows that in the unimodal transitive frames of finite height, the bounded cluster property can be expressed by modal formulas \(\mathrm{bc}_n\), where \(n\) bounds the size of clusters. Consequently, in the case of \(k\)-transitive \(\mathrm{A}\)-frames, the corresponding property is expressed by formulas \({ [\mathrm{bc}_n ]}^{k}\), which will be called bounded cluster formulas.

For a pretransitive logic \(L\), let \(\mathrm{tra}{(L)}\) be the least \(k\) such that \(L\) is \(k\)-transitive; \(k\) is called the pretransitivity index of \(L\). By Theorem 4, \(\mathrm{tra}{(L)}\) is defined for every locally tabular logic.

4 Examples↩︎

It is well known that for unimodal logics above \({\mathrm{\small K4}}\), local tabularity is equivalent to finite height [4],[5]. This criterion was extended for weaker systems in [23]: it holds for logics containing \(\lozenge^{k+1} p\rightarrow\lozenge p\vee p\) with \(k>0\).

For a transitive logic \(L\), let \(L[h]\) be its extension with the axiom \(B_h\) of finite height.

Let \({\mathrm{\small GL}}\) and \({\mathrm{\small Grz}}\) be the logics of converse well-founded partial orders, strict and non-strict, respectively. Let \({\mathrm{\small GL}}.3\) and \({\mathrm{\small Grz}}.3\) be their extensions for the case of linear orders. Clearly, these logics have the bounded cluster properties.

It is known [32] that if an \(\mathrm{A}\)-logic \(L\) contains a formula \(\Box_\mathrm{A}^m\bot\) for some \(m\), then this logic is locally tabular. In [7] (see also [8]), it was shown that \(L\times L\) is locally tabular. We notice that the bounded cluster property holds for \(L\)-frames: in this case, clusters are singletons. Hence, we have the following generalization of the above result.

5 Product finite model property↩︎

A modal logic \(L\) has the product fmp, if \(L\) is the logic of a class of finite product frames. The product fmp is stronger than the fmp: for example, \({\mathrm{\small K4}}\times {\mathrm{\small S5}}\) has the fmp [14], but lacks the product fmp [3]. Examples of logics with this property are also known: they include \({\mathrm{\small K}}\times {\mathrm{\small K}}\) (where \({\mathrm{\small K}}\) stands for the smallest unimodal logic) and \({\mathrm{\small K}}\times{\mathrm{\small S5}}\) [3], the logic \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) [29], or its extensions [17].

The product of a logic possesing the fmp with a tabular logic has the product fmp ([6], see Proposition 32 below). In this section, we show that the weaker property of local tabularity is not sufficient for the product fmp.

5.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.

Let \({\mathrm{\small Saw}}= \mathop{\mathrm{Log}}(F_S).\) The next proposition follows from simple semantic observations:

We define the formula \(\varphi\in {\mathrm{\small ML}}(\mathrm{A}\cup \{\lozenge_{{\mathrm{\small S5}}}\})\) as \(\varphi = \varphi_1 \land \varphi_2 \land \varphi_3,\) where \[\begin{gather} \varphi_1 = \lozenge\top; \\ \varphi_2 = \Box \lozenge_{{\mathrm{\small S5}}} \left(\lozenge_l \lnot p \land \lozenge_r p\right); \\ \varphi_3 = \Box \Box_{{\mathrm{\small S5}}} \left(\lozenge_l p \to \lozenge_r p\right). \end{gather}\]

5.2 Product fmp and products of small height↩︎

As follows from Theorem 4 and Corollary 3, 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 can classify the locally tabular logics \(L_1 \times L_2\) with respect to the height of \(L_1\) and \(L_2\). For this section, we will assume that \(L_1 \vdash [bc_n]^{\mathrm{tra}{(L_1)}}\) for some \(n < \omega\). We will describe how the product fmp depends on the height of \(L_1\) and \(L_2.\)

By Proposition 31, the product fmp fails 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. A logic is called tabular, if it is the logic of a single finite frame.

Observe that \(L_1\) is Kripke complete by 1. Since \(L_1\) is locally tabular, it is the logic of its class of frames. Every \(L_1\)-frame has unit height, so it consists of one cluster, which has size at most \(n\) by the frame condition of \([bc_n]^{\mathrm{tra}{(L)}}\). Then \(L_1\) is tabular by Proposition 32.

Proposition 31 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.

6 Logics above \({\mathrm{\small S4}}\times{\mathrm{\small S5}}\)↩︎

6.1 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 \({\mathrm{\small S4}}\), see [15], [16], or [18]. One of them is the logic \({\mathrm{\small S5}}\). Another is the logic \({\mathrm{\small Tack}}\) defined below.

An important fact about \({\mathrm{\small S5}}^2\) was established in [17]: this logic is prelocally tabular, that is, the following theorem holds.

While \({\mathrm{\small S5}}^2\) is prelocally tabular, it turns out that products of pretabular logics can be not prelocally tabular even for the case of height 2.

The (one-dimensional) tack frame \(\mathrm{\small T}\) 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 \({\mathrm{\small Tack}}\) be the logic of its frame. \({\mathrm{\small Tack}}\) is one of exactly five pretabular logics above \({\mathrm{\small S4}}\).

In this subsection we show that \({\mathrm{\small Tack}}\times {\mathrm{\small S5}}\) is not prelocally tabular, and give an axiomatic criterion of local tabularity for a family of logics that contains \({\mathrm{\small Tack}}\times {\mathrm{\small S5}}\) and its extensions.

We say that the product rpp criterion holds for a logic \(L\), if for any normal extension \(L'\) of \(L\), we have:

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

The unimodal logic \({\mathrm{\small S4.1}}\) is the extension of \({\mathrm{\small S4}}\) 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 \[\label{eq:s4461-condition} \forall x\,\exists y\,\left(xRy \land \forall z \left(yRz \to z = y\right)\right),\tag{9}\] see, e.g., [19].

Hence, in our notation, the unimodal logic \({\mathrm{\small S4.1}}[2]\) is the extension of \({\mathrm{\small S4}}\) with the axioms \(\Box\lozenge p\rightarrow\lozenge\Box p\) and \(B_2\). Now we are going to show that the product rpp criterion holds for \({\mathrm{\small S4.1}}[2] \times {\mathrm{\small S5}}\).

A point \(a\in X\) is called \(R\)-terminal in a transitive frame \((X,R)\), if \(R(a) = \{a\}\).

::: {#lem:S4.1[h]xS5_terminal .lemma} Lemma 2. Let \(F = (X, R, \approx)\models{{\mathrm{\small S4.1}}[h]\times {\mathrm{\small S5}}}\). If \(a\in X\) is \(R\)-terminal, then \([a]_\approx\) contains only \(R\)-terminal elements. :::

Let \(\mathcal{F}_h\) be the class of all \({\mathrm{\small S4.1}}[h]\times {\mathrm{\small S5}}\)-frames that do not validate \({\mathrm{\small S5}}^2.\) For any \(F = (X,R,\approx)\in \mathcal{F}_h,\) let \(Z_F\) be the set of all \(R\)-terminal elements in \(F.\) We define \(\alpha(F)\) to be the subframe \(F {\upharpoonright}\left(X \setminus Z_F\right).\) Notice that if \(Z_F = X,\) then \(R\) is an equivalence relation, so \(F \models {\mathrm{\small S5}}^2.\) It follows that \(\alpha(F)\) is not empty for any \(F\in \mathcal{F}_h.\)

Let \(L_1\) be an \(\mathrm{A}\)-logic and \(L_2\) be an \(\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 axioms \(\mathrm{com}(a,b),\,\mathrm{com}(b,a)\) and \(\mathrm{chr}(a,b)\) for all \(a\in \mathrm{A}\) and \(b\in\mathrm{B},\) where \[\begin{align} \mathrm{com}(a,b) &= \lozenge_a \lozenge_b p \to \lozenge_b \lozenge_a p; \\ \mathrm{chr}(a,b) &= \lozenge_a \Box_b p \to \Box_b \lozenge_a p. \end{align}\] The validity of \(\mathrm{com}(a,b)\) in an \((\mathrm{A}\cup\mathrm{B})\)-frame \((X,(R_a)_{a\in \mathrm{A}}, (R_b)_{a\in \mathrm{B}})\) is equivalent to the commutativity \(R_a\circ R_b = R_b \circ R_a.\) The formula \(\mathrm{chr}(a,b)\) defines the Church-Rosser property \[\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))\] 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]\) [3].

The product rpp criterion holds for \({\mathrm{\small S5}} \times {\mathrm{\small S5}}\). Indeed, \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) has no product rpp, and is not locally tabular. All extensions of \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) are locally tabular, and hence they have the product rpp by Proposition 21. It is well known that \({\mathrm{\small S5}} \times {\mathrm{\small S5}}=\left[{\mathrm{\small S5}},{\mathrm{\small S5}}\right]\) [29]. Hence, we have

6.2 Two dimensional tack↩︎

A prelocally tabular logic \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) has height \(1\). In this subsection, we give another example of a prelocally tabular logic above \({\mathrm{\small S4}}\times {\mathrm{\small S5}}\), 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 \(\mathrm{\small T}(X,Y)={{(\boldsymbol{X} \times \boldsymbol{Y})}\,\oplus\, \circ}\). The two dimensional tack is the frame \(\mathrm{\small T}(\omega,\omega)\). Let \({\mathrm{\small Tack}}_2 = \mathop{\mathrm{Log}}{\mathrm{\small T}(\omega,\omega)}.\) We show that \({\mathrm{\small Tack}}_2\) is canonical, has the finite model property, and is prelocally tabular.

Firstly, we identify some axioms of \({\mathrm{\small Tack}}_2\), study its abstract frames, and then give a complete axiomatization.

Notice that the composition of relations \(R=R_1\circ R_2\) in \(\mathrm{\small T}(\omega,\omega)\) is a preorder. Let \(\lozenge\) denote the compound modality \(\lozenge_1\lozenge_2\).

Observe that the skeleton of \(\mathrm{\small T}(\omega,\omega)\) is a two-element chain. Hence, \({\mathrm{\small Tack}}_2\) contains the axiom of height two for the compound modality \(\lozenge\). Moreover, the height of the first relation in \(\mathrm{\small T}(\omega,\omega)\) is 2, so the fragment of \({\mathrm{\small Tack}}_2\) in the first modality contains \({\mathrm{\small S4}}[2]\). Clearly, its fragment in the second modality is \({\mathrm{\small S5}}\).

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 \(\mathrm{\small T}(\omega,\omega)\) satisfies the Church-Rosser property, and hence, the formula \(\lozenge\Box p\rightarrow\Box \lozenge p\), which is an abbreviation for \[\label{eq:TL-CR} \lozenge_1\lozenge_2 \Box_1\Box_2 p\rightarrow\Box_1\Box_2 \lozenge_1\lozenge_2 p,\tag{10}\] is a valid principle of \({\mathrm{\small Tack}}_2\). In the combination with height 2, it follows that in every rooted \({\mathrm{\small Tack}}_2\)-frame, there is a top cluster. 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 \[\label{eq:TackMC} \Box_1\Box_2\lozenge_1\lozenge_2 p\rightarrow\lozenge_1\lozenge_2\Box_1\Box_2 p,\tag{11}\] belongs to the logic \({\mathrm{\small Tack}}_2\). In particular, it follows that in every rooted \({\mathrm{\small Tack}}_2\)-frame, the top cluster is a singleton.

Our next step aims to express the symmetry property in the bottom cluster of an arbitrary rooted \({\mathrm{\small Tack}}_2\)-frame (notice that in clusters of \({\mathrm{\small S4}}\times {\mathrm{\small S5}}\)-frames, the symmetry of the first relation is not guaranteed). Consider the following relativized version of the symmetry axiom: \[\label{eq:relativized-sym} \lozenge_1\Box_1 q \wedge\neg q\wedge p\rightarrow\Box_1 (\neg q\rightarrow\lozenge_1 p)\tag{12}\] Readily, this formula is valid in \(\mathrm{\small T}(\omega,\omega)\). Let \(F\) be a point-generated \({\mathrm{\small Tack}}_2\)-frame of height 2. We claim that its rooted cluster \(C\), considered as a frame-restriction, validates \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\). 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 \([{\mathrm{\small S4}}[2], {\mathrm{\small S5}}]\) with the axioms 10 , 11 , and 12 . Putting our observations together, we obtain

Our next goal is to prove completeness.

This lemma follows from [33]. The semi-ordered sum \({{F}\,\oplus\, \circ}\) is the sum of frames \(F\) and the singleton \(\circ\) over the indexing frame \((2,\leq,\varnothing)\) in the sense of [33]. Two classes are interchangeable, if they have the same logic in the language enriched with the universal modality. It was shown that in a class of sums, replacing interchangeable classes of summands does not change the logic of the sums. Classes \(\mathcal{C}\) and \(\mathcal{D}\) are interchangeable, since the universal modality is expressible as \(\lozenge_1\lozenge_2\) in \({\mathrm{\small S5}}^2\)-frames. Hence \(\mathop{\mathrm{Log}}\{{{C}\,\oplus\, \circ}\mid C\in \mathcal{C}\} =\mathop{\mathrm{Log}}\{{{D}\,\oplus\, \circ}\mid D\in \mathcal{D}\}\). See Appendix, Section 9.2, for details.

It follows from Lemma 5 that \({\mathrm{\small Tack}}_2\) has an analog of the product fmp:

7 Conclusion↩︎

7.1 Summary of the results↩︎

1. The main result of this paper is the criteria obtained in Section 3.

2. In Section 4, the criteria are applied to describe new families of locally tabular products. In particular, we generalized results from [7], [8].

3. In Section 5, we discussed the product finite model property. In particular, we showed that the local tabularity of a product logic does not imply the product fmp, even in the case of height 3.

4. We showed in Theorem 39 that the product rpp formula gives an axiomatic criterion of local tabularity for all extensions of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\).

5. Finally, we described a prelocally tabular extension of \({\mathrm{\small S4}}\times{\mathrm{\small S5}}\) of height 2.

7.2 Open problems↩︎

7.2.1 Criterion for extensions of products↩︎

According to Theorem 26, local tabularity of the factors and a product rpp formula are equivalent to the local tabularity of the product. In particular, in the case of transitive logics of finite height, local tabularity of the product is equivalent to the product rpp due to Corollary 4. These facts do not give a criterion for normal extensions of a product. Unlike these facts, Theorem 39 gives an axiomatic criterion for all extensions of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\). We conjecture that Theorem 39 can be generalized for a wider class of logics.³

Problem. Let \(S4[h]\) be the extension of \({\mathrm{\small S4}}\) with the axiom of finite height \(B_h\). Does the product rpp criterion hold for every extension \(L\) of \({\mathrm{\small S4}}[h]\times {\mathrm{\small S5}}\)?

If not, what is the largest such \(h\)?

7.2.2 Prelocal tabularity in products↩︎

It is a well-known open problem whether every non-locally tabular unimodal logic is contained in a prelocally tabular [18]. For the case of logics above \({\mathrm{\small S4}}\times {\mathrm{\small S4}}\), this question is also open. We conjecture that this is true for logics above \({\mathrm{\small S4}}\times {\mathrm{\small S5}}\).

7.2.3 Local tabularity in the symmetric case↩︎

One of the central tools for our results was the criterion given in Theorem 7 [23], which, informally, says, that under the necessary conditions of pretransitivity and finite height, only local tabularity on clusters matters. While this criterion has many applications, there is an obvious limitation for this approach. Namely, even in the unimodal case, if the relation is symmetric, then every point-generated frame consists of one cluster, and no additional structure is given by the skeleton construction. Hence, it is of definite interest to study local finiteness of symmetric relations. Under the necessary conditions of local finiteness, this means that we are interested in graphs of finite diameters. No axiomatic criterion is known for this case, and it is not guaranteed that an explicit axiomatic characterization of local finiteness is possible in this case.

8 Acknowledgements↩︎

We are grateful to Guram Bezhanishvili and Valentin Shehtman for valuable discussions.

9 Appendix↩︎

9.1 Proof of Theorem 7↩︎

Proof of Theorem 7. ‘Only if’. Finite height follows from Theorem 4. The logic of subframes of frames in \(\mathcal{F}\) is contained in the logic of the clusters \(Cl{(\mathcal{F})}\) and is locally tabular by Proposition 6. Hence, the logic of \(Cl{(\mathcal{F})}\) is locally tabular.

‘If’. Let \(\mathcal{F}_h=\{F\in \mathcal{F}\mid h(F)\leq h\}\), \(1\leq h<\omega\). By induction on \(h\) we show that \(\mathcal{F}_h\) is \(g_h\)-tunable for some monotone \(g_h:\omega\to\omega\). Let \(h=1\). The class \(\mathcal{F}_1\) consists of disjoint sums of frames in \(Cl{(\mathcal{F})}\), so \(\mathop{\mathrm{Log}}\mathcal{F}_1=\mathop{\mathrm{Log}}Cl{(\mathcal{F})}\). Since \(\mathop{\mathrm{Log}}\mathcal{F}_1\) is locally tabular, the class \(\mathcal{F}_1\) is \(f\)-tunable for some \(f\) by Theorem 5. Put \(g_1(n)=\max\{f(i)\mid i\leq n\}\); clearly, \(\mathcal{F}_1\) is \(g_1\)-tunable. Let \(h>1\). By induction hypothesis, \(\mathcal{F}_{h-1}\) is \(g_{h-1}\)-tunable for some monotone \(g_{h-1}\). Put \(g_h(n) = g_1(n) + g_{h-1}\left(n\cdot2^{g_1(n)\cdot |\mathrm{A}|} \right).\) Consider \(F\in \mathcal{F}_{h}\). Let \(F_1\) be the restriction of \(F\) on its maximal clusters, \(X_1=\mathop{\mathrm{dom}}F_1\), \(X_2=(\mathop{\mathrm{dom}}F){\setminus}X_1\). If \(X_2 =\varnothing\), then \(F\in\mathcal{F}_1\), and so is \(g_1\)-tunable; hence, \(F\) is \(g_h\)-tunable. If \(X_2 \neq \varnothing\), \(F\) is \(g_h\)-tunable by Lemma 8.

Since \(\mathcal{F}=\mathcal{F}_h\) for some \(h\), \(\mathcal{F}\) is uniformly tunable, and hence its logic is locally tabular by Theorem 5. 0◻

9.2 Sums↩︎

The following fact follows from [33].

9.3 Productivization↩︎

By Theorem 33 [17], all proper extensions of \({\mathrm{\small S5}}^2\) are locally tabular. Assuming Kripke completeness of a proper extension \(L\) of \({\mathrm{\small S5}}^2\), local tabularity is a simple corollary of Theorem 26 and our previous observations. Indeed, let \(\mathcal{F}\) be the class of point-generated frames of \(L\). By Lemma 10, \(L \subseteq \mathop{\mathrm{Log}}{\widetilde{\mathcal{F}}}\). So \(\mathop{\mathrm{Log}}{\widetilde{\mathcal{F}}}\) is a proper extension of \({\mathrm{\small S5}}^2\) as well, and hence \(n = \sup\{m \mid \exists F\in\mathcal{F}\; \,(\widetilde{F}\twoheadrightarrow\boldsymbol{m} \times \boldsymbol{m} )\}\) is finite. For \(i = 1,\,2\), let \(\mathcal{G}_i\) be the class of frames of form \(\boldsymbol{X}_1 \times \boldsymbol{X}_2\) with \(|X_i|\leq n\). By Lemma 12, each frame in \(\widetilde{\mathcal{F}}\) is isomorphic to a frame in \(\mathcal{G}_1 \cup \mathcal{G}_2\). Both classes \(\mathcal{G}_i\) are uniformly tunable by Theorem 26, and so is the class \(\widetilde{\mathcal{F}}\).⁴ Then \(L\) is locally tabular by Lemma 11.

This does not give a complete proof of Theorem 33: we need to exclude the case of incomplete logics. For a logic \(L\), let \(F_L\) be its canonical frame [19]. The following reasoning is a variant of the proof given in [17];⁵ we provide it for the self-containment of the text. Together with the previous reasoning, it completes the proof of Theorem 33.

Now Theorem 33 follows: if \(L\) is a proper extension of \({\mathrm{\small S5}}^2\), then so is the logic \(\mathop{\mathrm{Log}}F_{L}\) of the canonical frame of \(L\); the latter logic is Kripke complete and so is locally tabular; since \(\mathop{\mathrm{Log}}F_{L}\subseteq L\), \(L\) is locally tabular.

References↩︎

---

1. To avoid any ambiguity, we remark that we write \(R_F^{\leq m}\) for \((R_F)^{\leq m}\), and \(R_F^*\) for \((R_F)^*\).↩︎

2. This is a particular case of the following general fact. If the varieties generated by classes \(\mathcal{C}_1\) and \(\mathcal{C}_2\) are locally finite, then the variety generated by the class \(\mathcal{C}_1 \cup \mathcal{C}_2\) is locally finite as well: \(\mathcal{C}_1 \cup \mathcal{C}_2\) is uniformly locally finite by Malcev criterion given in Theorem 2.↩︎

3. In a very recent preprint [35], it was announced that Theorem 39 extends to logics above \({\mathrm{\small S4}}[2]\times {\mathrm{\small S5}}\).↩︎

4. This is a particular case of the following general fact. If the varieties generated by classes \(\mathcal{C}_1\) and \(\mathcal{C}_2\) are locally finite, then the variety generated by the class \(\mathcal{C}_1 \cup \mathcal{C}_2\) is locally finite as well: \(\mathcal{C}_1 \cup \mathcal{C}_2\) is uniformly locally finite by Malcev criterion given in Theorem 2.↩︎

5. We are grateful for an anonymous reviewer for providing the reference to this claim.↩︎