FINITE AXIOMATIZABILITY OF TRANSITIVE MODAL LOGICS OF FINITE DEPTH AND WIDTH WITH RESPECT TO PROPER-SUCCESSOR-EQUIVALENCE

Abstract

This paper proves the finite axiomatizability of transitive modal logics of finite depth and finite width w.r.t. proper-successor-equivalence. The frame condition of the latter requires, in a rooted transitive frame, a finite upper bound of cardinality for antichains of points with different sets of proper successors. The result generalizes Rybakov’s result of the finite axiomatizability of extensions of $\mathbf {S4}$ of finite depth and finite width.

1 Introduction

This paper presents a study of the finite axiomatizability of transitive modal logics, or simply transitive logic, of finite depth and finite width w.r.t. proper-successor-equivalence. A transitive logic is of finite depth if it contains $\mathsf {B}_{n}$ (see Section 2) for some $n\geqslant 1$ , is of finite width if it contains $\mathsf {Wid}_{n}$ below for some $n\geqslant 1$ , and is of finite width w.r.t. proper-successor-equivalence, or simply, of finite suc-eq-width, if it contains $\mathsf {Wid}_{n}^{\ast }$ below for some $n\geqslant 1$ . For all $i,j\in \omega $ , let us fix $\theta _{i,j}=\Diamond (p_{i}\wedge \Box (\Diamond p_{i}\vee q_{j}))$ , and for each $n\geqslant 1$ , let

$$ \begin{align*} \mathsf{Wid}_{n} & ={ {\textstyle\bigwedge\nolimits_{0\leqslant i\leqslant n}} }\Diamond p_{i}\rightarrow{ {\textstyle\bigvee\nolimits_{0\leqslant i\neq j\leqslant n}} }\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))\text{,}\\ \mathsf{Wid}_{n}^{\ast} & ={ {\textstyle\bigwedge\nolimits_{0\leqslant i\leqslant n}} }\Diamond(p_{i}\wedge\Box q_{i})\rightarrow{ {\textstyle\bigvee\nolimits_{0\leqslant i\neq j\leqslant n}} (}\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j}))\vee(\theta_{i,j}\wedge \theta_{j,i}))\text{.} \end{align*} $$

It can be shown that $\mathsf {Wid}_{n}^{\ast }\in \mathbf {K}\oplus \mathsf {Wid}_{n}$ for each $n\geqslant 1$ , and hence each transitive logic of finite depth and finite width is an extension of a transitive logic of finite depth and finite suc-eq-width. The frame condition for $\mathsf {Wid}_{n} ^{\ast }$ resembles that for $\mathsf {Wid}_{n}$ . Within rooted transitive frames, $\mathsf {Wid}_{n}$ corresponds to the condition that each antichain is of cardinality at most n (see Proposition 2.5), whereas $\mathsf {Wid}_{n}^{\ast }$ corresponds to the condition that each antichain of points with different sets of proper successors is of cardinality at most n (see Proposition 3.1).

It is well known (see [9, theorem 6.6]) that all transitive logics of finite depth have the finite model property. Rybakov proved (see [8, theorem 1]) that if a superintuitionistic logic $\mathbf {L}$ is tabular, then all extensions of $\tau \mathbf {L}$ are finitely axiomatizable, where $\tau \mathbf {L}$ is the least modal companion of $\mathbf {L}$ . A superintuitionistic logic is tabular iff it is of finite width and finite depth (see, e.g., [2, corollary 12.2]). Therefore, all modal companions of a superintuitionistic logic of finite width and depth are finitely axiomatizable, which gives that all extensions of $\mathbf {S4}$ containing axioms of finite depth and finite width are finitely axiomatizable. In this paper, we generalize this result and prove the finite axiomatizability of transitive logics of finite depth and finite suc-eq-width. Among others, this result also implies the finite axiomatizability of transitive logics of finite depth and finite width, the finite axiomatizability of transitive logics of depth at most 2, the finite axiomatizability of weakly convergent transitive logics of depth at most 3, etc.

The rest of the paper is organized as follows. Section 2 provides preliminary notions and facts. Section 3 gives the frame conditions of finite suc-eq-width axioms and a new construction built upon the skeletons of transitive frames. Section 4 provides criteria for all extensions of a modal logic to be finitely axiomatizable. Section 5 discusses well quasi-orders on lists. Section 6 proves the main theorem, i.e., the finite axiomatizability of all transitive logics of finite depth and suc-eq-width. Finally, we apply the main theorem to obtain further results and offer some final remarks in Section 7.

2 Preliminary notions

Modal formulas are built up from propositional letters $p_{0},p_{1},\ldots $ and the constant $\bot $ , using truth-functional operators $\rightarrow ,\wedge ,\vee $ and the necessity operator $\Box $ . We will simply call them formulas. As usual, $\lnot \phi $ is the abbreviation for $\phi \rightarrow \bot $ and $\Diamond \phi $ for $\lnot \Box \lnot \phi $ . A normal modal logic is a set of modal formulas that contains all truth-functional tautologies and $\Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)$ , and is closed under modus ponens, substitution and necessitation. As usual, we use $\mathbf {K}$ ( $\mathbf {K4}$ ) for the smallest normal modal logic (containing $\Box p\rightarrow \Box \Box p$ ). For each normal modal logic $\mathbf {L}$ , a normal extension of $\mathbf {L}$ is a normal modal logic $\mathbf {L}^{\prime }$ such that $\mathbf {L}\subseteq \mathbf {L}^{\prime }$ ; we use $\mathsf {NExt}\mathbf {L}$ for the lattice of all normal extensions of $\mathbf {L}$ . Transitive logics are logics in $\mathsf {NExt} \mathbf {K4}$ . All logics we deal with in this paper are normal modal logics, and thus we will drop “normal,”and simply speak of modal logics and their extensions. Let $\mathbf {L}$ be any modal logic. For each set $\Delta $ of formulas, $\mathbf {L}\oplus \Delta $ is the smallest modal logic including $\mathbf {L}\cup \Delta $ ; and for each formula $\phi $ , $\mathbf {L}\oplus \phi =\mathbf {L}\oplus \{\phi \}$ . A modal logic $\mathbf {L}^{\prime }$ is finitely axiomatizable over $\mathbf {L}$ if $\mathbf {L}^{\prime }=\mathbf {L}\oplus \Delta $ for a finite $\Delta $ , and is finitely axiomatizable if it is finitely axiomatizable over $\mathbf {K}$ .

Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any frame with $w\in W$ , and let $\mathfrak {M}$ be any model on $\mathfrak {F}$ . For each formula $\phi $ , we use $\mathfrak {M},w\vDash \phi $ for that $\mathfrak {M}$ satisfies $\phi $ at w, $\mathfrak {M}\vDash \phi $ for that $\phi $ is globally or universally true in $\mathfrak {M}$ ( $\mathfrak {M}$ is a model for $\phi $ ), and $\mathfrak {F}\vDash \phi $ for that $\phi $ is valid in $\mathfrak {F}$ ( $\mathfrak {F}$ is a frame for $\phi $ ); for any set $\Delta $ of formulas, $\Delta $ is valid in $\mathfrak {F}$ ( $\mathfrak {F}$ is a frame for $\Delta $ ) if each member of $\Delta $ is valid in $\mathfrak {F}$ . Let $\mathscr {C}$ be a class of frames (models). $\mathscr {C}\vDash \phi $ if each member of $\mathscr {C}$ is a frame (model) for $\phi $ ; the logic of $\mathscr {C}$ is $\mathbf {Log}(\mathscr {C})=\{\phi :\mathscr {C}\vDash \phi \}$ , and we write $\mathbf {Log}(\mathfrak {F})$ instead of $\mathbf {Log}(\{\mathfrak {F}\})$ ; a modal logic $\mathbf {L}$ is characterized by the class $\mathscr {C}$ if $\mathbf {L}=\mathbf {Log}(\mathscr {C})$ . A modal logic has the finite model property (f.m.p.) if it is characterized by some class of finite models.

Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any frame. For all $u,v\in W$ , let $\vec {R}uv$ iff $Ruv$ but not $Rvu$ . For all $u,v\in W$ , when $Ruv$ , we say that u sees v, and call v a successor of u; and when $\vec {R}uv$ , we call v a proper successor of u, and u a proper predecessor of v. For each $X\subseteq W$ , let $\left. X\right \uparrow _{R}=\{v:Ruv$ for a $u\in X\}$ , $\left. X\right \downarrow _{R}=\{v:Rvu$ for a $u\in X\}$ , $\left. X\right \uparrow _{R}^{-}=\left. X\right \uparrow _{R}-X$ and $\left. X\right \downarrow _{R}^{-}=\left. X\right \downarrow _{R}-X$ . When R is clear from the context, we drop “ $_{R}$ ” and use “ $\left. X\right \uparrow $ ” and “ $\left. X\right \downarrow , $ ” etc. For each $w\in W$ , let $\left. w\right \uparrow =\{w\}{\uparrow }$ , $\left. w\right \downarrow =\{w\}{\downarrow }$ , $\left. w\right \uparrow ^{-}=\{w\}{\uparrow }^{-}$ and $\left. w\right \downarrow ^{-}=\{w\}{\downarrow }^{-}$ .

We assume the reader’s familiarity with disjoint unions, subframes and submodels, generated subframes and submodels, reductions (or p-morphisms), and with the related theorems on preservation of validity or truth under these frame or model constructions. For each family $\{\mathfrak {F}_{i}\}_{i\in I}$ of pairwise disjoint frames, we use $\biguplus _{i\in I}\mathfrak {F}_{i}$ for the disjoint union of $\{\mathfrak {F}_{i}\}_{i\in I}$ . Let $\mathfrak {F} =\left \langle W,R\right \rangle $ and $\mathfrak {G}=\left \langle U,S\right \rangle $ be any frames. When $\mathfrak {F}$ and $\mathfrak {G}$ are disjoint, let $\mathfrak {F}\oplus \mathfrak {G}=\left \langle V,Q\right \rangle $ where $V=W\cup U$ and $Q=R\cup S\cup \{\left \langle u,v\right \rangle :u\in W$ and $v\in U\}$ . For each nonempty $X\subseteq W$ , we use $\mathfrak {F} \upharpoonright X$ for the restriction of $\mathfrak {F}$ to X. A function f from W onto U is a reduction (or p-morphism) from $\mathfrak {F}$ to $\mathfrak {G}$ if the following conditions hold for all $x,y\in W$ :

1. (i) If $Rxy$ , then $Sf(x)f(y)$ .

