Modal Logics of Finite Direct Powers of $\omega$ Have the Finite Model Property

Abstract

Let $(\omega ^n,\preceq )$ be the n-th direct power of $(\omega ,\le )$, natural numbers with the standard ordering, and let $(\omega ^n,\prec )$ be the n-th direct power of $(\omega ,<)$. We show that for all finite n, the modal algebras of $(\omega ^n,\preceq )$ and of $(\omega ^n,\prec )$ are locally finite. In particular, it follows that the modal logics of these frames have the finite model property.

The work on this paper was supported by the Russian Science Foundation under grant 16-11-10252 and performed at Steklov Mathematical Institute of Russian Academy of Sciences.

1 Introduction

We consider modal logics of direct products of linear orders. It is known that the logics of finite direct powers of real numbers and of rational numbers with the standard non-strict ordering have the finite model property, are finitely axiomatizable, and consequently are decidable. These non-trivial results were obtained in [5], and independently in [16]. Later, analogous results were obtained for the logics of finite direct powers of $(\mathbb {R},<)$ [14]. Recently, it was shown that the direct squares $(\mathbb {R},\le ,\ge )^2$ and $(\mathbb {R},<,>)^2$ have decidable bimodal logics [6, 7]. Direct products of well-founded orders have never been investigated before in the context of modal logic.

Let $(\omega ^n,\preceq )$ be the n-th direct power of $(\omega ,\le )$, natural numbers with the standard ordering: for $x,y\in \omega ^n$, $x\preceq y$ iff $x(i)\le y(i)$ for all $i<n$. Likewise, let $(\omega ^n,\prec )$ be the the direct power $(\omega ,<)^n$: $x\prec y$ iff $x(i)< y(i)$ for all $i<n$.

The main result of this paper (Theorem 1) shows that for all finite $n>0$, the modal algebras of the frames $(\omega ^n,\preceq )$ and $(\omega ^n,\prec )$ are locally finite. It particular, it follows that the modal logics of these frames have the finite model property.

2 Partitions of Frames, Local Finiteness, and the Finite Model Property

We assume the reader is familiar with the basic notions of modal logics [1, 4]. By a logic we mean a normal propositional modal logic. For a (Kripke) frame $\mathsf {F}$, $Log(\mathsf {F})$ denotes its modal logic, i.e., the set of all modal formulas that are valid in $\mathsf {F}$. For a set W, $\mathcal {P}(W)$ denotes the powerset of W. The (complex) algebra of a frame (W, R) is the modal algebra $(\mathcal {P}(W),R^{-1})$. The algebra of $\mathsf {F}$ is denoted by $\mathsf {A}(\mathsf {F})$. A logic has the finite model property if it is complete with respect to a class of finite frames (equivalently, finite algebras).

A partition $\mathcal {A}$ of a set W is a set of non-empty pairwise disjoint sets such that $W=\bigcup \mathcal {A}$. A partition $\mathcal {B}$ refines $\mathcal {A}$, if each element of $\mathcal {A}$ is the union of some elements of $\mathcal {B}$.

Definition 1

Let $\mathsf {F}=(W,R)$ be a Kripke frame. A partition $\mathcal {A}$ of W is tuned (in $\mathsf {F}$) if for every $U,V\in \mathcal {A}$,

$$\exists u\in U \, \exists v\in V \, uR v \;\Rightarrow \; \forall u\in U\,\exists v\in V\,uRv.$$

$\mathsf {F}$ is tunable if for every finite partition $\mathcal {A}$ of $\mathsf {F}$ there exists a finite tuned refinement $\mathcal {B}$ of $\mathcal {A}$.

Proposition 1

If $\mathsf {F}$ is tunable, then $Log(\mathsf {F})$ has the finite model property.

