TABULARITY AND POST-COMPLETENESS IN TENSE LOGIC

Abstract

A new characterization of tabularity in tense logic is established, namely, a tense logic L is tabular if and only if $\mathsf {tab}_n^T\in L$ for some $n\geq 1$. Two characterization theorems for the Post-completeness in tabular tense logics are given. Furthermore, a characterization of the Post-completeness in the lattice of all tense logics is established. Post numbers of some tense logics are shown.

1 Introduction

Tabularity and Post-completeness in modal logic has been explored for a long time in the literature. Let us recall some notions and results from [4, 8]. We consider the monomodal language $\mathscr {L}_\Box $ in which $\Diamond $ is defined as the dual of $\Box $ . From the semantic perspective, every class $\mathscr {C}$ of relational structures has its modal theory $Th(\mathscr {C})$ which consists of modal formulas true or valid in $\mathscr {C}$ . Let $\mathsf {K}$ be the modal theory of the class of all frames. A quasi-normal modal logic is a set of modal formulas S containing $\mathsf {K}$ and closed under modus ponens and uniform substitution. A quasi-normal modal logic is normal if it is closed under the rule of necessitation. Let $\mathsf {Ext}(S)$ and $\mathsf {NExt}(S)$ denote lattices of all quasi-normal and normal extensions of S respectively.

A modal logic S is tabular if $S=Th(\mathfrak {F})$ for some finite frame $\mathfrak {F}$ . It is well-known that the tabularity in quasi-normal modal logics can be characterized by peculiar modal formulas (cf., e.g., [4, p. 417]). A quasi-normal modal logic $S\in \mathsf {Ext}(\mathsf {K})$ is tabular if and only if $\mathsf {tab}_n\in S$ for some natural number $n\in \omega $ , where $\mathsf {tab}_n=\psi _n\wedge \chi _n$ is the formula defined as follows:

$$ \begin{align*} \psi_n &= \neg(\varphi_1\wedge\Diamond(\varphi_2\wedge\Diamond(\varphi_2\wedge\cdots\wedge\Diamond\varphi_n)\ldots)),\\[6pt] \chi_n &= \bigwedge_{m<n}\neg\Diamond^m(\Diamond\varphi_1\wedge\cdots\wedge\Diamond\varphi_n),\\[6pt] \varphi_i &= p_1\wedge\cdots \wedge p_{i-1}\wedge\neg p_i\wedge p_{i+1}\wedge\cdots\wedge p_n~\text{for}\ 1\leq i\leq n. \end{align*} $$

As a corollary, a normal modal logic $S\in \mathsf {NExt}(\mathsf {K})$ is tabular if and only if $\mathsf {alt}_n\wedge \mathsf {tra}_n\in S$ for some $n\in \omega $ , where $\mathsf {alt}_n\wedge \mathsf {tra}_n$ is the formula defined as follows:

$$ \begin{align*} \mathsf{alt}_n &= \Box p_0\vee\Box(p_0\to p_1)\vee\cdots\vee\Box(p_0\wedge\cdots\wedge p_{n-1}\to p_{n}),\\ \mathsf{tra}_n &= \bigwedge_{i\leq n}\Box^i p\to \Box^{n+1}p. \end{align*} $$

Every tabular modal logic has finitely many extensions and all of them are tabular, and all tabular modal logics are finitely axiomatizable (cf., e.g., [4, 24, 25]).

A consistent modal logic S is Post-complete if there exists no consistent proper extension of S. This property in lattices of quasi-normal modal logics is quite complicated (cf., e.g., [4, 5, 11, 14, 15]). There are $2^{\aleph _0}$ Post-complete logics in $\mathsf {Ext}(\mathsf {K4})$ (cf. [4, Theorem 13.15]). However, there are exactly two Post-complete logics in $\mathsf {NExt}(\mathsf {K})$ (cf. [4, 8, 10]). Post-completeness is also related to tabularity. A consistent logic in $\mathsf {Ext}(\mathsf {K})$ is anti-tabular if it has no finite models. A logic $S\in \mathsf {Ext}(\mathsf {K})$ is anti-tabular if and only if all Post-complete extensions of S are not tabular. If $S\in \mathsf {Ext}(\mathsf {K4})$ has infinitely many Post-complete extensions, it has an anti-tabular extension (cf. [4, Theorem 13.22]).

The present work is going to study tabularity and Post-completeness in tense logics. The tense language extends the modal language with a past modality $\blacklozenge $ such that $(\blacklozenge , \Box )$ forms an adjoint pair. Dually we get the adjoint pair of operators $(\Diamond ,\blacksquare )$ . Let $\mathscr {L}_\Box $ and $\mathscr {L}_t$ be the sets of all modal and tense formulas respectively. The least tense logic is denoted by $\mathsf {K}_t$ . Let $\Lambda (L)$ be the lattice of extensions of a tense logic L (cf. Definition 2.5). Normal modal and tense logics are correlated. Given a normal modal logic S and tense logic L, let $S^+$ be the smallest tense logic containing S, and $L_+$ be the normal modal logic $L\cap \mathscr {L}_\Box $ . We say that $S^+$ is the minimal tense extension of S and $L_+$ the modal restriction of L. This gives maps $(.)^+ : \mathsf {NExt}(\mathsf {K})\to \Lambda (\mathsf {K}_t)$ and $(.)_+ : \Lambda (\mathsf {K}_t) \to \mathsf {NExt}(\mathsf {K})$ . If S is Kripke-complete, then $(S^+)_+= S$ . However, the map $((.)^+)_+$ is in general not injective, namely, there exists $S\in \mathsf {NExt}(\mathsf {K})$ with $(S^+)_+\neq S$ (cf. [17, p. 84]).

There are many results on lattices of tense logics in the literature. A tense logic L has codimension n with $n\in \omega $ , if there exists a chain $L=L_0\subset L_1\subset \cdots \subset L_n=\mathscr {L}_t$ which cannot be refined (cf. [8, 13]). Post-complete tense logics are exactly those of codimension $1$ . Thomason [16] gives a Kripke-incomplete tense logic of codimension $1$ . Rautenburg [13] gives a characterization of Post-completeness in the set of all tabular tense logics and describes the splittings of $\Lambda (\mathsf {K}_t)$ . Kracht [7] proves results on the splittings of lattices $\Lambda (\mathsf {K}_t)$ , $\Lambda (\mathsf {K4}^+)$ and $\Lambda (\mathsf {S4}^+)$ . As far as the notion of codimension concerned, Kracht [7] proves that for $n\geq 3$ there are infinitely many logics of codimension n in the lattice $\Lambda (\mathsf {Ga})$ (cf. [8, Section 7.9]). It is remarkable that many properties like completeness, finite model property, decidability and finitely axiomatizability are thoroughly investigated in a series of works by Wolter (cf. [17–23]).

A characterization of tabularity in $\Lambda (\mathsf {K}_t)$ has been given by Chagrov and Shehtman [3]. It says that a tense logic L is tabular if and only if $\alpha _n\wedge \beta _n\in L$ for some $n\in \omega $ . Details are found in Remark 3.10. We shall give a new criterion of tabularity in $\Lambda (\mathsf {K}_t)$ by defining formulas $\mathsf {tab}_n^T$ with $n\geq 1$ (Theorem 3.7). As far as the Post-completeness in $\Lambda (\mathsf {K}_t)$ is concerned, it is known that there are infinitely many Post-complete tense logics (cf., e.g., [9, 21]). In the present work, we give three characterization theorems for the Post-completeness in $\Lambda (\mathsf {K}_t)$ : (i) the first theorem gives three equivalent conditions for the Post-completeness of a tense logic $Th(\mathfrak F)$ where $\mathfrak F$ is a finite point-generated frame (Theorem 4.9), and Rautenburg’s characterization in [13] follows from this result; (ii) a tabular tense logic L is Post-complete if and only if L has only one point-generated frame up to isomorphism (Theorem 4.12); and (iii) a consistent tense logic L is Post-complete if and only if it satisfies two conditions on constant formulas (Theorem 5.3). Using these results, we give the Post numbers of some tense logics. It is worth mentioning that there exist $2^{\aleph _0}$ Post-complete extensions of a bimodal logic (cf. [6, 8]). Note that tense logics discussed in the present work are bimodal logics with adjointness between modal operators.

This paper is structured as follows. Section 2 gives some preliminaries on tense logic. Section 3 gives a new characterization of tabularity in $\Lambda (\mathsf {K}_t)$ . Section 4 proves two characterization theorems on the Post-completeness in the set of all tabular tense logics. Section 5 gives a characterization theorem for the Post-completeness in $\Lambda (\mathsf {K}_t)$ . Section 6 gives some concluding remarks.

2 Preliminaries

We recall some preliminaries on tense logic from [9]. The cardinality of a set X is denoted by $|X|$ . Boolean operations of union $\cup $ , intersection $\cap $ and complement $\overline {(.)}$ on the powerset $\mathcal {P}(X)$ shall be used. Let $\aleph _0$ be the least infinite cardinal number. The language of tense logic consists of a denumerable set of variables $\Phi =\{p_i: i\in \omega \}$ , connectives $\bot $ (falsum) and $\to $ (implication), and tense operators $\Diamond $ (the future) and $\blacklozenge $ (the past).

Definition 2.1. The set of all formulas $\mathscr {L}_t$ is defined inductively as follows:

$$ \begin{align*} \mathscr{L}_t\ni \varphi ::= p\mid \bot\mid (\varphi_1\to\varphi_2)\mid \Diamond\varphi\mid \blacklozenge\varphi, \end{align*} $$

where $p\in \Phi $ . Let $var(\varphi )$ be the set of all variables appearing in $\varphi $ . A formula $\varphi $ is constant, if $var(\varphi )=\varnothing $ . Let $\mathscr {L}_t^0$ be the set of all constant formulas.

We shall use abbreviations $\neg \varphi :=\varphi \to \bot $ (negation), $\top :=\neg \bot $ (true), $\varphi \wedge \psi := \neg (\varphi \to \neg \psi )$ (conjunction), $\varphi \vee \psi :=\neg \varphi \to \psi $ (disjunction) and $\varphi \leftrightarrow \psi :=(\varphi \to \psi )\wedge (\psi \to \varphi )$ (equivalence). Let $\Box \varphi :=\neg \Diamond \neg \varphi $ (future necessity) and $\blacksquare \varphi :=\neg \blacklozenge \neg \varphi $ (past necessity). For every finite set $\Gamma $ of formulas, let $\bigvee \Gamma $ be the conjunction of all formulas in $\Gamma $ . In particular, let $\bigvee \varnothing =\bot $ .

Note that $\mathscr {L}_t$ forms the formula algebra, and $\mathscr {L}_t^0$ forms the constant formula algebra. A substitution is a homomorphism $s:\mathscr {L}_t\to \mathscr {L}_t$ . Let $\varphi ^s$ be the formula obtained from $\varphi $ by the substitution s. A constant substitution is a homomorphism $s:\mathscr {L}_t\to \mathscr {L}_t^0$ . Let $\mathsf {CS}$ be the set of all constant substitutions.

Definition 2.2. A frame is a pair $\mathfrak {F} = ( {W,R} )$ where $W\neq \varnothing $ and $R\subseteq W\times W$ . The inverse of R is defined as $\breve {R}=\{(v,w): wRv\}$ . For every $w\in W$ , one defines

$$ \begin{align*} R(w)=\{u\in W: wRu\}\ \text{and}\ \breve{R}(w)=\{u\in W: uRw\}. \end{align*} $$

For every $X\subseteq W$ , let $R(X)=\bigcup _{w\in X}R(w)$ and $\breve {R}(X)=\bigcup _{w\in X}\breve {R}(w)$ . The unary operations $\Diamond _R$ and $\blacklozenge _R$ on $\mathcal {P}(W)$ are defined by setting

$$ \begin{align*} \Diamond_RX = \{w\in W: R(w)\cap X\neq\varnothing\}\ \text{and}\ \blacklozenge_RX = \{w\in W: \breve{R}(w)\cap X\neq\varnothing\}. \end{align*} $$