2. (ii) If $Sf(x)f(y)$ , then $\exists z\in U(Rxz\wedge f(y)=f(z))$ .

A function f reduces $\mathfrak {F}$ to $\mathfrak {G}$ when f is a reduction from $\mathfrak {F}$ to $\mathfrak {G}$ , and that $\mathfrak {F}$ is reducible to $\mathfrak {G}$ if there is a function reduces $\mathfrak {F}$ to $\mathfrak {G}$ .

Fact 2.1. Let $\mathfrak {F}=\biguplus _{i\in I}\mathfrak {F}_{i}$ and $\mathfrak {G} =\biguplus _{i\in I}\mathfrak {G}_{i}$ such that for each $i\in I$ , $f_{i}$ reduces $\mathfrak {F}_{i}$ to $\mathfrak {G}_{i}$ . Then $\bigcup _{i\in I}f_{i}$ reduces $\mathfrak {F}$ to $\mathfrak {G}$ .

Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be a transitive frame. Define on W an equivalence relation $\sim $ by taking: for all $x,y\in W$ , $x\sim y$ iff either $x=y$ , or $Rxy$ and $Ryx$ . A cluster in $\mathfrak {F}$ is an equivalence class modulo $\sim $ . For each $w\in W$ , we use $\mathbf {c}_{(w)}$ for the cluster in $\mathfrak {F}$ to which w belongs. Furthermore, for each cluster $\mathbf {c}$ in $\mathfrak {F}$ , $\mathbf {c}$ is degenerate if it is a singleton of an irreflexive point; $\mathbf {c}$ is nondegenerate if it is not degenerate; $\mathbf {c}$ is final if $\left. \mathbf {c}\right \uparrow ^{-}=\varnothing $ . The skeleton of $\mathfrak {F}$ is $\mathfrak {sk}(\mathfrak {F})=\left \langle \mathfrak {sk} (W),\preceq _{R}\right \rangle $ , where $\mathfrak {sk}(W)$ is the set of clusters in $\mathfrak {F}$ , and for all $\mathbf {c},\mathbf {d}\in \mathfrak {sk}(W)$ , $\mathbf {c}\preceq _{R}\mathbf {d}$ iff $Rwu$ for some $w\in \mathbf {c}$ and $u\in \mathbf {d}$ (in fact, iff $Rwu$ for all $w\in \mathbf {c}$ and $u\in \mathbf {d}$ ). We let $\mathbf {c}\prec _{R}\mathbf {d}$ iff $\mathbf {c}\preceq _{R}\mathbf {d}$ but $\mathbf {d}\npreceq _{R}\mathbf {c}$ (not $\mathbf {d}\preceq _{R}\mathbf {c}$ ). When R is clear from the context, we will drop “ $_{R}$ ,”and use $\preceq $ and $\prec $ respectively for $\preceq _{R}$ and $\prec _{R}$ . Let $k\geqslant 1$ . A point $u_{1}$ in $\mathfrak {F}$ is of rank greater than k if there is an $\vec {R}$ -chain $\{u_{1},\ldots ,u_{n}\}$ with $n>k$ , and is of rank k if there is an $\vec {R}$ -chain $\{u_{1},\ldots ,u_{k}\}$ and $u_{1}$ is not of rank greater than k. $\mathfrak {F}$ is of rank k if it contains a point of rank k but no point of rank greater than k, and $\mathfrak {F}$ is of finite rank if it is of rank k for some $k\geqslant 1$ , otherwise it is of infinite rank.

Fact 2.2. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any transitive frame, and let $\mathbf {c}$ and $\mathbf {d}$ be any points in $\mathfrak {sk}(\mathfrak {F})$ . Then the following hold:

1. (i) $\mathfrak {sk}(\mathfrak {F})$ is a transitive frame, and is of the same rank as $\mathfrak {F}$ is.

2. (ii) If $\mathfrak {F}$ is of finite rank and $\left. \mathbf {c} \right \uparrow ^{-}=\left. \mathbf {d}\right \uparrow ^{-}$ , then $\mathbf {c}$ and $\mathbf {d}$ are of the same rank.

3. (iii) If either $\left. \mathbf {c}\right \downarrow ^{-}=\left. \mathbf {d}\right \downarrow ^{-}$ or $\left. \mathbf {c}\right \uparrow ^{-}=\left. \mathbf {d}\right \uparrow ^{-}$ , then neither $\mathbf {c} \prec \mathbf {d}$ nor $\mathbf {d}\prec \mathbf {c}$ .

4. (iv) $\mathbf {c}\subseteq \mathbf {d}{\uparrow }^{-}$ iff $\mathbf {d} \prec \mathbf {c}$ iff $\mathbf {d}\subseteq \left. \mathbf {c}\right \downarrow ^{-}$ .

The following formulas are from [9, p. 133], where $i\geqslant 1$ :

$$ \begin{align*} \mathsf{B}_{1} & =\Diamond\Box p_{1}\rightarrow p_{1}\text{,}\\ \mathsf{B}_{i+1} & =\Diamond(\Box p_{i+1}\wedge\lnot\mathsf{B} _{i})\rightarrow p_{i+1}\text{.} \end{align*} $$

A transitive logic is of depth n ( $n\geqslant 1$ ) if it contains $\mathsf {B}_{n}$ but not $\mathsf {B}_{k}$ for any $1\leqslant k<n$ , and is of finite depth if it contains $\mathsf {B}_{n}$ for some $n\geqslant 1$ . We recall Proposition 2.3 (see, e.g., [2, proposition 3.44]) and Proposition 2.4 (see [9, theorem 6.6]):

Proposition 2.3. For each transitive frame $\mathfrak {F}$ and each $n\geqslant 1$ , $\mathfrak {F}\vDash \mathsf {B}_{n}$ iff $\mathfrak {F}$ is of rank at most $n$ .

Theorem 2.4. All transitive logics of finite depth have the f.m.p.

An antichain in a frame $\mathfrak {F}=\left \langle W,R\right \rangle $ is a set $A\subseteq W$ such that for all $u,v\in A$ , $uRv$ implies $u=v$ . Whenever we speak of an antichain $\{u_{0},\ldots ,u_{n}\}$ in a frame, we presuppose that $u_{0},\ldots ,u_{n}$ are distinct. A transitive frame is of width at most n ( $n\geqslant 1$ ) if $\left \vert A\right \vert \leqslant n$ for each antichain A in the frame. A transitive logic is of width n ( $n\geqslant 1$ ) if it contains $\mathsf {Wid}_{n}$ but not $\mathsf {Wid}_{k}$ for any $1\leqslant k<n$ , and is of finite width if it contains $\mathsf {Wid}_{n}$ for a $n\geqslant 1$ . We recall Proposition 2.5 (see [5, sec. 3, theorem 1]):

Proposition 2.5. For each rooted transitive frame $\mathfrak {F}$ and each $n\geqslant 1$ , $\mathfrak {F}\vDash \mathsf {Wid}_{n}$ iff $\mathfrak {F}$ is of width at most $n$ .

3 Transitive frames of finite suc-eq-width

In this section, we discuss frame conditions of $\mathsf {Wid}_{n}^{\ast }$ , introduce a new construction built upon the skeletons of transitive frames, which always results finite frames when applied to transitive frames of finite rank and suc-eq-width, and prove some auxiliary results of it, which will be used in our main theorem.

Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be a transitive frame. Note that for all $u,v\in W$ , u and v have the same set of proper successors iff $\mathbf {c}_{(u)}{\uparrow }^{-}=\mathbf {c}_{(v)}{\uparrow }^{-}$ , and they have the same set of proper predecessors iff $\mathbf {c}_{(u)}{\downarrow } ^{-}=\mathbf {c}_{(v)}{\downarrow }^{-}$ . For each $k\geqslant 1$ , $\mathfrak {F}$ is of suc-eq-width at most k if each antichain in $\mathfrak {F}$ contains at most k points with different sets of proper successors, i.e., for each antichain A in $\mathfrak {F}$ , if $\left \vert A\right \vert>k$ , at least two points in A have the same set of proper successors. $\mathfrak {F}$ is of finite suc-eq-width if for some $k\geqslant 1$ , $\mathfrak {F}$ is of suc-eq-width at most k. It is clear that a transitive frame is of suc-eq-width at most k if it is of width at most k. A transitive logic is of suc-eq-width n ( $n\geqslant 1$ ) if it contains $\mathsf {Wid} _{n}^{\ast }$ but not $\mathsf {Wid}_{k}^{\ast }$ for any $1\leqslant k<n$ , and is of finite suc-eq-width if it contains $\mathsf {Wid}_{n}^{\ast }$ for an $n\geqslant 1$ . The following proposition gives the frame conditions of suc-eq-width formulas $\mathsf {Wid}_{n}^{\ast }$ (see [11, proposition 3.3]).

Proposition 3.1. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any transitive frame, and let $w\in W$ and $n\geqslant 1$ . Then $\mathfrak {F},w\vDash \mathsf {Wid} _{n}^{\ast }$ iff for each antichain $\{u_{0},\ldots ,u_{n}\}\subseteq \left. w\right \uparrow $ , there are distinct $i,j\leqslant n$ such that $\mathbf {c}_{(u_{i})}{\uparrow }^{-}=\mathbf {c}_{(u_{j})}{\uparrow }^{-}$ . Hence, if $\mathfrak {F}$ is rooted, then $\mathfrak {F}\vDash \mathsf {Wid} _{n}^{\ast }$ iff $\mathfrak {F}$ is of suc-eq-width at most $n$ .

We now give infinitely many transitive logics of finite depth and of suc-eq-width $1$ but not of finite width. For each $n>0$ , let $\mathfrak {D} _{n}=\mathfrak {A}^{\circ }\oplus \mathfrak {B\oplus C}_{n}$ , where $\mathfrak {A} ^{\circ }=\left \langle \{a\},\{\left \langle a,a\right \rangle \}\right \rangle $ , $\mathfrak {B}=\left \langle \{b_{i}:i\in \omega \},\varnothing \right \rangle $ and $\mathfrak {C}_{n}=\left \langle \{c_{i}:0\leqslant i<n\},\{\left \langle c_{i},c_{j}\right \rangle :i<j\}\right \rangle $ . It is clear that although $b_{0},b_{1},b_{2},\ldots $ have the same set of proper successors, they form an infinite antichain in $\mathfrak {D}_{n}$ for each $n>0$ ; so all $\mathfrak {D}_{n}$ are frames for $\mathsf {Wid}_{1}^{\ast }$ but not frames for any $\mathsf {Wid}_{n}$ . It is also easy to see that all $\mathfrak {D}_{n}$ are transitive frames of finite rank. Therefore, all $\mathbf {Log}(\mathfrak {D} _{n})$ are transitive logics of finite depth and of suc-eq-width $1$ but not of finite width. For each $k>0$ , let

