Modal logics of finite direct powers of $\omega$ have the finite model property

TL;DR

This paper proves that the modal logics of finite direct powers of natural numbers with standard and strict orderings have the finite model property, and their modal algebras are locally finite, advancing understanding of their logical structure.

Contribution

It establishes the finite model property and local finiteness of modal algebras for frames based on finite powers of 0 with standard and strict orderings, which was previously unknown.

Findings

Modal logics of (0^n,\u2261) have the finite model property.

Modal logics of (0^n,<) have the finite model property.

Modal algebras of these frames are locally finite.

Abstract

Let $(\omega^n,\preceq)$ be the direct power of $n$ instances of $(\omega,\leq)$, natural numbers with the standard ordering, $(\omega^n,\prec)$ the direct power of $n$ instances of $(\omega,<)$. We show that for all finite $n$, the modal logics of $(\omega^n,\preceq)$ and of $(\omega^n,\prec)$ have the finite model property and moreover, the modal algebras of the frames $(\omega^n,\preceq)$ and $(\omega^n,\prec)$ are locally finite.

Equations

$$\exists u\in U\exists v\in VuRv\Rightarrow \forall u\in U\exists v\in VuRv.$$

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

$$\begin{array}[]{llll}&J(V)&=\{i<n\mid\exists x\in V\,\exists y\in V\;x(i)\neq 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}$$

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

$$\forall x\in \overline{V}\exists y\in Vx⪯y.$$

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

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

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

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

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

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

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

$$V_I$$

$$\mathcal{A}\cup \bigcup _{K\subset I}\{{\mathrm{Pr}}_I(A)\mid A\in V_K\}.$$

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

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

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

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

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

Full text

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 [Gol80], and independently in [She83]. Later, analogous results were obtained for the logics of finite direct powers of $(\mathbb{R},<)$ [SS03]. Recently, it was shown that the direct squares $(\mathbb{R},\leq,\geq)^{2}$ and $(\mathbb{R},<,>)^{2}$ have decidable bimodal logics [HR18], [HM18]. Direct products of well-founded orders have never been considered before in the context of modal logic.

Let $(\omega^{n},\preceq)$ be the direct power of $n$ instances of $(\omega,\leq)$, natural numbers with the standard ordering: for $x,y\in\omega^{n}$, $x\preceq y$ iff $x(i)\leq y(i)$ for all $i<n$. Likewise, let $(\omega^{n},\prec)$ be the the direct power $(\omega,<)^{n}$. We will show that for all finite $n>0$, the logics $Log(\omega^{n},\preceq)$ and $Log(\omega^{n},\prec)$ have the finite model property and moreover, the algebras of the frames $(\omega^{n},\preceq)$ and $(\omega^{n},\prec)$ are locally finite.

2 Partitions of frames, local finiteness, and the finite model property

We assume the reader is familiar with the basic notions of modal logics [BdRV02, CZ97]. 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 valid in $\mathsf{F}$ modal formulas. 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 frame (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}$,

[TABLE]

$\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 [Seg73]). For the proof, we notice the following: a finite partition $\mathcal{B}$ is tuned in a frame $(W,R)$ iff the family $\{\cup x\mid x\subseteq\mathcal{B}\}$ of subsets of $W$ forms a subalgebra of the modal algebra $(\mathcal{P}(W),R^{-1})$. Recall that an algebra $\mathsf{A}$ is locally finite if every finitely generated subalgebra of $\mathsf{A}$ is finite. Thus, from Definition 1 we have:

Proposition 2

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

If $L$ is the logic of a frame $\mathsf{F}$, then $L$ is the logic of the modal algebra $\mathsf{A}(\mathsf{F})$. Equivalently, $L$ is the logic of finitely generated subalgebras of $\mathsf{A}(\mathsf{F})$. It follows that if $\mathsf{A}(\mathsf{F})$ is locally finite, then $L$ has the finite model property.

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,\leq)$, 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,\leq)$ and in $(\omega,<)$. Otherwise, let $k_{0}$ be the greatest element of the finite set $\bigcup\{A\in\mathcal{A}\mid A\textrm{ is finite}\}$, and $U=\{k\mid k_{0}<k<\omega\}$. Consider the following finite partition $\mathcal{B}$ of $\omega$:

[TABLE]

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,\leq)$ and in $(\omega,<)$.

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

Remark 1

Although the algebras of the frames $(\omega,\leq)$ and $(\omega,<)$ are locally finite, the logics of these frames are not.

Recall that a logic $L$ is locally finite (or locally tabular) if the Lindenbaum algebra of $L$ is locally finite. A logic of a transitive frame is locally finite iff the frame is of finite height [Seg71],[Mak75]. It terms of tuned partitions, local finiteness of a logic is characterized as follows [SS16]: the logic of a frame $\mathsf{F}$ is locally finite iff there exists a function $f:\omega\to\omega$ such that for every finite partition $\mathcal{A}$ of $W$ there exists a tuned in $\mathsf{F}$ refinement $\mathcal{B}$ of $\mathcal{A}$ such that $|\mathcal{B}|\leq f(|\mathcal{A}|)$.

