April 02, 2024
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. We provide extra semantic and axiomatic conditions which give criteria of local tabularity of the product of two locally tabular logics. Then we apply them to identify new families of locally tabular products.
product of modal logics, local tabularity, finite height, pretransitive logic
A logic is locally tabular, if each of its finite-variable fragments contains only a finite number of pairwise nonequivalent formulas. It is well known that for unimodal logics above \({\mathrm{\small K4}}\), local tabularity is equivalent to finite height [1],[2]. In the non-transitive unimodal, and in the polymodal case, no axiomatic criterion of local tabularity is known.
We are interested in locally tabular products of modal logics. Local tabularity is established for some families of products. In [3], it was shown that \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) is prelocally tabular: every extension of \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) is locally tabular. A family of locally tabular modal products was identified in [4], see also [5]. For close systems, intuitionistic modal logics, locally tabular families were identified in [6], [7], [8], and a recent manuscript [9].
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}}\) [10] . We provide extra semantic (Theorem [thm:criterion-frames-general]) 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. Then we apply them to identify new families of locally tabular products (Section 3.7).
The proof of prelocal tabularity of \({\mathrm{\small S5}}\times {\mathrm{\small S5}}\) given in [3] was algebraic; in Section 4.2 we give a semantic argument via Theorem [thm:criterion-frames-general].
The logic \({\mathrm{\small S5}}\) is known to be one of the five pretabular logics above \({\mathrm{\small S4}}\) [11], [12]. We show 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.
Finally, we consider a weaker than \({\mathrm{\small Tack}}\) logic \({\mathrm{\small S4}}.1 [ 2 ]\), and give an axiomatic criterion of local tabularity for all normal extensions of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\).
For basic notions in modal logic, see, e.g., [13] or [14].
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. [14]. The term unimodal refers to the case \(\mathrm{A}=\{\lozenge\}\).
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 [14] 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., [14] or [13].
The notions of generated subframe and p-morphism (or bounded morphism) are defined in the standard way, see, e.g., [14]. 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
\(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
\(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}\) [14].
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).\]
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\).
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., [13].
Let \(L, L'\) be \(\mathrm{A}\)-logics, \(L\) locally tabular, \(L\subseteq L'\). Then:
\(L'\) is locally tabular.
\(L'\) has the finite model property, that is, \(L'\) is the logic of a class of finite frames.
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^*\).1 \(F\) is pretransitive, if it is \(m\)-transitive for some finite \(m\). The following fact is standard.
If \(\mathop{\mathrm{Log}}G\subseteq \mathop{\mathrm{Log}}F\), \(G\) is pretransitive, and \(F\) is finite and rooted, then there exists a point-generated subframe \(H\) of \(G\) such that \(H\twoheadrightarrow F\).
For any \(\mathrm{A}\)-frame \(F\), we have the following equivalence [15]: \[\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 recursively defined as follows: \({ [\bot ]}^{m}=\bot\), \({ [p ]}^{m}=p\) for variables, \({ [\psi_1\rightarrow\psi_2 ]}^{m}={ [\psi_1 ]}^{m}\rightarrow{ [\psi_2 ]}^{m}\), and \({ [\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_A^*\cap (R_A^*)^{-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\), 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 [1]: \(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.
Theorem 1. [16] Let \(L\) be an \(\mathrm{A}\)-logic. If \(L\) is 1-finite, then for some \(h,m<\omega\), \(L\) contains \(\lozenge_\mathrm{A}^{m+1} p \rightarrow\lozenge_\mathrm{A}^{\leq m} p\) and \({ [B_h ]}^{m}.\)
In [16], this fact was stated for the unimodal case; its polymodal generalization is straightforward, details can be found in [17].
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 1. 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}\), \[\label{eq:part} \exists a\in U \exists b\in V \, (aR b) \,\text{ implies }\, \forall a\in U \exists b\in V \, (aR b).\qquad{(1)}\] 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 \(\eqref{eq:part}\) 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., [18] for details.
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\).*
Theorem 2. [16]The logic of a class \(\mathcal{F}\) of \(\mathrm{A}\)-frames is locally tabular iff \(\mathcal{F}\) is uniformly tunable.
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}\}.\]
[[17]][]{#prop:LF-for-subframess label=“prop:LF-for-subframess”} If \(\mathop{\mathrm{Log}}\mathcal{F}\) is \(k\)-finite for some positive \(k<\omega\), then the logic of \(\mathop{\mathrm{Sub}}{\mathcal{F}}\) is \({(k{-}1)}\)-finite.
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}\}.\] \(\mathcal{F}\) is of uniformly finite height, if for some finite \(h\), for every \(F\in \mathcal{F}\), we have \(h(F)\leq h\).
Theorem 3. [16]A logic \(\mathop{\mathrm{Log}}\mathcal{F}\) is locally tabular iff \(\mathcal{F}\) is of uniformly finite height and \(\mathop{\mathrm{Log}}Cl{(\mathcal{F})}\) is locally tabular.
Remark. In [16], Theorems 2 and 3 were stated for the unimodal case. Their polymodal generalizations are straightforward. For Theorem 2, details are given in [17]. The polymodal version of Theorem 3 was not considered before; for the sake of rigor, we prove it in Appendix.
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.
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 finite logics can be not locally finite. The simplest example is the logic \({\mathrm{\small S5}}^2\): that \({\mathrm{\small S5}}\) is locally finite 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 finite [10]. 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.
Theorem 4. [19],[20] If \(\mathcal{X}\) and \(\mathcal{Y}\) are families of non-empty sets and \(\sup\{|X| \mid X\in\mathcal{X}\}\) and \(\sup\{|Y| \mid X\in\mathcal{Y}\}\) are infinite, then \(\mathop{\mathrm{Log}}\{\boldsymbol{X} \times \boldsymbol{Y}\mid X\in \mathcal{X}\text{ and } Y\in\mathcal{Y}\}\) is \({\mathrm{\small S5}}^2\).
Let \(R_h\) and \(R_v\) be the unions of all horizontal and all vertical relations of \(F\times G\), respectively. Then \(R_{F\times G}^* = R_h^* \circ R_v^*=R_v^* \circ R_h^*\).
Proof. If \(R\) is a vertical and \(S\) is a horizontal relation in \(F\times G\), then they commute: \(R\circ S=S\circ R\). By a routine argument, \(R_v^i\) and \(R_h^j\) commute for all \(i,j\). It follows that \(R_h^* \circ R_v^*=R_v^* \circ R_h^*\).
Since \(R_h^*\) and \(R_v^*\) are contained in the transitive relation \(R_{F\times G}^*\), we have \(R_h^* \circ R_v^*\subseteq R_{F\times G}^*\). By induction on \(m\), one can easily check that \(R_{F\times G}^{\leq m} \subseteq R_h^* \circ R_v^*\) for all \(m\). Hence, \(R_{F\times G}^* \subseteq R_h^* \circ R_v^*\). ◻
If \(F\) is \(m\)-transitive and \(G\) is \(n\)-transitive, then \(F\times G\) is \((m+n)\)-transitive.
The product of two pretransitive logics is pretransitive.
Proof. The second statement is immediate from the first. To check the first statement, let \(R_h\) and \(R_v\) be the unions of all horizontal and all vertical relations of \(F\times G\), respectively. Since \(F\) is \(m\)-transitive, \(R_h\) is \(m\)-transitive; similarly, \(R_v\) is \(n\)-transitive. By Proposition [prop:corner], we have \(R^*_{F\times G}=R_h^* \circ R_v^*=R_h^{\leq m} \circ R_v^{\leq n}\subseteq R^{\leq m}_{F\times G}\circ R^{\leq n}_{F\times G} = R^{\leq m+n}_{F\times G}\). ◻
Example 1. \({\mathrm{\small S4}}^2\), \({\mathrm{\small S4}}\times {\mathrm{\small S5}}\), \({\mathrm{\small S5}}^2\) are 2-transitive logics.
If \(h(F)=h_1\) and \(h(G)=h_2\) for some finite \(h_1, h_2\), then \(h(F\times G)=h_1+h_2-1\).
Proof. Consider a chain \([a_0] < [a_1] < \ldots < [a_{h_1}]\) in \(\mathop{\mathrm{Sk}}F\) and a chain \([b_0]< [b_1] < \ldots < [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)\): \[[(a_0,\,b_0)] < [(a_1,\,b_0)] < \ldots < [(a_{h_1},\,b_0)] < [(a_{h_1},\,b_1)] < \ldots < [(a_{h_1},\,b_{h_2})]\] Hence, \(h(F\times G) \geq h_1 + h_2 -1\).
If \(\Sigma\) is a chain of size \(l\) in \(\mathop{\mathrm{Sk}}(F\times G)\) with the least \([(a,b)]\) and the largest \([(c,d)]\), then there is a chain \(\Sigma_1\) in \(\mathop{\mathrm{Sk}}F\) with the least \([a]\) and the largest \([c]\), and a chain \(\Sigma_2\) in \(\mathop{\mathrm{Sk}}G\) with the least \([b]\) and the largest \([d]\) such that \(|\Sigma_1|+|\Sigma_2|=l+1\). This follows by induction on \(l\). Hence, every chain in \(\mathop{\mathrm{Sk}}(F\times G)\) has at most \(h_1+h_2-1\) elements. ◻
Example 2. \({\mathrm{\small S5}}^2\) is the logic of height 1.
For a formula \(\varphi\) in the alphabet \(\{\lozenge_1,\lozenge_2\}\), let \({ [\varphi ]}^{m,n}\) be the formula in the alphabet \(\mathrm{A}\cup\mathrm{B}\) recursively defined as follows: \({ [\bot ]}^{m,n}=\bot\), \({ [p ]}^{m,n}=p\) for variables, \({ [\psi_1\rightarrow\psi_2 ]}^{m,n}={ [\psi_1 ]}^{m,n}\rightarrow{ [\psi_2 ]}^{m,n}\), and \({ [\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:
If \(F\) is an \(m\)-transitive \(\mathrm{A}\)-frame and \(G\) is an \(n\)-transitive \(\mathrm{B}\)-frame, then \(F\times G\vDash{ [\varphi ]}^{m,n}\) iff \(F^*\times G^*\vDash\varphi\).
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{F}\}\) are infinite, then \(\{\varphi\in {\mathrm{\small ML}}(\lozenge_1,\lozenge_2) \mid \mathcal{F}\times \mathcal{G}\vDash{ [\varphi ]}^{m,n}\} ={\mathrm{\small S5}}^2\).
Proof. Follows from Proposition [prop:express] and Theorem 4. ◻
Assume that a frame \(F\) is \(f\)-tunable, and a frame \(G\) is finite. Then \(F\times G\) is \(g\)-tunable for \(g(n)=f\left(n^{|G|}\right)|G|\).
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 \[\alpha(a) = ([(a,\,b)]_\mathcal{V})_{b\in\mathop{\mathrm{dom}}G},\quad a\in \mathop{\mathrm{dom}}F.\] 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{U}\) 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}\). ◻
Corollary 1. If \(L_1\) is locally tabular and \(L_2\) is tabular, then \(L_1\times L_2\) is locally tabular.
Proof. Follows from [21] and Proposition [prop:product-with-fin]. ◻
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})}\).
Theorem 5. Let \(\mathcal{F}\) and \(\mathcal{G}\) be non-empty classes of \(\mathrm{A}\)- and \(\mathrm{B}\)-frames, respectively. The logic \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular iff the logics \(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular, and at least one of the classes \(\mathcal{F}\), \(\mathcal{G}\) has the bounded cluster property.
Proof. Assume that \(L=\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular. Then \(L_1=\mathop{\mathrm{Log}}\mathcal{F}\) and \(L_2=\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular, since \(L\) is a conservative extension of each of them. By Theorem 1, \(L_1\) and \(L_2\) are pretransitive. Let \(\mathcal{C}_1=Cl{(\mathcal{F})}\), \(\mathcal{C}_2=Cl{(\mathcal{G})}\), and \(\mathcal{C}=Cl{(\mathcal{F}\times \mathcal{G})}\). It follows from Proposition [prop:corner] that \(\mathcal{C}_1\times \mathcal{C}_2=\mathcal{C}\). By Theorem 3, the logic of \(\mathcal{C}\) is locally tabular. On the other hand, \({\mathrm{\small S5}}^2\) is not locally tabular. By Proposition [prop:pretrans-exprS5xS5], for some finite \(n\) we have \(|C|<n\) for all \(C\) in \(\mathcal{C}_1\) or for all \(C\) in \(\mathcal{C}_2\).
The other direction follows from the facts that locally finite logics have finite height (Theorem 1), which is preserved under the product (Proposition [prop:product-preserve-height]). By Theorem 3, it is enough to show that clusters occurring in the underlying products form a uniformly tunable class. The required partitions exist according to the bounded cluster property, in view of Proposition [prop:product-with-fin]. ◻
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. The following fact was stated in [16]: if a class of unimodal frames is uniformly tunable (equivalently, has a locally tabular logic), then it has the rpp. If reducible path property of clusters is sufficient for local tabularity was left as an open question. 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.
There is a unimodal cluster \(C\) such that \(\mathrm{RP}_2\) holds in \(C\), while its logic is not locally tabular.
Proof. Let \(C=(\omega,R)\), where \(m R n \text{ iff }m\neq n+1\). Clearly, \(C\) is a cluster: \(m R^2 n\) for all \(m,n\). Consider a path \(m_0 R m_1 R m_2 R m_3\) in \(C.\) If \(m_0,\,\ldots,\,m_3\) are distinct and \(m_0 = m_2 + 1\) then \(m_0 \ne m_3 +1,\) so \(m_0 R m_2\) or \(m_0 R m_3.\) In either case, the path \(m_0 R \ldots R m_3\) can be reduced. Therefore \(C\) satisfies \(\mathrm{RP}_2.\)
Consider a valuation \(\theta\) on \(\omega\) with \(\theta(p) = \{0\}.\) Let \(\varphi_0 = p\), \(\varphi_{n+1} = \lnot\lozenge\varphi_n\). A simple induction on \(n\) shows that \((F,\,\theta),\,n\models \varphi_m\) \(n=m.\) So the logic of \(F\) is not not locally tabular (in fact, not 1-finite). ◻
Assume that \(\mathcal{F}^*\times \mathcal{G}^*\) has the rpp. Then \(\mathcal{F}\) or \(\mathcal{G}\) has the bounded cluster 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 \[a_0R_H a_1 R_H a_2 R_H \ldots R_H a_{2l}\] 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 5 and Proposition [prop:rpp-implies-bcp], we obtain
Corollary 2. If the logics \(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular, and \(\mathcal{F}^*\times \mathcal{G}^*\) has the rpp, then \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular.
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}).\]
For a frame \(F=(X,R)\), \(F\vDash\mathrm{rp}_m(\lozenge)\) iff \(F\) satisfies \(\mathrm{RP}_m\).
Proof. Straightforward. ◻
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.
For a frame \(F=(X,(R_\lozenge)_{\lozenge\in\mathrm{A}\cup\mathrm{B}})\), we have \(F \vDash\mathrm{rp}_m(k,n)\) iff \((X,(\bigcup_{\lozenge\in\mathrm{A}} R_\lozenge)^{\leq k})\cup (\bigcup_{\lozenge\in\mathrm{B}} R_\lozenge)^{\leq n})\) satisfies \(\mathrm{RP}_m\).
Proof. Follows from Proposition [prop:rpp-to-modal-uni]. ◻
Formulas \(\mathrm{rp}_m(k,n)\) are canonical.
Proof. These formulas are Sahlqvist. ◻
Let \(\mathcal{F}\) be a class of \(k\)-transitive \(\mathrm{A}\)-frames, and \(\mathcal{G}\) a class of \(n\)-transitive \(\mathrm{B}\)-frames. If \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular, then \(\mathcal{F}^*\times \mathcal{G}^*\) has the rpp, and \(\mathcal{F}\times \mathcal{G}\vDash\mathrm{rp}_m(k,n)\) for some \(m\).
Proof. For a unimodal formula \(\varphi\), we define \([\varphi]^\star\) as follows: \([\bot]^\star=\bot\), \([p]^\star=p\), \([\psi_1\rightarrow\psi_2]^\star= [\psi_1]^\star\rightarrow[\psi_2]^\star\), and \([\lozenge\psi]^\star=\lozenge_\mathrm{A}^{\leq k}[\varphi]^\star \vee \lozenge_\mathrm{B}^{\leq n}[\varphi]^\star\). Consider frames \(F\) and \(G\), and assume that \(F^*\times G^*\) is \((X\times Y, R_1,R_2)\); then put \(F \star G=(X\times Y,R_1\cup R_2)\).
It is straightforward that for \(k\)-transitive \(F\) and \(n\)-transitive \(G\) we have \[\label{eq:star-RPP} F\times G \vDash[\varphi]^\star \text{ iff }F\star G\vDash\varphi.\tag{3}\] It follows that \(L=\{ \varphi\in {\mathrm{\small ML}}(\lozenge) \mid F\times G \vDash[\varphi]^\star \}\) is a unimodal logic. Since \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular, \(L\) is locally tabular as well. Hence the class \(\mathcal{H}=\{F \star G\mid F\in\mathcal{F}\text{ and } G\in \mathcal{G}\}\) has the rpp [16]; by Proposition [prop:rpp-to-modal-poly], \(\mathcal{F}\times \mathcal{G}\vDash\mathrm{rp}_m(k,n)\). ◻
It is known that above \({\mathrm{\small S4}}\), 1-finiteness is sufficient for local tabularity [22]. In general, there are 1-finite logics that are not locally tabular [17], [23]. We show that for products of locally tabular logics, \(1\)-finiteness guarantees local tabularity.
Theorem 6. If the logics \(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular, and \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is one-finite, then \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular.
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{R}\) be the class of rectangles \(\boldsymbol{X}_1 \times \boldsymbol{X}_2\) such that \(X_i\) is the domain of \(C_i\in \mathcal{C}_i\), \(i=1,2\).
For the sake of contradiction, assume that \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is not locally tabular. Then \(\mathop{\mathrm{Log}}\mathcal{R}={\mathrm{\small S5}}^2\) according to Theorem 5 and Proposition [prop:pretrans-exprS5xS5]. It is known that \({\mathrm{\small S5}}^2\) is not 1-finite [10]. Hence, for each \(l\), there is a model \(M=(R,\theta)\) on \(R\in \mathcal{R}\) and formulas \(\psi_1, \ldots, \psi_l\) in the single variable \(p\) such that all sets \(\bar{\theta}(\psi_i)\) are pairwise distinct. 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 \(R\). 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\) of \(\top\) on \(M\). By Theorem 1, 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 [prop:corner], we have: \[\text{M',a\vDash\bar{\lozenge} p iff a belongs to C_1\times C_2.}\] For bimodal formulas \(\varphi\) in the single variable \(p\), we define \([\bot]^\star=\bot\), \([p]^\star=p\), \([\psi_1\rightarrow\psi_2]^\star=\bar{\lozenge} p\wedge( [\psi_1]^\star\rightarrow[\psi_2]^\star)\), and \([\lozenge_1 \psi]^\star=\bar{\lozenge} p \wedge\lozenge_\mathrm{A}^{\leq m} [\psi]^\star\), \([\lozenge_2 \psi]^\star=\bar{\lozenge} p\wedge\lozenge_\mathrm{B}^{\leq n} [\psi]^\star\). Then we have \[\text{ M',a\vDash[\varphi]^\star iff (a is in M and M,a\vDash\varphi). }\] So formulas \([\psi_1]^\star, \ldots, [\psi_l]^\star\) are pairwise non-equivalent in \(M'\). It follows that \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is not 1-finite. ◻
We combine our previous observations in the following criteria.
Theorem 7. Let \(\mathcal{F}\) and \(\mathcal{G}\) be non-empty. TFAE:
\(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is locally tabular.
\(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular and at least one of the classes \(\mathcal{F}\), \(\mathcal{G}\) has the bounded cluster property.
\(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular and \(\mathcal{F}^*\times \mathcal{G}^*\) has the rpp.
\(\mathop{\mathrm{Log}}\mathcal{F}\) and \(\mathop{\mathrm{Log}}\mathcal{G}\) are locally tabular and \(\mathop{\mathrm{Log}}(\mathcal{F}\times \mathcal{G})\) is 1-finite.
Proof. Theorem 5 shows the equivalence between [cr-i0] and [cr-i1]. By Proposition [prop:LTimpliesrpp], [cr-i0] implies [cr-i2]. By Proposition [prop:rpp-implies-bcp], [cr-i2] implies [cr-i1].
By Theorem 6, [cr-i4] implies [cr-i0]; the converse is trivial. ◻
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 [13]. 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 1, \(\mathrm{tra}{(L)}\) is defined for every locally tabular logic.
Corollary 3. Let \(L_1, L_2\) be Kripke complete consistent logics. TFAE:
\(L_1\times L_2\) is locally tabular.
\(L_1\) and \(L_2\) are locally tabular and at least one of them contains a bounded cluster formula \({ [\mathrm{bc}_n ]}^{k}\), where \(k\) is the pretransitivity index of this logic.
\(L_1\) and \(L_2\) are locally tabular and \(L_1\times L_2\) contains a product rpp formula \(\mathrm{rp}_m(k_1,k_2)\), where \(k_i=\mathrm{tra}{(L_i)}\).
It is well known that for unimodal logics above \({\mathrm{\small K4}}\), local tabularity is equivalent to finite height [1],[2]. This criterion was extended for weaker systems in [16]: it holds for logics containing \(\lozenge^{k+1} p\rightarrow\lozenge p\vee p\) with \(k>0\).
Corollary 4. Let \(L_1, L_2\) be Kripke complete consistent unimodal logics, and for some \(k,n>0\), \(L_1\) contains \(\lozenge^{k+1} p\rightarrow\lozenge p\vee p\) and \(L_2\) contains \(\lozenge^{n+1} p\rightarrow\lozenge p\vee p\). In this case, \(L_1\times L_2\) is locally tabular iff \(L_1\) and \(L_2\) contain formulas of finite height and for some \(m\), \(L_1\times L_2\) contains the product rpp formula \(\mathrm{rp}_m(k,n)\).
Let \({\mathrm{\small Grz}}.3\) be the logic of converse well-founded non-strict linear orders, \({\mathrm{\small Grz}}.3[h]\) its extension with \(B_h\).
Corollary 5. For a locally tabular \(L\), all \({\mathrm{\small Grz}}.3[h]\times L\) are locally tabular.
It is known [24] 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 [4] (see also [5]), it was shown that \(L^2\) is locally tabular. It is immediate 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.
Corollary 6. If \(L_1\) contains a formula \(\Box_\mathrm{A}^m\bot\) and \(L_2\) is locally tabular, then \(L_1\times L_2\) is locally tabular.
Definition 2. Let \(F = (X,\,(R_\lozenge)_{\lozenge\in A})\) be an \(\mathrm{A}\)-frame, where all \(R_\lozenge\) are preorders. Define the equivalence relation \({\sim}=\bigcap_{\lozenge\in A} (R_\lozenge\cap R_\lozenge^{-1}).\) The quotient frame \({F}{/}{\sim}\) is denoted \(\widetilde{F}\). Given a class \(\mathcal{F}\) of \(\mathrm{A}\)-frames, let \(\widetilde{\mathcal{F}} = \{\widetilde{F} \mid F\in \mathcal{F}\}.\)
Lemma 1. If the relations of \(F\) are preorders, then \(F\twoheadrightarrow\widetilde{F}.\)
Proof. For any frame, the quotient map is a surjective homomorphism. To show that \(F\) satisfies the back condition, assume that \([a]\widetilde{R_\lozenge}[b]\) for some \(a,\,b\in X\) and \(\lozenge\in \mathrm{A}.\) Then \(a' R_\lozenge b'\) for some \(a'\sim a\) and \(b'\sim b.\) By the definition, \(a ' R_\lozenge a\) and \(b' R_\lozenge^{-1}b,\) so \(a' R_\lozenge a R_\lozenge b R_\lozenge b' ,\) hence \(a R_\lozenge b\) by transitivity. ◻
Definition 3. Consider an \(\mathrm{A}\)-frame \(I=(Y,(S_\lozenge)_{\lozenge\in \mathrm{A}})\) and a family \((F_i)_{i\in Y}\) of \(\mathrm{A}\)-frames \(F_i=(X_i,(R_{i,\lozenge})_{\lozenge\in \mathrm{A}})\). The sum \({\textstyle \sum_{I}{F_i}}\) of the family \((F_i)_{i\in Y}\) over \(I\)* is the \(\mathrm{A}\)-frame \((\bigsqcup_{i \in Y} X_i, (R^\Sigma_\lozenge)_{\lozenge\in \mathrm{A}})\), where \(\bigsqcup_{i\in Y}{X_i}=\bigcup_{i\in Y}(\{i\}\times X_i)\), and \[(i,a)R^\Sigma_\lozenge(j,b) \quad \text{ iff }\quad (i = j \text{ and }a R_{i,\lozenge} b) \text{ or } (i\neq j \text{ and } iS_\lozenge j).\] For classes \(\mathcal{I}\), \(\mathcal{F}\) of \(\mathrm{A}\)-frames, let \({\textstyle \sum_{\mathcal{I}}{\mathcal{F}}}\) be the class of all sums \({\textstyle \sum_{I}{F_i}}\) such that \(I\in \mathcal{I}\) and \(F_i\in \mathcal{F}\) for every \(i\) in \(I\).*
Theorem 8. [17]Let \(\mathcal{F}\) and \(\mathcal{I}\) be classes of \(\mathrm{A}\)-frames. If the logics \(\mathop{\mathrm{Log}}{\mathcal{F}}\) and \(\mathop{\mathrm{Log}}{\mathcal{I}}\) are locally tabular, then \(\mathop{\mathrm{Log}}{{\textstyle \sum_{\mathcal{I}}{\mathcal{F}}}}\) is locally tabular as well.
Lemma 2. Let \(\mathcal{F}\) be a class of frames such that in every \(F\in\mathcal{F}\), all relations are preorders. Then \(\mathop{\mathrm{Log}}\widetilde{\mathcal{F}}\) is locally tabular iff \(\mathop{\mathrm{Log}}\mathcal{F}\) is locally tabular.
Proof. The ‘if’ direction is trivial, since \(\mathop{\mathrm{Log}}\mathcal{F}\subseteq \mathop{\mathrm{Log}}\widetilde{\mathcal{F}}\) by Lemma 1.
‘Only if’. Consider \(F=(X,\,(R_\lozenge)_{\lozenge\in \mathrm{A}})\in \mathcal{F}.\) Let \(\sim\) be defined as in Definition 2, and denote \(Y = X/{\sim}.\)
We claim that \(F \cong {\textstyle \sum_{\widetilde{F}}{(}}{F{\upharpoonright}U})\), where \(U\subseteq X\) ranges over the equivalence classes in \(Y\). Define \(f:\:X \to \bigsqcup_{U \in Y} U\) by \(f(a) = ([a]_{\sim},\,a).\) It is trivial that \(f\) is injective. If \((U,\,a)\in \bigsqcup_{U \in Y} U\) then \(a\in U\subseteq X\) by the definition, so \(U = [a]_{\sim},\) hence \((U,\,a) = f(a).\) Then \(f\) is surjective.
Suppose \(a,b\in X,\,a R_\lozenge b.\) If \(a \sim b\) then \(f(b) = ([a]_{\sim},\,b),\) so \(f(a)R^\Sigma_\lozenge f(b).\) Otherwise \([a]_{\sim} {\ne} [b]_{\sim};\) observe that \([a]_{\sim} \widetilde{R_\lozenge} [b]_{\sim}\) by the definition of \(\widetilde{R_\lozenge},\) so \(f(a) R^\Sigma_\lozenge f(b).\)
Conversely, let \(f(a) R^\Sigma_\lozenge f(b).\) If \([a]_{\sim} {=} [b]_{\sim}\) then \(a R_\lozenge b;\) if \([a]_{\sim}{\ne} [b]_\sim\) then \([a]_\sim \widetilde{R_\lozenge} [b]_\sim.\) By the definition of \(\widetilde{R_\lozenge},\) there exist \(a'\sim a\) and \(b'\sim b\) such that \(a' R_\lozenge b'.\) By the definition of \(\sim,\) \(a R_\lozenge a'\) and \(b' R_\lozenge b,\) so by transitivity \(a R_\lozenge b.\)
The isomorphism implies that \(\mathop{\mathrm{Log}}\mathcal{F}= \mathop{\mathrm{Log}}{{\textstyle \sum_{\widetilde{\mathcal{F}}}{\mathcal{G}}}}\) where \(\mathcal{G}\) is the class of all frames \(F{\upharpoonright}U\) where \(F\in \mathcal{F}\) and \(U \in \mathop{\mathrm{dom}}F/{\sim}.\) In any frame of \(\mathcal{G},\) the relations are transitive and symmetric by the definition of \(\sim\). Then \(\mathcal{G}\) is uniformly tunable since on the frames of \(\mathcal{G}\) any partition is tuned, so \(\mathop{\mathrm{Log}}\mathcal{G}\) is locally tabular by Theorem 2. By hypothesis, \(\mathop{\mathrm{Log}}\widetilde{\mathcal{F}}\) is also locally tabular. Then \(\mathop{\mathrm{Log}}\mathcal{F}\) is locally tabular by Theorem 8. ◻
Lemma 3. Let \(F=(X,R_1,R_2)\) be a point-generated \({\mathrm{\small S5}}^2\)-frame, \(|{X}{/}{R_1}|=\kappa\), \(|{X}{/}{R_2}|=\mu\). Then \(\widetilde{F}\) is isomorphic to \(\boldsymbol{\kappa} \times \boldsymbol{\mu}\).
Proof. Let \(\{H_\alpha\}_{\alpha < \kappa}\) and \(\{V_\beta\}_{\beta < \mu }\) be the elements of \({X}{/}{R_1}\) and \({X}{/}{R_2},\) respectively. We claim that \(H_\alpha\cap V_\beta\ne \varnothing\) for any \(\alpha< \kappa,\,\beta < \mu.\) Let \(a \in H_\alpha\) and \(b\in V_\beta.\) Since \(F\) is point-generated, \(b\in R_2[R_1(a)],\) so there exists \(c\in X\) such that \(a R_1 c\) and \(c R_2 b.\) Then \(c \in R_1(a) = H_\alpha\) and \(c\in R_2(b) = V_\beta,\) so \(c\in H_\alpha\cap V_\beta.\)
Define \(f:\:\kappa\times \mu \to {X}{/}{\sim}\) by \(f(\alpha,\,\beta) = H_\alpha \cap V_\beta.\) We claim that \(f\) is an isomorphism between \(\boldsymbol{\kappa} \times \boldsymbol{\mu}\) and \(\widetilde{F}.\) For any \([a]\in {X}{/}{\sim}\) there exist unique \(H_\alpha,\,V_\beta\) such that \(a\in H_\alpha \cap V_\beta,\) so \([a] = H_\alpha\cap V_\beta,\) thus \(f\) is a bijection. Let \(R_H\) and \(R_V\) denote the horizontal and vertical relations in \(\boldsymbol{\kappa} \times \boldsymbol{\mu}\). If \((\alpha,\beta) R_H (\alpha',\beta')\) then \(\alpha = \alpha'.\) Consider \(a\in H_\alpha\cap V_\beta\) and \(b\in H_\alpha\cap V_\beta'.\) Observe that \(H_\alpha = R_1(a),\) so \(a R_1 b,\) thus \(f(\alpha,\beta) = [a] \widetilde{R_1}[b] = f(\alpha',\beta').\) Conversely, if \(f(\alpha,\beta) \widetilde{R_1} f(\alpha',\beta'),\) there exist \(a\in H_\alpha\cap V_\beta\) and \(b\in H_\alpha'\cap V_\beta'\) such that \(a R_1 b.\) Then \(H_\alpha = R_1(a) = R_1(b) = H_\alpha',\) so \(\alpha = \alpha'\) and \((\alpha,\beta) R_H (\alpha,\beta') = (\alpha',\beta').\) An analogous argument applies for \(R_V.\) ◻
An important fact about \({\mathrm{\small S5}}^2\) was established in [3]: this logic is prelocally tabular, that is the following theorem holds.
Theorem 9. [3]All proper extensions of \({\mathrm{\small S5}}^2\) are locally tabular.
The proof given in [3] was algebraic. Below we give a semantic argument via Theorem [thm:criterion-frames-general].
Lemma 4. Let \(\mathcal{H}\) be a class of bimodal frames such that \(\mathop{\mathrm{Log}}\mathcal{H}\) is a proper extension of \({\mathrm{\small S5}}^2\). Then \(\mathcal{H}\) is uniformly tunable.
Proof. Let \(\mathcal{F}\) be the class of point-generated subframes of frames in \(\mathcal{H}\), and define \(n = \sup\{m \mid \exists F\in\mathcal{F}\; \,(\widetilde{F}\twoheadrightarrow\boldsymbol{m} \times \boldsymbol{m} )\}.\) Then \(n < \omega\) since otherwise \(\mathop{\mathrm{Log}}{\widetilde{\mathcal{F}}} \subseteq\mathop{\mathrm{Log}}\{\boldsymbol{m} \times \boldsymbol{m}\mid m < \omega\} = {\mathrm{\small S5}}^2,\) and by Lemma 1 \(L \subseteq \mathop{\mathrm{Log}}{\widetilde{\mathcal{F}}} \subseteq {\mathrm{\small S5}}^2.\) By Lemma 3, \(\widetilde{\mathcal{F}} \subseteq \mathcal{F}_1 \cup \mathcal{F}_2,\) where \(\mathcal{F}_i=\{\boldsymbol{k}_1 \times \boldsymbol{k}_2\mid k_1,\,k_2 < \omega,\, k_i \le n\}\) for \(i = 1,\,2.\) Both classes \(\mathcal{F}_i\) are uniformly tunable by Theorem [thm:criterion-frames-general], and so is the class \(\widetilde{\mathcal{F}}\). Then \(\mathop{\mathrm{Log}}{\mathcal{F}}\) is locally tabular by Lemma 2. ◻
For a logic \(L\), let \(F_L\) be its canonical frame [14].
Lemma 5. If \(L\) is a proper extension of \({\mathrm{\small S5}}^2\), then so is \(\mathop{\mathrm{Log}}{F_L}\).
Proof. For the sake of contradiction, assume that \(\mathop{\mathrm{Log}}{F_L} = {\mathrm{\small S5}}^2\). We show that in this case \(L={\mathrm{\small S5}}^2\).
Let \(m<\omega\). By Proposition [prop:Jankov-Fine], \(f:F\twoheadrightarrow\boldsymbol{m} \times \boldsymbol{m}\) for a point-generated subframe \(F=(X,R_1,R_2)\) of \(F_L\) and a p-morphism \(f\).
The logic \({\mathrm{\small S5}}^2\) is canonical [19]. It follows that \(R_1\) and \(R_2\) are equivalences, and for all \(a,b\in X\), we have \[\label{eq:cone} a (R_1\circ R_2) b \text{ and } a (R_2\circ R_1) b.\tag{4}\]
For \(i<m\), choose \(d_i\in f^{-1}(i,i)\). For distinct \(i,j<m\), we have \((d_j,d_i)\notin R_1\cup R_2;\) hence, there is a formula \(\delta_{ij}\in d_i\) such that \(\lozenge_1\delta_{ij}\vee \lozenge_2\delta_{ij}\notin d_j\). For \(i>0\), put \(\delta_i=\bigwedge_{i\neq j<m} \delta_{ij}\); put \(\delta_0=\bigwedge_{0<k<m} \neg (\lozenge_1\delta_{k}\vee \lozenge_2\delta_{k})\). We claim that \[\label{eq:dij} \delta_i\in d_i.\tag{5}\] For \(i>0\), this is trivial. To show that \(\delta_0\in d_0\), assume that \(\delta_{k}\in a\) for some \(a\in X\) and \(k>0\). Then \(\delta_{k0}\in a\) and \(\neg (\lozenge_1\delta_{k0}\vee \lozenge_2\delta_{k0})\in d_0\). Hence, \((d_0,a)\notin R_1\cup R_2\). Hence, \(\neg (\lozenge_1\delta_{k}\vee \lozenge_2\delta_{k})\in d_0\).
Define horizontal and vertical sets: \(H_i=\{a\in X\mid \lozenge_1 \delta_i\in a\}\), \(V_i=\{a\in X\mid \lozenge_2 \delta_i\in a\}\). We have \[\label{eq:lift} R_1(d_i) \subseteq H_i \text{ and }R_2(d_i) \subseteq V_i.\tag{6}\] Since \(R_1\) and \(R_2\) are equivalence relations, we also have \[\label{eq:HVmon} \text{R_1[H_i]=H_i and R_2[V_i]=V_i.}\tag{7}\] All sets \(H_i\) and \(V_i\) are non-empty, since \(d_i\in H_i\cap V_i\).
Let us check that \(\bigcup_{i<m} H_i=\bigcup_{i<m} V_i=X\). For this, assume that \(a\in X\), and \(a\notin \bigcup_{0<i<m} V_i\). By 4 , \(d_0R_1bR_2a\) for some \(b\). Let \(0<k<m\). Hence: \(\neg \lozenge_1\delta_{k}\in b\), since \(d_0 R_1b\); \(\neg \lozenge_2\delta_{k}\in b\), since \(bR_2a\); hence, \(\delta_0\in b\), and so \(a\in H_0\). Likewise, \(\bigcup_{i<m} H_i=X\).
Let us check that \(H_i \cap H_j =\varnothing=V_i \cap V_j\) for distinct \(i,j\). Indeed, if \(a\in H_i \cap H_j\), then \(\lozenge_1 \delta_i\wedge\lozenge_1 \delta_j\in a\), and so \(\delta_i\wedge\lozenge_1 \delta_j\in b\) for some \(b\in R_1(a)\), which implies \(i=j\). Similarly for vertical sets. It follows that \(\{H_i\}_{i<m}\) and \(\{V_i\}_{i<m}\) are \(m\)-element partitions of \(X\).
Put \(C_{ij}=V_i \cap H_j\). By 4 , we have \(d_i R_2 a R_1 d_j\) for some \(a\), and so each \(C_{ij}\) is non-empty according to 6 . It follows that \(\{C_{ij}\}_{i,j<m}\) is an \(m^2\)-element partition of \(X\). For \(a\in C_{ij}\), put \(g(a)=(i,j)\). Hence, \(g\) maps \(X\) onto \(m\times m\).
We claim that \(g\) is a p-morphism. By 7 , \(g\) is a homomorphism. It remains to check the back property. Let \(a\in C_{ij}\), and assume that in \(\boldsymbol{m} \times \boldsymbol{m}\), \(\tau\) is related to \((i,j)\) by the horizontal relation. Then \(\tau=(k,j)\) for some \(k<m\). We have \(a R_1 b R_2 d_{k}\) for some \(b\) due to 6 . Hence, \(b\in C_{kj}\) and so \(g(b)=(k,j)\). The proof for \(R_2\) is completely analogous.
Assume that a formula \(\varphi\) is satisfiable in a model \((\boldsymbol{m} \times \boldsymbol{m},\theta)\). Define the following valuation \(\eta\) on \(F\): put \(\eta(p)=\bigcup\{C_{ij}\mid (i,j)\in \theta(p)\}\). Then \(g\) is a p-morphism of \((F,\eta)\) onto \((\boldsymbol{m} \times \boldsymbol{m},\theta)\). So \(\varphi\) is satisfiable in \((F,\eta)\).
We have \((F,\theta_L)\vDash L\), where \(\theta_L\) is the restriction of the canonical valuation on \(F\). Let \(\psi_p\) be the formula \(\bigvee \{\lozenge_1 \delta_i\wedge\lozenge_2 \delta_j \mid (i,j)\in \theta(p) \}\). For each \(a\in X\), we have \(a\in \eta(p) \text{ iff } \psi_p \in a,\) so \((F,\eta)\vDash L\). It follows that \(L={\mathrm{\small S5}}^2\). ◻
Now Theorem 9 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 locally tabular according to Lemma 4; since \(\mathop{\mathrm{Log}}F_{L}\subseteq L\), \(L\) is locally tabular.
A logic is tabular, if it is characterized by a single finite frame. A logic is pretabular, if every its proper extension is tabular. There are exactly five pretabular logics above \({\mathrm{\small S4}}\), see [11], [12], or [13]. One of them is the logic \({\mathrm{\small S5}}\). Another is the logic \({\mathrm{\small Tack}}\) defined below. While \({\mathrm{\small S5}}^2\) is prelocally tabular, it turns out that products of pretabular logics can be not prelocally tabular.
The tack frame \(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. 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 of its extensions.
\({\mathrm{\small Tack}}\times {\mathrm{\small S5}}\) is not prelocally tabular.
Proof. Let \(H=T\times \boldsymbol{\omega}\). The formula \(\varphi=\lozenge_2\lozenge_1\Box_1 p\rightarrow\Box_1\lozenge_1 p\) is not valid in \(H\): consider a model \(M=(H,\theta)\) with \(\theta(p)=\{(\omega,1)\}\); then \(\varphi\) is falsified in \(M\) at \((0,0)\).
Consider the equivalence \(\equiv\) on \(\mathop{\mathrm{dom}}H\) that extends the diagonal by the set of pairs of form \(((\omega,m),(\omega,n))\). It is easy to check that \(H \twoheadrightarrow{H}{/}{\equiv}\), hence the logic \(L\) of the latter frame extends \({\mathrm{\small Tack}}\). It is also straightforward that \(\varphi\) is valid in \({H}{/}{\equiv}\), so \(L\) is a proper extension of \({\mathrm{\small Tack}}\). Finally, we observe that \(L\) is not locally tabular: \({H}{/}{\equiv}\) contains \(\boldsymbol{\omega} \times \boldsymbol{\omega}\) as a subframe, and the logic \({\mathrm{\small S5}}^2\) of this subframe is not locally tabular. ◻
Let \({\mathrm{\small S4.1[2]}}\) be the extension of \({\mathrm{\small S4}}\) with the formulas \(B_2\) and \(\Box\lozenge p\rightarrow\lozenge\Box p\) In transitive frames, \(\Box\lozenge p\rightarrow\lozenge\Box p\) defines the following first-order property: \[\label{eq:s4461-condition} \forall x\,\exists y\,\left(xRy \land \forall z \left(yRz \to z = y\right)\right),\tag{8}\] see [14]. The tack frame \(T\) has this property; since it is transitive and has height \(2,\) \({\mathrm{\small S4.1[2]}}\subseteq {\mathrm{\small Tack}}\).
We say that a bimodal frame \((X,R,\approx)\) is simple, if \(\approx\) is \(X\times X\).
Lemma 6. Every cluster in \(Cl{({\mathrm{\small S4}}.1 [ 2 ] \times {\mathrm{\small S5}})}\) is a point-generated \({\mathrm{\small S5}}^2\)-frame, or a simple frame.
Proof. Let \(C=(X,R,\approx) \in Cl{({\mathrm{\small S4}}.1 [ 2 ] \times {\mathrm{\small S5}})}\). The frame \((X,R)\) is a preorder and \(\approx\) is an equivalence on \(X\), and we have \(R\,\circ\, \approx\; = \; X\times X\). Assume that \(C\) is not simple. We claim that in this case \(R\) is symmetric. Assume \(xRy\). There is \(z\in X\) such that \(y\not\approx z\). We have \(yRz'\approx z\) for some \(z'\). Then \(y\neq z'\). It follows that \(y\) is not maximal in \((X,R)\) since by 8 the maximality would imply \(R(y) = \{y\}.\) Hence \(yRx\). ◻
We conclude this paper with the following axiomatic criterion of local tabularity above \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\).
Theorem 10. Let \(L\) be an extension of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\). Then \(L\) is locally tabular iff for some \(m\), \(L\) contains the product rpp formula \(\mathrm{rp}_m(1,1)\).
Proof. The ‘only if’ direction is given by Corollary 3.
‘If’. Let \(F_L\) be the canonical frame of \(L\), \(\mathcal{C}\) the set of cluster frames in \(F\), \(\mathcal{C}_0\) simple frames in \(\mathcal{C}\), and \(\mathcal{C}_1\) other frames in \(\mathcal{C}\).
Since the logic \({\mathrm{\small S4}}.1 [ 2 ]\) is locally tabular, the class of its frames is uniformly tunable, and so is \(\mathcal{C}_0\).
By Proposition [prop:rpp-canon], \(F_L\vDash\mathrm{rp}_m(1,1)\). Due to the first order characterization of \(\mathrm{rp}_m(1,1)\) given in Proposition [prop:rpp-to-modal-poly], \(\mathrm{rp}_m(1,1)\) is valid in each subframe \(C\in \mathcal{C}_1\) of \(F_L\). Hence, we have \(\mathcal{C}_1\vDash\mathrm{rp}_m(1,1)\). By Lemma 6, the logic \(L_0\) of \(\mathcal{C}_1\) is an extension of \({\mathrm{\small S5}}^2\); since \(\mathrm{rp}_m(1,1)\) is not in \({\mathrm{\small S5}}^2\), this extension is proper. By Theorem 9, \(L_0\) is locally tabular, and so \(\mathcal{C}_1\) is uniformly tunable.
It follows that \(\mathcal{C}=\mathcal{C}_0\cup\mathcal{C}_1\) is uniformly tunable. The formulas \(B_h\) are known to be canonical [1], so \(h(F_L)\leq 2\). By Theorem 3, the logic of \(F_L\) is locally tabular. Since \(\mathop{\mathrm{Log}}F_L\subseteq L\), \(L\) is locally tabular as well. ◻
According to Theorem [thm:criterion-frames-general], 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 10 gives an axiomatic criterion for all extensions of \({\mathrm{\small S4}}.1 [ 2 ]\times {\mathrm{\small S5}}\). We conjecture that Theorem 10 can be generalized for a wider class of logics.
Question 1. Let \(S4[h]\) be the extension of \({\mathrm{\small S4}}\) with the axiom of finite height \(B_h\). Does the following equivalence hold for every extension \(L\) of \({\mathrm{\small S4}}[h]\times {\mathrm{\small S5}}\)?
\(L\) contains a product rpp formula iff \(L\) is locally tabular.
We are grateful to Guram Bezhanishvili and Valentin Shehtman for valuable discussions.
The work of the first author was supported by NSF Grant DMS - 2231414.
Lemma 7. Let \(\mathrm{A}\) be finite, \(F\) an \(\mathrm{A}\)-frame such that:
(a) \(\mathop{\mathrm{dom}}F = X_1\cup X_2\) for disjoint \(X_1\) and \(X_2\), and
(b) \(F{\upharpoonright}X_1\) is a generated subframe of \(F,\) and
(c) \(F{\upharpoonright}X_i\) is \(f_i\)-tunable for some monotone \(f_i:\:\omega\to \omega,\) \(i = 1, 2.\)
Then \(F\) is \(g\)-tunable for \[g(n) = f_1(n) + f_2\left(n\cdot2^{f_1(n)\cdot |\mathrm{A}|} \right).\]
Proof. Let \(\mathcal{V}\) be a partition of \(\mathop{\mathrm{dom}}F,\,|\mathcal{V}| = n < \omega.\) Then \(\mathcal{V}\) induces partitions \(\mathcal{V}_1,\,\mathcal{V}_2\) of \(X_1\) and \(X_2,\) respectively. There exists a refinement \(\mathcal{U}_1\) of \(\mathcal{V}_1\) such that \(\mathcal{U}_1\) is tuned in \(F_1\) and \[\label{eq:clusters-1} |\mathcal{U}_1| \le f_1(|\mathcal{V}_1|) \le f_1(n).\tag{9}\]
For \(\lozenge\in\mathrm{A}\), define \(\alpha_\lozenge:\:X_2 \to 2^{\mathcal{U}_1}\) by letting \[\alpha_\lozenge(x) = \{U\in \mathcal{U}_1 \mid x\in R_\lozenge^{-1}[U]\}.\] Let \(\sim_\lozenge\) be the equivalence induced by \(\alpha_\lozenge\); it has at most \(2^{|\mathcal{U}_1|}\) classes. Hence, the equivalence \(\sim\; = \;\bigcap\{ \sim_\lozenge\mid \lozenge\in \mathrm{A}\}\) has at most \(2^{f_1(n)\cdot |\mathrm{A}|}\) classes. Let \(\equiv\) be the equivalence on \(X_2\) whose quotient is \(\mathcal{V}_2\). Put \(\mathcal{S}={X_2}{/}{(\sim\cap \equiv)}\). We have \[\label{eq:clusters-2} |\mathcal{S}| \le |\mathcal{V}_2| \cdot 2^{|\mathcal{U}_1|\cdot |\mathrm{A}|} \le n \cdot 2^{f_1(n)\cdot |\mathrm{A}|},\tag{10}\] where the latter inequality holds by 9 . Hence, there exists a refinement \(\mathcal{T}\) of \(\mathcal{S}\) of size at most \(f_2\left(n\cdot 2^{f_1(n)\cdot |\mathrm{A}|}\right)\), which is tuned in \(F_2\).
Consider the partition \(\mathcal{U}=\mathcal{U}_1 \cup \mathcal{T}\) of \(F\). Clearly, it refines \(\mathcal{V}\), and it has at most \(g(n)\) elements in view of 9 and 10 . So it remains to check that \(\mathcal{U}\) is tuned in \(F\).
Let \(xR_{\lozenge} y\) for some \(x,\,y\in X\) and \(\lozenge\in \mathrm{A}\), and let \(x'\in [x]_\mathcal{U}.\) We will show that \(x' R_\lozenge y'\) for some \(y'\in [y]_\mathcal{U}\).
Assume that \(x\in X_1\). Then \(y\in X_1\), since \(F{\upharpoonright}X_1\) is a generated subframe of \(F\). In this case, \(x\) and \(x'\) belong to the same element of \(\mathcal{U}_1.\) Since \(\mathcal{U}_1\) is tuned in \(F_1\), \(x' R_{\lozenge} y'\) for some \(y'\in [y]_{\mathcal{U}_1}=[y]_\mathcal{U}\), as desired.
Now assume \(x\in X_2\). Then \(x'\in [x]_\mathcal{T}\), so \(\alpha_\lozenge(x) = \alpha_\lozenge(x').\) If \(y\in X_1\), then \([y]_{\mathcal{U}_1}\in \alpha_\lozenge(x) = \alpha_\lozenge(x')\), so \(x' R_\lozenge y'\) for some \(y'\in [y]_{\mathcal{U}_1}=[y]_\mathcal{T}\), as desired. If \(y\in X_2\), then \(x' R_{\lozenge} y'\) for some \(y'\in [y]_\mathcal{T}=[y]_\mathcal{U}\), since \(\mathcal{T}\) is tuned in \(F_2\). ◻
Proof of theorem 3. ‘Only if’. Finite height follows from Theorem 1. 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 [prop:LF-for-subframess]. 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 2. 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 7.
Since \(\mathcal{F}=\mathcal{F}_h\) for some \(h\), \(\mathcal{F}\) is uniformly tunable, and hence its logic is locally tabular by Theorem 2. 0◻
To avoid any ambiguity, we remark that we write \(R_F^{\leq m}\) for \((R_F)^{\leq m}\), and \(R_F^*\) for \((R_F)^*\). The notation \(R_F^*\).\(\,^1\) refers to a footnote.↩︎