$$\begin{align*}\mathsf{Z}_{k}=\Diamond\Box^{-}\Box^{k}\bot\wedge\lnot\mathsf{GL} \rightarrow\Diamond\Box^{-}\Box^{k+1}\bot, \end{align*}$$

where $\Box ^{-}\phi =\Box \phi \wedge \lnot \phi $ and $\mathsf {GL}=\Box (\Box p\rightarrow p)\rightarrow \Box p$ . ¹ Note that for each model $\mathfrak {M}=\left \langle \mathfrak {D} _{n},V\right \rangle $ and each $w$ in $\mathfrak {M}$ , $\mathfrak {M} ,w\vDash \lnot \mathsf {GL}$ iff $w=a$ and $V(p)=\{b_{i}:i\in \omega \}\cup \{c_{i}:0\leqslant i<n\}$ . To see that these $\mathbf {Log}(\mathfrak {D}_{n})$ are distinct, note that $\mathfrak {D}_{n}\vDash \mathsf {Z}_{k}$ iff $k\neq n$ for all $n,k>0$ , and hence $\mathsf {Z}_{m}\in \mathbf {Log}(\mathfrak {D} _{n})-\mathbf {Log}(\mathfrak {D}_{m})$ and $\mathsf {Z}_{n}\in \mathbf {Log} (\mathfrak {D}_{m})-\mathbf {Log}(\mathfrak {D}_{n})$ for all distinct $m,n>0$ . This shows that $\{\mathbf {Log}(\mathfrak {D}_{n}):n>0\}$ forms an infinite antichain in $\mathsf {NExt}\mathbf {K4}$ . Nevertheless, our main theorem will imply that all of them and their extensions are finitely axiomatizable.

Let $\mathfrak {F}$ be a transitive frame of finite rank. We know that $\mathfrak {sk}(\mathfrak {F})$ is finite whenever $\mathfrak {F}$ is of finite width. However, $\mathfrak {sk}(\mathfrak {F})$ may still be infinite if $\mathfrak {F}$ is only of finite suc-eq-width. For example, $\mathfrak {sk} (\mathfrak {D}_{n})$ is of the same cardinality as $\mathfrak {D}_{n}$ for all $\mathfrak {D}_{n}$ above. In what follows, we introduce a new construction built upon the skeletons of transitive frames, which gives finite frames when applied to transitive frames of finite rank and finite suc-eq-width.

Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any transitive frame. For all $\mathbf {c},\mathbf {d}\in \mathfrak {sk}(W)$ , let $\mathbf {c}\cong _{\mathsf {s}}\mathbf {d}$ iff $\left. \mathbf {c}\right \uparrow ^{-}=\left. \mathbf {d}\right \uparrow ^{-}$ , let $\mathbf {c}\cong _{\mathsf {p}}\mathbf {d}$ iff $\left. \mathbf {c}\right \downarrow ^{-}=\left. \mathbf {d} \right \downarrow ^{-}$ , and let $\mathbf {c}\cong \mathbf {d}$ iff $\left. \mathbf {c}\right \uparrow ^{-}=\left. \mathbf {d}\right \uparrow ^{-}$ and $\left. \mathbf {c}\right \downarrow ^{-}=\left. \mathbf {d}\right \downarrow ^{-}$ . It is clear that $\cong _{\mathsf {s}},\cong _{\mathsf {p}}$ and $\cong $ are equivalence relations on $\mathfrak {sk}(W)$ . For each $\mathbf {c} \in \mathfrak {sk}(W)$ , we use $[\mathbf {c}]_{\mathsf {s}},[\mathbf {c} ]_{\mathsf {p}}$ and $[\mathbf {c}]_{\cong }$ respectively for the equivalence classes modulo $\cong _{\mathsf {s}},\cong _{\mathsf {p}}$ and $\cong $ to which $\mathbf {c}$ belongs, and use $\mathfrak {eq}_{\mathsf {s}}(W),\mathfrak {eq} _{\mathsf {p}}(W)$ and $\mathfrak {eq}(W)$ respectively for the sets of equivalence classes modulo $\cong _{\mathsf {s}},\cong _{\mathsf {p}}$ and $\cong $ . Let $\mathfrak {eq}(\mathfrak {F})=\left \langle \mathfrak {eq} (W),\mathfrak {eq}(R)\right \rangle $ where for all $\mathcal {A},\mathcal {B} \in \mathfrak {eq}(W)$ , $\left \langle \mathcal {A},\mathcal {B}\right \rangle \in \mathfrak {eq}(R)$ iff $\mathbf {c}\prec _{R}\mathbf {d}$ for some $\mathbf {c}\in \mathcal {A}$ and $\mathbf {d}\in \mathcal {B}$ . The following is easily verifiable by definition and Fact 2.2.

Fact 3.2. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any transitive frame. Then the following hold:

1. (i) $\mathfrak {eq}(\mathfrak {F})$ is a transitive frame, and is of the same rank as $\mathfrak {F}$ is.

2. (ii) $\mathfrak {eq}(\mathfrak {F})$ is rooted if $\mathfrak {F}$ is, and each member of $\mathfrak {eq}(W)$ is an antichain in $\mathfrak {sk}(\mathfrak {F} )$ .

3. (iii) For all $\mathcal {A},\mathcal {B}\in \mathfrak {eq}(W)$ , $\left \langle \mathcal {A},\mathcal {B}\right \rangle \in \mathfrak {eq}(R)$ iff $\mathbf {c} \prec _{R}\mathbf {d}$ for all $\mathbf {c}\in \mathcal {A}$ and $\mathbf {d} \in \mathcal {B}$ .

Lemma 3.3. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be any transitive frame. Then $|\mathfrak {eq}_{\mathsf {p}}(W)|\leqslant 2^{|\mathfrak {eq}_{\mathsf {s} }(W)|}$ .

Proof. Let $\mathbf {c}\in \mathfrak {sk}(W)$ and $\mathcal {A}\in \mathfrak {eq} _{\mathsf {s}}(W)$ . Assume that $(\bigcup \mathcal {A})\cap \left. \mathbf {c} \right \downarrow ^{-}\neq \varnothing $ . Then for some $\mathbf {d}\in \mathcal {A}$ , $\mathbf {d}\cap \left. \mathbf {c}\right \downarrow ^{-} \neq \varnothing $ , which implies that $\mathbf {d}\subseteq \left. \mathbf {c}\right \downarrow ^{-}$ , and thus $\mathbf {c}\subseteq \left. \mathbf {d}\right \uparrow ^{-}$ by Fact 2.2 (iv); and then for each $\mathbf {e} \in \mathcal {A}$ , $\mathbf {c}\subseteq \left. \mathbf {e}\right \uparrow ^{-}$ because $\left. \mathbf {d}\right \uparrow ^{-}=\left. \mathbf {e} \right \uparrow ^{-}$ , which implies by Fact 2.2 (iv) that $\mathbf {e}\subseteq \left. \mathbf {c}\right \downarrow ^{-}$ , and hence $\bigcup \mathcal {A}\subseteq \left. \mathbf {c}\right \downarrow ^{-}$ . It then follows that for each $\mathbf {c}\in \mathfrak {sk}(W)$ , $\left. \mathbf {c}\right \downarrow ^{-}=\bigcup \bigcup \{[\mathbf {c}_{(w)}]_{\mathsf {s}}\in \mathfrak {eq} _{\mathsf {s}}(W):w\in \left. \mathbf {c}\right \downarrow ^{-}\}$ , which implies that $\left. \mathbf {c}\right \downarrow ^{-}=\bigcup \bigcup \mathcal {Z}$ for a $\mathcal {Z}\subseteq \mathfrak {eq}_{\mathsf {s}}(W)$ , and hence $|\mathfrak {eq} _{\mathsf {p}}(W)|\leqslant 2^{|\mathfrak {eq}_{\mathsf {s}}(W)|}$ .

Proposition 3.4. Let $k,n\geqslant 1$ , and let $\mathfrak {F}=\left \langle W,R\right \rangle $ be a transitive frame of rank at most $n$ and of suc-eq-width at most $k$ . Then $\left \Vert \mathfrak {eq}(W)\right \Vert \leqslant n\times k\times 2^{n\times k}$ .

Proof. For each i such that $1\leqslant i\leqslant n$ , let $A_{(i)}$ be the set of all clusters in $\mathfrak {sk}(\mathfrak {F})$ of rank i, and let $\mathcal {B}_{i}=\{[\mathbf {c}]_{\mathsf {s}}:\mathbf {c}\in A_{(i)}\}$ . By hypothesis, $\left \vert \mathcal {B}_{i}\right \vert \leqslant k$ for each i with $1\leqslant i\leqslant n$ . Let $\mathcal {B}=\bigcup \nolimits _{1\leqslant i\leqslant n}\mathcal {B}_{i}$ . It follows that for each $\mathcal {C} \in \mathfrak {eq}_{\mathsf {s}}(W)$ , $\mathcal {B}$ contains $\mathcal {C}$ , and then $|\mathfrak {eq}_{\mathsf {s}}(W)|\leqslant \left \vert \mathcal {B} \right \vert \leqslant n\times k$ , and hence $|\mathfrak {eq}_{\mathsf {p} }(W)|\leqslant 2^{n\times k}$ by Lemma 3.3. Because $[\mathbf {c}]_{\cong }=[\mathbf {c}]_{\mathsf {s}}\cap \lbrack \mathbf {c}]_{\mathsf {p}}$ for each $\mathbf {c}\in \mathfrak {sk}(W)$ , it then follows that $|\mathfrak {eq} (W)|\leqslant n\times k\times 2^{n\times k}$ .

Note that for all clusters $\mathbf {c},\mathbf {d}$ in a transitive frame $\mathfrak {F}$ , $\mathbf {c}\ncong \mathbf {d}$ if either $\mathbf {c} \prec \mathbf {d}$ or $\mathbf {c}\ncong _{\mathsf {s}}\mathbf {d}$ , and thus both the rank and suc-eq-width of $\mathfrak {F}$ are at most n if $\mathfrak {sk} (\mathfrak {F})$ contains n equivalence classes modulo $\cong $ . Hence we have the following by Proposition 3.4.

Corollary 3.5. For each transitive frame $\mathfrak {F}$ , the following are equivalent:

1. (i) $\mathfrak {F}$ is of finite rank and finite suc-eq-width;

