1 Introduction↩︎

A central part of the study of modal logic is to determine whether a logic has a certain property, such as Kripke completeness, the finite model property (FMP), and decidability. From a global viewpoint, this gives rise to the following algorithmic problems: In a class of logics, is it decidable whether a logic has a certain property?¹ More precisely, a logics’ property (or simply, property) \(P\) in a class \(\mathcal{C}\) of logics is identified with a subclass of \(\mathcal{C}\), and \(P\) is decidable if there exists an algorithm such that, for any finitely axiomatizable logic \(L \in \mathcal{C}\), given by its finite axiomatization, the algorithm decides whether \(L\) has the property \(P\).² We refer to [@Chagrov.Zakharyaschev1997] and [@Wolter.Zakharyaschev2007] for historical accounts. See Table 1 for a summary of the results discussed in this introduction.

Let \(\mathsf{K}_n\) denote the least normal \(n\)-modal logic and \(\mathsf{K}= \mathsf{K}_1\). For a normal modal logic \(L\), let \(\mathsf{NExt}L\) be the lattice of all normal extensions of \(L\). In the unimodal case, many properties have been shown to be undecidable in \(\mathsf{NExt}\mathsf{K}\). Thomason [@Thomason1982] showed the undecidability of Kripke completeness, and a series of works by Chagrov and his co-authors [@chagrov1990I; @chagrov1990II; @Chagrov.Zakharyaschev1993; @Chagrov.Chagrova1995; @Chagrov2002] introduced a general method to show the undecidability of various properties, including the FMP, first-order definability, decidability, tabularity, and the coincidence with a fixed tabular logic. Kracht and Wolter [@Kracht.Wolter1999] proved independently that decidability, the FMP, and tabularity are undecidable in \(\mathsf{NExt}\mathsf{K}\) via the Thomason-Simulation [@Thomason1974a; @Thomason1975b]. On the positive side, it is well-known that consistency is decidable for normal unimodal logics as the lattice \(\mathsf{NExt}\mathsf{K}\) has only two coatoms [@Makinson1971] (see also [@Chagrov.Zakharyaschev1997]). Recently, Takahashi [@Takahashi2026] proved that the property of being a union-splitting of \(\mathsf{NExt}\mathsf{K}\) and strict Kripke completeness are decidable in \(\mathsf{NExt}\mathsf{K}\) (see also [@TakahashiThesis]).

If \(P\) is decidable in \(\mathsf{NExt}L\), then it is also decidable in \(\mathsf{NExt}L'\) for any extension \(L'\) of \(L\) with finitely many axioms (Proposition [prop:finite-extension]). On the other hand, a property that is undecidable in a given lattice \(\mathcal{C}\) of logics may become decidable in a sublattice of \(\mathcal{C}\). For example, in the lattice \(\mathsf{NExt}\mathsf{K4}\) of transitive modal logics (recall that \(\mathsf{K4} = \mathsf{K} \oplus \Box p \to \Box \Box p\)), a sublattice of \(\mathsf{NExt}\mathsf{K}\), every tabular logic has only finitely many immediate predecessors and all of them are tabular [@Blok1980], so the coincidence with a fixed tabular logic is decidable in this setting [@Jankov1968b; @Rautenberg1979a] (see also [@Chagrov.Zakharyaschev1997]). Moreover, as far as we know, the decidability of tabularity in \(\mathsf{NExt}\mathsf{K4}\) is still open [@rautenbergWillemBlokModal2006], whereas it is undecidable in \(\mathsf{NExt}\mathsf{K}\) as mentioned above.

In this paper, we study the decision problem for properties for tense logics. Tense logics are normal bimodal logics extending the logic \(\mathsf{K}_t = \mathsf{K}_2 \oplus {\{ p \to \Box\blacklozenge p, p \to \blacksquare\Diamond p \}}\), where, following convention, we denote the two modalities \(\Box\) and \(\blacksquare\) with their duals \(\Diamond\) and \(\blacklozenge\). The intended meaning of \(\Box\) and \(\blacksquare\) are “always true in the future” and “always true in the past”, respectively. The least tense logic \(\mathsf{K}_t\) was introduced in the 1960s by Prior [@Prior1967; @Prior1968]. Philosophically, tense logics can be viewed as logics of time; for example, \(\mathsf{K4}_t = \mathsf{K}_t \oplus \Diamond\Diamond p \to \Diamond p\) is the logic of transitive time flows, and \(\mathsf{Lin}_t = \mathsf{K4}_t \oplus (\Diamond\blacklozenge p \vee \blacklozenge\Diamond p \to p \vee \Diamond p \vee \blacklozenge p)\) is the logic of linear time flows (see also [@Wolter.Zakharyaschev2007]). Algebraically, the modalities \(\Box\) and \(\blacklozenge\) are adjoint, in the sense that \(\blacklozenge\varphi\to \psi \in L\) if and only if \(\varphi\to \Box\psi \in L\) for any tense logic \(L\). Thus, tense logics may also be viewed as “logics of adjointness,” and they serve as examples of bimodal logics in which two modalities interact in a natural way.