Apparently, this fact was first observed by H. Franzén (see [13]). This proposition can be explained as follows. Let $L$ be the logic of a frame $\mathsf {F}$, or in other words, the logic of the modal algebra $\mathsf {A}(\mathsf {F})$. Equivalently, $L$ is the logic of finitely generated subalgebras of $\mathsf {A}(\mathsf {F})$. Recall that an algebra $\mathsf {A}$ is locally finite if every finitely generated subalgebra of $\mathsf {A}$ is finite. It follows that if $\mathsf {A}(\mathsf {F})$ is locally finite, then $L$ has the finite model property. Hence, Proposition 1 is a corollary of the following observation.

Proposition 2

The algebra of a frame $\mathsf {F}$ is locally finite iff $\mathsf {F}$ is tunable.

Proof

From Definition 1 we have: a finite partition $\mathcal {B}$ is tuned in $\mathsf {F}=(W,R)$ iff the family $\{\cup x\mid x\subseteq \mathcal {B}\}$ of subsets of W forms a subalgebra of the modal algebra $\mathsf {A}(\mathsf {F})=(\mathcal {P}(W), R^{-1})$.

Assume that $\mathsf {A}(\mathsf {F})$ is locally finite and $\mathcal {A}$ is a finite partition of W. Consider the subalgebra $\mathsf {B}$ of $\mathsf {A}(\mathsf {F})$ generated by the elements of $\mathcal {A}$. Then the set $\mathcal {B}$ of the atoms of $\mathsf {B}$ is a finite tuned refinement of $\mathcal {A}$.

Now assume that $\mathsf {F}$ is tunable and $\mathsf {B}$ is the subalgebra of $\mathsf {A}(\mathsf {F})$ generated by a finite family $\mathcal {V}$ of subsets of W. Let $\mathcal {A}$ be the quotient set $W/{\sim }$, where

$$u\sim v \text { iff } \forall A\in \mathcal {V}\, (u\in A\Leftrightarrow v\in A).$$

Since $\mathcal {A}$ is a finite partition of W, there exists its finite tuned refinement $\mathcal {B}$. The finite family $\{\cup x\mid x\subseteq \mathcal {B}\}$ is the carrier of a subalgebra of $\mathsf {A}(\mathsf {F})$ and contains $\mathcal {V}$. Hence the algebra $\mathsf {B}$ is finite.    $\square$

Thus, logics of tunable frames have the finite model property, and moreover, algebras of tunable frames are locally finite.

Example 1

Consider the frame $(\omega ,\le )$, natural numbers with the standard ordering. Suppose that $\mathcal {A}$ is a finite partition of $\omega$. If every $A\in \mathcal {A}$ is infinite, then $\mathcal {A}$ is tuned in $(\omega ,\le )$ and in $(\omega ,<)$. Otherwise, let $k_0$ be the greatest element of the finite set $\bigcup \{A\in \mathcal {A}\mid A \text { is finite}\}$, and $U=\{k\mid k_0<k<\omega \}$. Consider the following finite partition $\mathcal {B}$ of $\omega$:

$$\mathcal {B}=\{\{k\}\mid k\le k_0\} \cup \{A\cap U\mid A \text { is an infinite element of } \mathcal {A}\}.$$

Each element of $\mathcal {B}$ is either infinite, or a singleton, and singletons in $\mathcal {B}$ cover an initial segment of $\omega$. Thus, $\mathcal {B}$ is a finite refinement of $\mathcal {A}$ which is tuned in $(\omega ,\le )$ and in $(\omega ,<)$.

It follows that the algebras of the frames $(\omega ,\le )$ and $(\omega ,<)$ are locally finite.

Remark 1

Recall that a logic $L$ is locally finite (in another terminology, locally tabular) if the Lindenbaum algebra of $L$ is locally finite [4]. Equivalently, a logic $L$ is locally finite if the variety of its algebras is locally finite, i.e., every finitely generated algebra validating $L$ is finite.

A logic of a transitive frame is locally finite iff the frame is of finite height [8, 11]. Thus, although the algebras of the frames $(\omega ,\le )$ and $(\omega ,<)$ are locally finite, the logics of these frames are not. Hence, local finiteness of the algebra $\mathsf {A}(\mathsf {F})$ does not imply local finiteness of the logic $Log(\mathsf {F})$.