Let $\Box _RX=\overline {\Diamond _R\overline {X}}$ and $\blacksquare _RX=\overline {\blacklozenge _R\overline {X}}$ . The cardinality of a frame $\mathfrak {F} = ( {W,R} )$ is defined as the cardinality $|W|$ and denoted by $|\mathfrak {F}|$ . A frame $\mathfrak {F}$ is finite, if $|\mathfrak {F}|<\aleph _0$ .

A model is a triple $\mathfrak {M}=(W,R,V)$ where $(W,R)$ is a frame and $V:\Phi \rightarrow \mathcal {P}(W)$ is a function which is called a valuation in $(W,R)$ . A valuation V is extended to the set of all formulas $\mathscr {L}_t$ by the following rules:

$$ \begin{align*} V(\bot) &=\varnothing, & V(\varphi\to\psi) &= \overline{V(\varphi)}\cup V(\psi),\\ V(\Diamond\varphi) &= \Diamond_RV(\varphi), & V(\blacklozenge\varphi) &= \blacklozenge_RV(\varphi). \end{align*} $$

A formula $\varphi $ is true at $w$ in $\mathfrak {M}$ (notation: $\mathfrak {M},w\models \varphi $ ) if $w\in V(\varphi )$ .

A formula $\varphi $ is valid at $w$ in $\mathfrak {F}$ (notation: $\mathfrak {F},w\models \varphi $ ) if $w\in V(\varphi )$ for every valuation V in $\mathfrak {F}$ . A formula $\varphi $ is valid in $\mathfrak {F}$ , notation $\mathfrak {F}\models \varphi $ , if $\mathfrak {F},w\models \varphi $ for every $w\in W$ . A formula $\varphi $ is valid in a class $\mathcal {K}$ of frames, notation $\mathcal {K}\models \varphi $ , if $\mathfrak {F}\models \varphi $ for every $\mathfrak {F}\in \mathcal {K}$ . The theory of a class $\mathcal {K}$ of frames is defined as the set

$$ \begin{align*} Th(\mathcal{K})=\{\varphi: \mathcal{K}\models\varphi\}. \end{align*} $$

If $\mathcal {K}=\{\mathfrak {F}\}$ , we write $Th(\mathfrak {F})$ . A frame $\mathfrak F$ is called a frame for a set $\Gamma $ of formulas (notation: $\mathfrak {F}\models \Gamma $ ) if $\mathfrak {F}\models \varphi $ for all $\varphi \in \Gamma $ . Let $\mathsf {Fr}(\Gamma )=\{\mathfrak F: \mathfrak F\models \Gamma \}$ and $\mathsf {Fr}^{<\aleph _0}(\Gamma )=\{\mathfrak F: \mathfrak F\models \Gamma ~\&~|\mathfrak F|<\aleph _0\}$ . If $\Gamma =\{\varphi \}$ , we write $\mathsf {Fr}(\varphi )$ and $\mathsf {Fr}^{<\aleph _0}(\varphi )$ .

Definition 2.3. Let $\mathfrak {F}=(W,R)$ be a frame, $w\in W$ and $\varnothing \neq X\subseteq W$ . Let

$$ \begin{align*} R(X)=\bigcup_{w\in X}R(w)\ \text{and}\ \breve{R}(X)=\bigcup_{w\in X}\breve{R}(w). \end{align*} $$

For $k\geq 0$ , we define $S^k(\mathfrak {F},w)$ and $S^\omega (\mathfrak {F},w)$ as follows:

$$ \begin{align*} S_*^0(\mathfrak{F},w) &= \{w\}, & S_*^{k+1}(\mathfrak{F},w) &= R(S^k(\mathfrak{F},w))\cup \breve{R}(S^k(\mathfrak{F},w)),\\ S^k(\mathfrak{F},w) &= \bigcup_{m\leq k}S_*^m(\mathfrak{F},w), & S^\omega(\mathfrak{F},w) &= \bigcup_{k\geq 0}S^k(\mathfrak{F},w). \end{align*} $$

Let $S(\mathfrak {F},w) = S^1(\mathfrak {F},w)$ and $S^\omega (\mathfrak {F},X) =\bigcup _{w\in X}S^\omega (\mathfrak {F},w)$ . The subframe of $\mathfrak {F}$ induced by X is defined as $\mathfrak {F}{\upharpoonright }X =(X,R{\upharpoonright }X)$ where $R{\upharpoonright }X=R\cap (X\times X)$ . The subframe of $\mathfrak {F}$ generated by X is defined as $\mathfrak {F}{\upharpoonright }S^\omega (\mathfrak {F},X)$ . A frame $\mathfrak {G}$ is a generated subframe of $\mathfrak {F}=(W,R)$ , if $\mathfrak {G}=\mathfrak {F}{\upharpoonright }S^\omega (\mathfrak {F},X)$ for some $\varnothing \neq X\subseteq W$ . We write $\mathfrak {F}_w = \mathfrak {F}{\upharpoonright }S^\omega (\mathfrak {F},w)$ . A frame $\mathfrak {F}$ is point-generated, if $\mathfrak {F}=\mathfrak {F}_w$ for some $w$ in $\mathfrak {F}$ .

We use $\mathsf {Fr}_{g}(\Gamma )$ to denote the class of all point-generated frames for a set $\Gamma $ of formulas. Let $\mathsf {Fr}^{<\aleph _0}_g(\Gamma )= \mathsf {Fr}_{g}(\Gamma )\cap \mathsf {Fr}^{<\aleph _0}(\Gamma )$ . By [9, Proposition 2.3], if $\mathfrak {G}$ is a generated subframe of $\mathfrak {F}$ , then $Th(\mathfrak {F})\subseteq Th(\mathfrak {G})$ .

Definition 2.4. Let $\mathfrak {F} = (W,R)$ and $\mathfrak {F}' = (W',R')$ be frames. We use $\mathfrak {F}\cong \mathfrak {F}'$ to denote that $\mathfrak {F}$ is isomorphic to $\mathfrak {F}'$ , i.e., there exists a bijective function $f:W\to W'$ such that, for all $w,u\in W$ , $wRu$ if and only if $f(w)R'f(u)$ .

A mapping $f :W \rightarrow W^\prime $ is a bounded morphism from $\mathfrak {F}$ to $\mathfrak {F}'$ , notation $f:\mathfrak F\twoheadrightarrow \mathfrak F'$ , if for all $w,v\in W$ , $v'\in W'$ , the following conditions hold:

1. (1) If $wR v$ , then $f(w)R'f(v)$ .

2. (2) If $f(w) R' v'$ , there exists $v \in R(w)$ with $f(v) = v'$ .