3 Main result

Theorem 3.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

[TABLE]

The hull of $V$ is the set

[TABLE]

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

[TABLE]

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}$:

[TABLE]

We have

[TABLE]

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^{\prime}\in B$ we have $u\preceq u^{\prime}$.

By (1), we have $y(i)\leq u(i)$ for all $i<n$: indeed, $y(i)=x(i)\leq 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^{\prime}$. 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^{\prime}$, we have $y\prec u^{\prime}$, as required.

∎

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

[TABLE]

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

[TABLE]

Lemma 2

If $\mathcal{A}$ is a finite partition of $\omega^{n}$, then there exists its finite monotone refinement.

Proof

By induction on $n$.

Suppose $n=1$. Let $k_{0}$ be the greatest element of the finite set

[TABLE]

Put $\mathcal{B}=\{\{k\}\mid k\leq k_{0}\}\cup\{k\mid k_{0}<k<\omega\}$. Let $\mathcal{C}$ be the the partition induced by $\mathcal{A}\cup\mathcal{B}$ on $\omega$. Consider $x\in\omega$ and put $A=[x]_{\mathcal{C}}$. If $x\leq k_{0}$, then $A=\overline{A}=\{x\}$ and $J(A)=\varnothing$. If $x>k_{0}$, then $A$ is cofinal in $\omega$, $\overline{A}=\omega$, $J(A)=\{0\}$. In 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)\geq k\text{ for all }i<n\}$. Since $\mathcal{A}$ is finite, we can chose a natural number $k_{0}$ such that

if $y\in U_{k_{0}}$, then $[y]_{\mathcal{A}}$ is cofinal in $\omega^{n}$.

It follows that the partition $\mathcal{A}{\upharpoonright}U_{k_{0}}$ is monotone: it consists of cofinal in $\omega^{n}$ sets which 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}$, …, $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

[TABLE]

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

[TABLE]

Then $\{V_{I}\mid\varnothing\neq 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:

[TABLE]

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}(y)\in V_{I}$. Let $\mathcal{D}$ be the partition induced on $V_{I}$ by the family

[TABLE]

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 (2).

We put

[TABLE]

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

[TABLE]

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 (4) holds, since $[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:

[TABLE]

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 (3), $\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 $[\Pr\nolimits_{I}(y)]_{\mathcal{C}}$ is a subset of $\Pr\nolimits_{I}([y]_{\mathcal{C}})$. This yields the second inclusion. The third inclusion is immediate from Definition 2. Thus, we have (4), which proves the claim. ∎

From Claim A one can easily 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}$ such that $\mathcal{B}\subseteq\mathcal{C}$.

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

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 the Theorem 3.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 Open problems and conjectures

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

Question 1

Let $L$ be an extension of $Log(\omega^{n},\preceq)$ for some finite $n>0$. 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 [Seg71],[Mak75]). Thus, Theorem 3.1 does not answer Question 1.

At the same time, Theorem 3.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 [SS16]). From Proposition 2, we have:

Proposition 3

If the algebra of a frame $\mathsf{F}$ is locally finite, then the algebras of all subframes of $\mathsf{F}$ are.

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,\leq)$ is not locally finite, the intermediate logic ${ILog}(\omega,\leq)$ is.

Conjecture 1

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

The logics of finite direct powers of $(\mathbb{R},\leq)$ and of $(\mathbb{R},<)$ have the finite model property, are finitely axiomatizable, and consequently are decidable [Gol80], [She83], [SS03]. Recently, it was shown that the direct squares $(\mathbb{R},\leq,\geq)^{2}$ and $(\mathbb{R},<,>)^{2}$ have decidable bimodal logics [HR18], [HM18].

Question 2

Let $n>1$. Is $Log(\omega^{n},\preceq)$ decidable? recursively axiomatizable? Does $Log(\omega^{n},\preceq,\succeq)$ have the finite model property?

Proposition 4

If $\mathsf{F}$ is tunable and $\mathsf{G}$ is finite, then $\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 tuned refinement $\mathcal{C}$. Consider the partition

[TABLE]

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}$. ∎

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 3.1 immediately follows from the simple one-dimensional case. And, moreover, in this case Theorem 3.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,\leq)$, $\mathsf{A}(\alpha,<)$ are locally finite.

Proof

By induction on $\alpha$ we show that the frames $(\alpha,\leq)$, $(\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,\leq)$ and in $(\alpha,<)$. Otherwise, we put

[TABLE]

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}$. ∎

Question 4

Let $(\alpha_{i})_{i\in I}$ be a finite family of ordinals. Are the algebras of the direct products $\prod_{i\in I}(\alpha_{i},\leq)$, $\prod_{i\in I}(\alpha_{i},<)$ locally finite? Do the logics of these products have the finite model property?