Local finiteness of the variety generated by an algebra $\mathsf {A}$ of a finite signature is equivalent to uniform local finiteness of $\mathsf {A}$: an algebra $\mathsf {A}$ is uniformly locally finite if there exists a function $f:\omega \rightarrow \omega$ such that the cardinality of a subalgebra of $\mathsf {A}$ generated by $m<\omega$ elements does not exceed f(m); see [9, Sect. 14, Theorem 3].

Local finiteness of modal logics is formulated in terms of tuned partitions as follows [15]: the logic of a frame $\mathsf {F}$ is locally finite iff there exists a function $f:\omega \rightarrow \omega$ such that for every finite partition $\mathcal {A}$ of W there exists a refinement $\mathcal {B}$ of $\mathcal {A}$ such that $|\mathcal {B}|\le f(|\mathcal {A}|)$ and $\mathcal {B}$ is tuned in $\mathsf {F}$.

3 Main Result

Theorem 1

For all finite $n>0$, the algebras $\mathsf {A}(\omega ^n,\preceq )$ and $\mathsf {A}(\omega ^n,\prec )$ are locally finite.

The simple case $n=1$ was considered in Example 1. To prove the theorem for the case of arbitrary finite n, we need some auxiliary constructions.

Definition 2

Consider a non-empty $V\subseteq \omega ^n$. Put

$$ \begin{array}{llll} &{}J(V)&{}= \{i<n\mid \exists x\in V\,\exists y\in V\; x(i)\ne y(i)\}, \\ &{}I(V)&{}=\{i<n\mid \forall x\in V\,\forall y\in V\; x(i)= y(i)\}=n{\setminus }J(V). \end{array} $$

The hull of V is the set

$$\overline{V}=\{y\in \omega ^n \mid \forall i\in I(V)\, (y(i)=x(i) \text { for some (for all) } x\in V)\}.$$

V is pre-cofinal if it is cofinal in its hull, i.e.,

$$\forall x\in \overline{V} \, \exists y\in V \, x\preceq y.$$

A partition $\mathcal {A}$ of $V\subseteq \omega ^n$ is monotone if

• all of its elements are pre-cofinal, and

• for all $x,y\in V$ such that $x\preceq y$ we have $J([x]_\mathcal {A})\subseteq J([y]_\mathcal {A})$,

where $[x]_\mathcal {A}$ is the element of $\mathcal {A}$ containing x.

Lemma 1

If $\mathcal {A}$ is a monotone partition of $\omega ^n$, then $\mathcal {A}$ is tuned in $(\omega ^n, \preceq )$ and in $(\omega ^n, \prec )$.

Proof

Let $A,B\in \mathcal {A}$, $x,y\in A$, $x\preceq z\in B$. Let u be the following point in $\omega ^n$:

$$\begin{aligned} u(i)=y(i)+1 \text { for }i\in J(A), \text { and } u(i)=z(i) \text { for } i\in I(A). \end{aligned}$$

(1)

We have

$$\{i<n\mid u(i)\ne z(i)\} \; \subseteq \; n{\setminus }I(A)\; =\; J(A) \; \subseteq \; J(B);$$

the first inclusion follows from (1), the second follows from the monotonicity of $\mathcal {A}$. Hence, we have $u(i)=z(i)$ for all $i\in I(B)$. By the definition of $\overline{B}$, we have $u\in \overline{B}$. Since B is cofinal in $\overline{B}$ (we use monotonicity again), for some $u'\in B$ we have $u\preceq u'$.

By (1), we have $y(i)\le u(i)$ for all $i<n$: indeed, $y(i)=x(i)\le z(i)=u(i)$ for $i\in I(A)$, and $u(i)= y(i)+1$ otherwise. Thus, $y\preceq u$, and so $y\preceq u'$. It follows that $\mathcal {A}$ is tuned in $(\omega ^n, \preceq )$.