The bimodal logics \(\mathsf{K}_2 \subseteq\mathsf{K}_t \subseteq\mathsf{K4}_t \subseteq\mathsf{Lin}_t\) form a chain in \(\mathsf{NExt}\mathsf{K}_2\). Many properties, including Kripke completeness, the FMP, decidability, and even consistency, are undecidable in \(\mathsf{NExt}\mathsf{K}_n\) for \(n \geq 2\) [@Thomason1982]. On the other hand, the aforementioned properties are all decidable in \(\mathsf{NExt}\mathsf{Lin}_t\) [@Wolter1996a; @Wolter1997]. These results indicate that the interactions of modalities significantly affect the decidability of properties, which naturally raises the question of whether these properties are decidable in \(\mathsf{NExt}\mathsf{K}_t\) or \(\mathsf{NExt}\mathsf{K4}_t\). Chagrov and Shehtman [@Chagrov.Shehtman1995] proved that tabularity, the coincidence with a fixed tabular tense logic, and consistency are undecidable in \(\mathsf{NExt}\mathsf{K4}_t\) (and thus also undecidable in \(\mathsf{NExt}\mathsf{K}_t\)), while the decidability of other properties, such as Kripke completeness, the FMP, and decidability, remained open.

Although \(\mathsf{K}_t\) and \(\mathsf{K4}_t\) are the minimal tense extensions of \(\mathsf{K}\) and \(\mathsf{K4}\) respectively, the undecidability of properties in \(\mathsf{NExt}\mathsf{K}_t\) and \(\mathsf{NExt}\mathsf{K4}_t\) does not follow directly from the undecidability results for \(\mathsf{NExt}\mathsf{K4}\) and \(\mathsf{NExt}\mathsf{K}\). The minimal tense extension map \((\cdot)_t: \mathsf{NExt}\mathsf{K} \to \mathsf{NExt}\mathsf{K}_t\) is not injective [@Wolter1993], while it remains unknown whether \((\cdot)_t{\upharpoonright}\mathsf{NExt}\mathsf{K4}\) is injective [@Wolter1997a]. Moreover, Wolter [@Wolter1996] presented a modal logic \(L \in \mathsf{NExt}\mathsf{K4}\) having the FMP whose minimal tense extension \(L_t \in \mathsf{NExt}\mathsf{K4}_t\) is Kripke incomplete. It follows that the map \((\cdot)_t\) preserves neither Kripke completeness nor the FMP, while it remains open whether decidability is preserved (see [@Wolter1997a]). The interactions between tense modalities make lattices of tense logics completely different from those of unimodal logics (see [@Kracht1992; @Ma.Chen2021; @Ma.Chen2023; @Chen.Ma2024]).

In this paper, we provide a general criterion (Theorem 2) for a property to be undecidable in \(\mathsf{NExt}\mathsf{K4}_t\). Most properties studied for logics fall into this criterion, including Kripke completeness, the FMP, and decidability; see Corollary 1 for a more comprehensive list of undecidable properties in \(\mathsf{NExt}\mathsf{K4}_t\) following from the theorem. It follows that these properties are also undecidable in \(\mathsf{NExt}\mathsf{K}_t\).