3. (3) If $f(w) \breve {R'} v'$ , there exists $v \in \breve {R}(w)$ with $f(v) = v'$ .

A frame $\mathfrak {F}'$ is a bounded morphic image of $\mathfrak {F}$ , if there exists a surjective bounded morphism from $\mathfrak {F}$ to $\mathfrak {F}'$ .

For a class $\mathcal {K}$ of frames, let $|\mathcal {K}|$ be the cardinality of $\mathcal {K}$ up to isomorphism. By [9, Proposition 2.3], if $\mathfrak {G}$ is a bounded morphic image of $\mathfrak {F}$ , then $Th(\mathfrak {F})\subseteq Th(\mathfrak {G})$ .

Definition 2.5. A tense logic is a set of formulas $L\subseteq \mathscr {L}_t$ such that

1. (Tau) L contains all instances of classical propositional tautologies;

2. (Dual) $\Diamond p\leftrightarrow \neg \Box \neg p\in L$ ;

3. (Adj) $\blacklozenge \varphi \to \psi \in L$ if and only if $\varphi \to \Box \psi \in L$ ;

4. (MP) if $\varphi ,\varphi \to \psi \in L$ , then $\psi \in L$ ;

5. (Sub) if $\varphi \in L$ , then $\varphi ^s\in L$ for every substitution s.

The least tense logic is denoted by $\mathsf {K}_t$ . For every tense logic L and a set $\Sigma $ of formulas, let $L\oplus \Sigma $ denote the smallest tense logic containing $L\cup \Sigma $ . A tense logic L is consistent if $\bot \not \in L$ . A tense logic L is finitely axiomatizable, if there is a finite set $\Sigma $ of formulas such that $L=\mathsf {K}_t\oplus \Sigma $ . A tense logic $L_2$ is an extension of $L_1$ , if $L_1\subseteq L_2$ ; and $L_2$ is a proper extension of $L_1$ (notation: $L_1\subset L_2$ ), if $L_1\subseteq L_2$ and $L_1\neq L_2$ .

A formula $\varphi $ is deducible in a tense logic Lfrom a set $\Gamma $ of formulas (notation: $\Gamma \vdash _L\varphi $ ), if $\varphi \in L$ or there exist $\psi _1,\ldots ,\psi _n \in \Gamma $ with $(\psi _1\wedge \cdots \wedge \psi _n) \to \varphi \in L$ . A set $\Gamma $ of formulas is L-consistent if $\, \Gamma \not \vdash _L\bot $ . A set $\Gamma $ of formulas is maximal L-consistent if $\, \Gamma $ is L-consistent and it has no L-consistent proper extension.

Remark 2.6. Let L be a tense logic. We can show that the following dual statement of (Adj) holds for L:

$$ \begin{align*} (\mathrm{Adj}^\partial) \Diamond\varphi\to\psi\in L\ \text{if and only if}\ \varphi\to\blacksquare\psi\in L. \end{align*} $$

Assume $\Diamond \varphi \to \psi \in L$ . Then $\neg \psi \to \Box \neg \varphi \in L$ . By (Adj), $\blacklozenge \neg \psi \to \neg \varphi \in L$ and so $\varphi \to \blacksquare \psi \in L$ . The other direction is similar. Now we show that L is normal, i.e., if $\varphi \in L$ , then $\Box \varphi ,\blacksquare \varphi \in L$ . Assume $\varphi \in L$ . Then $\blacklozenge \top \to \varphi ,\Diamond \top \to \varphi \in L$ . By (Adj) and $(\mathrm {Adj}^\partial )$ , we have $\top \to \Box \varphi ,\top \to \blacksquare \varphi \in L$ . Hence $\Box \varphi ,\blacksquare \varphi \in L$ .

Let $\Lambda (L)$ be the set of all extensions of a tense logic L. Note that $\Lambda (L)$ is closed under the operations $\cap $ and $\oplus $ . Indeed, $(\Lambda (L), \cap ,\oplus )$ forms a lattice with top $ \mathscr {L}_t$ and bottom L. A tense logic L is consistent if $\bot \not \in L$ . It is obvious that $\mathscr {L}_t$ is the unique inconsistent tense logic.

Definition 2.7. A tense logic L is Kripke-complete if $L=Th(\mathsf {Fr}(L))$ . A tense logic L is tabular if $L = Th(\mathfrak {F})$ for some finite frame $\mathfrak {F}$ . Let $\mathsf {TAB}$ be the set of all tabular tense logics. A consistent tense logic L is Post-complete if there is no consistent proper extension of L. Let $\mathsf {PC}$ be the set of all Post-complete tense logics. The Post number of a tense logic L is the cardinality $\mathsf {PN}(L)=|\Lambda (L)\cap \mathsf {PC}|$ .

If a tense logic L is Kripke-complete, then $L=Th(\mathsf {Fr}_g(L))$ . If $L = Th(\mathcal {K})$ for some finite set $\mathcal {K}$ of finite frames, then L is tabular. Every tabular tense logic is obviously Kripke-complete. These results can be found in, e.g., [9]. The canonical model for a tense logic L is defined as $\mathfrak {M}^L = (W^L,R^L,V^L)$ where (i) $W^L$ is the set of all maximal L-consistent sets of formulas; (ii) $R^L =\{(w,v)\in W^L\times W^L : \Diamond \varphi \in w~\text {for all}~\varphi \in v\}$ ; and (iii) $V^L(p)=\{w\in W^L : p\in w\}$ for each $p\in \Phi $ . The canonical frame for L is defined as $\mathfrak F^L = (W^L,R^L)$ . Some Kripke-completeness results are obtained by the canonical model method (cf. [9]).

Definition 2.8. A general frame is a pair $\mathbb {F} = (\mathfrak F,A)$ where $\mathfrak F = (W,R)$ is a frame and $A\subseteq \mathcal {P}(W)$ satisfies the following conditions:

1. (1) $\varnothing \in A$ .

2. (2) If $X,Y\in A$ , then $X\cup Y\in A$ .

3. (3) If $X\in A$ , then $\overline {X},\blacklozenge _RX,\Diamond _RX\in A$ .

For a general frame $\mathbb {F}=(\mathfrak {F},A)$ , let $\kappa \mathbb {F}=\mathfrak {F}$ . A valuation V in $\mathfrak {F}$ is admissible for $\mathbb {F}$ , if $V(p) \in A$ for every $p\in \Phi $ . A general model is a triple $\mathbb {M} = (\mathfrak F,A,V)$ where $(\mathfrak F,A)$ is a general frame and V is an admissible valuation.

Validity in general frames is defined as in Definition 2.2 by replacing valuation with admissible valuation. Let $Th(\mathbb {K})$ be the theory of a class $\mathbb {K}$ of general frames. Descriptive frames are defined as in [9, Definition 3.5]. Let $DF(\Gamma )$ be the class of all descriptive general frames for a set $\Gamma $ of formulas.

For every general frame $\mathbb {F}$ the theory $Th(\mathbb {F})$ is a tense logic. The general canonical frame for a tense logic L is defined as $\mathbb {F}^L = (\mathfrak {F}^L, A^L)$ where $A^L = \{V^L(\varphi ) : \varphi \in \mathscr {L}_t\}$ . Obviously $\mathbb {F}^L$ is descriptive. By [9, Lemma 3.6], $L=Th(\mathbb {F}^L)$ . Moreover, by [9, Theorem 3.7], $DF(L)\neq \varnothing $ and $L=Th(DF(L))$ .

Definition 2.9. Let $\mathbb {F}=(\mathfrak {F},A)$ and $\mathbb {F}'=(\mathfrak {F}',A')$ be general frames where $\mathfrak {F}=(W, R)$ and $\mathfrak {F}'=(W',R')$ . For every $\varnothing \neq X\subseteq W$ , the subframe of $\mathfrak {F}$ induced by X is defined as $\mathbb {F}{\upharpoonright }X=(\mathfrak {F}{\upharpoonright }X,A{\upharpoonright }X)$ where $\mathfrak F{\upharpoonright }X$ is the subframe of $\mathfrak F$ induced by X and $A{\upharpoonright }X=\{Y\cap X: Y\in A\}$ . The general subframe of $\mathbb {F}$ generated by X is defined as $\mathbb {F}{\upharpoonright }S^\omega (\mathfrak F,X)$ . We say that $\mathbb {F}$ is a generated general subframe of $\mathbb {F}'$ , if $\mathbb {F}=\mathbb {F}^\prime {\upharpoonright }S^\omega (\mathfrak F,X)$ for some $\varnothing \neq X\subseteq W$ . We write $\mathbb {F}_w$ for $\mathbb {F}{\upharpoonright }S^\omega (\mathfrak F,\{w\})$ . A general frame $\mathbb {F}$ is point-generated if $\mathbb {F}=\mathbb {F}_w$ for some $w\in W$ .

Generated general subframe preserves validity (cf. [9]), i.e., if $\mathbb {G}$ is a generated general subframe of $\mathbb {F}$ , then $Th(\mathbb {F})\subseteq Th(\mathbb {G})$ .

Definition 2.10. Let $\mathbb {F}=(\mathfrak {F},A)$ and $\mathbb {F}'=(\mathfrak {F}',A')$ be general frames where $\mathfrak {F}=(W, R)$ and $\mathfrak {F}'=(W',R')$ . A map $f:W\rightarrow W^\prime $ is a bounded morphism from $\mathbb {F}$ to $\mathbb {F}^\prime $ if f is a bounded morphism from $\mathfrak F$ to $\mathfrak F^\prime $ such that $f^{-1}(a^\prime )\in A$ for every $a^\prime \in A^\prime $ . We say that $\mathbb {F}^\prime $ is a bounded morphic image of $\mathbb {F}$ if there is a bounded morphism from $\mathbb {F}$ to $\mathbb {F}^\prime $ .

Bounded morphic image of general frame also preserves validity (cf. [9]), i.e., if $\mathbb {G}$ is a bounded morphic image of $\mathbb {F}$ , then $Th(\mathbb {F})\subseteq Th(\mathbb {G})$ .

3 A new characterization of tabularity in $\Lambda (\mathsf {K}_t)$

In this section, we present a new characterization of tabularity in tense logics. We give some required notions first. For every $n\in \omega $ , let $\mathsf {P}(n)=\{\Diamond ,\blacklozenge \}^n$ be the set of all n-tuples of tense operators in $\{\Diamond , \blacklozenge \}$ . Let $\mathsf {P}(0)=\{\varepsilon \}$ and $\mathsf {P}(\omega )=\bigcup _{n<\omega }\mathsf {P}(n)$ . A possibility is an element in $\mathsf {P}(\omega )$ . We use $\pi $ with or without subscripts for possibilities. The length of a possibility $\pi $ , denoted by $|\pi |$ , is the number of occurrences of tense operators in $\pi $ . Let $|\epsilon |=0$ . For every possibility $\pi $ and formula $\varphi $ , let $\pi \varphi $ be the formula obtained by putting the sequence of operators $\pi $ in front of $\varphi $ .

Definition 3.1. For every $n\geq 1$ and $\varphi \in \mathscr {L}_t$ , the formula $\Delta _n$ is defined as

$$ \begin{align*} \Delta_n\varphi=\bigvee\{\pi\varphi:\pi\in\mathsf{P}(\omega), |\pi|\leq n\}. \end{align*} $$

Let $\nabla _n\varphi :=\neg \Delta _n\neg \varphi $ . The formula $\mathsf {tab}^T_n$ is defined as

$$ \begin{align*} \mathsf{tab}^T_n=\neg(\Delta_n\psi_0\wedge\cdots\wedge\Delta_n\psi_n), \end{align*} $$

where $\psi _i=\neg p_0\wedge \cdots \wedge \neg p_{i-1}\wedge p_i$ for each $i\leq n$ . Note that $\psi _0=p_0$ .

For example, $\Delta _1p = p\vee \Diamond p\vee \blacklozenge p$ and $\Delta _2p=p\vee \Diamond p\vee \blacklozenge p\vee \Diamond \Diamond p\vee \Diamond \blacklozenge p\vee \blacklozenge \Diamond p\vee \blacklozenge \blacklozenge p$ , and $\mathsf {tab}^T_1=\neg ((p_0\vee \Diamond p_0\vee \blacklozenge p_0)\wedge ((\neg p_0\wedge p_1)\vee \Diamond (\neg p_0\wedge p_1)\vee \blacklozenge (\neg p_0\wedge p_1)))$ .

Let $\mathfrak F=(W,R)$ be a frame and $w,u\in W$ . For every $n\geq 1$ , a finite sequence $\langle v_1,\ldots ,v_n \rangle \in W^n$ is called a route of length n between $w$ and u, if $w=v_1$ , $u=v_n$ and $v_iRv_{i+1}$ or $v_i\breve {R}v_{i+1}$ for all $i\in \{1,2,\ldots ,n-1\}$ . Let $\mathsf {R}_n(w,u)$ be the set of all routes of length n between $w$ and u. Let $\mathsf {R}(w,u)=\bigcup _{n\geq 1}\mathsf {R}_n(w,u)$ whose elements are called routes between $w$ and u. We use $\rho $ with or without subscripts for a route. The length of a route $\rho $ , denoted by $|\rho |$ , is the number of occurrences of elements in the sequence.

Lemma 3.2. Let $\mathfrak F=(W,R)$ be a frame. Then $(1)$ for every $n\geq 1$ , $w\in W$ and $u\in S^{n}(\mathfrak F,w)$ , there exists $\rho \in \mathsf {R}(w,u)$ with $|\rho |\leq n+1$ ; and $(2)$ if $\mathfrak {F}$ is point-generated, then $\mathsf {R}(w,u)\neq \varnothing $ for all $w,u\in W$ .

Proof. Clearly (1) follows from Definition 2.3. For (2), let $\mathfrak {F}=\mathfrak {F}_v$ for some $v\in W$ . Let $w,u\in W$ . Then $w\in S^k(\mathfrak {F},v)$ and $u\in S^l(\mathfrak {F},v)$ for some $k,l<\omega $ . By Definition 2.3, there exists a route between $w$ and u.

Lemma 3.3. Let $\mathfrak F=(W,R)$ be a frame, $\mathfrak M=(\mathfrak F,V)$ be a model and $w,u\in W$ . If $\mathsf {R}_{n+1}(w,u)\neq \varnothing $ , there exists $\pi \in \mathsf {P}(n)$ such that for all $\varphi \in \mathscr {L}_t$ and $\psi \in \mathscr {L}_t^0$ , $(1)$ if $\mathfrak M,u\models \varphi $ , then $\mathfrak M,w\models \pi \varphi $ ; and $(2)$ if $\mathfrak F,u\models \psi $ , then $\mathfrak F,w\models \pi \psi $ .

Proof. Clearly (2) follows from (1). The proof proceeds by induction on n. Assume $n=0$ . Suppose $\mathsf {R}_{1}(w,u)\neq \varnothing $ . Then $w=u$ and so $\pi =\varepsilon $ is required. Let $n>0$ . Suppose $\langle v_1,\ldots ,v_n,v_{n+1} \rangle \in \mathsf {R}_{n+1}(w,u)$ . Then $v_1=w$ , $v_{n+1}=u$ and $\langle v_1,\ldots ,v_n \rangle \in \mathsf {R}_{n}(w,v_n)$ . By induction hypothesis, there exists a possibility $\pi \in \mathsf {P}(n)$ such that for all $\varphi \in \mathscr {L}_t$ , if $\mathfrak M,v_n\models \varphi $ , then $\mathfrak M,w\models \pi \varphi $ . Suppose $v_nRu$ . If $\varphi \in \mathscr {L}_t$ and $\mathfrak M,u\models \varphi $ , then $\mathfrak M,v_n\models \Diamond \varphi $ and so $\mathfrak M,w\models \Diamond \pi \varphi $ . Hence $\Diamond \pi $ is required. Similarly, if $v_n\breve {R}u$ , then $\blacklozenge \pi $ is required.

Lemma 3.4. For every $n\in \omega $ , $\mathfrak F,w\models \mathsf {tab}^T_n$ if and only if $|S^n(\mathfrak F,w)|\leq n$ .

Proof. Let $\mathfrak F=(W,R)$ be a frame and $w\in W$ . Assume $|S^n(\mathfrak F,w)|>n$ . Then there exists $X=\{w_0,\ldots ,w_n\}\subseteq S^n(\mathfrak F,w)$ with $|X|=n+1$ . Let V be a valuation on $\mathfrak F$ such that $V(p_i)\cap X=\{w_i\}$ for all $i\leq n$ . By Lemmas 3.2 and 3.3, we have $\mathfrak F,V,w\models \Delta _n\psi _i$ for each $i\leq n$ . Hence $\mathfrak F,w\not \models \mathsf {tab}^T_n\!$ . Assume $\mathfrak F,w\not \models \mathsf {tab}^T_n\!$ . Then $\mathfrak M,w\models \neg \mathsf {tab}^T_n$ for some model $\mathfrak M=(\mathfrak F,V)$ . Then for each $i\leq n$ , $\mathfrak M,w\models \Delta _n\psi _i$ , and so $\mathfrak M,w_i\models \psi _i$ for some $w_i\in W$ . Clearly $\{w_0,\ldots ,w_n\}\subseteq S^n(\mathfrak F,w)$ and $w_i\neq w_j$ for $i\neq j\leq n$ . Hence $|S^n(\mathfrak F,w)|>n$ .

Lemma 3.5. For every $n\in \omega $ , $S^{n}(\mathfrak F,w)\neq S^{n+1}(\mathfrak F,w)$ if and only if $S^n(\mathfrak F,w)\neq S^\omega (\mathfrak F,w)$ .

Proof. The left-to-right direction is trivial. Assume $S^{n}(\mathfrak F,w)= S^{n+1}(\mathfrak F,w)$ . By Definition 2.3, $S^n(\mathfrak F,w)= S^\omega (\mathfrak F,w)$ .

Lemma 3.6. For every $n\geq 1$ , if $\mathfrak F,w\models \mathsf {tab}^T_n\!$ , then $|S^\omega (\mathfrak F,w)|\leq n$ .

Proof. Assume $\mathfrak F,w\models \mathsf {tab}^T_n\!$ . By Lemma 3.4, $|S^n(\mathfrak F,w)|\leq n$ . Suppose $S^n(\mathfrak F,w)\neq S^\omega (\mathfrak F,w)$ . Then $S^i(\mathfrak F,w)\neq S^\omega (\mathfrak F,w)$ for all $i\leq n$ . By Lemma 3.5, $1=|S^0(\mathfrak F,w)|<|S^1(\mathfrak F,w)|<\cdots <|S^n(\mathfrak F,w)|$ . Then $|S^n(\mathfrak F,w)|>n$ which contradicts $|S^n(\mathfrak F,w)|\leq n$ . Hence $S^n(\mathfrak F,w)=S^\omega (\mathfrak F,w)$ and $|S^\omega (\mathfrak F,w)|\leq n$ .

For a new characterization of tabularity, we recall finitely alternative tense logics from [9]. For every $n,m\in \omega $ , the $(n,m)$ -alternative tense logic is the tense logic $T_{m,n}=\mathsf {K}_t\oplus \{\mathrm {Alt}_n^F,\mathrm {Alt}_m^P\}$ where

$$ \begin{align*} \mathrm{Alt}^F_n &= \Box p_0 \vee \Box(p_0 \rightarrow p_1) \vee \cdots \vee \Box(p_0 \wedge \cdots \wedge p_{n-1} \rightarrow p_{n}),\\ \mathrm{Alt}^P_m &= \blacksquare p_0 \vee \blacksquare(p_0 \rightarrow p_1) \vee \cdots \vee \blacksquare(p_0 \wedge \cdots \wedge p_{m-1} \rightarrow p_{m}). \end{align*} $$

For every frame $\mathfrak {F}=(W, R)$ and $w\in W$ , (i) $\mathfrak {F},w\models \mathrm {Alt}^F_n$ if and only if $|R(w)|\leq n$ ; and (ii) $\mathfrak {F},w\models \mathrm {Alt}^P_n$ if and only if $|\breve {R}(w)|\leq n$ . By [9, Theorem 3.10], every consistent tense logic $L\in \Lambda (T_{n,m})$ is Kripke-complete and so $L=Th(\mathsf {Fr}_g(L))$ .

Theorem 3.7. For every consistent logic $L\in \Lambda (\mathsf {K}_t)$ , $L\in \mathsf {TAB}$ if and only if $\mathsf {tab}^T_n\in L$ for some $n\geq 1$ .

Proof. Assume $L\in \mathsf {TAB}$ . Then $L=Th(\mathfrak F)$ for some frame $\mathfrak F$ with $|\mathfrak F|=n\in \omega $ . By Lemma 3.4, $\mathfrak F\models \mathsf {tab}^T_n\!$ , i.e., $\mathsf {tab}^T_n\in L$ . Assume $\mathsf {tab}^T_n\in L$ for some $n\geq 1$ . Let $\mathfrak F=(W,R)$ be a point-generated frame for L and $w\in W$ . Then $\mathfrak F, w\models \mathsf {tab}^T_n\!$ . By Lemma 3.6, $|W|=|S^\omega (\mathfrak F,w)|=|S^n(\mathfrak F,w)|\leq n$ . It follows that $T_{nn,\subseteq } L$ . By [9, Theorem 3.10], $L=Th(\mathsf {Fr}_g(L))$ . Clearly $|\mathfrak F|\leq n$ for all $\mathfrak F\in \mathsf {Fr}_g(L)$ . Then $|\mathsf {Fr}_g(L)|< \aleph _0$ . By [9, Proposition 3.4], $L\in \mathsf {TAB}$ .

Lemma 3.8. If $L\in \mathsf {TAB}$ , then all consistent logics in $\Lambda (L)$ are Kripke-complete.

Proof. Let $L=Th(\mathfrak F)$ for some frame $\mathfrak F$ with $|\mathfrak F|=k\in \omega $ . Obviously $\mathfrak F\models \mathrm {Alt}_k^F\wedge \mathrm {Alt}_k^P$ . Then $T_{kk,\subseteq } L$ . It follows that $\Lambda (L)\subseteq \Lambda (T_{kk,)}$ . By [9, Theorem 3.10], all consistent logics in $\Lambda (L)$ are Kripke-complete.

Theorem 3.9. If $L\in \mathsf {TAB}$ , then $(1)\ \Lambda\ (L)$ is finite and every consistent logic in $\Lambda (L)$ is tabular;and $(2)\ L$ is finitely axiomatizable.

Proof. Let $L\in \mathsf {TAB}$ and $L'\in \Lambda (L)$ . For (1), by Theorem 3.7, $\mathsf {tab}^T_n\in L\subseteq L'$ . By the proof of Theorem 3.7, $L'$ is tabular. Let $f: \Lambda (L)\to \mathcal {P}(\mathsf {Fr}_g(L))$ be the function given by $f(L')=Fr_g(L')$ . Clearly $Fr_g(L')\subseteq Fr_g(L)$ . By Lemma 3.8, every consistent tense logic in $\Lambda (L)$ is Kripke-complete. Then f is injective and $|\Lambda (L)|\leq 2^{|\mathsf {Fr}_g(L)|}$ . By the proof of Theorem 3.7, $|\mathsf {Fr}_g(L)|<\aleph _0$ . For (2), it is well-known that every tabular logic is finitely axiomatizable (cf., e.g., [3, 4, 8]).

