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

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.

The following formulas are from [Reference Segerberg9, 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., [Reference Chagrov and Zakharyaschev2, proposition 3.44]) and Proposition 2.4 (see [Reference Segerberg9, theorem 6.6]):

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 [Reference Fine5, sec. 3, theorem 1]):

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 [Reference Xu11, proposition 3.3]).

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$ .Footnote ¹ 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.

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.

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., [Reference Chagrov and Zakharyaschev2, theorem 4.12]):

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.

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 Footnote ² 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.

The following is Lemma 3.20 from [Reference Blackburn, de Rijke and Venema1], whose proof is left to the readers.

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., [Reference Fine3, Reference Nagle7, Reference Xu10]).

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

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., [Reference Gallier6, lemma 2.6]).

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

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

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

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

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.

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.

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

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:

Rybakov proved (see [Reference Rybakov8, 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:

It has been shown (see [Reference Fine4, 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 [Reference Segerberg9]), 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 [Reference Rybakov8, 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:

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

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:

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 [Reference Rybakov8, theorem 1]).

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

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:

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 [Reference Zhang12], 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 [Reference Zhang12, 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 [Reference Zhang12, corollary 2]) that all extensions of it are finitely axiomatizable.