Our proof adapts the method of [@Chagrov.Shehtman1995], reducing an undecidable problem regarding Minsky machines to the decision problem for a property. Minsky machines, also called counter machines or register machines, are a type of mathematical model of computation as strong as Turing machines [@minskyComputationFiniteInfinite1967]. There exist a Minsky machine \(\mathsf{M}\) and a configuration \(c_0\) of \(\mathsf{M}\) such that it is undecidable whether a given configuration of \(\mathsf{M}\) is reachable from \(c_0\) by computation of \(\mathsf{M}\) (see, e.g., [@Chagrov.Zakharyaschev1997]). Let us call this undecidable problem \(Q\). Given a property \(P\), we will find a logic \(L \in \mathsf{NExt}\mathsf{K4}_t\) that has \(P\) and construct a computable reduction from \(Q\) to the decision problem for \(P\) as follows. For a configuration \(c\), the reduction produces a logic \(L(c) \in \mathsf{NExt}\mathsf{K4}_t\) such that:

1. if \(c\) is reachable from \(c_0\), then \(L(c) = L\), which implies that \(L(c)\) has \(P\);

2. if \(c\) is not reachable from \(c_0\), then \(L(c)\) does not have \(P\).

Thus, if we could decide whether a logic in \(\mathsf{NExt}\mathsf{K4}_t\) has \(P\), we would be able to decide the problem \(Q\): Given a configuration \(c\), we compute the logic \(L(c)\) and ask if it has the property \(P\), the answer of which is also the answer to \(Q\). Since \(Q\) is undecidable, it follows that \(P\) is undecidable.

Table 1 summarizes the results on the decidability of some major properties discussed so far. The entries marked with are results established in this paper.

This paper is organized as follows. Section 2 introduces preliminaries on tense logics and Minsky machines. In section 3, we prove the main theorem and apply it to show the undecidability of logics’ properties. Finally, Section 4 concludes the paper with an overview of future work.

2 Preliminaries↩︎

2.1 Preliminaries of modal and tense logic↩︎

Recall that for each \(n \in \mathbb{Z}^+\), the \(n\)-modal language \(\mathscr{L}_n\) is obtained by adding the modalities \(\Box_0, \cdots, \Box_{n-1}\) to the propositional language. A normal \(n\)-modal logic is a set of \(\mathscr{L}_n\)-formulas which contains all classical tautologies, K-axioms \(\Box_i(p \to q) \to (\Box_i p \to \Box_i q) \in L\) for all \(i < n\), and is closed under the rules Modus Ponens (\(\varphi,\varphi\to \psi/\psi\)), Substitution (\(\varphi(p_1,\cdots,p_n)/\varphi(\psi_1,\cdots,\psi_n)\)) and Necessitation (\(\varphi/\Box_i\varphi\)). Let \(\mathsf{K}_n\) denote the minimal normal \(n\)-modal logic. We refer to \(2\)-modal logics as bimodal logics. A tense logic is a normal bimodal logic containing the axioms \(p \to \Box_0\Diamond_1 p\) and \(p \to \Box_1\Diamond_0 p\). For tense logics, we write \(\mathscr{L}_t\) for the formal language, \(\Box\) for \(\Box_0\) and \(\blacksquare\) for \(\Box_1\). Let \(\mathsf{K}_t\) denote the minimal tense logic. For each tense logic \(L\), let \(\mathsf{NExt}L\) denote the lattice of all normal extensions of \(L\). For every tense logic \(L\) and set of formulas \(\Sigma\), let \(L\oplus\Sigma\) denote the smallest tense logic containing \(L\cup\Sigma\). We write \(L \oplus \varphi\) for \(L \oplus {\{ \varphi \}}\). A tense logic \(L\) is finitely axiomatizable if \(L = \mathsf{K}_t \oplus \varphi\) for some \(\varphi\in \mathscr{L}_t\). A tense logic \(L\) is consistent if \(\bot\not\in L\), and so the only inconsistent tense logic is \(\mathscr{L}_t\).

A general frame is a triple \(\mathbb{F}=(X,R,A)\) where \(X\) is a non-empty set, \(R\) a binary relation on \(X\) and \(A\) a subset of \({\mathcal{P}(X)}\) such that (i) \(\varnothing\in A\), and (ii) \(A\) is closed under Boolean operations on \({\mathcal{P}(X)}\), \(R[\cdot]\) and \({{R}^{-1}}[\cdot]\), where \(R[Y] \mathrel{\vcenter{:}}= {\{ x \in X: \exists{y\in Y}(Ryx) \}}\) and \({{R}^{-1}}[Y] \mathrel{\vcenter{:}}= {\{ x \in X: \exists{y\in Y}(Rxy) \}}\) for all \(Y \subseteq X\). A Kripke frame \(\mathfrak{F}\) is a general frame of the form \((X,R,{\mathcal{P}(X)})\) and we simply write \((X,R)\). Let \(\mathsf{GFr}\), \(\mathsf{Fr}\), and \(\mathsf{Fin}\) denote the classes of all general frames, Kripke frames, and finite Kripke frames, respectively.