Remark 3.10. The characterization of tabularity given by Chagrov and Shehtman [3] uses formulas $\alpha _n$ and $\beta _n$ with $n\geq 1$ which are defined as follows:

(1) $\alpha _n$ is the conjunction of all formulas of the form

$$ \begin{align*} \neg(\gamma_1\wedge M_1(\gamma_2\wedge M_2(\gamma_3\wedge\cdots\wedge M_{n-1}\gamma_n))\cdots), \end{align*} $$

(2) $\beta _n$ is the conjunction of all formulas of the form

$$ \begin{align*} \neg M_1\cdots M_s(M_{s+1}\gamma_1\wedge\cdots\wedge M_{s+n}\gamma_n), \end{align*} $$

where $s<n$ , each $M_i\in \{\Diamond ,\blacklozenge \}$ with $1\leq i\leq s+n$ , and for each $1\leq i\leq n$ , $\gamma _i=p_1\wedge \cdots \wedge p_{i-1}\wedge \neg p_i\wedge p_{i+1}\wedge \cdots \wedge p_n$ . For every frame $\mathfrak F=(W,R)$ and $w\in W$ , (i) $\mathfrak F,w\not \models \alpha _n$ if and only if there exists a route $\langle w_0,\ldots ,w_{n-1} \rangle $ with $w=w_0$ and $w_i\neq w_j$ for all $i\neq j<n$ ; and (ii) $\mathfrak F,w\not \models \beta _n$ if and only if there exist $m<n$ and $u\in S^m(\mathfrak F,w)$ with $|R(u)\cup \breve {R}(u)|\geq n$ . It follows that

(†) $$ \begin{align} \text{if}\ \mathfrak F_w,w\models\alpha_n\wedge\beta_n,\ \text{then}\ |\mathfrak F_w|<f(n)=\sum_{k=0}^{n-1}(n-1)^k. \end{align} $$

By these results, the tabularity in tense logic is characterized as follows [3]:

(‡) $$ \begin{align} \text{A consistent logic}\ L\in\mathsf{TAB}\ \text{if and only if}\ \alpha_n\wedge\beta_n\in L\ \text{for some}\ n\geq 1. \end{align} $$

Theorem 3.9 also follows from $(\ddagger )$ . For every $n\geq 1$ , we can show the difference between $\mathsf {tab}^T_n$ and $\alpha _n\wedge \beta _n$ . Consider frames $\mathfrak F_1,\mathfrak F_2,\mathfrak G_1$ and $\mathfrak G_2$ in Figure 1. Clearly $\mathfrak F_1,w_1\models \alpha _n\wedge \beta _m$ if and only if $\mathfrak F_2,w_2\models \alpha _n\wedge \beta _m$ for each $n,m\geq 1$ . It follows that $\alpha _n\wedge \beta _n$ for all $n\geq 1$ cannot distinguish $(\mathfrak F_1,w_1)$ from $(\mathfrak F_2,w_2)$ . However $\mathfrak F_1,w_1\models \mathsf {tab}^T_7$ and $\mathfrak F_2,w_2\not \models \mathsf {tab}^T_7\!$ . On the other hand, for all $n\geq 1$ , $\mathfrak {G}_1\models \mathsf {tab}^T_n$ if and only if $\mathfrak {G}_2\models \mathsf {tab}^T_n\!$ . However $\mathfrak {G}_1,u_1\models \alpha _3\wedge \beta _3$ and $\mathfrak {G}_2,u_2\not \models \alpha _3\wedge \beta _3$ . In general, by Lemma 3.6, we can replace the function $f(n)$ in $(\dagger )$ with n when the cardinality of a frame is concerned. For every point-generated frame $\mathfrak {F}$ , $\alpha _n\wedge \beta _n$ just gives the boundary $f(n)$ for the cardinality $|\mathfrak {F}|$ , while $\mathsf {tab}^T_n$ tells the exact cardinality of $\mathfrak F$ since $|\mathfrak F|=n$ if and only if $\mathfrak F\models \mathsf {tab}^T_n$ and $\mathfrak F\not \models \mathsf {tab}^T_{n-1}$ .

Fig. 1 Frames $\mathfrak F_1,\mathfrak F_2,\mathfrak G_1$ and $\mathfrak G_2$ .

4 Post-completeness in $\mathsf {TAB}$

A characterization of Post-completeness in $\mathsf {TAB}$ has been given in [13, Proposition 2] without giving a proof. In this section, we present a new characterization which is called the first Post-completeness theorem (Theorem 4.9). We recall the notion of contraction from [13]. A partition of a nonempty set W is a subset $\delta \subseteq \mathcal {P}(W)$ such that $\varnothing \not \in \delta $ , $\bigcup \delta =W$ and $A_1\cap A_2=\varnothing $ for all $A_1,A_2\in \delta $ . We use $\mathrm {Part}(W)$ for the set of all partitions of W. For $\delta \in \mathrm {Part}(W)$ and $w\in W$ , we write $\delta (w)$ for $\delta $ if $w\in \delta $ , and call $\delta $ the block of $w$ . The trivial partition of W is $Id_W = \{\{w\}:w\in W\}$ . A partition $\delta _1$ is a refinement of $\delta _2$ , if for every $A\in \delta _1$ there exists $B\in \delta _2$ with $A\subseteq B$ .

Definition 4.1. Let $\mathfrak F=(W,R)$ be a frame. A partition $\delta $ of W is called a contraction, if for all $w,u\in W$ , the following conditions hold:

1. (C1) If $wRu$ and $w'\in \delta (w)$ , there exists $u'\in \delta (u)$ with $w'Ru'$ .

2. (C2) If $uRw$ and $w'\in \delta (w)$ , there exists $u'\in \delta (u)$ with $u'Rw'$ .

Let $Ctr(\mathfrak {F})$ be the set of all contraction of $\mathfrak {F}$ .