In order to show that $\mathcal {A}$ is tuned in $(\omega ^n, \prec )$, we now assume that $x\prec z$. Then we have $y(i)< u(i)$ for all $i<n$, since $y(i)=x(i)< z(i)=u(i)$ for $i\in I(A)$, and $u(i)= y(i)+1$ otherwise. Hence $y\prec u$. Since $u\preceq u'$, we have $y\prec u'$, as required.    $\square$

Let $\mathcal {A}$ be a partition of a set W. For $V\subseteq W$, the partition

$$ \mathcal {A}{\upharpoonright }V=\{A\cap V\mid A\in \mathcal {A}\; \& \;A\cap V\ne \varnothing \}$$

of V is called the restriction of $\mathcal {A}$ to V.

For a family $\mathcal {B}$ of subsets of W, the partition induced by $\mathcal {B}$ on $V\subseteq W$ is the quotient set $V/{\sim }$, where

$$x\sim y \text { iff } \forall A\in \mathcal {B}\, (x\in A\Leftrightarrow y\in A).$$

Lemma 2

Any finite partition of $\omega ^n$ has a finite monotone refinement.

Proof

By induction on n. Let $\mathcal {A}$ be a finite partition of $\omega ^n$.

Suppose $n=1$. Let $k_0$ be the greatest element of the finite set

$$\bigcup \{A\in \mathcal {A}\mid A \text { is finite}\}.$$

Put $\mathcal {B}=\{\{k\}\mid k\le k_0\}$. Let $\mathcal {C}$ be the partition induced by $\mathcal {A}\cup \mathcal {B}$ on $\omega$. Consider $x\in \omega$ and put $A=[x]_\mathcal {C}$. If $x\le k_0$, then $A=\overline{A}=\{x\}$ and $J(A)=\varnothing$. If $x>k_0$, then A is cofinal in $\omega =\overline{A}$, $J(A)=\{0\}$. It follows that $\mathcal {C}$ is the required monotone refinement of $\mathcal {A}$.

Suppose $n>1$. For $k\in \omega$ let $U_{k}=\{y\in \omega ^n\mid y(i)\ge k \text { for all }i<n\}$. Since $\mathcal {A}$ is finite, we can choose a natural number $k_0$ such that

$$\begin{aligned} \text {if }y\in U_{k_0},\text { then }[y]_\mathcal {A}\text { is cofinal in }\omega ^n. \end{aligned}$$

(2)

Indeed, if $A\in \mathcal {A}$ is not cofinal in $\omega ^n$, then $U_{k_A}\cap A=\varnothing$ for some $k_A<\omega$; hence, (2) holds whenever $k_0$ is greater than every such $k_A$.

It follows that the partition $\mathcal {A}{\upharpoonright }U_{k_0}$ is monotone: it consists of sets that are cofinal in $\omega ^n$ (and so, they are obviously pre-cofinal), and $J(A)=n$ for all $A\in \mathcal {A}{\upharpoonright }U_{k_0}$.

We are going to extend this partition step by step in order to obtain a sequence of finite monotone partitions of $U_{k_0-1}, \ldots , U_{0}=\omega ^n$, respectively refining $\mathcal {A}{\upharpoonright }U_{k_0-1}, \ldots , \mathcal {A}{\upharpoonright }U_{0}=\mathcal {A}$.

First, let us describe the construction for the case $k_0=1$, the crucial technical step of the proof.

Claim A. Suppose that $\mathcal {B}$ is a finite monotone partition of $U_1$ refining $\mathcal {A}{\upharpoonright }U_1$. Then there exists a finite monotone partition $\mathcal {C}$ of $\omega ^n$ refining $\mathcal {A}$ such that $\mathcal {B}\subseteq \mathcal {C}$.

Proof

$\mathcal {C}$ will be the union of $\mathcal {B}$ and a partition of the set