A model is a pair \(\mathfrak{M}=(\mathbb{F},V)\) where \(\mathbb{F}\in\mathsf{GFr}\) and \(V: \mathsf{Prop}\to A\) a valuation in \(\mathbb{F}\). \(V\) is extended to \(V:\mathscr{L}_t\to A\) as usual: \(V(\blacklozenge\varphi) = R[V(\varphi)]\) and \(V(\Box\varphi) \mathrel{\vcenter{:}}= X \setminus {{R}^{-1}}[X\setminus V(\varphi)]\). The expressions \(\mathfrak{M},x \models\varphi\), \(\mathbb{F},x \models\varphi\), \(\mathbb{F}\models\varphi\) and \(\mathbb{F}\models\Sigma\) are defined as usual. Note that \(\mathfrak{M},x \models\blacklozenge\varphi\) if and only if \(\mathfrak{M},y \models\varphi\) for some \(y \in {{R}^{-1}}[x]\). For all sets \(\Sigma\subseteq\mathscr{L}_t\) of formulas and classes \(\mathcal{K}\subseteq\mathsf{GFr}\) of general frames, let

For example, given a tense logic \(L\), we write \(\mathsf{Fin}(L)\) for the class of all finite frames validating \(L\). We call \(\mathsf{Log}(\mathcal{K})\) the tense logic of \(\mathcal{K}\). Recall that a Kripke frame \((X,R)\) is called transitive if \(R\) is transitive. Then \(\mathsf{K4}_t \mathrel{\vcenter{:}}= \mathsf{K}_t \oplus \Diamond\Diamond p \to \Diamond p\) is the tense logic of transitive frames. In other words, we have \(\mathsf{K4}_t = \mathsf{Log}({\{ \mathfrak{F}\in \mathsf{Fr}: \mathfrak{F}\text{ is transitive} \}})\). A tense logic \(L\) is transitive if \(L\) extends \(\mathsf{K4}_t\), i.e., \(L \supseteq \mathsf{K4}_t\).

Let us recall some properties of tense logics. Let \(L\) be a tense logic. Then (i) \(L\) is Kripke complete, if \(L = \mathsf{Log}(\mathsf{Fr}(L))\); (ii) \(L\) has the finite model property (FMP), if \(L = \mathsf{Log}(\mathsf{Fin}(L))\); (iii) \(L\) is tabular, if \(L = \mathsf{Log}(\mathfrak{F})\) for some finite frame \(\mathfrak{F}\); (iv) \(L\) is canonical, if \(L=\mathsf{Log}(\mathfrak{F}^L)\), where \(\mathfrak{F}^L\) is the canonical frame for \(L\); (v) \(L\) is first-order definable, if \(L = \mathsf{Log}(\mathcal{K})\), where \(\mathcal{K}\) is a class of Kripke frames defined by a set of first-order sentences. Moreover, we say that \(L\) is locally tabular if for each \(n \in \omega\), \(L\) contains only finitely many non-\(L\)-equivalent formulas built up from the propositional variables \(p_{0}, \cdots, p_{n-1}\). Finally, we say that \(L\) is decidable if there is an algorithm that, given a formula \(\varphi\), decides whether \(\varphi\in L\). This membership decidability is a property for logics, and should not be confused with decidability of logics’ properties; in particular, it is legitimate to say decidability, as a property, is decidable or not.

2.2 Decision problem for logics’ properties↩︎

In this section, instead of the decidability of logics, we focus on the decidability of logics’ properties. We refer to [@Chagrov.Zakharyaschev1997] and [@Wolter.Zakharyaschev2007] for a detailed introduction and survey of the decision problem for properties of modal logics. We will work in the tense (or more generally, bimodal) setting. We identify a property \(P\) in the lattice \(\mathsf{NExt}(L_0)\) with the set of logics in \(\mathsf{NExt}(L_0)\) that satisfy \(P\), that is, \(P = \{L \in \mathsf{NExt}(L_0): L \text{ satisfies } P\}\).