Obviously, for every frame $\mathfrak F=(W,R)$ , the trivial partition $Id_W$ belongs to $Ctr(\mathfrak F)$ . Then a frame $\mathfrak F$ has no nontrivial contraction if and only if $|Ctr(\mathfrak F)|=1$ . It is mentioned in [13] that a tabular tense logic L is Post-complete if and only if $L=Th(\mathfrak F)$ for some finite point-generated frame $\mathfrak F$ with $|Ctr(\mathfrak F)|=1$ . Now we give a new characterization of Post-completeness in $\mathsf {TAB}$ utilizing constant formulas. In what follows, for each frame $\mathfrak F=(W,R)$ and $w\in W$ , the constant theory of $w$ in $\mathfrak F$ is defined as the set $C_{\mathfrak {F}}(w) =\{\varphi \in \mathscr {L}_t^0: \mathfrak {F},w\models \varphi \}$ .

Definition 4.2. Let $\mathfrak F=(W,R)$ be a frame. The constant filtration of $\mathfrak {F}$ is defined as the frame $\mathfrak F^c=(W^c,R^c)$ where

1. (1) $W^c=\{C_{\mathfrak {F}}(w) : w\in W\}$ ,

2. (2) $C_{\mathfrak {F}}(w)R^cC_{\mathfrak {F}}(u)$ if and only if $\Diamond \varphi \in C_{\mathfrak {F}}(w)$ for every $\varphi \in C_{\mathfrak {F}}(u)$ .

For each $w\in W$ , let $[w]_c=\{u\in W:C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)\}$ . Let $\delta _{\mathfrak {F}}^c=\{[w]_c:w\in W\}$ .

Lemma 4.3. Let $\mathfrak F=(W,R)$ be a finite point-generated frame and $\delta \in Ctr(\mathfrak {F})$ . Then $(1) u\in \delta (w)$ implies $C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)$ ; and $(2) \delta _{\mathfrak {F}}^c\in \mathrm {Part}(W)$ and $\delta $ is a refinement of $\delta _{\mathfrak {F}}^c$ .

Proof. For (1), note that contraction is a particular case of bisimulation (cf. [1]). By (C1) and (C2), for every formula $\varphi \in \mathscr {L}_t^0$ and $w,u\in W$ , if $u\in \delta (w)$ , then $\mathfrak F,w\models \varphi $ if and only if $\mathfrak F, u\models \varphi $ . For (2), clearly $\delta _{\mathfrak {F}}^c\in \mathrm {Part}(W)$ . Let $\delta (w)\in \delta $ . Assume $u\in \delta (w)$ . By (1), $C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)$ which implies $u\in [w]_c$ . Then $\delta (w)\subseteq [w]_c$ . Hence $\delta $ is a refinement of $\delta _{\mathfrak {F}}^c$ .

Lemma 4.4. If $\mathfrak F=(W,R)$ is a finite point-generated frame, then $\delta _{\mathfrak {F}}^c\in Ctr(\mathfrak F)$ .

Proof. Let $\mathfrak F=(W,R)$ be finite point-generated. By Lemma 4.3(2), $\delta _{\mathfrak {F}}^c\in \mathrm {Part}(W)$ . Then $\delta _{\mathfrak {F}}^c$ is finite. Let $\delta _{\mathfrak {F}}^c = \{A_i : i\leq n\}$ . Then there exists a finite set of formulas $\{\varphi _i\in \mathscr {L}_t^0 : i \leq n\}$ such that, for every $i\leq n$ and $v\in W$ , $\mathfrak F,v\models \varphi _i$ if and only if $v\in A_i$ . Assume $wRu$ and $v\in \delta (w)$ . Let $w\in A_i$ and $u\in A_j$ with $i,j\leq n$ . Then $\mathfrak F,w\models \Diamond \varphi _j$ . By Lemma 4.3(1), $\mathfrak F,v\models \Diamond \varphi _j$ . Thus there exists $v'\in R(v)$ with $\mathfrak F,v^\prime \models \varphi _j$ . Then $v^\prime \in A_j$ . Hence (C1) holds. Similarly we can prove (C2). It follows that $\delta _{\mathfrak {F}}^c\in Ctr(\mathfrak F)$ .

Theorem 4.5. If $\mathfrak F=(W,R)$ is a finite point-generated frame, then $|Ctr(\mathfrak F)|=1$ if and only if $\delta _{\mathfrak {F}}^c=Id_W$ .

Proof. Let $\mathfrak F=(W,R)$ be finite point-generated. By Lemma 4.4, $\delta _{\mathfrak {F}}^c\in Ctr(\mathfrak F)$ . Hence $|Ctr(\mathfrak F)|=1$ which implies $\delta _{\mathfrak {F}}^c=Id_W$ . Suppose $\delta \in Ctr(\mathfrak F)$ and $\delta \neq Id_W$ . By Lemma 4.3(2), we have $\delta _{\mathfrak {F}}^c\neq Id_W$ .

Definition 4.6. Let $\mathfrak F=(W,R)$ be a frame and $X\subseteq W$ . A set of constant formulas $\Sigma $ is satisfiable in X, if there exists $w\in X$ with $\mathfrak F,w\models \varphi $ for all $\varphi \in \Sigma $ ; and $\Sigma $ is finitely satisfiable in X, if every finite subset of $\Sigma $ is satisfiable in X.

A frame $\mathfrak F$ is called $0$ -saturated, if for every $w\in W$ and $\Sigma \subseteq \mathscr {L}_t^0$ , the following conditions hold: (i) if $\Sigma $ is finitely satisfiable in $R(w)$ , then $\Sigma $ is satisfiable in $R(w)$ ; and (ii) if $\Sigma $ is finitely satisfiable in $\breve {R}(w)$ , then $\Sigma $ is satisfiable in $\breve {R}(w)$ .

Lemma 4.7. Let $\mathfrak F=(W,R)$ be $0$ -saturated and $f:W\rightarrow W^c$ be the function with $f(w)=C_{\mathfrak {F}}(w)$ for all $w\in W$ . Then $f:\mathfrak F\twoheadrightarrow \mathfrak F^c\!$ .

Proof. Clearly f is surjective. Suppose $wRu$ . Then $C_{\mathfrak {F}}(w)R^cC_{\mathfrak {F}}(u)$ . Assume $C_{\mathfrak {F}}(w)R^c C_{\mathfrak {F}}(u)$ . It suffices to to show that there exists $v\in R(w)$ with $C_{\mathfrak {F}}(u)=C_{\mathfrak {F}}(v)$ . Let $\Theta =\{\varphi _1,\ldots ,\varphi _n\}\subseteq C_{\mathfrak {F}}(u)$ . Then $\Diamond (\varphi _1\wedge \cdots \wedge \varphi _n)\in f(w)$ , i.e., $\mathfrak F,w\models \Diamond (\varphi _1\wedge \cdots \wedge \varphi _n)$ . Then $\Theta $ is satisfiable in $R(w)$ . Hence $C_{\mathfrak {F}}(u)$ is finitely satisfiable in $R(w)$ . Since $\mathfrak F$ is $0$ -saturated, there exists $v\in R(w)$ with $\mathfrak F,v\models \psi $ for all $\psi \in C_{\mathfrak {F}}(u)$ . Clearly $C_{\mathfrak {F}}(u)\subseteq C_{\mathfrak {F}}(v)$ . Suppose $\chi \not \in C_{\mathfrak {F}}(u)$ . Then $\neg \chi \in C_{\mathfrak {F}}(u)$ . Hence $\neg \chi \in C_{\mathfrak {F}}(v)$ , i.e., $\chi \not \in C_{\mathfrak {F}}(v)$ . Hence $C_{\mathfrak {F}}(u)=C_{\mathfrak {F}}(v)$ . Similarly $C_{\mathfrak {F}}(u)R^c C_{\mathfrak {F}}(w)$ implies $C_{\mathfrak {F}}(v)=C_{\mathfrak {F}}(u)$ for some $v\in \breve {R}(w)$ .

Lemma 4.8. If $\mathfrak F=(W,R)$ is a finite point-generated frame, then $\mathfrak F$ is 0-saturated and $Th(\mathfrak F)\subseteq Th(\mathfrak F^c)$ .

Proof. Let $\mathfrak F=(W,R)$ be finite point-generated, $w\in W$ and $\Sigma \subseteq \mathscr {L}_t^0$ . Let $R(w)=\{w_0,\ldots ,w_n\}$ and $|R(w)|=n+1$ . Suppose that $\Sigma $ is not satisfiable in $R(w)$ . Then for every $i\leq n$ , there exists $\varphi _i\in \Sigma $ with $\mathfrak F,w_i\models \neg \varphi _i$ . Hence $\mathfrak F, w\models \Box \neg (\varphi _0\wedge \cdots \wedge \varphi _n)$ . Let $\Theta =\{\varphi _0,\ldots ,\varphi _n\}$ . Then $\Theta $ is not satisfiable in $R(w)$ , i.e., $\Sigma $ is not finitely satisfiable in $R(w)$ . Similarly, if $\Sigma $ is finitely satisfiable in $\breve {R}(w)$ , then $\Sigma $ is satisfiable in $\breve {R}(w)$ . It follows that $\mathfrak F$ is 0-saturated. By Lemma 4.7, $\mathfrak F\twoheadrightarrow \mathfrak F^c\!$ . By [9, Proposition 2.6], $Th(\mathfrak F)\subseteq Th(\mathfrak F^c)$ .

Theorem 4.9 (The first Post-completeness theorem).

Let $\mathfrak F=(W,R)$ be a finite point-generated frame. The following are equivalent:

1. (1) $Th(\mathfrak F)$ is Post-complete.

2. (2) $ \mathfrak F\cong \mathfrak F^c\!$ .

3. (3) For every $w,u\in W$ , $C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)$ if and only if $w=u$ .

4. (4) $|Ctr(\mathfrak F)|=1$ .

Proof. By Lemma 4.5, (3) is equivalent to (4). Clearly (3) implies (2). Now we show that (1) implies (3). Assume $Th(\mathfrak F)\in \mathsf {PC}$ . For a contradiction, suppose $C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)$ and $w\neq u$ . Recall that $[w]_c=\{v\in W : C_{\mathfrak {F}}(v)=C_{\mathfrak {F}}(w)\}$ . Since $\mathfrak F$ is finite, there exists $\varphi _w\in C_{\mathfrak {F}}(w)$ such that $\mathfrak F,v\models \neg \varphi _w$ for all $v\not \in [w]_c$ . Since $\mathfrak F$ is point-generated, by Lemma 3.2(2), $\mathsf {R}(w,u)\neq \varnothing $ . Let $\mathfrak M=(\mathfrak F,V)$ be a model with $V(p)=\{w\}$ . By Lemma 3.3, there exists $\pi \in \mathsf {P}(\omega )$ such that $\mathfrak M,u\models \varphi $ implies $\mathfrak M,w\models \pi \varphi $ for all $\varphi \in \mathscr {L}_t$ . Thus $\mathfrak M,w\not \models (\varphi _w\wedge p)\rightarrow \neg \pi \neg (\varphi _w\rightarrow p)$ . Hence $\mathfrak F\not \models (\varphi _w\wedge p)\rightarrow \neg \pi \neg (\varphi _w\rightarrow p)$ . Let $\mathfrak F^c$ be the constant filtration of $\mathfrak F$ . Since $\mathfrak F$ is finite point-generated, by Lemma 4.8, $Th(\mathfrak F)\subseteq Th(\mathfrak F^c)$ . Note that $C_{\mathfrak {F}}(w)$ is the only point in $W^c$ validating $\varphi _w$ . Then $\mathfrak F^c\models (\varphi _w\wedge p)\rightarrow \neg \pi \neg (\varphi _w\rightarrow p)$ . Hence $Th(\mathfrak F)\subsetneq Th(\mathfrak F^c)$ which contradicts the assumption $Th(\mathfrak F)\in \mathsf {PC}$ .