$$V=\{x\in \omega ^n\mid x(i)=0 \text { for some } i<n\} = \omega ^n{\setminus }U_1.$$

To construct the required partition of V, for $I\subseteq n$ put

$$V_I=\{x\mid \forall i<n\,(i\in I \,\Leftrightarrow \, x(i)=0)\}.$$

Then $\{V_I\mid \varnothing \ne I\subseteq n\}$ is a partition of V, $V_\varnothing =U_1$.

Each $V_I$ considered with the order $\preceq$ on it is isomorphic to $(\omega ^{n-|I|},\preceq )$. Thus, by the induction hypothesis, for a non-empty $I\subseteq n$ we have:

$$\begin{aligned} \text {Each finite partition of }V_I\text { admits a finite monotone refinement.} \end{aligned}$$

(3)

For $I\subseteq n$, by induction on the cardinality of I we define a finite partition $\mathcal {C}_I$ of $V_I$.

We put $\mathcal {C}_\varnothing =\mathcal {B}$.

Assume that I is non-empty. Consider the projection $\Pr _I: x\mapsto y$ such that $y(i)=0$ whenever $i\in I$, and $y(i)=x(i)$ otherwise. Note that for all $K\subset I$, $x\in V_K$ implies $\Pr _I(x)\in V_I$. Let $\mathcal {D}$ be the partition induced on $V_I$ by the family

$$\begin{aligned} \mathcal {A}\cup \bigcup \limits _{K\subset I}\{\mathop {\Pr }\nolimits _I(A)\mid A\in V_K \}. \end{aligned}$$

(4)

By an immediate induction argument, $\mathcal {D}$ is finite. Let $\mathcal {C}_I$ be a finite monotone refinement of $\mathcal {D}$, which exists according to (3).

We put

$$\mathcal {C}=\bigcup _{I\subseteq n} \mathcal {C}_I.$$

Then $\mathcal {C}$ is a finite refinement of $\mathcal {A}$. We have to check monotonicity.

Every element A of $\mathcal {C}$ is pre-cofinal, because A is an element of a monotone partition $\mathcal {C}_I$ for some I. In order to check the second condition of monotonicity, we consider x, y in $\omega ^n$ with $x\preceq y$ and show that

$$\begin{aligned} J([x]_\mathcal {C})\subseteq J([y]_\mathcal {C}). \end{aligned}$$

(5)

Let $x \in V_I$, $y \in V_K$ for some $I,K\subseteq n$. Since $x\preceq y$, we have $K\subseteq I$. If $K=I$, then (5) holds, since in this case $[x]_\mathcal {C}$ and $[y]_\mathcal {C}$ belong to the same monotone partition $\mathcal {C}_I$. Assume that $K\subset I$. In this case we have:

$$J([x]_\mathcal {C})\subseteq J([\mathop {\Pr }\nolimits _I(y)]_\mathcal {C})\subseteq J(\mathop {\Pr }\nolimits _I([y]_\mathcal {C}))\subseteq J([y]_\mathcal {C}).$$

To check the first inclusion, we observe that $\Pr _I(y)$ belongs to $V_I$ (since $K\subset I$). This means that $[x]_\mathcal {C}$ and $[\Pr _I(y)]_\mathcal {C}$ are elements of the same partition $\mathcal {C}_I$. We have $x\preceq \Pr _I(y)$, since $x\in V_I$ and $x\preceq y$. Now the first inclusion follows from monotonicity of $\mathcal {C}_I$. By (4), $\mathop {\Pr }\nolimits _I([y]_\mathcal {C})$ is the union of some elements of $\mathcal {C}_I$ (since $K\subset I$ and $[y]_\mathcal {C}\in \mathcal {C}_K$); trivially, $\Pr _I(y)\in \Pr _I([y]_\mathcal {C})$, hence $[\mathop {\Pr }\nolimits _I(y)]_\mathcal {C}$ is a subset of $\mathop {\Pr }\nolimits _I([y]_\mathcal {C})$. This yields the second inclusion. The third inclusion is immediate from Definition 2. Thus, we have (5), which proves the claim.   $\square$