Following convention, we restrict ourselves to finitely axiomatizable logics because an input for an algorithm must be a finite object. We do not consider all recursively axiomatizable logics, as Kuznetsov showed that otherwise the only decidable properties would be the trivial ones (see [@Chagrov.Zakharyaschev1997]). Since most logics we encounter in practice are finitely axiomatizable, this is not a serious drawback. A finitely axiomatizable logic will be encoded by a finite set of formulas axiomatizing the logic, or equivalently, a single formula axiomatizing the logic.

Note that determining a property in a larger lattice of logics is at least as hard as in a smaller one, in the following sense.

Minsky machines↩︎

The most commonly used method for proving the undecidability of a decision problem is to construct a computable reduction from another problem that is already known to be undecidable to the problem. In this paper, we will use an undecidable problem about Minsky machines. We recall the basics of Minsky machines in the rest of this section and refer to [@Chagrov.Zakharyaschev1997] and [@minskyComputationFiniteInfinite1967] for more details; see also [@Chagrov.Zakharyaschev1997] for various applications of Minsky machines to obtain undecidability results.

A Minsky machine with two registers (also called a counter/register machine with two counters/registers) is a finite set of instructions acting on two registers. We will only use Minsky machines with two registers, so we simply call them Minsky machines. A Minsky machine has finitely many states. A register can store a natural number and is assumed to be unbounded. So, a situation of a Minsky machine is represented by a tuple \({\langle s, n, m \rangle}\), called a configuration, where \(s\) is the current state and \(n\) and \(m\) are the natural numbers on each register. An instruction operates on the state and one of the two registers: it increments the number in the register, or tests if the number in the register is zero and decrements it if not. More specifically, an instruction \(I\) has one of the following four forms:

• \(I = t \to {\langle t', 1, 0 \rangle}\) means that \(I\) turns the state \(t\) into \(t'\) and increment the first register,

• \(I = t \to {\langle t', 0, 1 \rangle}\) means that \(I\) turns the state \(t\) into \(t'\) and increment the second register,

• \(I = t \to {\langle t', -1, 0 \rangle} ({\langle t'', 0, 0 \rangle})\) means that \(I\) turns the state \(t\) into \(t'\) and decrements the first register if the number in the first register is non-zero, and turns the state \(t\) into \(t''\) otherwise,

• \(I = t \to {\langle t',0, -1 \rangle} ({\langle t'', 0, 0 \rangle})\) means that \(I\) turns the state \(t\) into \(t'\) and decrements the second register if the number in the second register is non-zero, and turns the state \(t\) into \(t''\) otherwise.

For example, applying the instruction \(I = s \to {\langle s', -1, 0 \rangle} ({\langle s'', 0, 0 \rangle})\) to the configuration \({\langle s, n, m \rangle}\), we obtain the configuration \({\langle s', n-1, m \rangle}\) if \(n \geq 1\) and the configuration \({\langle s'', n, m \rangle}\) if \(n = 0\).

In this paper, Minsky machines are assumed to be deterministic, that is, for each state \(t\) there is at most one instruction that acts on the state \(t\). For a Minsky machine \(\mathsf{M}\), we write \(\mathsf{M}: {\langle s,n,m \rangle} \rightsquigarrow {\langle t,k,l \rangle}\) if, starting from the configuration \({\langle s,n,m \rangle}\), by applying the instructions in \(\mathsf{M}\), we can reach the configuration \({\langle t,k,l \rangle}\) in finitely many (possibly 0) steps. We drop \(\mathsf{M}\) if it is clear from the context.

We will use the following undecidable problem, which is called the second configuration problem in [@Chagrov.Zakharyaschev1997].

3 Undecidable properties in \(\mathsf{NExt}\mathsf{K4}_t\)↩︎

The aim of this section is to prove the general undecidability result Theorem 2, which implies the undecidability of various properties summarized in Corollary 1. The proof idea follows Chagrov’s method of using Minsky machines [@chagrov1990I; @chagrov1990II; @Chagrov.Shehtman1995] (see also [@Wolter.Zakharyaschev2007]). Let \(\mathsf{M}\) be a Minsky machine and \({\langle s,n,m \rangle}\) be a configuration of \(\mathsf{M}\) such that the set \({\{ {\langle t,k,l \rangle}: \mathsf{M}: {\langle s,n,m \rangle}\rightsquigarrow{\langle t,k,l \rangle} \}}\) is undecidable, given by Theorem 1. Since the Minsky machine \(\mathsf{M}\) is finite, we may assume that \(\mathsf{M}\) contains \(t_0\) many states, labeled as \(0, \dots, t_0-1\). To state our main theorem, we introduce the following general frame that encodes the problem \({\{ {\langle t,k,l \rangle}:{\langle s,n,m \rangle}\rightsquigarrow{\langle t,k,l \rangle} \}}\).

It is clear that \(A\) is closed under \(\cap\), \(W\setminus(\cdot)\), \(R[\cdot]\) and \({{R}^{-1}}[\cdot]\), so \(\mathbb{F}\) is well-defined as a general frame. The underlying Kripke frame \((W,R)\) of \(\mathbb{F}\) is depicted in Figure 1.

Before studying properties of the general frame \(\mathbb{F}\), let us introduce a set of new modal operators \({\Delta^{\leq n}}\) and their duals \({\nabla^{\leq n}}\), which will play an important role in our proofs.

For each Kripke frame \(\mathfrak{F}= (X,R)\), let \({R}_\sharp\) be the binary relation \((= \cup R \cup {{R}^{-1}})\) on \(X\), that is,

It follows that for all \(x,y \in X\), if \(y \in {R}_\sharp^{n}[x]\), then there exists a sequence \(C = {\langle x_i : i \leq k \rangle}\) with \(k < n\) such that (i) \(x = x_0\), (ii) \(y = x_k\), and (iii) \(x_{i+1} \in {R}_\sharp[x_{i}]\) for all \(i < k\). We call \(C\) a \(k\)-path from \(x\) to \(y\).

Now we state the main theorem. Let \[\mathsf{KC} = {\{ L \in \mathsf{NExt}\mathsf{K4}_t : L \text{ is Kripke complete} \}}\] and \[\mathsf{DEC} = {\{ L \in \mathsf{NExt}\mathsf{K4}_t : L \text{ is decidable} \}}.\]

The rest of this section is dedicated to proving this theorem. We start by introducing formulas that define a point or a set of points in \(\mathbb{F}\). Their meaning is summarized in Lemma 2. For each \(n\in\omega\), we define the formulas \(\varphi_{c_{n}}\), \(\varphi_{a_{n}}\) and \(\varphi_{b_{n}}\) as follows:

• \(\varphi_{c_{0}}\mathrel{\vcenter{:}}=\Box\bot\land\blacksquare\blacklozenge\top\) and \(\varphi_{c_{k}}\mathrel{\vcenter{:}}=\Diamond^k\varphi_{c_{0}}\wedge\neg\Diamond^{k+1}\varphi_{c_{0}}\);

• \(\varphi_{a_{0}}\mathrel{\vcenter{:}}=\Box\bot\wedge\blacklozenge(\blacksquare\bot\wedge\Box\blacklozenge^2\top)\) and \(\varphi_{a_{k}}\mathrel{\vcenter{:}}=(\varphi_{a_{0}} \lor \Diamond\varphi_{a_{0}}) \land \Box\neg\varphi_{c_{0}}\land\blacklozenge\top \land \Diamond^k\varphi_{a_{0}}\wedge\neg\Diamond^{k+1}\varphi_{a_{0}}\);

• \(\varphi_{b_{0}}\mathrel{\vcenter{:}}=\Box\bot\wedge\blacklozenge\blacklozenge\top\land\blacklozenge\Diamond\blacksquare^2\bot\) and \(\varphi_{b_{k}}\mathrel{\vcenter{:}}=(\varphi_{b_{0}} \lor \Diamond\varphi_{b_{0}}) \land \Box\neg\varphi_{c_{0}} \land\blacklozenge\top \land \Diamond^k\varphi_{b_{0}}\wedge\neg\Diamond^{k+1}\varphi_{b_{0}}\).

Note that these formulas are all variable-free. Intuitively, for each \(x \in {\{ a,b,c \}}\) and \(n \in \omega\), the formula \(\varphi_{x_n}\) is designed to be true at exactly \(x_n\) in \(\mathbb{F}\), regardless of valuations. Moreover, we define

• \(\varphi_{A} \mathrel{\vcenter{:}}= (\varphi_{a_{0}} \lor \Diamond\varphi_{a_{0}}) \land \Box\neg\varphi_{c_{0}} \land \blacklozenge\top\);

• \(\varphi_{B} \mathrel{\vcenter{:}}= (\varphi_{b_{0}} \lor \Diamond\varphi_{b_{0}}) \land \Box\neg\varphi_{c_{0}}\land\blacklozenge\top\).

Similarly, \(\varphi_{A}\) and \(\varphi_{B}\) are true exactly at \({\{ a_n: n \in \omega \}}\) and \({\{ b_n: n \in \omega \}}\) in \(\mathbb{F}\), respectively. To simulate the action of \(+1\) and \(-1\) on the two tapes of \(\mathsf{M}\), we define the following formulas:

• \(\psi_{A} \mathrel{\vcenter{:}}= \varphi_{A} \land p_A \land \lnot \Diamond p_A\);

• \(\psi^+_{A} \mathrel{\vcenter{:}}= \varphi_{A} \land \Diamond p_A \land \lnot\Diamond\Diamond p_A\);

• \(\psi_B \mathrel{\vcenter{:}}= \varphi_{B} \land p_B \land \lnot\Diamond p_B\);

• \(\psi^+_B \mathrel{\vcenter{:}}= \varphi_{B} \land \Diamond p_B \land \lnot\Diamond\Diamond p_B\),

where \(p_A,p_B\) are fresh variables. Intuitively, if \(\psi_A\) is true at some point, then the point must be \(a_i\), where \(i = \min\{j: a_j \models p_A\}\); then \(\psi^+_A\) is true at the next point, namely, \(a_{i+1}\). A similar intuition applies to \(\psi_B\) and \(\psi^+_B\) as well. Moreover, a key syntactic observation is: if \(s\) is the substitution \([\Diamond^k \varphi_{a_{0}} / p_A, \Diamond^l \varphi_{b_{0}} / p_B]\) for some \(k, l \in \omega\), then \(s(\psi_{A}) = \varphi_{a_{k}}\), \(s(\psi^+_{A}) = \varphi_{a_{k+1}}\), \(s(\psi_B) = \varphi_{b_{l}}\), and \(s(\psi^+_B) = \varphi_{b_{l+1}}\). This will be used in Lemma 3.

Finally, for each state \(t\) of \(\mathsf{M}\) and formulas \(\pi,\kappa\in\mathscr{L}_t\), we define: \[\sigma(t,\pi,\kappa) \mathrel{\vcenter{:}}= \Diamond\varphi_{c_{t}} \wedge \Box\neg\varphi_{c_{t+1}} \wedge \Diamond\pi \wedge \Box\lnot(\Diamond\pi \land \Box\lnot\varphi_{c_{0}}) \wedge \Diamond\kappa \wedge \Box\lnot(\Diamond\kappa \land \Box\lnot\varphi_{c_{0}}).\] As we will see in Lemma 2, the formula \(\sigma(t,\pi,\kappa)\) is true exactly at the point \({\langle t,k,l \rangle}\) if the formulas \(\pi\) and \(\kappa\) are true exactly at \(a_k\) and \(b_l\), respectively.

Next, we encode the behavior of the Minsky machine \(\mathsf{M}\) by formulas. With each instruction \(I\) in \(\mathsf{M}\), we associate a formula \(AxI\) as follows.

• \(AxI\mathrel{\vcenter{:}}= \neg\alpha \wedge {\Delta^{\leq 5}}\sigma(t,\psi_{A},\psi_B) \to \neg\alpha \wedge {\Delta^{\leq 5}}\sigma(t',\psi^+_{A},\psi_B)\), if \(I=t\to{\langle t',1,0 \rangle}\).

• \(AxI\mathrel{\vcenter{:}}= \neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t,\psi_{A},\psi_B)\to\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t',\psi_{A},\psi^+_B)\), if \(I=t\to{\langle t',0,1 \rangle}\).

• \(AxI\mathrel{\vcenter{:}}= [\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t,\psi^+_{A},\psi_B)\to\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t',\psi_{A},\psi_B)]\)
  \(\land [\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t,\varphi_{a_{0}},\psi_B)\to\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t'',\varphi_{a_{0}},\psi_B)]\), if \(I=t\to{\langle t',-1,0 \rangle} ({\langle t'',0,0 \rangle})\).

• \(AxI\mathrel{\vcenter{:}}= [\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t,\psi_{A},\psi^+_B)\to\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t',\psi_{A},\psi_B)]\)
  \(\land [\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t,\psi_{A},\varphi_{b_{0}})\to\neg\alpha\wedge{\Delta^{\leq 5}}\sigma(t'',\psi_{A},\varphi_{b_{0}})]\), if \(I=t\to{\langle t',0,-1 \rangle} ({\langle t'',0,0 \rangle})\).

Each formula encodes the behavior of the corresponding instruction. Let \(AxM\mathrel{\vcenter{:}}=\bigwedge_{I \in M} AxI\). This is a well-defined formula since there are only finitely many instructions in \(\mathsf{M}\).

Now we construct the reduction, extending that in [@Chagrov.Shehtman1995]. For each configuration \({\langle t,k,l \rangle}\), we define the logic \[\begin{align} L(t,k,l) \mathrel{\vcenter{:}}= \mathsf{K4}_t & \oplus AxM \oplus (\lnot\alpha\land{\Delta^{\leq 5}}\sigma(s,\varphi_{a_{n}},\varphi_{b_{m}})\to\lnot\alpha\land{\Delta^{\leq 5}}\sigma(t,\varphi_{a_{k}},\varphi_{b_{l}}))\to\alpha\\ & \oplus (\neg\alpha\to{\nabla^{\leq 5}}(\varphi_{c_{t_0}}\to\varphi_0)\wedge{\Delta^{\leq 5}}\varphi_{c_{t_0}}) \end{align}\] where

and \(p\) and \(q\) are fresh variables w.r.t. \(AxM\) and \(\alpha\). Note that the axioms of \(L(t,k,l)\) are computable from a configuration \({\langle t,k,l \rangle}\). The subsequent lemmas show some properties of \(L(t,k,l)\). Intuitively, the formula \(\varphi_0\) is designed to be such that any extension of \(\mathsf{K4}_t\oplus\varphi_0\) is Kripke incomplete. More precisely, we have

On the other hand, the following lemma holds:

The following two lemmas summarize how the reduction works.

Now we are ready to prove the main theorem.

As a corollary of Theorem 2, we obtain the following undecidable properties in \(\mathsf{NExt}\mathsf{K4}_t\).

4 Conclusion↩︎

The main motivation behind this paper is to understand how interactions of modalities affect the decidability of logics’ properties. We have shown that most properties, as listed in Corollary 1, are undecidable in the lattice \(\mathsf{NExt}\mathsf{K4}_t\). These results, together with the known ones (see Table 1), suggest that the interactions of modalities only make the decision problem for properties harder. We would conjecture that, for a property \(P\) such as Kripke completeness, the finite model property, or decidability, if \(P\) is undecidable in \(\mathsf{NExt}L\) for a unimodal logic \(L\), then it is also undecidable in \(\mathsf{NExt}L_t\). Note that this does not follow directly from the minimal tense extension map \((\cdot)_t: \mathsf{NExt}\mathsf{K} \to \mathsf{NExt}\mathsf{K}_t\), as the map may not preserve or reflect these properties, as discussed in the introduction.

Moreover, another observation from Table 1 is that a stronger base logic tends to make a property decidable. The undecidability results for \(\mathsf{NExt}\mathsf{K4}_t\) indicate that \(\mathsf{K4}_t\) is not strong enough in this sense. We leave it for future research to analyze the decidability of logics’ properties in the lattice of extensions of other, stronger or incomparable bimodal logics. For example, the tense logic \(\mathsf{S4}_t\) of pre-orders, \(\mathsf{Grz}_t\) of posets and the product logic \(\mathsf{S5}\times\mathsf{S5}\) would be natural choices.

Acknowledgment↩︎

The authors would like to thank Nick Bezhanishvili for his valuable comments on the draft of this paper. The authors are also grateful for the anonymous reviewers’ comments, which significantly improved the presentation of the paper. The first author is supported by Tsinghua University’s Initiative for Advancing First-Class and World-Leading Disciplines in the Humanities and Social Sciences. The second author was supported by the Student Exchange Support Program (Graduate Scholarship for Degree Seeking Students) of the Japan Student Services Organization.

---

1. This should not be confused with the decidability of logics; a logic is decidable if its membership problem is decidable.↩︎

2. We have to restrict to finitely axiomatizable logics because an input of an algorithm must be a finite object; see Subsection 2.2 and [@Chagrov.Zakharyaschev1997] for more discussions.↩︎