2. (ii) $\mathfrak {sk}(\mathfrak {F})$ has only finitely many equivalence classes modulo $\cong $ ;

3. (iii) $\mathfrak {F}$ has only finitely many equivalence classes modulo the relation of having the same set of proper successors and the same set of proper predecessors.

Theorem 3.6. A transitive logic $\mathbf {L}$ is of finite depth and finite suc-eq-width iff for some $m\geqslant 1$ , $\mathbf {L}$ is characterized by a class $\mathscr {C}$ of finite rooted transitive frames such that $|\mathfrak {eq}(\mathfrak {F} )|\leqslant m$ for each $\mathfrak {F\in }\mathscr {C}$ .

Proof. Let $\mathbf {L}$ be a transitive logic. If $\mathbf {L}$ is of finite depth and finite suc-eq-width, then $\mathsf {B}_{n},\mathsf {Wid}_{k}^{\ast }\in \mathbf {L}$ for some $n,k\geqslant 1$ , and by Theorem 2.3, $\mathbf {L}$ is characterized by a class $\mathscr {C}$ of finite rooted transitive frames for $\mathbf {L}$ . It then follows from Propositions 2.3 and 3.1 that for each $\mathfrak {F\in }\mathscr {C}$ , $\mathfrak {F}$ is of rank at most n and of suc-eq-width at most k, which implies by Proposition 3.4 that $|\mathfrak {eq}(\mathfrak {F})|\leqslant n\times k\times 2^{n\times k}$ for each $\mathfrak {F\in }\mathscr {C}$ . Let $m=n\times k\times 2^{n\times k}$ . Hence, $\mathbf {L}$ is characterized by a class $\mathscr {C}$ of finite rooted transitive frames such that $|\mathfrak {eq}(\mathfrak {F})|\leqslant m$ for each $\mathfrak {F\in }\mathscr {C}$ .

If for some $m\geqslant 1$ , $\mathbf {L}$ is characterized by a class $\mathscr {C}$ of finite rooted transitive frames such that $|\mathfrak {eq} (\mathfrak {F})|\leqslant m$ for each $\mathfrak {F\in }\mathscr {C}$ , then $\mathbf {L}$ is characterized by a class of finite rooted transitive frames whose rank and suc-eq-width are both at most m, and hence by Propositions 2.3 and 3.1, $\mathsf {B}_{m},\mathsf {Wid}_{m}^{\ast }\in \mathbf {L}$ , which gives that $\mathbf {L}$ is of finite depth and finite suc-eq-width.

4 Criteria of finite axiomatizability

In the section, we present some necessary and sufficient conditions for all extensions of a modal logic $\mathbf {L}$ to be finitely axiomatizable over $\mathbf {L}$ . For each family $\{\mathbf {L}_{i}\}_{i\in I}$ of modal logics, we use $\bigoplus \nolimits _{i\in I}\mathbf {L}_{i}$ for the smallest modal logic including $\bigcup \nolimits _{i\in I}\mathbf {L}_{i}$ . The following is a well-known theorem from Tarski (see, e.g., [2, theorem 4.12]):

Theorem 4.1. Let $\mathbf {L}$ and $\mathbf {L}^{\prime }$ be any modal logics such that $\mathbf {L}\subseteq \mathbf {L}^{\prime }$ . Then $\mathbf {L}^{\prime }$ is finitely axiomatizable over $\mathbf {L}$ iff there is no infinite ascending $\subset $ -chain $\mathbf {L}_{0}\subset \mathbf {L}_{1}\subset \mathbf {L} _{2}\subset \cdots $ of extensions of $\mathbf {L}$ such that $\mathbf {L} ^{\prime }= {\textstyle \bigoplus \nolimits _{i\in \omega }} \mathbf {L}_{i}$ .

Let $\{\mathfrak {F}_{i}\}_{i\in \omega }$ be any infinite sequence of frames. $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is sub-distinguishable if for each $i\in \omega $ , there is a formula $\phi $ such that $\mathfrak {F}_{i}\nvDash \phi $ , and $\mathfrak {F}_{j}\vDash \phi $ for all $j\in \omega $ with $i<j$ .

The following theorem provides a sufficient and necessary condition of finite axiomatizability in terms of sub-distinguishable sequences, and is proved by applying Theorem 4.1.

Theorem 4.2. Let $\mathbf {L}$ be a modal logic, and let $\mathscr {C}$ be a class of frames for $\mathbf {L}$ such that each extension of $\mathbf {L}$ is characterized by a subclass of $\mathscr {C}$ . Then all extensions of $\mathbf {L}$ are finitely axiomatizable over $\mathbf {L}$ iff there is no sub-distinguishable sequence of members of $\mathscr {C}$ .

Proof. Suppose that $\mathbf {L}^{\prime }$ extends $\mathbf {L}$ but is not finitely axiomatizable over $\mathbf {L}$ . By Theorem 4.1, there is an infinite ascending $\subset $ -chain $\mathbf {L}_{0}\subset \mathbf {L}_{1}\subset \cdots $ of extensions of $\mathbf {L}$ , and then for each $i\in \omega $ , there is a $\phi _{i}\in \mathbf {L}_{i+1}-\mathbf {L}_{i}$ , and hence because $\mathbf {L}_{i}$ is by hypothesis characterized by a subclass of $ \mathscr {C} $ , $\mathfrak {F}_{i}\nvDash \phi _{i}$ for a member $\mathfrak {F}_{i}$ of $ \mathscr {C} $ such that $\mathfrak {F}_{i}\vDash \mathbf {L}_{i}$ . Consider the sequence $\{\mathfrak {F}_{i}\}_{i\in \omega }$ . We have that for each $i,j\in \omega $ with $i<j$ , $\mathfrak {F}_{i}\nvDash \phi _{i}\in \mathbf {L}_{i+1}\subseteq \mathbf {L}_{j}$ and $\mathfrak {F}_{j}\vDash \mathbf {L}_{j}$ , and hence $\mathfrak {F}_{j}\vDash \phi _{i}$ . Therefore, $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is a sub-distinguishable sequence of members of $\mathscr {C}$ .

Suppose that $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is a sub-distinguishable sequence of members of $\mathscr {C}$ . For each $k\in \omega $ , let $\mathbf {L}_{k}= {\textstyle \bigcap \nolimits _{k\leqslant i\in \omega }} \mathbf {Log}(\mathfrak {F}_{i})$ . Consider any $i\in \omega $ . By definition, $\mathbf {L}\subseteq \mathbf {L}_{i}\subseteq \mathbf {L}_{i+1}$ , and there is a $\phi $ such that $\mathfrak {F}_{i}\nvDash \phi $ and $\mathfrak {F}_{j}\vDash \phi $ for all $j>i$ , and then $\phi \notin \mathbf {L}_{i}$ and $\phi _{i} \in \mathbf {L}_{i+1}$ , and consequently $\mathbf {L}_{i}\subset \mathbf {L}_{i+1} $ . Hence $\{\mathbf {L}_{i}\}_{i\in \omega }$ is an infinite ascending $\subset $ -chain. Let $\mathbf {L}^{\prime }= {\textstyle \bigoplus \nolimits _{i\in \omega }} \mathbf {L}_{i}$ . We know that $\mathbf {L}^{\prime }$ extends $\mathbf {L}$ , and hence by Theorem 4.1 that $\mathbf {L} ^{\prime }$ is not finitely axiomatizable over $\mathbf {L}$ .

Corollary 4.3. Let $\mathbf {L}$ be any modal logic whose extensions all have the f.m.p. Then all extensions of $\mathbf {L}$ are finitely axiomatizable over $\mathbf {L}$ iff there is no sub-distinguishable sequence of finite rooted frames for $\mathbf {L}$ .

Proof. Let $ \mathscr {C} $ be the class of finite rooted frames for $\mathbf {L}$ . It follows from hypothesis that each extension of $\mathbf {L}$ is characterized by a subclass of $ \mathscr {C} $ . Hence the conclusion follows from Theorem 4.2.

Let $\{\mathfrak {F}_{i}\}_{i\in \omega }$ be any infinite sequence of frames. $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is backward irreducible if for all $i,j\in I$ with $i<j$ , no point-generated subframe of $\mathfrak {F}_{j}$ is reducible to $\mathfrak {F}_{i}$ . We show in the following that $\{\mathfrak {F} _{i}\}_{i\in \omega }$ is sub-distinguishable iff $\{\mathfrak {F}_{i} \}_{i\in \omega }$ is backward irreducible under the supposition that all $\mathfrak {F}_{i}$ are finite rooted transitive frames. Let $\mathfrak {F} =\left \langle W,R\right \rangle $ be a finite rooted transitive frame, where $W=\{w_{0},\ldots ,w_{n}\}$ with $w_{0}$ to be a root of $\mathfrak {F}$ , and $w_{0},\ldots ,w_{n}$ to be all distinct. We call $\left \langle w_{0} ,\ldots ,w_{n}\right \rangle $ an ordering of points in $\mathfrak {F}$ . Let $p_{0},\ldots ,p_{n}$ be distinct propositional letters, and let us call a conjunction of the following formulas a frame formula for $\mathfrak {F}$ w.r.t. $\left \langle w_{0},\ldots ,w_{n}\right \rangle $ :

• • $p_{0}$ ,

• • $\Box (p_{0}\vee \cdots \vee p_{n})$ ,

• • $ {\textstyle \bigwedge } \{(p_{i}\rightarrow \lnot p_{j})\wedge \Box (p_{i}\rightarrow \lnot p_{j} ):i,j\leqslant n$ and $i\neq j\}$ ,

• • $ {\textstyle \bigwedge } \{(p_{i}\rightarrow \Diamond p_{j})\wedge \Box (p_{i}\rightarrow \Diamond p_{j}):i,j\leqslant n$ and $Rw_{i}w_{j}\}$ ,

• • $ {\textstyle \bigwedge } \{(p_{i}\rightarrow \lnot \Diamond p_{j})\wedge \Box (p_{i}\rightarrow \lnot \Diamond p_{j}):i,j\leqslant n$ and not $Rw_{i}w_{j}\}$ .

A frame formula ² for $\mathfrak {F}$ is a frame formula for $\mathfrak {F}$ w.r.t. an ordering $\left \langle u_{0} ,\ldots ,u_{n}\right \rangle $ of points in $\mathfrak {F}$ , where $u_{0}$ is a root.

Lemma 4.4. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ be a finite rooted transitive frame, for which $\phi $ is a frame formula w.r.t. an ordering $\left \langle w_{0},\ldots ,w_{n}\right \rangle $ of points in $\mathfrak {F}$ . Then $\phi $ is satisfiable in $\mathfrak {F}$ at its root $w_{0}$ .