From Claim A it is not difficult to obtain the following:

Claim B. Let $0<k<\omega$. If $\mathcal {B}$ is a finite monotone partition of $U_k$ refining $\mathcal {A}{\upharpoonright }U_k$, then there exists a finite monotone partition $\mathcal {C}$ of $U_{k-1}$ refining $\mathcal {A}{\upharpoonright }U_{k-1}$ such that $\mathcal {B}\subseteq \mathcal {C}$.

Proof

Consider the translation $\mathop {\mathrm {Tr}}:U_{k-1}\rightarrow \omega ^n$ taking $(x_i)_{i<n}$ to $(x_i-k+1)_{i<n}$. Let $\mathcal {B}'$ be the set $\{\mathop {\mathrm {Tr}}(A)\mid A\in \mathcal {B}\}$ of images of elements of $\mathcal {B}$ by $\mathop {\mathrm {Tr}}$, and $\mathcal {A}'$ be the set $\{\mathop {\mathrm {Tr}}(A)\mid A\in \mathcal {A}{\upharpoonright }U_{k-1}\}$. Then $\mathcal {A}'$ is a partition of $\omega ^n$, $\mathcal {B}'$ is a finite monotone partition of $U_1$ refining $\mathcal {A}'{\upharpoonright }U_1$. By Claim A, there exists a finite monotone partition $\mathcal {C}'$ of $\omega ^n$ refining $\mathcal {A}'$ such that $\mathcal {B}'\subseteq \mathcal {C}'$. The family is the required partition of $U_{k-1}$.    $\square$

Applying Claim B $k_0$ times, we obtain the required monotone refinement of $\mathcal {A}$. This proves Lemma 2.   $\square$

From the above two lemmas we obtain that the frames $(\omega ^n, \preceq )$ and $(\omega ^n, \prec )$, $0<n<\omega$, are tunable. Now the proof of Theorem 1 immediately follows from Proposition 2.

Corollary 1

For all finite n, the logics $Log(\omega ^n,\preceq )$ and $Log(\omega ^n,\prec )$ have the finite model property.

4 Questions and Conjectures

It is well-known that every extension of $Log(\omega ,\le )$ has the finite model property [3].

Question 1

Let $L$ be an extension of $Log(\omega ^n,\preceq )$ for some finite $n>1$. Does $L$ have the finite model property?

Every extension of a locally finite logic is locally finite, and so has the finite model property. Although the algebras of the frames $(\omega ^n,\preceq )$ and $(\omega ^n,\prec )$ are locally finite, the logics of these frames are not (recall that a logic of a transitive frame is locally finite iff the frame is of finite height [8, 11]). Thus, Theorem 1 does not answer Question 1.

At the same time, Theorem 1 yields another corollary. A subframe of a frame (W, R) is the restriction $(V,R\cap (V\times V))$, where V is a non-empty subset of W. It follows from Definition 1 that if a frame is tunable then all its subframes are (details can be found in the proof of Lemma 5.9 in [15]). From Proposition 2, we have:

Proposition 3

If the algebra of a frame $\mathsf {F}$ is locally finite, then the algebra of any subframe of $\mathsf {F}$ is also locally finite.

Corollary 2

For all finite n, if $\mathsf {F}$ is a subframe of $(\omega ^n,\preceq )$ or of $(\omega ^n,\prec )$, then $\mathsf {A}(\mathsf {F})$ is locally finite, and $Log(\mathsf {F})$ has the finite model property.

While $Log(\omega ,\le )$ is not locally finite, the intermediate logic ${ILog}(\omega ,\le )$ is (see, e.g., [17, Sect. 3.4]).

Conjecture 1

For all finite n, ${ILog}(\omega ^n,\preceq )$ is locally finite.