Now we show that (2) implies (1). Suppose $\mathfrak F\cong \mathfrak F^c$ and $Th(\mathfrak F)\subseteq L$ where L is a consistent tense logic. Let $W=\{w_0,\ldots ,w_n\}$ and $|W|=n+1$ . Since $\mathfrak F\cong \mathfrak F^c\!$ , for every $i\neq j\leq n$ , $C_{\mathfrak {F}}(w_i)\neq C_{\mathfrak {F}}(w_j)$ . For each $i\leq n$ , there exists $\varphi _i\in \mathscr {L}_t^0$ such that $\mathfrak F,w\models \varphi _i$ if and only if $w=w_i$ . For every $\psi \in { \mathscr {L}_t^0}$ and $i\leq n$ , $\mathfrak F,w_i\models \psi $ implies $\mathfrak F\models \varphi _i\rightarrow \psi $ . Hence $\{\varphi _i\rightarrow \psi \in { \mathscr {L}_t^0}:\mathfrak F,w_i\models \psi \}\subseteq Th(\mathfrak F)$ for all $i\leq n$ . Since $\mathfrak F$ is point-generated, by Lemmas 3.2 and 3.3, for all $i,j\leq n$ , there exists $\pi _{i,j}\in \mathsf {P}(\omega )$ with $\mathfrak F,w_i\models \pi _{i,j}\varphi _j$ . By Lemma 3.8, L is Kripke-complete. Then $\mathsf {Fr}_g(L)\neq \varnothing $ . Let $\mathfrak F'=(W',R')$ be a point-generated frame for L. Now we show ${W'}^c=W^c$ as follows:

1. (i) Assume $u\in W'$ . Clearly $\bigvee _{i\leq n}\varphi _i\in Th(\mathfrak F)\subseteq L$ . Then $\mathfrak F^\prime ,u\models \varphi _{i_u}$ for some $i_u\leq n$ . Clearly $\{\varphi _{i_u}\rightarrow \psi \in { \mathscr {L}_t^0}:\mathfrak F,w_{i_u}\models \psi \}\subseteq Th(\mathfrak F)$ . Suppose $\psi \in C_{\mathfrak {F}}(w_{i_u})$ . Then $\varphi _{i_u}\rightarrow \psi \in Th(\mathfrak F)\subseteq L$ . Then $\mathfrak F'\models \varphi _{i_u}\rightarrow \psi $ . By $\mathfrak F',u\models \varphi _{i_u}$ , we have $\mathfrak F',u\models \psi $ , i.e., $\psi \in C_{\mathfrak F'}(u)$ . Then $C_{\mathfrak {F}}(w_{i_u})\subseteq C_{\mathfrak F'}(u)$ . If $\chi \not \in C_{\mathfrak {F}}(w_{i_u})$ , then $\neg \chi \in C_{\mathfrak {F}}(w_{i_u})$ and $\neg \chi \in C_{\mathfrak F'}(u)$ , i.e., $\chi \not \in C_{\mathfrak F'}(u)$ . Hence $C_{\mathfrak F'}(u)\subseteq C_{\mathfrak {F}}(w_{i_u})$ . Then $C_{\mathfrak F'}(u)=C_{\mathfrak {F}}(w_{i_u})$ . Hence ${W'}^c\subseteq W^c$ .

2. (ii) Assume $w_k\in W$ . Take any $u\in W'$ . By (i), $C_{\mathfrak F'}(u)=C_{\mathfrak {F}}(w_{i_u})$ for some $i_u\leq n$ . Clearly $\mathfrak F, w_{i_u}\models \pi _{i_u,k}\varphi _k$ . Then $\mathfrak F', u\models \pi _{i_u,k}\varphi _k$ . There exists $u_k\in S^\omega (\mathfrak F^\prime ,u)=W^\prime $ with $\mathfrak F^\prime ,u_k\models \varphi _k$ . Clearly $\{\varphi _k\rightarrow \psi \in { \mathscr {L}_t^0}:\mathfrak F,w_k\models \psi \}\subseteq Th(\mathfrak F)$ . Like the proof (i), we have $C_{\mathfrak F'}(u_k)=C_{\mathfrak {F}}(w_k)$ . Hence $W^c\subseteq {W'}^c$ .

Then ${\mathfrak F'}^c=\mathfrak F^c\cong \mathfrak F$ . By $|\mathfrak F|=n+1$ and Lemma 3.4, $\mathfrak F\models \mathsf {tab}^T_{n+1}$ . Then $\mathfrak F'\models \mathsf {tab}^T_{n+1}$ . Since $\mathfrak F'$ is point-generated, by Lemma 3.6, $\mathfrak F'$ is finite. By Lemma 4.8, $L\subseteq Th(\mathfrak F')\subseteq Th({\mathfrak F'}^c)=Th(\mathfrak F)\subseteq L$ . Then $Th(\mathfrak F)=L$ . Hence $Th(\mathfrak F)\in \mathsf {PC}$ .

Corollary 4.10. The Post-completeness of the tense logic $Th(\mathfrak {F})$ for a given finite frame $\mathfrak {F}$ is decidable.

Proof. Let $\mathfrak F=(W,R)$ be a finite frame. Then $Ctr(\mathfrak F)$ is finite. By Theorem 4.9, it suffices to check if there exists a non-trivial contraction in $Ctr(\mathfrak F)$ . This is done in finitely many steps.

By Theorem 4.9, we can check the Post-completeness of $Th(\mathfrak F)$ for certain finite frames $\mathfrak F$ . For example, consider frames $\mathfrak {H}_1$ , $\mathfrak {H}_2$ , $\mathfrak {H}_3$ , and $\mathfrak {H}_4$ in Figure 2 and their theories $L_1,L_2,L_3$ and $L_4$ respectively. For $\mathfrak {H}_1,\mathfrak {H}_2$ and $\mathfrak {H}_3$ , we can distinguish different points by constant formulas as in Figure 2. For $\mathfrak {H}_4$ , clearly $C_{\mathfrak {H}_4}(x)=C_{\mathfrak {H}_4}(y)$ while $x\neq y$ . By Theorem 4.9, $L_1,L_2$ and $L_3$ are Post-complete but $L_4$ is not. Note that $L_1$ was incorrectly claimed not to be Post-complete in [13].

Fig. 2 Frames $\mathfrak {H}_1,\mathfrak {H}_2, \mathfrak {H}_3$ and $\mathfrak {H}_4$ .

Lemma 4.11. Let $\mathfrak F = (W,R)$ be a finite point-generated frame. If $L=Th(\mathfrak F)\in \mathsf {PC}$ , then $|\mathsf {Fr}_g(L)|=1$ .

Proof. Let $\mathfrak F = (W,R)$ be finite point-generated and $W=\{w_0,\ldots ,w_{n-1}\}$ . Assume $L=Th(\mathfrak F)\in \mathsf {PC}$ . By Theorem 4.9, for all $w,u\in W$ , $C_{\mathfrak {F}}(w)=C_{\mathfrak {F}}(u)$ if and only if $w=u$ . Then there exist $\varphi _0,\ldots ,\varphi _{n-1}\in { \mathscr {L}_t^0}$ such that

(♯) $$ \begin{align} \text{for all}\ u\in W\ \text{and}\ i<n, \mathfrak F,u\models\varphi_i\ \text{if and only if}\ u=w_i. \end{align} $$

Indeed, we have the following claims:

1. (i) $\mathsf {tab}^T_n\in L$ . Since $\mathfrak F$ is finite point-generated, by Lemma 3.4, $\mathfrak F\models \mathsf {tab}^T_n\!$ .

2. (ii) $\Delta _n\varphi _i\in L$ for every $i<n$ . Since $\mathfrak F$ is point-generated, for every $u\in W$ , we obtain $S^n(\mathfrak F, u)=W$ . By Lemma 3.3, $\mathfrak F\models \Delta _n\varphi _i$ for every $i<n$ .

3. (iii) $\varphi _i\wedge \varphi _j\rightarrow \bot \in L$ whenever $i\neq j<n$ . This follows from $(\sharp )$ .

4. (iv) If $w_iRw_j$ , then $\varphi _i\rightarrow \Diamond \varphi _j \in L$ . This follows from $(\sharp )$ .

Suppose $\mathfrak G=(U,T)\in \mathsf {Fr}_g(L)$ . By (i) and Lemma 3.6, $|U|\leq n$ . By (ii) and (iii), for every $i<n$ , there exists $u\in U$ with $\mathfrak G,u\models \varphi _i\wedge \bigwedge _{j\neq i}\neg \varphi _j$ . Hence $|U|=n$ . Let $U=\{u_0,\ldots ,u_{n-1}\}$ . Without loss of generality, let $\mathfrak G,u_i\models \varphi _i$ for each $i<n$ . Let $f:W\rightarrow U$ be the function with $f(w_i)=u_i$ for each $i<n$ . Clearly f is bijective. Assume $w_iRw_j$ . By (iv), $\varphi _i\rightarrow \Diamond \varphi _j\in L$ . Since $\varphi _i$ holds only in $u_i$ and $\varphi _j$ holds only in $u_j$ , we have $u_iTu_j$ . Similarly $u_iTu_j$ implies $w_iRw_j$ . Then $\mathfrak F\cong \mathfrak G$ . Hence $|\mathsf {Fr}_g(L)|=1$ .

Theorem 4.12 (The second Post-completeness theorem).

Let $L\in \mathsf {TAB}$ . Then L is Post-complete if and only if $|\mathsf {Fr}_g(L)|=1$ .

Proof. Let $L\in \mathsf {TAB}$ . Assume $|\mathsf {Fr}_g(L)|=1$ . Suppose $L\subseteq L'$ where $L'$ is a consistent tense logic. By Lemma 3.9(1), $L'$ is tabular. By Lemma 3.8, $L'$ is Kripke-complete and so $L'=Th(\mathsf {Fr}_g(L'))$ . Clearly $\mathsf {Fr}_g(L')\subseteq \mathsf {Fr}_g(L)$ . Then $L= Th(\mathsf {Fr}_g(L))\subseteq Th(\mathsf {Fr}_g(L'))=L'$ . Hence $L=L'$ . It follows that $L\in \mathsf {PC}$ . The other way round, assume $L\in \mathsf {PC}$ . Since $L\in \mathsf {TAB}$ , there exists a finite frame $\mathfrak F=(W,R)$ with $L=Th(\mathfrak F)$ . Let $w\in W$ . By [9, Proposition 2.3], $Th(\mathfrak F)\subseteq Th(\mathfrak F_w)$ . Since $L\in \mathsf {PC}$ , $L=Th(\mathfrak F)= Th(\mathfrak F_w)$ . By Lemma 4.11, $|\mathsf {Fr}_g(L)|=1$ .

The second Post-completeness theorem gives a new characterization of Post-completeness in $\mathsf {TAB}$ . Consider frames in Figure 2 and their tense logics which are tabular. Note that $\mathsf {Fr}_g(L_i)=\{\mathfrak {H}_i\}$ for $i=1,2,3$ , and $\mathsf {Fr}_g(L_4)=\{\mathfrak {H}_2,\mathfrak {H}_4\}$ . Then $L_1,L_2, L_3\in \mathsf {PC}$ and $L_4\not \in \mathsf {PC}$ .

5 Post-completeness in $\Lambda (\mathsf {K}_t)$

In this section, we explore the Post-completeness in the lattice $\Lambda (\mathsf {K}_t)$ and prove the third Post-completeness theorem (Theorem 5.3). Note that Theorem 4.9 gives a characterization of the Post-completeness of $Th(\mathfrak F)$ where $\mathfrak F$ is a finite point-generated frame. We first show that there exists a Post-complete tense logic which has no finite frames. In what follows, the $0$ -general frame based on a frame $\mathfrak F=(W,R)$ is defined as $\mathfrak F^\clubsuit =(W, R, A^\clubsuit )$ where $A^\clubsuit = \{V(\varphi ):\varphi \in { \mathscr {L}_t^0}\}$ for arbitrary valuation V in $\mathfrak F$ . The definition of $A^\clubsuit $ does not depend on the choice of valuation V.

Proposition 5.1. Let $\mathfrak {N}=(\omega ,<)$ where $<$ is the strict natural order on $\omega $ . Let $L=Th(\mathfrak {N}^\clubsuit )$ . Then $\mathsf {Fr}^{<\aleph _0}(L)=\varnothing $ and L is Post-complete.