Proof. Let $\mathfrak {M}=\left \langle \mathfrak {F},V\right \rangle $ where $V(p_{i})=\{w_{i}\}$ for each $i\leqslant n$ . It is routine to check that $\mathfrak {M},w_{0}\vDash \phi $ .

The following is Lemma 3.20 from [1], whose proof is left to the readers.

Lemma 4.5. Let $\mathfrak {F}$ be a finite rooted transitive frame, for which $\phi $ is a frame formula, and let $\mathfrak {G}=\left \langle U,S\right \rangle $ be any transitive frame with $u\in U$ . Then $\phi $ is satisfiable in $\mathfrak {G}$ at u iff the subframe of $\mathfrak {G}$ generated by u is reducible to $\mathfrak {F}$ .

Proposition 4.6. Let $\{\mathfrak {F}_{i} \}_{i\in \omega }$ be an infinite sequence of finite rooted transitive frames. Then $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is sub-distinguishable iff $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is backward irreducible.

Proof. Suppose that $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is not backward irreducible. Then there are $i,j\in \omega $ such that $i<j$ and a point-generated subframe of $\mathfrak {F}_{j}$ is reducible to $\mathfrak {F}_{i}$ . Hence, for any formula $\phi $ , $\mathfrak {F}_{i}\nvDash \phi $ yields $\mathfrak {F}_{j} \nvDash \phi $ , which implies that $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is not sub-distinguishable.

Suppose that $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is backward irreducible. For each $i\in \omega $ , let $\phi _{i}$ be a frame formula for $\mathfrak {F}_{i}$ . Then we have by Lemma 4.4 that $\phi _{i}$ is satisfiable in $\mathfrak {F}_{i}$ , and thus $\mathfrak {F}_{i}\nvDash \lnot \phi _{i}$ . For each $j\in \omega $ with $i<j$ , we know from the supposition that no point-generated subframe of $\mathfrak {F}_{j}$ is reducible to $\mathfrak {F}_{i}$ , and it then follows from Lemma 4.5 that $\phi _{i}$ is not satisfiable in $\mathfrak {F}_{i}$ , and so $\mathfrak {F} _{j}\vDash \lnot \phi _{i}$ . Therefore, $\{\mathfrak {F}_{i}\}_{i\in \omega }$ is sub-distinguishable.

The right to the left direction of the following theorem is often applied in studies of finite axiomatizability of modal logics whose extensions have the f.m.p. (see, e.g., [3, 7, 10]).

Theorem 4.7. Let $\mathbf {L}$ be a transitive logic whose extensions all have the f.m.p. Then all extensions of $\mathbf {L}$ are finitely axiomatizable over $\mathbf {L}$ iff there is no backward irreducible sequence of finite rooted frames for $\mathbf {L}$ .

Proof. Since $\mathbf {L}$ is a transitive logic, so all frames for $\mathbf {L}$ are transitive. It then follows from Corollary 4.3 that all extensions of $\mathbf {L}$ are finitely axiomatizable over $\mathbf {L}$ iff there is no sub-distinguishable sequence of finite rooted frames for $\mathbf {L}$ , by Proposition 4.6, iff there is no backward irreducible sequence of finite rooted frames for $\mathbf {L}$ .

5 Well quasi-orders on lists

A binary relation is a quasi-order if it is reflexive and transitive. A quasi-order $\preceq $ on a set A is a well quasi-order (or A is well quasi-ordered by $\preceq $ ) if for every infinite sequence $(a_{i})_{i\in \omega }$ of elements in A, there are indices $i<j\in \omega $ such that $a_{i}\preceq a_{j}$ . Let $\eqslantless $ be a binary relation on $\omega $ defined by taking: $m\eqslantless n$ iff either $m=n=0$ or $0<m\leqslant n$ .

Fact 5.1. Both $\leqslant $ and $\eqslantless $ are well quasi-orders on $\omega $ .

Let $\preceq _{1}$ and $\preceq _{2}$ be quasi-orders on sets $A_{1}$ and $A_{2}$ respectively, and let $\preceq $ be an order on $A_{1}\times A_{2}$ defined by: $\left \langle a_{1},a_{2}\right \rangle \preceq \left \langle a_{1}^{\prime },a_{2}^{\prime }\right \rangle $ iff $a_{1}\preceq _{1} a_{1}^{\prime }$ and $a_{2}\preceq _{2}a_{2}^{\prime }$ . It is clear that $\preceq $ is a quasi-order. Furthermore, we have the following lemma (see, e.g., [6, lemma 2.6]).

Lemma 5.2. If $\preceq _{1}$ and $\preceq _{2}$ are well quasi-orders, then $\preceq $ is a well quasi-order.

Let A be any nonempty set. A list of members of A is a finite nonempty sequence of members of A. We will use $\mathsf {List}(A)$ for the set of all lists of members of A, and $\mathsf {List}_{n}(A)$ for the set of all lists in $\mathsf {List}(A)$ with length n ( $n\geqslant 1$ ). For convenience, let $\omega _{+}=\omega -\{0\}$ .

Definition 5.3. Let $s,t\in \mathsf {List}(\omega _{+})$ where $s=(a_{i})_{i\leqslant k}$ and $t=(b_{i})_{i\leqslant n}$ . $s\vartriangleleft t$ iff there are integers $j_{0},\ldots ,j_{k}$ such that $0\leqslant j_{0}<j_{1}<\cdots <j_{k}=n$ and $a_{i}\leqslant b_{j_{i}}$ for each $i\leqslant k$ .

The following proposition has been proved in [3, sec. 3, corollary], and we can also prove it by Higman’s theorem (see, e.g., [6, theorem 3.2]).

Proposition 5.4. $\vartriangleleft $ is a well quasi-order on $\mathsf {List}(\omega _{+} )$ .

Let us fix the following sets of lists:

(1) $$ \begin{align} \mathbb{C}=\{(s,n):s\in\mathsf{List}(\omega_{+})\cup\{(0)\}\text{ and } n\in\omega\}\text{.} \end{align} $$

Definition 5.5. Let $\mathsf {u}=(s,m)$ and $\mathsf {v}=(t,n)$ be any members of $\mathbb {C}$ . $\mathsf {u}\vartriangleleft _{0}\mathsf {v}$ iff $m\eqslantless n$ , and either $s=t=(0)$ or $s\vartriangleleft t$ with $s,t\in \mathsf {List}(\omega _{+})$ . Let $\mathbf {s} =(\mathsf {u}_{i})_{i\in k}$ and $\mathbf {t}=(\mathsf {v}_{i})_{i\in n}$ be any members of $\mathsf {List}(\mathbb {C})$ . $\mathbf {s}\vartriangleleft _{1}\mathbf {t}$ iff $k=n$ and $\mathsf {u}_{i}\vartriangleleft _{0} \mathsf {v}_{i}$ for each $i\leqslant k$ .

It is easy to verify that $\vartriangleleft _{0}$ and $\vartriangleleft _{1}$ are quasi-orders on $\mathbb {C}$ and $\mathsf {List}(\mathbb {C})$ respectively.

Proposition 5.6. $\vartriangleleft _{0}$ is a well quasi-order on $\mathbb {C}$ ; and for each $n\geqslant 1$ , $\mathsf {List} _{n}(\mathbb {C})$ is well quasi-ordered by $\vartriangleleft _{1} $ .

Proof. By Fact 5.1 and Lemma 5.2, to show $\vartriangleleft _{0}$ is a well quasi-order, it suffices to prove that $\preceq $ defined in (2) is a well quasi-order on $\mathsf {List}(\omega _{+})\cup \{(0)\}$ :

(2) $$ \begin{align} s\preceq t\text{ iff }s=t=(0)\text{ or }s\vartriangleleft t\text{ with } s,t\in\mathsf{List}(\omega_{+})\text{.} \end{align} $$

It is routine to verify that $\preceq $ is a quasi-order. Let $(s_{i} )_{i\in \omega }$ be any infinite sequence of elements in $\mathsf {List} (\omega _{+})\cup \{(0)\}$ . Then $(s_{i})_{i\in \omega }$ contains an infinite subsequence $(s_{i})_{i\in I}$ such that either $s_{i}=(0)$ for each $i\in I$ , or $s_{i}\in \mathsf {List}(\omega _{+})$ for each $i\in I$ . If the former holds, then $s_{i}\preceq s_{j}$ for any $i<j$ with $i,j\in I$ ; if the latter holds, then by Proposition 5.4, there are $i,j\in I$ such that $i<j$ and $s_{i}\vartriangleleft s_{j}$ , and hence $s_{i}\preceq s_{j}$ . Therefore, $\preceq $ is a well quasi-order.

Since $\vartriangleleft _{0}$ is a well quasi-order, to obtain that $\mathsf {List}_{n}(\mathbb {C})$ is well quasi-ordered by $\vartriangleleft _{1}$ , simply apply Lemma 5.2 n times.

6 Finite axiomatizability

In the section, we prove our main result, i.e., the finite axiomatizability of transitive logics of finite depth and suc-eq-width (Theorem 6.5).

Let $\mathfrak {F}$ be any finite transitive frame, and let $\mathcal {A}$ be any antichain in $\mathfrak {sk}(\mathfrak {F})$ . We use $\mathcal {A}^{+}$ for the set of nondegenerate clusters in $\mathfrak {F}$ contained in $\mathcal {A} $ , and use $\mathcal {A}^{-}$ for the set of degenerate clusters in $\mathfrak {F}$ contained in $\mathcal {A}$ . If $\mathcal {A}^{+}\neq \varnothing $ , we assume that members of $\mathcal {A}^{+}$ are arranged as $\mathbf {c} _{0},\ldots ,\mathbf {c}_{n}$ for an $n\in \omega $ such that $\left \vert \mathbf {c}_{n}\right \vert =\min (\{\left \vert \mathbf {c}_{i}\right \vert :i\leqslant n\})$ , i.e., $\mathbf {c}_{n}$ is of the smallest size among members of $\mathcal {A}^{+}$ . Let $s_{\mathcal {A}^{+}}$ be the following list:

(3) $$ \begin{align} s_{\mathcal{A}^{+}}=\left\{\hspace{-5pt} \begin{array}[c]{ll} (0), & \text{if }\mathcal{A}^{+}=\varnothing\text{,}\\ (\left\vert \mathbf{c}_{i}\right\vert )_{i\leqslant n}, & \text{if } \mathcal{A}^{+}=\{\mathbf{c}_{0},\ldots,\mathbf{c}_{n}\}\neq\varnothing \text{.} \end{array} \right. \end{align} $$

We call the following list a standard representation list of $\mathcal {A}$ (an s.r.l. of $\mathcal {A}$ for short), where the subscript “ $\mathsf {ac}$ ” is a reminder of antichain (of clusters):

(4) $$ \begin{align} g_{\mathsf{ac}}(\mathcal{A})=(s_{\mathcal{A}^{+}},|\mathcal{A}^{-}|)\text{.} \end{align} $$

It is easy to verify that $g_{\mathsf {ac}}(\mathcal {A})\in \mathbb {C}$ (see (1)). Note that $\mathcal {A}^{+}$ is an antichain in $\mathfrak {sk}(\mathfrak {F})$ , and thus the natural order between members of $s_{\mathcal {A}^{+}}$ is inessential, except for the position of its last member.

Lemma 6.1. Let $\mathfrak {F}$ and $\mathfrak {G}$ be finite transitive frames, let $\mathcal {A}$ and $\mathcal {B}$ be nonempty antichains in $\mathfrak {sk} (\mathfrak {F})$ and $\mathfrak {sk}(\mathfrak {G})$ respectively, and let $g_{\mathsf {ac}}(\mathcal {B})\vartriangleleft _{0}g_{\mathsf {ac}}(\mathcal {A} )$ . Then $\mathfrak {F}\upharpoonright ( {\textstyle \bigcup } \mathcal {A})$ is reducible to $\mathfrak {G}\upharpoonright ( {\textstyle \bigcup } \mathcal {B})$ .

Proof. Let $g_{\mathsf {ac}}(\mathcal {A})=(t,m)$ and $g_{\mathsf {ac}}(\mathcal {B} )=(s,l)$ , and let $X_{\mathcal {A}^{\prime }}= {\textstyle \bigcup } \mathcal {A}^{\prime }$ and $Y_{\mathcal {B}^{\prime }}= {\textstyle \bigcup } \mathcal {B}^{\prime }$ for each $\mathcal {A}^{\prime }\subseteq \mathcal {A}$ and each $\mathcal {B}^{\prime }\subseteq \mathcal {B}$ . By hypothesis,

(5) $$ \begin{align} (s,l)\vartriangleleft_{0}(t,m)\text{, and hence }l\eqslantless m\text{.} \end{align} $$

Case 1, $s=(0)$ . By (5) and Definition 5.5, $t=(0)$ , and then $\mathcal {A} ^{+}=\mathcal {B}^{+}=\varnothing $ . Because $\mathcal {A},\mathcal {B} \neq \varnothing $ , $\mathcal {A}^{-},\mathcal {B}^{-}\neq \varnothing $ , and hence $0<|\mathcal {B}^{-}|=l\leqslant m=|\mathcal {A}^{-}|$ by (5). Let f be a surjection from $X_{\mathcal {A}^{-}}$ to $Y_{\mathcal {B}^{-}}$ , which reduces $\mathfrak {F} \upharpoonright X_{\mathcal {A}}$ to $\mathfrak {G}\upharpoonright Y_{\mathcal {B}}$ .

Case 2, $s\neq (0)$ . By (5) and Definition 5.5, $t\neq (0)$ , and then $\mathcal {A} ^{+},\mathcal {B}^{+}\neq \varnothing $ and $s,t\in \mathsf {List}(\omega _{+})$ . By (3), there are $k,n\in \omega $ such that

$$\begin{align*}s=s_{\mathcal{B}^{+}}=(|\mathbf{d}_{j}|)_{j\leqslant k}\text{ and }t=s_{\mathcal{A}^{+}}=(|\mathbf{c}_{j}|)_{j\leqslant n}\text{,} \end{align*}$$

where $\mathcal {B}^{+}=\{\mathbf {d}_{0},\ldots ,\mathbf {d}_{k}\}$ with $\left \vert \mathbf {d}_{k}\right \vert =\min (\{\left \vert \mathbf {d} _{j}\right \vert :j\leqslant k\})$ , and $\mathcal {A}^{+}=\{\mathbf {c} _{0},\ldots ,\mathbf {c}_{n}\}$ with $\left \vert \mathbf {c}_{n}\right \vert =\min (\{\left \vert \mathbf {c}_{j}\right \vert :j\leqslant n\})$ . Because $s\vartriangleleft t$ by (5), there is an injective order-preserving function h from $\{0,\ldots ,k\}$ to $\{0,\ldots ,n\}$ such that $h(k)=n$ and $|\mathbf {d}_{j}|\leqslant |\mathbf {c}_{h(j)}|$ for each $j\leqslant k$ . For each $j\leqslant k$ , because $0<|\mathbf {d}_{j}|\leqslant |\mathbf {c}_{h(j)}|$ , there is a surjection $g_{j}$ from $\mathbf {c}_{h(j)}$ to $\mathbf {d}_{j}$ . For each $j\leqslant n$ such that $j\notin \{h(j^{\prime }):j^{\prime }\leqslant k\}$ , because $|\mathbf {c}_{j}|\geqslant |\mathbf {c}_{n}|\geqslant |\mathbf {d}_{k}|$ , there is a surjection $g_{j}$ from $\mathbf {c}_{j}$ to $\mathbf {d}_{k}$ . Let $g=\bigcup _{j\leqslant n}g_{j}$ . It is easy to verify that g reduces $\mathfrak {F}\upharpoonright X_{\mathcal {A}^{+}}$ to $\mathfrak {G} \upharpoonright Y_{\mathcal {B}^{+}}$ . Now if $l=0$ , $m=0$ by (5), and then $\mathcal {A}^{-} =\mathcal {B}^{-}=\varnothing $ , and hence g reduces $\mathfrak {F} \upharpoonright X_{\mathcal {A}}$ to $\mathfrak {G}\upharpoonright Y_{\mathcal {B}}$ . Suppose that $l>0$ . Then $\mathcal {B}^{-},\mathcal {A} ^{-}\neq \varnothing $ and $0<l\leqslant m$ by (5), and thus, similar to case 1, there is a reduction f of $\mathfrak {F}\upharpoonright X_{\mathcal {A}^{-}}$ to $\mathfrak {G}\upharpoonright Y_{\mathcal {B}^{-}}$ . It is clear that $\mathfrak {F}\upharpoonright X_{\mathcal {A}}$ is the disjoint union of $\mathfrak {F}\upharpoonright X_{\mathcal {A}^{+}}$ and $\mathfrak {F} \upharpoonright X_{\mathcal {A}^{-}}$ , while $\mathfrak {G}\upharpoonright Y_{\mathcal {B}}$ is the disjoint union of $\mathfrak {G}\upharpoonright Y_{\mathcal {B}^{+}}$ and $\mathfrak {G}\upharpoonright Y_{\mathcal {B}^{-}}$ . Hence $f\cup g$ reduces $\mathfrak {F}\upharpoonright X_{\mathcal {A}}$ to $\mathfrak {G}\upharpoonright Y_{\mathcal {B}}$ by Fact 2.1.

Lemma 6.2. Let $\mathfrak {F}=\left \langle W,R\right \rangle $ and $\mathfrak {G}$ be finite transitive frames and $\mathfrak {eq} (W)=\{\mathcal {A}_{0},\ldots ,\mathcal {A}_{k}\}$ , let h be an isomorphism from $\mathfrak {eq}(\mathfrak {F})$ to $\mathfrak {eq}(\mathfrak {G})$ , and let $g(\mathfrak {G})\vartriangleleft _{1}g(\mathfrak {F})$ where $g(\mathfrak {F} )=\left ( g_{\mathsf {ac}}(\mathcal {A}_{0}),\ldots ,g_{\mathsf {ac}} (\mathcal {A}_{k})\right ) $ and $g(\mathfrak {G})=\left ( g_{\mathsf {ac} }(h(\mathcal {A}_{0})),\ldots ,g_{\mathsf {ac}}(h(\mathcal {A}_{k}))\right ) $ . Then $\mathfrak {F}$ is reducible to $\mathfrak {G}$ .

Proof. For each $i\leqslant k$ , $g_{\mathsf {ac}}(h(\mathcal {A}_{i}))\vartriangleleft _{0}g_{\mathsf {ac}}(\mathcal {A}_{i})$ because $g(\mathfrak {G})\vartriangleleft _{1}g(\mathfrak {F})$ , and then by Fact 3.2 (ii) and Lemma 6.1, there is a reduction $f_{i}$ of $\mathfrak {F} \upharpoonright (\bigcup \mathcal {A}_{i})$ to $\mathfrak {G}\upharpoonright (\bigcup h(\mathcal {A}_{i}))$ . Letting $f=\bigcup _{i\leqslant k}f_{i}$ , we show below that f reduces $\mathfrak {F}$ to $\mathfrak {G}$ .

Assume that $\mathfrak {G}=\left \langle U,S\right \rangle $ . We have that $\{\bigcup \mathcal {A}_{0},\ldots ,\bigcup \mathcal {A}_{k}\}$ is a partition of W, and $\{\bigcup h(\mathcal {A}_{0}),\ldots ,\bigcup h(\mathcal {A}_{k})\}$ is a partition of U. Then f is a function from W to U. Because each $f_{i}$ with $i\leqslant k$ is a surjection, it follows that so is f.

Suppose that $Rwu$ where $w\in \bigcup \mathcal {A}_{i}$ and $u\in \bigcup \mathcal {A}_{j}$ with $i,j\leqslant k$ . If $i=j$ , then $Sf_{i}(w)f_{i}(u)$ because $f_{i}$ reduces $\mathfrak {F}\upharpoonright (\bigcup \mathcal {A}_{i})$ to $\mathfrak {G}\upharpoonright (\bigcup h(\mathcal {A}_{i}))$ , and thus $Sf(w)f(u)$ . Assume that $i\neq j$ . Let $\mathbf {c}\in \mathcal {A}_{i}$ and $\mathbf {c}^{\prime }\in \mathcal {A}_{j}$ such that $w\in \mathbf {c}$ and $u\in \mathbf {c}^{\prime }$ . Then $\mathbf {c\neq c}^{\prime }$ . Because $f_{i}(w)\in \bigcup h(\mathcal {A}_{i})$ and $f_{j}(u)\in \bigcup h(\mathcal {A} _{j})$ , it is clear that $f_{i}(w)\in \mathbf {d}$ and $f_{j}(u)\in \mathbf {d}^{\prime }$ for a $\mathbf {d}\in h(\mathcal {A}_{i})$ and a $\mathbf {d}^{\prime }\in h(\mathcal {A}_{j})$ . Since $Rwu$ and $\mathbf {c\neq c}^{\prime }$ , $\mathbf {c}\prec _{R}\mathbf {c}^{\prime }$ , and then $\left \langle \mathcal {A}_{i},\mathcal {A}_{j}\right \rangle \in \mathfrak {eq}(R)$ by definition. It then follows that $\left \langle h(\mathcal {A}_{i} ),h(\mathcal {A}_{j})\right \rangle \in \mathfrak {eq}(S)$ , and thus by Fact 3.2 (iii), $\mathbf {d}\prec _{S}\mathbf {d}^{\prime }$ , and then $Sf_{i}(w)f_{j}(u)$ , and hence $Sf(w)f(u)$ .

Suppose that $Sf(w)f(u)$ , where $w\in {\textstyle \bigcup } \mathcal {A}_{i}$ and $u\in {\textstyle \bigcup } \mathcal {A}_{j}$ with $i,j\leqslant k$ . If $i=j$ , $Sf_{i}(w)f_{i}(u)$ , and then there is a $v\in \bigcup \mathcal {A}_{i}$ such that $Rwv$ and $f_{i}(v)=f_{i}(u)$ , and thus $f(v)=f(u)$ . Assume that $i\neq j$ . Let $\mathbf {c}_{0}\in \mathcal {A}_{i}$ and $\mathbf {c}_{1}\in \mathcal {A}_{j}$ such that $w\in \mathbf {c}_{0}$ and $u\in \mathbf {c}_{1}$ , and let $\mathbf {d}_{0}\in h(\mathcal {A}_{i})$ and $\mathbf {d}_{1}\in h(\mathcal {A}_{j})$ such that $f(w)\in \mathbf {d}_{0}$ and $f(u)\in \mathbf {d}_{1}$ . Since $\mathcal {A} _{i}\neq \mathcal {A}_{j}$ , $h(\mathcal {A}_{i})\neq h(\mathcal {A}_{j})$ , and so $\mathbf {d}_{0}\neq \mathbf {d}_{1}$ . It then follows from $Sf(w)f(u)$ that $\mathbf {d}_{0}\prec _{S}\mathbf {d}_{1}$ , and thus $\left \langle h(\mathcal {A} _{i}),h(\mathcal {A}_{j})\right \rangle \in \mathfrak {eq}(S)$ , which implies that $\left \langle \mathcal {A}_{i},\mathcal {A}_{j}\right \rangle \in \mathfrak {eq} (R)$ . We then have by Fact 3.2 (iii) that $\mathbf {c}_{0}\prec _{R} \mathbf {c}_{1}$ , and hence $Rwu$ .

Let $\mathsf {S}=\{\mathfrak {F}_{i}\}_{i\in I}$ be an infinite sequence of finite transitive frames such that all frames in $\{\mathfrak {eq} (\mathfrak {F}_{i})\}_{i\in I}$ are isomorphic, and let $\mathfrak {F} _{i}=\left \langle W_{i},R_{i}\right \rangle $ for each $i\in I$ . Assume that $i^{\ast }$ is the smallest in I and $\mathfrak {eq}(W_{i^{\ast } })=\{\mathcal {A}_{0},\ldots ,\mathcal {A}_{m}\}$ . We then know that for each $i\in I$ , there is an isomorphism $h_{i}$ from $\mathfrak {eq}(\mathfrak {F} _{i^{\ast }})$ to $\mathfrak {eq}(\mathfrak {F}_{i})$ . Now for each $i\in I$ , assuming that each $g_{\mathsf {ac}}(h_{i}(\mathcal {A}_{j}))$ with $j\leqslant m$ is an s.r.l. of $h_{i}(\mathcal {A}_{j})$ , we let

$$\begin{align*}g_{\mathsf{S}}(\mathfrak{F}_{i})=\left( g_{\mathsf{ac}}(h_{i}(\mathcal{A} _{0})),\ldots,g_{\mathsf{ac}}(h_{i}(\mathcal{A}_{m}))\right) \text{,} \end{align*}$$

and call it a representation list of $\mathfrak {F}_{i}$ w.r.t. $\ \mathsf {S}$ . It is easy to verify that each $g_{\mathsf {S}}(\mathfrak {F} _{i})$ above with $i\in I$ is a member of $\mathsf {List}_{m+1}(\mathbb {C})$ (see (1), (3) and (4)).

Fact 6.3. Let $\{\mathfrak {F}_{i}\}_{i\in \omega }$ be an infinite sequence of frames such that for an $m\geqslant 1$ , $|\mathfrak {F}_{i}|\leqslant m$ for all $i\in \omega $ . Then there is an infinite $I\subseteq \omega $ such that all frames in $\{\mathfrak {F} _{i}\}_{i\in I}$ are isomorphic.

Lemma 6.4. Let $\mathbf {L}$ be a transitive logic of finite depth and finite suc-eq-width, let A be any nonempty set of finite rooted frames for $\mathbf {L}$ , and for any frames $\mathfrak {F\ }$ and $\mathfrak {F}^{\prime }$ in A, let $\mathfrak {F\preceq F}^{\prime }$ iff $\mathfrak {F}^{\prime }$ is reducible to $\mathfrak {F}$ . Then A is well quasi-ordered by $\mathfrak {\preceq }$ .

Proof. It is routine to verify that $\mathfrak {\preceq }$ is a quasi-order. To show that $\mathfrak {\preceq }$ is a well quasi-order, let $\{\mathfrak {F} _{i}\}_{i\in \omega }$ be an infinite sequence of elements of A. Since $\mathsf {B}_{n},\mathsf {Wid}_{k}^{\ast }\in \mathbf {L}$ for some $n,k\geqslant 1$ , we have by Propositions 2.3 and 3.1 that $\mathfrak {F}_{i}$ is of rank at most n and of suc-eq-width at most k for each $i\in \omega $ . It follows from Proposition 3.4 that $\left \vert \mathfrak {eq} (\mathfrak {F}_{i})\right \vert \leqslant n\times k\times 2^{n\times k}$ for all $i\in \omega $ , and then by Fact 6.3, there is an infinite $J\subseteq \omega $ such that all frames in $\{\mathfrak {eq} (\mathfrak {F}_{i})\}_{i\in J}$ are isomorphic. Let $\mathsf {S}=\{\mathfrak {F} _{i}\}_{i\in J}$ , and consider the sequence $(g_{\mathsf {S}}(\mathfrak {F} _{i}))_{i\in J}$ of lists, where each $g_{\mathsf {S}}(\mathfrak {F}_{i})$ with $i\in J$ is a representation list of $\mathfrak {F}_{i}$ w.r.t. $\ \mathsf {S}$ . As noted earlier, there is an $m\in \omega $ such that each $g_{\mathsf {S} }(\mathfrak {F}_{i})$ with $i\in J$ is a member of $\mathsf {List} _{m+1}(\mathbb {C})$ , and then by Proposition 5.6, there are $i<j\in J$ such that $g_{\mathsf {S}}(\mathfrak {F}_{i} )\vartriangleleft _{1}g_{\mathsf {S}}(\mathfrak {F}_{j})$ , and hence by Lemma 6.2, $\mathfrak {F}_{j}$ is reducible to $\mathfrak {F}_{i}$ , which gives that $\mathfrak {F}_{i}\mathfrak {\preceq F} _{j}$ .

Theorem 6.5. For all $k,n\geqslant 1$ , all extensions of $\mathbf {K4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}^{\ast }\}$ are finitely axiomatizable, and are hence decidable.