The logics of finite direct powers of $(\mathbb {R},\le )$ and of $(\mathbb {R},<)$ have the finite model property, are finitely axiomatizable, and consequently are decidable [5, 14, 16].

Question 2

Let $n>1$. Are logics $Log(\omega ^n,\preceq )$ and $Log(\omega ^n,\prec )$ decidable or at least recursively axiomatizable?

In the one-dimensional case, decidability is a classical result: apparently, the first published proof of finite axiomatizability and the finite model property of the logic $Log(\omega ,\le )$ is given in [2]; for the logic $Log(\omega ,<)$, these properties were established in [10] and [12].

Finally, let us address the following question: does the direct product operation on frames preserve local finiteness of their modal algebras?

Proposition 4

If a frame $\mathsf {F}$ is tunable and a frame $\mathsf {G}$ is finite, then the direct product $\mathsf {F}\times \mathsf {G}$ is tunable.

Proof

Let $\mathsf {F}=(F,R)$, $\mathsf {G}=(G,S)$, and $\mathcal {A}$ be a finite partition of $F\times G$. For A in $\mathcal {A}$ and y in G, we put $\Pr _y(A)=\{x\in F\mid (x,y)\in A\}$, $\mathcal {A}_y={\{ \Pr _y(A)\mid A\in \mathcal {A}\}}$. Let $\mathcal {B}$ be the partition induced on F by the family $\bigcup _{y\in G} \mathcal {A}_y$. Since $\mathcal {B}$ is finite, there exists its finite refinement $\mathcal {C}$ that is tuned in $\mathsf {F}$. Consider the partition

$$ \mathcal {D}=\{A\times \{y\}\mid A\in \mathcal {C}\, \& \, y\in G \}$$

of $F\times G$. Then $\mathcal {D}$ is a finite refinement of $\mathcal {A}$. It is not difficult to check that $\mathcal {D}$ is tuned in $\mathsf {F}\times \mathsf {G}$.    $\square$

If follows that if the algebra of $\mathsf {F}$ is locally finite and $\mathsf {G}$ is finite, then the algebra of $\mathsf {F}\times \mathsf {G}$ is locally finite.

Question 3

Consider tunable frames $\mathsf {F}_1$ and $\mathsf {F}_2$. Is the direct product $\mathsf {F}_1\times \mathsf {F}_2$ tunable?

If this is true, then Theorem 1 immediately follows from the simple one-dimensional case. And, moreover, in this case Theorem 1 can be generalized to arbitrary ordinals in view of the following observation.

Proposition 5

For every ordinal $\alpha >0$, the modal algebras $\mathsf {A}(\alpha ,\le )$, $\mathsf {A}(\alpha ,<)$ are locally finite.

Proof

By induction on $\alpha$ we show that the frames $(\alpha ,\le )$, $(\alpha ,<)$ are tunable.

For a finite $\alpha$, the statement is trivial.

Suppose that $\mathcal {A}$ is a finite partition of an infinite $\alpha$. If every element of $\mathcal {A}$ is cofinal in $\alpha$, then $\mathcal {A}$ is tuned in $(\alpha ,\le )$ and in $(\alpha ,<)$. Otherwise, we put

$$ \beta =\sup \bigcup \{A\in \mathcal {A}\mid A \text { is bounded in } \alpha \}. $$

Since $\mathcal {A}$ is finite, we have $\beta <\alpha$. Put $\mathcal {B}=\mathcal {A}{\upharpoonright }\beta$. By the induction hypothesis, there exists a finite tuned refinement $\mathcal {C}$ of $\mathcal {B}$. Then the partition of $\alpha$ induced by $\mathcal {A}\cup \mathcal {C}$ is the required refinement of $\mathcal {A}$.    $\square$

Conjecture 2

If $(\alpha _i)_{i< n}$ is a finite family of ordinals, then the algebras of the direct products $\prod _{i<n}(\alpha _i,\le )$, $\prod _{i< n}(\alpha _i,<)$ are locally finite.