Proof. Assume $\mathfrak F\models L$ and $\mathfrak F=(W,R)$ . Clearly $\blacklozenge \blacksquare \bot \vee \blacksquare \bot \in L$ . It is easy to verify that $\mathfrak {N}^\clubsuit ,0\models \Diamond (\blacklozenge ^n\top \wedge \blacksquare ^{n+1}\bot )$ for all $n\in \omega $ , and $\mathfrak {N}^\clubsuit ,m\not \models \blacksquare \bot $ for all $m>0$ . Then $\{\blacksquare \bot \rightarrow \Diamond (\blacklozenge ^n\top \wedge \blacksquare ^{n+1}\bot ):n\in \omega \}\subseteq L$ . By $\mathfrak F\models L$ , we have $\mathfrak F\models \blacklozenge \blacksquare \bot \vee \blacksquare \bot $ . Then for every $n\in \omega $ , $\{w\in W : \mathfrak {F},w\models \blacklozenge ^n\top \wedge \blacksquare ^{n+1}\bot \}\neq \varnothing $ . We choose a set $\{w_n:n\in \omega \}\subseteq W$ such that (i) $\mathfrak F,w_n\models \blacklozenge ^n\top \wedge \blacksquare ^{n+1}\bot $ for each $n\in \omega $ ; and (ii) for every $i,j\in \omega $ , $w_i=w_j$ if and only if $i=j$ . Then $\aleph _0=|\{w_n:n\in \omega \}|\leq |W|$ , i.e., $\mathfrak F$ is infinite. It follows that $\mathsf {Fr}^{<\aleph _0}(L)=\varnothing $ .

Assume $\varphi \not \in L$ . Then $\mathfrak {N}^\clubsuit ,V,w\models \neg \varphi $ for some admissible valuation V in $\mathfrak {N}^\clubsuit $ and $w\in W$ . Let $var(\varphi )=\{p_1,\ldots ,p_n\}$ . For every $p\in var(\varphi )$ , we choose a constant formula $\psi _p\in { \mathscr {L}_t^0}$ with $V(p)=V(\psi _p)$ . Let s be a substitution with $s(p_k)=\psi _{p_k}$ for each $1\leq k\leq n$ . Then $\mathfrak {N}^\clubsuit ,w\models \neg \varphi ^s$ and $\blacksquare \bot \rightarrow (\Diamond \neg \varphi ^s\vee \neg \varphi ^s)\in L$ . Suppose that $L\oplus \varphi $ is consistent. Then $\mathbb {F}\models L\oplus \varphi $ for some descriptive frame $\mathbb {F}$ . By $\mathbb {F}\models L$ , we have $\mathbb {F},w_0\models \blacksquare \bot $ for some $w_0\in W$ . By $\blacksquare \bot \rightarrow (\Diamond \neg \varphi ^s\vee \neg \varphi ^s)\in L$ , we have $\mathbb {F},u\models \neg \varphi ^s$ for some $u\in W$ . Then $\mathbb {F}\not \models \varphi $ which contradicts $\mathbb {F}\models L\oplus \varphi $ . Then $L\oplus \varphi $ is not consistent. Hence $L\in \mathsf {PC}$ .

Lemma 5.2. Let $\mathfrak F=(W,R)$ be a frame and $L=Th(\mathfrak {F}^\clubsuit )$ . For every formula $\varphi \in \mathscr {L}_t$ , if $\varphi \not \in L$ , then $\varphi ^s\not \in L$ for some $s\in \mathsf {CS}$ .

Proof. Assume $\varphi \not \in L$ . Then $\mathfrak {F}^\clubsuit ,V,w\models \neg \varphi $ for some $w\in W$ and admissible valuation V in $\mathfrak F^\clubsuit $ . For each $p\in \Phi $ , we choose $\psi _p\in { \mathscr {L}_t^0}$ with $V(p)=V(\psi _p)$ . Let s be the constant substitution with $s(p)=\psi _p$ for each $p\in \Phi $ . Then $\mathfrak F^\clubsuit ,w\models \neg \varphi ^s$ . By $\mathfrak F^\clubsuit \models L$ , we have $\varphi ^s\not \in L$ .

Theorem 5.3 (The third Post-completeness theorem).

A consistent tense logic L is Post-complete if and only if the following conditions hold:

1. (1) For every $\psi \in \mathscr {L}_t^0$ , if $\neg \psi \not \in L$ , then $\Delta _n\psi \in L$ for some $n\in \omega $ .

2. (2) For every $\varphi \in \mathscr {L}_t$ , if $\varphi \not \in L$ , then $\varphi ^s\not \in L$ for some $s\in \mathsf {CS}$ .

Proof. Assume $L\in \mathsf {PC}$ . For (1), suppose that there exists $\psi \in { \mathscr {L}_t^0}$ such that $\neg \psi \not \in L$ and $\Delta _n\psi \not \in L$ for all $n\in \omega $ . Now we show that $\Sigma =\{\nabla _n\neg \psi :n\in \omega \}$ is L-consistent. Suppose not. There exist $n_1,\ldots ,n_k\in \omega $ with $\neg (\nabla _{n_1}\neg \psi \wedge \cdots \wedge \nabla _{n_k}\neg \psi )\in L$ , i.e., $\Delta _{n_1}\psi \vee \cdots \vee \Delta _{n_k}\psi \in L$ . Clearly, if $1\leq i\leq j\leq k$ , then $\Delta _{n_i}\psi \to \Delta _{n_j}\psi \in L$ . Let $h=max\{n_1,\ldots ,n_k\}$ . Then $\Delta _h\psi \in L$ which contradicts $\Delta _h\psi \not \in L$ . Hence $\Sigma $ is L-consistent. Let $w$ be a maximal L-consistent set with $\Sigma \subseteq w$ . Then $\mathbb {F}^L_w\models L$ . By $\mathbb {F}^L_w\models \Sigma $ , we have $\mathbb {F}^L_w\models \neg \psi $ . Hence $\mathbb {F}^L_w\models L\oplus \neg \psi $ . Then $L\subsetneq Th(\mathbb {F}^L_w)$ which contradicts $L\in \mathsf {PC}$ . For (2), $Th(\mathbb {F}^L)\subseteq Th((\mathfrak F^L)^\clubsuit )$ . By $L\in \mathsf {PC}$ , $L=Th(\mathbb {F}^L)\subseteq Th((\mathfrak F^L)^\clubsuit )=L$ . By Lemma 5.2, (2) holds.

Assume $L\not \in \mathsf {PC}$ . For a contradiction, suppose that both (1) and (2) hold. By the assumption, there exists a formula $\varphi \not \in L$ such that $L'=L\oplus \varphi $ is consistent. By $\varphi \not \in L$ and (2), $\varphi ^s\not \in L$ for some $s\in \mathsf {CS}$ . Then $\neg \neg \varphi ^s\not \in L$ . By (1), $\Delta _n\neg \varphi ^s\in L$ for some $n\in \omega $ . Then $\Delta _n\neg \varphi ^s\in L'$ . By $\varphi ^s\in L'$ , we have $\nabla _n\varphi ^s\in L'$ which contradicts $\Delta _n\neg \varphi ^s\in L'$ .

Corollary 5.4. If $\mathfrak F=(W,R)$ is a finite point-generated frame, then $Th(\mathfrak F^\clubsuit )$ is Post-complete.

Proof. Let $\mathfrak F=(W,R)$ be finite point-generated. It suffices to show that the conditions (1) and (2) in Theorem 5.3 hold. For (1), assume $\psi \in \mathscr {L}_t^0$ and $\neg \psi \not \in Th(\mathfrak F^\clubsuit )$ . Then there exists $w\in W$ with $\mathfrak F^\clubsuit ,w\not \models \neg \psi $ . Then $\mathfrak F^\clubsuit , w\models \psi $ . Let $n=|W|$ . Then $\mathfrak F^\clubsuit \models \Delta _n\psi $ . Moreover, (2) follows from Lemma 5.2.

Corollary 5.5. Let $\mathfrak F=(W,R)$ be a point-generated frame. If $W=S^n(\mathfrak F, w)$ for some $w\in W$ and $n\in \omega $ , then $Th(\mathfrak F^\clubsuit )$ is Post-complete.

Proof. Assume $W=S^n(\mathfrak F, w)$ with $w\in W$ and $n\in \omega $ . It suffices to show that the conditions (1) and (2) in Theorem 5.3 hold. For (1), assume $\psi \in \mathscr {L}_t^0$ and $\neg \psi \not \in Th(\mathfrak F^\clubsuit )$ . Then $\mathfrak F^\clubsuit ,u\models \psi $ for some $u\in W$ . By the assumption, $w\in S^m(\mathfrak {F}, u)$ for some $m\leq n$ . Then $S^{m+n}(\mathfrak F, u)=W$ which yields $\Delta _{n+m}\psi \in Th(\mathfrak F^\clubsuit )$ . Note that (2) follows from Lemma 5.2.

Remark 5.6. Kracht [7, Corollary 16] claims that every extension of $\mathsf {K}_t\mathsf {4}$ of finite codimension is complete and of finite alternativity. This claim is incorrect since Thomason [16] gives a tense logic of codimension 1 in $\Lambda (\mathsf {K}_t\mathsf {4})$ which is Kripke incomplete (cf., e.g., [8, Theorem 7.9.1]). Here we give another counterexample. Consider the general frame $\mathfrak {N}^\clubsuit $ in Proposition 5.1. Actually $Th(\mathfrak {N}^\clubsuit )\in \Lambda (\mathsf {K}_t\mathsf {4})$ is of codimension 1. Since $\mathfrak {N}$ is transitive and has no infinite descending chain, we have $\mathfrak {N}^\clubsuit \models \blacksquare (\blacksquare p\to p)\to \blacksquare p$ . For every $\varphi \in \mathscr {L}_t^0$ , $V(\varphi )\in A^\clubsuit $ is either finite or cofinite. Then $\mathfrak {N}^\clubsuit \models \neg (\Diamond p\wedge \Box (p\to \Diamond (\neg p\wedge \Diamond p)))$ . Every transitive frame validating $\neg (\Diamond p\wedge \Box (p\to \Diamond (\neg p\wedge \Diamond p)))$ does not contain infinite ascending chains. Every frame validating $\blacksquare (\blacksquare p\to p)\to \blacksquare p$ is irreflexive. Then for every $\mathfrak F\in \mathsf {Fr}(Th(\mathfrak {N}^\clubsuit ))$ , $\mathfrak F\models \Diamond \top \to \Diamond \Box \bot $ . Clearly $\mathfrak {N}^\clubsuit \not \models \Diamond \top \to \Diamond \Box \bot $ . Hence $Th(\mathfrak {N}^\clubsuit )$ is Kripke incomplete and so it is a counterexample for Kracht’s claim. Furthermore, by checking Kracht’s proof, we find that it is based on the following claims:

1. (K1) If $L\in \Lambda (\mathsf {K}_t\mathsf {4})$ is of finite codimension, then $L_+$ is tabular.

2. (K2) For all $S\in \Lambda (\mathsf {K})$ and $L\in \Lambda (\mathsf {K}_t)$ , $S\subseteq L_+$ if and only if $S^+\subseteq L$ .

Here the operations $(.)_+$ and $(.)^+$ are explained in the section of introduction. Note that (K2) holds. This is shown as follows. If $S\subseteq L_+ \subseteq L$ , then $S\subseteq L$ and so $S^+\subseteq L$ . Assume $S^+\subseteq L$ . Let $\varphi \in S$ . Then $\varphi \in S^+\subseteq L$ and so $\varphi \in L\cap \mathscr {L}_\Box =L_+$ . Hence $S\subseteq L_+$ . However (K1) is incorrect. For a contradiction, suppose (K1) holds. Consider again the Post-complete logic $L=Th(\mathfrak {N}^\clubsuit )$ . Obviously ${Alt}^F_n\not \in L$ for every $n\in \omega $ . Then $L\oplus \mathrm {Alt}^F_n= \mathscr {L}_t$ for all $n\in \omega $ . By (K1), $L_+$ is tabular. Then $\mathsf {K}\oplus \mathsf {alt}_m\subseteq L_+$ for some $m\in \omega $ . By (K2), $\mathsf {K}_t\oplus \mathrm {Alt}^F_m=(\mathsf {K}\oplus \mathsf {alt}_m)^+\subseteq L$ which is impossible. Hence (K1) does not hold.