Proof. Let $\mathbf {L}=\mathbf {K4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}^{\ast }\}$ with $k,n\geqslant 1$ . By Theorem 2.4, all extensions of $\mathbf {L}$ have the f.m.p. To show that all extensions of $\mathbf {L}$ are finitely axiomatizable, let $\{\mathfrak {F}_{i}\}_{i\in \omega }$ be any infinite sequence of finite rooted frames for $\mathbf {L}$ . According to Lemma 6.4, $\mathfrak {F}_{j}$ is reducible to $\mathfrak {F}_{i}$ for some $i,j\in I$ with $i<j$ , and hence $\{\mathfrak {F} _{i}\}_{i\in \omega }$ is not a backward irreducible sequence. Therefore by Theorem 4.7, all extensions of $\mathbf {L}$ are finitely axiomatizable.

From the above, we know that all extensions of $\mathbf {L}$ are finitely axiomatizable. By Theorem 2.3, they all have the f.m.p., and hence are all decidable.

Some direct consequences of Theorem 6.5 are discussed in Section 7.

7 Further results

We have proved the finite axiomatizability of all transitive logics of finite depth and finite suc-eq-width. Applying this, let us go over a few classes of finitely axiomatizable transitive logics of finite depth. Firstly, each logic $\mathbf {Log}(\mathfrak {D}_{n})$ with $n>0$ from Section 3 is a transitive logic of finite depth and of suc-eq-width $1$ . Hence we have the following by Theorem 6.5:

Corollary 7.1. For each $n>0$ , all extensions of $\mathbf {Log}(\mathfrak {D}_{n})$ are finitely axiomatizable, and are hence decidable.

Rybakov proved (see [8, theorem 3]) that all extensions of $\mathbf {S4}\oplus \mathsf {B}_{2}$ are finitely axiomatizable. By applying our main theorem, we can generalize the result easily to all extensions of $\mathbf {K4}\oplus \mathsf {B}_{2}$ . Since each transitive logic $\mathbf {L}$ of depth at most $2$ is characterized by a class of rooted transitive frames of rank at most $2$ , we have $\mathsf {Wid}_{1}^{\ast } \in \mathbf {L}$ as all these frames are of suc-eq-width $1$ . Hence we obtain the following by Theorem 6.5:

Corollary 7.2. All transitive logics of depth at most 2 are finitely axiomatizable, and are hence decidable.

It has been shown (see [4, sec. 4]) that for all $n\geqslant 3$ , there is a continuum of extensions of $\mathbf {K4}\oplus \mathsf {B}_{n}$ , and hence there are non-finitely axiomatizable extensions of $\mathbf {K4}\oplus \mathsf {B}_{n}$ .

A transitive logic is weakly convergent if it contains $\Diamond (p\vee \Box p)\rightarrow \Box (p\vee \Diamond p)$ ( $\mathsf {G}_{1}$ , as named in [9]), which corresponds to piecewise weak convergence, i.e.,

$$\begin{align*}\forall x\forall y\forall z(Rxy\wedge Rxz\wedge y\neq z\wedge\lnot Ryz\wedge\lnot Rzy\rightarrow\exists x^{\prime}(Ryx^{\prime}\wedge Rzx^{\prime})). \end{align*}$$

Rybakov proved (see [8, theorem 2]) that all extensions of $\mathbf {S4}\oplus \{\mathsf {B}_{3},\mathsf {G}_{1}\}$ are finitely axiomatizable. By applying our main theorem, we generalize it to the case of $\mathbf {K4}\oplus \{\mathsf {B}_{3},\mathsf {G}_{1}\}$ . Since each weakly convergent transitive logic $\mathbf {L}$ of depth at most $3$ is characterized by a class of rooted transitive frames of rank at most $3$ satisfying piecewise weak convergence, we have $\mathsf {Wid}_{1}^{\ast } \in \mathbf {L}$ as all these frames are of suc-eq-width $1$ . Hence we obtain the following by Theorem 6.5:

Corollary 7.3. All weakly convergent transitive logics of depth at most 3 are finitely axiomatizable, and are hence decidable.

Let $a,b_{0},b_{1},\ldots ,c_{0},c_{1},\ldots $ be all distinct. For each $n\in \omega $ , let $B_{n}=\{b_{k}:k\leqslant n+1\}$ and $C_{n}=\{c_{k} :k\leqslant n+1\}$ , and let $\mathfrak {G}_{n}=\left \langle U_{n} ,S_{n}\right \rangle $ where

$$ \begin{align*} U_{n} & =\{a\}\cup B_{n}\cup C_{n}\text{,}\\ S_{n} & =\{\left\langle a,u\right\rangle :u\in B_{n}\cup C_{n}\}\cup \{\left\langle b_{k},c_{m}\right\rangle :k,m\leqslant n+1\text{ and }k\neq m\}\text{.} \end{align*} $$

Intuitively speaking, each $\mathfrak {G}_{n}$ with $n\in \omega $ is a finite rooted strict partial order of rank $3$ in which a is the root, and each $b_{k}$ ( $c_{k}$ ) with $k\leqslant n+1$ is of rank $2$ (rank $1$ ) and sees all points of rank $1$ except $c_{k}$ . Let $\mathfrak {A}=\left \langle \{d\},\varnothing \right \rangle $ , where d is a new point not in any $U_{n}$ , and for each $n\in \omega $ , let $\mathfrak {B}_{n}=\mathfrak {G}_{n} \oplus \mathfrak {A}$ . Each $\mathfrak {B}_{n}$ is a weakly convergent frame of rank $4$ . It can be shown that $\{\mathfrak {B}_{n}\}_{n\in \omega }$ is backward irreducible, and hence by Theorem 4.7, there are non-finitely axiomatizable extensions of $\mathbf {K4}\oplus \{\mathsf {B} _{n},\mathsf {G}_{1}\}$ for all $n\geqslant 4$ .

Consider the following formulas, where $k\geqslant 1$ :

$$\begin{align*}\mathsf{Wid}_{k}^{\Box}={ {\textstyle\bigwedge\nolimits_{0\leqslant i\leqslant k}} }\Diamond(p_{i}\wedge\Box p_{i})\rightarrow{ {\textstyle\bigvee\nolimits_{0\leqslant i\neq j\leqslant k}} }\Diamond(p_{i}\wedge p_{j}). \end{align*}$$

Recall that a cluster $\mathbf {c}$ is final if $\left. \mathbf {c} \right \uparrow ^{-}=\varnothing $ , that is, it has no proper successors. A transitive frame $\mathfrak {F}=\left \langle W,R\right \rangle $ is bounded if each maximal R-chain includes an element of some final cluster in $\mathfrak {F}$ .

Fact 7.4. Let $\mathfrak {F}$ be any rooted transitive frame and $k\geqslant 1$ . Then $\mathfrak {F}\vDash \mathsf {Wid}_{k}^{\Box }$ iff $|A|\leqslant k$ for each antichain A in $\mathfrak {F}$ such that $\left. x\right \uparrow \cap \left. y\right \uparrow =\varnothing $ for all distinct $x,y\in A$ ; and consequently, if $\mathfrak {F}$ is bounded, then $\mathfrak {F}\vDash \mathsf {Wid}_{k}^{\Box }$ iff the number of final clusters in $\mathfrak {F}$ is at most $k$ .

By Fact 7.4, each rooted transitive frame of rank $3$ for $\mathsf {Wid}_{k}^{\Box }$ is of suc-eq-width at most $2^{k}$ ; furthermore, each extension of $\mathbf {K4}\oplus \{\mathsf {B}_{3},\mathsf {Wid}_{k}^{\Box }\}$ is characterized by a class of these frames. Hence all extensions of $\mathbf {K4}\oplus \{\mathsf {B}_{3},\mathsf {Wid}_{k}^{\Box }\}$ are of suc-eq-width at most $2^{k}$ , which implies by Theorem 6.5 the following generalization of Corollary 7.3:

Corollary 7.5. For each $k\geqslant 1$ , all extensions of $\mathbf {K4}\oplus \{\mathsf {B} _{3},\mathsf {Wid}_{k}^{\Box }\}$ are finitely axiomatizable, and are hence decidable.

For each $k\geqslant 1$ , let $\mathfrak {A}_{k}=\left \langle \{d_{0} ,\ldots ,d_{k-1}\},\varnothing \right \rangle $ , where $d_{0},d_{1},\ldots $ are all distinct new points, and let $\mathfrak {B}_{n,k}=\mathfrak {G}_{n} \oplus \mathfrak {A}_{k}$ for each $n\in \omega $ . Each $\mathfrak {B}_{n,k}$ is a frame of rank $4$ and has k final clusters. It can be proved that $\{\mathfrak {B}_{n,k}\}_{n\in \omega }$ is backward irreducible for each $k\geqslant 1$ , and hence by Theorem 4.7, there are non-finitely axiomatizable extensions of $\mathbf {K4}\oplus \{\mathsf {B} _{n},\mathsf {Wid}_{k}^{\Box }\}$ for all $n\geqslant 4$ and $k\geqslant 1$ .

Since transitive logics of finite width are of finite suc-eq-width, we have the following corollary by Theorem 6.5, which generalizes Rybakov’s result of the finite axiomatizability of all extensions of $\mathbf {S4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}\}$ with $n,k\geqslant 1$ (see [8, theorem 1]).

Corollary 7.6. All transitive logics of finite depth and of finite width are finitely axiomatizable, and are hence decidable.

Consider the following formulas, where $k\geqslant 1$ :

$$\begin{align*}\mathsf{Wid}_{k}^{1}={ {\textstyle\bigwedge\nolimits_{0\leqslant i\leqslant k}} }\Diamond(p_{i}\wedge\Diamond\Box q_{i}\wedge\lnot q_{i})\rightarrow{ {\textstyle\bigvee\nolimits_{0\leqslant i\neq j\leqslant k}} }\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j})). \end{align*}$$

Fact 7.7. Let $\mathfrak {F}$ be any rooted transitive frame, and $k\geqslant 1$ . Then $\mathfrak {F}\vDash \mathsf {Wid}_{k}^{1}$ iff each antichain in $\mathfrak {F}$ contains at most $k$ points of rank greater than $1$ .

By Fact 7.7, each rooted transitive frame of finite rank for $\mathsf {Wid}_{k}^{1}$ is of suc-eq-width at most $k+1$ ; furthermore, each extension of $\mathbf {K4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}^{1}\}$ is characterized by a class of these frames. Hence all extensions of $\mathbf {K4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}^{1}\}$ are of suc-eq-width at most $k+1$ , which gives the following generalization of Corollary 7.6 by Theorem 6.5:

Corollary 7.8. For each $n\geqslant 1$ and each $k\geqslant 1$ , all extensions of $\mathbf {K4}\oplus \{\mathsf {B}_{n},\mathsf {Wid}_{k}^{\mathsf {1}}\}$ are finitely axiomatizable, and are hence decidable.

Although our Theorem 6.5 is general enough to imply the results above, it does not include all transitive logics of finite depth whose extensions are all finitely axiomatizable. Consider the following formulas from [12], where $n\geqslant 1$ :

$$\begin{align*}\mathsf{Wid}_{n}^{+}=q\wedge\Diamond(\lnot\Box q\wedge{ {\textstyle\bigwedge\nolimits_{0\leqslant i\leqslant n}} }\Diamond p_{i})\rightarrow{ {\textstyle\bigvee\nolimits_{0\leqslant i\neq j\leqslant n}} }\Diamond(p_{i}\wedge(p_{j}\vee\Diamond p_{j})). \end{align*}$$

It has been proved (see [12, proposition 10]) that for any transitive frame $\mathfrak {F}=\left \langle W,R\right \rangle $ and any $n\geqslant 1$ , $\mathfrak {F}\vDash \mathsf {Wid}_{n}^{+}$ iff for each $w,u\in W$ with $\vec {R}wu$ , the subframe of $\mathfrak {F}$ generated by u is of width at most n. Let $a,b_{0},b_{1},\ldots ,c_{0},c_{1},\ldots $ be all distinct, for each $n\in \omega $ , let $B_{n}=\{b_{k}:k\leqslant n+1\}$ and $C_{n}=\{c_{k}:k\leqslant n+1\}$ , and let $\mathfrak {G}_{n}^{^{\prime } }=\left \langle U_{n},S_{n}^{\prime }\right \rangle $ where

$$ \begin{align*} U_{n}= & \{a\}\cup B_{n}\cup C_{n}\text{,}\\ S_{n}^{\prime}= & \{\left\langle u,u\right\rangle :u\in U_{n}\}\cup \{\left\langle a,u\right\rangle :u\in B_{n}\cup C_{n}\}\\ & \cup\{\left\langle b_{k},c_{m}\right\rangle :k,m\leqslant n+1\text{ and }k=m\}\text{.} \end{align*} $$

Intuitively speaking, each $\mathfrak {G}_{n}^{\prime }$ with $n\in \omega $ is a finite rooted partial order of rank $3$ in which a is the root, and each $b_{k}$ ( $c_{k}$ ) with $k\leqslant n+1$ is of rank $2$ (rank $1$ ) and sees only point $c_{k}$ of rank $1$ . It should be clear that all $\mathfrak {G} _{n}^{\prime }$ are frames for $\mathbf {S4}\oplus \{\mathsf {B}_{k} ,\mathsf {Wid}_{1}^{+}\}$ with $k\geqslant 3$ , and the suc-eq-width of these $\mathfrak {G}_{n}^{\prime }$ are unbounded. Hence, $\mathbf {S4}\oplus \{\mathsf {B}_{k},\mathsf {Wid}_{1}^{+}\}$ is not a logic of finite suc-eq-width, although it has been shown (see [12, corollary 2]) that all extensions of it are finitely axiomatizable.