Using the third Post-completeness theorem and its consequences, we can show some results on the Post number of some tense logics. Recall that the Post number $\mathsf {PN}(L)$ of a tense logic L is the number of Post-complete extensions of L. For tense logics $L_1$ and $L_2$ , if $L_1\subseteq L_2$ , then $\mathsf {PN}(L_2)\leq \mathsf {PN}(L_1)$ and so $\mathsf {PN}(L_1)=2^{\aleph _0}$ implies $\mathsf {PN}(L_2)=2^{\aleph _0}$ . We consider tense logics in Table 1.

Table 1 Some tense logics.

Proposition 5.7. $\mathsf {PN}(\mathsf {K}_t\mathsf {D}^+\mathsf {4})=\mathsf {PN}(\mathsf {K}_t\mathsf {D}^-\mathsf {4})=2^{\aleph _0}$ and hence $\mathsf {PN}(\mathsf {K}_t\mathsf {D}^+)=\mathsf {PN}(\mathsf {K}_t\mathsf {D}^-) = \mathsf {PN}(\mathsf {K}_t\mathsf {4})=2^{\aleph _0}$ .

Proof. (1) $\mathsf {PN}(\mathsf {K}_t\mathsf {D}^+\mathsf {4})=2^{\aleph _0}$ . For every subset $I\subseteq \omega \setminus \{0,1\}$ , let $I^* = \{i^\ast :i\in I\}$ . Let $\mathfrak F_I=(W_I, R_I)$ be the frame where $W_I=\omega \cup I^\ast $ and $R_I=\{(n,m)\in \omega \times \omega : n<m\}\cup \{(n^\ast ,m)\in I^\ast \times \omega :n\leq m\}$ . Clearly $S^2(\mathfrak F_I,0)=W_I$ for every $I\subseteq \omega $ . (Examples of frames $\mathfrak {F}_\varnothing , \mathfrak F_{\{2,5\}}$ and $\mathfrak F_{\mathbb {P}}$ where $\mathbb {P}$ is the set of prime numbers are presented in Figure 3.) For every $I\subseteq \omega $ , let $L_I=Th(\mathfrak F_I^\clubsuit )$ . Note that, for every frame $\mathfrak F=(W, R)$ , $\mathfrak F\models \mathsf {K}_t\mathsf {D}^+\mathsf {4}$ if and only if $R(w)\neq \varnothing $ and $R(R(w))\subseteq R(w)$ for all $w\in W$ . Obviously $\mathfrak F_I^\clubsuit \models \mathsf {K}_t\mathsf {D}^+\mathsf {4}$ . Then $L_I\in \Lambda (\mathsf {K}_t\mathsf {D}^+\mathsf {4})$ for every $I\subseteq \omega $ . By Corollary 5.5, $L_I$ is Post-complete. It suffices to show that $L_I\neq L_J$ when $I\neq J$ . Assume $I\neq J$ . Let $i\in I\setminus J$ without loss of generality. By $\mathfrak F^\clubsuit _I,i\models \blacksquare ^{i+1}\bot $ and $i^*R_Ii$ , we have $\mathfrak F^\clubsuit _I,i^*\models \Diamond \blacksquare ^{i+1}\bot $ . Clearly $R_I(i^*)=\{k\in \omega :k\geq i\}$ . Then $\mathfrak F^\clubsuit _I,k\models \blacklozenge ^i\top $ for each $k\in R_I(i^*)$ . Note that $\breve {R_I}(i^*)=\varnothing $ . Then $\mathfrak F^\clubsuit _I,i^*\models \blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top $ . By $S^2(\mathfrak F_I,i^*)=W_I$ , we have $\Delta _2(\blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top )\in L_I$ . Suppose that there exists $v\in W_J$ with $\mathfrak F^\clubsuit _J,v\models \blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top $ . Then $\breve {R_J}(v)=\varnothing $ which yields $v\in J^*\cup \{0\}$ . Assume $v=j^*$ for some $j>i$ . Then $R_J(v)\subseteq \{l\in \omega :l>i\}$ and so $\mathfrak F^\clubsuit _J,v\not \models \Diamond \blacksquare ^{i+1}\bot $ . Thus $v\in \{l^*:l<i\}\cup \{0\}$ . Note that $\mathfrak F^\clubsuit _J,i-1\models \blacksquare ^i\bot $ and $uR_J(i-1)$ for all $u\in \{l^*:l<i\}\cup \{0\}$ . Then $\mathfrak F^\clubsuit _J,v\not \models \Box \blacklozenge ^i\top $ which contradicts $\mathfrak F^\clubsuit _J,v\models \Box \blacklozenge ^i\top $ . Hence $\mathfrak F^\clubsuit _J\models \neg (\blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top )$ . Then $\nabla _2\neg (\blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top )\in L_J$ and $\Delta _2(\blacksquare \bot \wedge \Diamond \blacksquare ^{i+1}\bot \wedge \Box \blacklozenge ^{i}\top )\in L_I\setminus L_J$ . Hence $L_I\neq L_J$ .

(2) $\mathsf {PN}(\mathsf {K}_t\mathsf {D}^-\mathsf {4})=2^{\aleph _0}$ . The proof is similar to (1). It suffices to observe that $\mathfrak F_I=(W_I, \breve {R_I})$ is a frame for $\mathsf {K}_t\mathsf {D}^-\mathsf {4}$ .

Fig. 3 Frames $\mathfrak {F}_\varnothing , \mathfrak F_{\{1,5\}}$ and $\mathfrak F_{\mathbb {P}}$ .

Proposition 5.8. For every $0<\kappa \leq \aleph _0$ , there exists a consistent tense logic $L\in \Lambda (\mathsf {K}_t)$ such that $\mathsf {PN}(L)=\kappa $ .

Proof. For every $0<j< \aleph _0$ , let $\mathfrak {C}_j = (\{0,\ldots , j-1\},\{\langle i,i+1 \rangle :i<j\})$ be the chain of j elements. By [9, Theorem 4.8], $Th(\mathfrak {C}_j)\in \mathsf {PC}$ . For every $0< n< \aleph _0$ , let $\mathcal {C}_n=\{\mathfrak {C}_i:1\leq i\leq n\}$ and $L_n=Th(\mathcal {C}_n)$ . By [9, Theorem 4.22], $\Lambda (L_n)\cap \mathsf {PC}=\{Th(\mathfrak {C}_i):1\leq i\leq n\}$ . By [9, Corollary 4.5], $Th(\mathfrak {C}_i)\neq Th(\mathfrak {C}_j)$ for $1\leq i\neq j\leq n$ . Hence $\mathsf {PN}(L_n)=n$ . By [9, Theorem 4.24], $\mathsf {PN}(T_{1,1})=\aleph _0$ .

Remark 5.9. In the proof of Proposition 5.8, all frames $\mathfrak {C}_j$ with $2<j<\aleph _0$ are intransitive and hence not finite frames for the tense logic of linear time $\mathsf {Lin}_t$ containing the transitivity axioms $\Box p\to \Box \Box p$ and linearity axioms $\mathsf {.3}$ formulated for $\Box $ and $\blacksquare $ . Wolter [21] gives a description of the lattice $\Lambda (\mathsf {Lin}_t)$ and proves that all logics in this lattice are independently axiomatizable. One could prove results on the Post numbers of tense logics in $\Lambda (\mathsf {Lin}_t)$ .

Proposition 5.10. $\mathsf {PN}(\mathsf {K}_t\mathsf {D})=\mathsf {PN}(\mathsf {K}_t\mathsf {T})=1$ and $\mathsf {PN}(\mathsf {K}_t\mathsf {B})=2$ .

Proof. (1) Let $L\in \mathsf {PC}\cap \Lambda (\mathsf {K}_t\mathsf {D})$ . Let $\mathbb {F}=(W,R,A)$ be a general frame with $\mathbb {F}\models L$ . Then $\mathbb {F}\models \Diamond \top $ . Hence $R(w)\neq \varnothing $ for every $w\in W$ . Let $\mathbb {F}_\circ =(\{\circ \},\{(\circ ,\circ )\},\{\varnothing ,\{\circ \}\})$ . Let $f:W\to \{\circ \}$ be the function with $f(w)=\circ $ for all $w\in W$ . Clearly f is a bounded morphism from $\mathbb {F}$ to $\mathbb {F}_\circ $ . Then $\mathbb {F}_\circ \models L$ . Hence $L=Th(\mathbb {F}_\circ )=\mathsf {K}_t\oplus p\leftrightarrow \Box p$ . Then $\mathsf {PN}(\mathsf {K}_t\mathsf {D})=1$ . By $\mathsf {K}_t\mathsf {D}\subseteq \mathsf {K}_t\mathsf {T}$ , $\mathsf {PN}(\mathsf {K}_t\mathsf {T})=1$ .

(2) Let $L\in \mathsf {PC}\cap \Lambda (\mathsf {K}_t\mathsf {B})$ . Let $\mathbb {F}=(W,R,A)$ be a point-generated general frame with $\mathbb {F}\models L$ . Then $L=Th(\mathbb {F})$ . Suppose $R=\varnothing $ . Then $W=\{\bullet \}$ and $A=\{\varnothing , \{\bullet \}\}$ . Hence $L=\mathsf {K}_t\oplus \Box \bot $ . Suppose $R\neq \varnothing $ . Then $R(w)\cup \breve {R}(w)\neq \varnothing $ for every $w\in W$ . Clearly $\Diamond \top \leftrightarrow \blacklozenge \top \in \mathsf {K}_t\mathsf {B}\subseteq L$ . It follows that $R(w)\neq \varnothing $ and $\breve {R}(w)\neq \varnothing $ for every $w\in W$ . Hence $\Diamond \top ,\blacklozenge \top \in L$ , i.e., $\mathsf {K}_t\mathsf {D}\subseteq L$ . By the proof of (1), $L=\mathsf {K}_t\oplus p\leftrightarrow \Box p$ . It follows that $\mathsf {PN}(\mathsf {K}_t\mathsf {B})=2$ .

6 Concluding remarks

The present work contributes a series of results on tabularity and Post-completeness in tense logic. A new characterization of tabularity, two characterization theorems on Post-completeness in tabular tense logics, and a characterization of Post-completeness in the lattice of all tense logics are established. The Post numbers of some tense logics are determined. There are many problems which need to be explored. We list here some of them.

The first problem concerns the pretabularity in tense logic. It is well-known that there are exactly five pretabular normal modal logics over $\mathsf {S4}$ [12]; and there are $2^{\aleph _0}$ pretabular normal modal logics over $\mathsf {K4}$ [2]. By [9], there are infinitely many pretabular tense logics in $\Lambda (T_{n,m})$ with $nm\geq 2$ . The general question is to find the number of pretabular logics in $\Lambda (L)$ for a tense logic L. An additional problem concerns if there exists a polynomial time algorithm for deciding the Post-completeness of tabular tense logics (cf. Corollary 4.10).

The second problem concerns Post numbers of tense logics. In Section 5, we give Post numbers of some tense logics. An interesting problem is to characterize the set of tense logics $\{L\in \Lambda (\mathsf {K}_t): \mathsf {PN}(L)=\kappa \}$ for a given cardinal $\kappa \leq 2^{\aleph _0}$ . Moreover, the decidability of $\mathsf {PC}$ is not known.

The third problem concerns the classification of tense logics $\Lambda (\mathsf {K}_t)$ . Makinson’s classification theorem in [10] states that, for every consistent normal modal logic L, if $\Diamond \top \in L$ , then $L\subseteq \mathsf {K}\oplus \Box p\leftrightarrow p$ ; and if $\Diamond \top \not \in L$ , then $L\subseteq \mathsf {K}\oplus \Box \bot $ . Here the formula $\Diamond \top $ is called the critical formula for $\Lambda (\mathsf {K})$ . The possibility of finding critical formulas for lattices of tense logics needs to be explored.