1 Introduction
We study local tabularity of normal propositional (poly)modal logics.
A logic L is locally tabular, if, for every finite k, L contains only a finite number of pairwise nonequivalent formulas in a given k variables. Equivalently, a logic L is locally tabular iff the variety of its algebras is locally finite, i.e., every L-algebra is locally finite. Local tabularity is a strong property: if a logic is locally tabular, then it has the finite model property (thus it is Kripke complete); every extension of a locally tabular logic is locally tabular (thus it has the finite model property); every finitely axiomatizable extension of a locally tabular logic is decidable.
Local tabularity is well-studied for the case of unimodal transitive logics (a logic is transitive, if it contains the formula
$\lozenge \lozenge p\rightarrow \lozenge p$
, which expresses the transitivity of a binary relation). According to the classical results by Segerberg [Reference Segerberg28] and Maksimova [Reference Maksimova24], a transitive logic is locally tabular iff it contains a modal formula
$B_h$
of finite height for some finite h.
In the non-transitive unimodal, and in the polymodal case, no axiomatic criterion of local tabularity is known. We provide sufficient semantic and axiomatic conditions for local tabularity.
The paper is organized as follows.
In Section 2, we provide basic definitions and an exposition of some previous results.
In Section 3, we discuss k-finite logics: we say that L is k-finite for
$k<\omega $
, if L contains only a finite number of pairwise nonequivalent formulas in a given k variables. It is known [Reference Maksimova25] that every unimodal transitive 1-finite logic is locally tabular. Recently [Reference Shapirovsky33] it was observed that without transitivity, this equivalence does not hold. In Section 3, we give corollaries of k-finiteness and in particular, give a necessary axiomatic condition for
$2$
-finiteness of a logic.
In Section 4, we prove that local tabularity does not depend on reflexivity. Namely, given a class
$\mathcal {F}$
of frames, consider the class
$\mathcal {F}^{\mathrm {r}}$
of frames, where the reflexive closure operation was applied to every relation in every frame in
$\mathcal {F}$
. We show that if the logic of
$\mathcal {F}^{\mathrm {r}}$
is locally tabular, then the logic of
$\mathcal {F}$
is locally tabular as well (the converse implication is trivial).
In Section 5, we consider the operation of sum on Kripke frames, where a family of frames–summands is indexed by elements of another frame. There is a number of transfer results for sums in modal logic: they relate to questions of complete axiomatization [Reference Balbiani, Ghilardi and Sebastiani2–Reference Beklemishev4], finite model property and decidability [Reference Babenyshev and Rybakov1, Reference Shapirovsky31], computational complexity [Reference Shapirovsky30, Reference Shapirovsky34]. Local tabularity also transfers under the operation of sum: we show that if both the logic of indices and the logic of summands are locally tabular, then the logic of corresponding sums is locally tabular. This fact implies the following axiomatic transfer result. Consider two disjoint alphabets
$\mathrm {A}$
and
$\mathrm {B}$
of modalities. Let
$\Phi (\mathrm {A},\mathrm {B})$
be the set of all formulas
$$ \begin{align*} {\lozenge^{\mathrm{h}}} {\lozenge^{\mathrm{v}}} p\to {\lozenge^{\mathrm{v}}} p, \; {\lozenge^{\mathrm{v}}}{\lozenge^{\mathrm{h}}} p\to {\lozenge^{\mathrm{v}}} p, \;{\lozenge^{\mathrm{v}}} p\to \Box^{\mathrm{h}} {\lozenge^{\mathrm{v}}} p \end{align*} $$
with
${\lozenge ^{\mathrm {v}}}$
in
$\mathrm {A}$
and
${\lozenge ^{\mathrm {h}}}$
in
$\mathrm {B}$
. These formulas were considered earlier in [Reference Balbiani, Ghilardi and Sebastiani2] in connection with axiomatization problems for lexicographic products of modal logics, and also in [Reference Beklemishev4] in the context of polymodal provability logic. Let
$L_1$
be a locally tabular logic in the language of
$\mathrm {A}$
, and let
$L_2$
be a locally tabular logic in the language of
$\mathrm {B}$
. Let
$L_1*L_2$
be the fusion of
$L_1$
and
$L_2$
, that is, the smallest logic in the language of
$\mathrm {A}\cup \mathrm {B}$
that contains
$L_1\cup L_2$
. It is well-known that the fusion operation does not preserve local tabularity. However, the extension of
$L_1*L_2$
with the formulas
$\Phi (\mathrm {A},\mathrm {B})$
remains locally tabular, provided that this extension is Kripke complete, in particular, if
$L_1$
and
$L_2$
are canonical.
2 Preliminaries
2.1 Basic definitions
We assume that the reader is familiar with basic notions in modal logic; see, e.g., [Reference Blackburn, De Rijke and Venema10, Reference Chagrov and Zakharyaschev14] for the references.
2.1.1 Modal syntax.
Fix a set
$\mathrm {A}$
, the alphabet of modalities. We will always assume that
$\mathrm {A}$
is finite.
The set of modal formulas over
$\mathrm {A}$
is built from a countable set of variables 
using Boolean connectives
$\bot ,\rightarrow $
and unary connectives
$\lozenge \in \mathrm {A}$
(modalities). Other logical connectives are defined as abbreviations in the standard way, in particular
$\Box \varphi $
denotes
$\neg \lozenge \neg \varphi $
(perhaps with an index).
We will also use the following abbreviations:
$\lozenge ^0 \varphi =\varphi $
,
$\lozenge ^{i+1}\varphi =\lozenge ^i\lozenge \varphi $
,
$\lozenge ^{\leq m} \varphi = \bigvee _{i\leq m} \lozenge ^i \varphi $
,
$\Box ^{\leq m} \varphi =\neg \lozenge ^{\leq m} \neg \varphi $
. Additionally, we write
$\lozenge _{\mathrm {A}}\varphi $
for
$\bigvee _{\lozenge \in \mathrm {A}}\lozenge \varphi $
.
The term unimodal refers to the case when
$\mathrm {A}$
is a singleton.
A modal formula
$\varphi $
is said to be a k-formula for
$k\leq \omega $
, if every variable occurring in
$\varphi $
belongs to
$\{p_i\mid i<k\}$
.
2.1.2 Relational and algebraic semantics.
An
$\mathrm {A}$
-frame is a structure
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
, where X is a set and
${R_\lozenge \subseteq X{\times }X}$
for
$\lozenge \in \mathrm {A}$
. We write
$\mathop {\mathrm {dom}}{F}$
for X, the domain of F.Footnote
1
For
$a\in X$
,
$Y\subseteq X$
, we put
$R_\lozenge (a)=\{b\mid aR_\lozenge b\}$
,
$R_\lozenge [Y]=\bigcup _{a\in Y} R_\lozenge (a)$
.
Let
$k\leq \omega $
. A k-valuation in a frame F is a map
$\{p_i\mid i<k\}\to \mathcal {P}(X)$
, where
$\mathcal {P}(X)$
is the set of all subsets of X. A (Kripke) k-model on F is a pair
$(F,\theta )$
, where
$\theta $
is a k-valuation. The truth of k-formulas in a k-model is defined in the usual way, in particular
${(F,\theta ),a\vDash \lozenge \varphi }$
means that
${(F,\theta ),b\vDash \varphi }$
for some b in
$R_\lozenge (a)$
. We put
$$ \begin{align*}\bar{\theta}(\varphi)=\{a\mid (F,\theta),a\vDash\varphi\}.\end{align*} $$
A k-formula
$\varphi $
is true in a k-model M, if
$M,a\vDash \varphi $
for all a in M. A k-formula
$\varphi $
is valid in a frame F, in symbols
$F\vDash \varphi $
, if
$\varphi $
is true in every k-model on F.
For a binary relation R on a set X, let
$R^*$
denote its transitive reflexive closure
$\bigcup _{i <\omega } R^i$
, where
$R^0$
is the diagonal
$\{(a,a)\mid a\in X\}$
on X,
$R^{i+1}=R\circ R^i$
, and
$\circ $
is the composition. For an
$\mathrm {A}$
-frame
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
, let
$$ \begin{align*}R_F=\bigcup_{\lozenge\in \mathrm{A}} R_\lozenge.\end{align*} $$
The restriction of F to its subset Y,
$F{\upharpoonright } Y$
in symbols, is the frame
$(Y, (R_\lozenge \cap (Y\times Y))_{\lozenge \in \mathrm {A}})$
.
The notions of p-morphism, generated subframe, disjoint sum of frames are defined in the standard way, see, e.g., [Reference Chagrov and Zakharyaschev14, Section 3.3] or [Reference Blackburn, De Rijke and Venema10, Sections 2.1 and 3.3].
An
$\mathrm {A}$
-modal algebra is a Boolean algebra endowed with unary operations
$f_\lozenge $
,
$\lozenge \in \mathrm {A}$
, that distribute w.r.t. finite disjunctions. A modal formula
$\varphi $
is valid in an algebra B, if
$\varphi =1$
holds in B. The (complex) algebra
$\mathop {\mathrm {Alg}}{F}$
of an
$\mathrm {A}$
-frame
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
is the powerset Boolean algebra of X endowed with the following unary operations
$f_\lozenge $
,
$\lozenge \in \mathrm {A}$
:
$f_\lozenge (Y)=R_\lozenge ^{-1}[Y]$
for
$Y\subseteq X$
. It is immediate that the algebra of an
$\mathrm {A}$
-frame is an
$\mathrm {A}$
-modal algebra, and that in a k-model
$(F,\theta )$
,
$\bar {\theta }(\varphi )$
is the value of
$\varphi $
under
$\theta $
in the modal algebra
$\mathop {\mathrm {Alg}}{F}$
, see [Reference Blackburn, De Rijke and Venema10, Section 5.2] for details.
A formula is valid in a class
$\mathcal {C}$
of (relational or algebraic) structures, if it is valid in every structure in
$\mathcal {C}$
. Validity of a set of formulas means validity of every formula in this set.
2.1.3 Logics.
A (propositional normal modal) logic in the language of
$\mathrm {A}$
is a set L of formulas over
$\mathrm {A}$
that contains all classical tautologies, the axioms
$\neg \lozenge \bot $
and
$\lozenge (p_0\vee p_1) \rightarrow \lozenge p_0\vee \lozenge p_1$
for each
$\lozenge $
in
$\mathrm {A}$
, and is closed under the rules of modus ponens, substitution, and monotonicity; the latter means that for each
$\lozenge $
in
$\mathrm {A}$
,
$\varphi \rightarrow \psi \in L$
implies
$\lozenge \varphi \rightarrow \lozenge \psi \in L$
. We write
$L\vdash \varphi $
for
$\varphi \in L$
. For a set
$\Phi $
of modal formulas over
$\mathrm {A}$
,
$L+\Phi $
is the smallest normal logic containing
$L\cup \Phi $
.
An L-structure (a frame or algebra) is a structure where L is valid.
The set of all formulas that are valid in a class
$\mathcal {C}$
of (relational or algebraic) structures is called the logic of
$\mathcal {C}$
and is denoted by
$\mathop {\mathrm {Log}}{\mathcal {C}}$
. It is straightforward the
$\mathop {\mathrm {Log}}{\mathcal {C}}$
is a propositional normal modal logic. Moreover, any propositional normal modal logic L is the logic of the class of L-algebras, see, e.g., [Reference Chagrov and Zakharyaschev14, Section 7.5]. For a structure B, we write
$\mathop {\mathrm {Log}}{B}$
for
$\mathop {\mathrm {Log}}{\{B\}}$
.
A logic L is Kripke complete, if L is the logic of a class of frames. A logic has the finite model property, if it is the logic of a class of finite frames (by the cardinality of a frame, algebra, or model we mean the cardinality of its domain).
The k-canonical model of L is built from maximal L-consistent sets of k-formulas; the canonical relations and the valuation are defined in the standard way. The following fact is well-known, see, e.g., [Reference Chagrov and Zakharyaschev14, Chapter 8].
Proposition 2.1 [Canonical Model Theorem].
Let M be the k-canonical model of a logic L. Then for all k-formulas
$\varphi $
we have:
$L\vdash \varphi $
iff
$\varphi $
is true in M.
2.2 Locally tabular logics; Maltsev’s criterion
The algebraic notions required for this subsection can be found in, e.g., [Reference Burris and Sankappanavar12, Chapter 2].
Recall that an algebra B is locally finite, if every finitely-generated subalgebra of B is finite.
Recall that a logic L is locally tabular, if, for every
$k<\omega $
, L contains only a finite number of pairwise nonequivalent k-formulas. The latter means that the countably generated free (or Lindenbaum) algebra
$\mathop {\mathrm {Lind}}(L,\omega )$
of L is locally finite. Equivalently, a logic L is locally tabular iff the variety of its algebras is locally finite, i.e., every L-algebra is locally finite.
For
$k<\omega $
, we say that L is k-finite, if L contains only a finite number of pairwise nonequivalent k-formulas. Equivalently, L is k-finite, if the k-generated free algebra
$\mathop {\mathrm {Lind}}(L,k)$
of L is finite, and equivalently, the k-canonical model of L is finite.
The following criterion of local finiteness was given by A. Maltsev [Reference Malcev26]. A class
$\mathcal {C}$
of algebras of a finite signature is said to be uniformly locally finite, if there exists a function
$f:\omega \to \omega $
such that the cardinality of a subalgebra of any
$B\in \mathcal {C}$
generated by
$k<\omega $
elements does not exceed
$f(k)$
. Local finiteness of the variety
$\mathcal {K}$
generated by
$\mathcal {C}$
is equivalent to uniform local finiteness of
$\mathcal {C}$
[Reference Malcev26, Section 14, Theorem 3]. Moreover, from the proof of this theorem it follows that if every k-generated subalgebra of any algebra
$A\in \mathcal {C}$
has at most n elements for a fixed finite n, then the k-generated free algebra of
$\mathcal {K}$
is finite. In terms of modal logic, we have:
Theorem 2.2 (Corollary of [Reference Malcev26]).
Let L be the logic of a class
$\mathcal {F}$
of
$\mathrm {A}$
-frames.
-
(1) L is locally tabular iff
$\{\mathop {\mathrm {Alg}}{F}\mid F\in \mathcal {F}\}$
is uniformly locally finite. -
(2) Let
$k<\omega $
. L is k-finite iff there exists
$n<\omega $
such that for every
$F\in \mathcal {F}$
, the cardinality of every subalgebra of
$\mathop {\mathrm {Alg}}{F}$
generated by k elements is not greater than n.
2.3 Local tabularity, pretransitivity, and finite height
In this subsection we discuss the criterion of local tabularity for unimodal logics of transitive frames given in [Reference Maksimova24, Reference Segerberg28], and its corollaries for all modal logics [Reference Chagrov and Zakharyaschev14], [Reference Shapirovsky and Shehtman35].
A poset is of height
$h<\omega $
, if it contains a chain of h elements and no chains of more than h elements.
Recall that in an
$\mathrm {A}$
-frame
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
,
$R_F=\bigcup _{\lozenge \in \mathrm {A}} R_\lozenge $
. A cluster in an
$\mathrm {A}$
-frame F is an equivalence class with respect to the relation
$\sim _F\; =\{(a,b)\mid a R^*_F b \text { and } b R^*_F a\}$
. For clusters
$C, D$
, put
$C\leq _F D$
iff
$a R^*_F b$
for some
$a\in C, b\in D$
. The poset
$(X{/}{\sim _F},\leq _F)$
is called the skeleton of F. The height of a frame F is the height of its skeleton.
Consider the following formulas:
$$ \begin{align} B_0=\bot, \quad B_{h} = p_{h} \to \Box(\lozenge p_{h} \lor B_{h-1}). \end{align} $$
In the unimodal transitive case, the following holds [Reference Segerberg28]:
$$ \begin{align} (X,R)\vDash B_h \text{ iff } \text{the height of }(X,R)\text{ is not greater than }h. \end{align} $$
A unimodal logic is called transitive, if it contains the formula
$\lozenge \lozenge p\rightarrow \lozenge p$
, which validity in a frame
$(X,R)$
means transitivity of R. The following criterion of local tabularity for unimodal transitive logics was given in [Reference Maksimova24, Reference Segerberg28] (see also [Reference Chagrov and Zakharyaschev14, Section 12.4]):
$$ \begin{align} \text{ A transitive logic is locally tabular iff it contains }B_h\text{ for some }h< \omega. \end{align} $$
In [Reference Shapirovsky and Shehtman35], this criterion was extended to unimodal logics of relations such that
$R^{m+1}\subseteq R\cup R^0$
for a fixed positive m: as well as in the transitive case, local tabularity is equivalent to finite height for such logics. However, an axiomatic criterion of local tabularity for polymodal logics, and even for all unimodal logics is unknown.
Finite height and some weaker version of transitivity is a necessary, but in general not a sufficient condition for local tabularity. Namely, for a binary relation R, put
$R^{\leq m}= \bigcup _{i \leq m} R^i$
. R is called m-transitive, if
$R^{\leq m}=R^*$
. R is called pretransitive, if it is m-transitive for some finite m. It is straightforward that
$$ \begin{align} R\text{ is }m\text{-transitive iff }R^{m+1}\subseteq R^{\leq m}. \end{align} $$
Recall that
$\lozenge ^{\leq m} \varphi = \bigvee _{i\leq m} \lozenge ^i \varphi $
,
$\Box ^{\leq m} \varphi =\neg \lozenge ^{\leq m} \neg \varphi $
, and
$\lozenge _{\mathrm {A}}\varphi $
denotes
$\bigvee _{\lozenge \in \mathrm {A}}\lozenge \varphi $
. For any
$\mathrm {A}$
-frame F, we have the following equivalence [Reference Kracht21, Section 3.4]:
$$ \begin{align} R_F\text{ is }m\text{-transitive iff }F\vDash \lozenge_{\mathrm{A}}^{m+1} p \rightarrow \lozenge_{\mathrm{A}}^{\leq m} p. \end{align} $$
A logic L is said to be m-transitive, if
$L\vdash \lozenge _{\mathrm {A}}^{m+1} p \rightarrow \lozenge _{\mathrm {A}}^{\leq m} p$
. L is pretransitive if it is m-transitive for some
$m\geq 0$
.
Put
$$ \begin{align*} B_0^{[m]} =\bot,\quad B^{[m]}_{h} = p_{h} \to \Box_{\mathrm{A}}^{\leq m} (\lozenge_{\mathrm{A}}^{\leq m} p_{h} \lor B^{[m]}_{h-1}). \end{align*} $$
Assume that
$F=(X,(R_i)_{i<n})$
is m-transitive. In this case, the modal operator
$\lozenge _{\mathrm {A}}^{\leq m}$
relates to
$R^*_F$
. Observe that the height of F is the height of the preorder
$(X,R^*_F)$
. Hence from (2) we obtain:
$$ \begin{align} F\vDash B^{\leq m}_h\text{ iff the height of }F\text{ is not greater than }h. \end{align} $$
For a unimodal formula
$\varphi $
, let
$\varphi ^{[m]}$
be the formula obtained from
$\varphi $
by replacing each occurrence of
$\lozenge $
in
$\varphi $
with
$\lozenge _{\mathrm {A}}^{\leq m}$
. The following fact follows from [Reference Gabbay, Shehtman and Skvortsov18, Lemma 1.3.45].
Proposition 2.3. For a pretransitive logic L, the set
$\{\varphi \mid L\vdash \varphi ^{[m]} \}$
is a transitive logic.
Assume that L is 1-finite. Then its 1-canonical frame is finite. Every finite frame is m-transitive for some m. Since m-transitivity is expressed by a formula in one variable, by the Canonical Model Theorem (Proposition 2.1) we obtain
$L\vdash \lozenge _{\mathrm {A}}^{m+1} p \rightarrow \lozenge _{\mathrm {A}}^{\leq m} p$
.Footnote
2
Moreover, if L is 1-finite, then L contains an axiom of finite height [Reference Shapirovsky and Shehtman35]. Indeed, by Proposition 2.3, the set
$^{[m]}L=\{\varphi \mid L\vdash \varphi ^{[m]} \}$
is a transitive logic. Since L is 1-finite, the logic
$^{[m]}L$
is also 1-finite. The following result was obtained in [Reference Maksimova25, Theorem 1]:
$$ \begin{align} \text{ A unimodal transitive logic is locally tabular iff it is 1-finite. } \end{align} $$
Hence,
$^{[m]}L$
is locally tabular, and by (3),
$^{[m]}L\vdash B_h$
for some
$h<\omega $
. It follows that
$L\vdash B_h^{[m]}.$
So we have the following necessary condition of 1-finiteness:
Theorem 2.4 [Reference Shapirovsky and Shehtman35].
If a logic L is 1-finite, then for some
$h,m<\omega $
,
$L\vdash \lozenge _{\mathrm {A}}^{m+1} p \rightarrow \lozenge _{\mathrm {A}}^{\leq m} p$
and
$L\vdash B_h^{[m]}.$
Unlike in the unimodal transitive case, in general the formulas in the above theorem do not imply local tabularity: there is a unimodal 2-transitive logic containing
$B^{[2]}_1$
that is not locally tabular [Reference Byrd13], and even not 1-finite [Reference Makinson23].
The equivalence (7) also does not transfer for the non-transitive case: in Section 3.1, we give examples of 1-finite but not locally tabular modal logics.
2.4 Locally finite modal algebras and partitions of frames
A partition
$\mathcal {V}$
of a set X is a family of non-empty pairwise disjoint sets such that
$X=\bigcup \mathcal {V}$
. Equivalently, a partition is the quotient set of X by an equivalence; this equivalence is denoted by
$\sim _{\mathcal {V}}$
. A partition
$\mathcal {U}$
refines
$\mathcal {V}$
, if each element of
$\mathcal {V}$
is the union of some elements of
$\mathcal {U}$
, equivalently,
$\sim _{\mathcal {U}}\;\subseteq \;\sim _{\mathcal {V}}$
. For a family
$\mathcal {S}$
of subsets of X, the partition induced by
$\mathcal {S}$
is the quotient set
$X/{\sim }$
, where
$$ \begin{align*}a\sim b \text{ iff } \forall Y\in\mathcal{S} \, (a\in Y \Leftrightarrow b\in Y).\end{align*} $$
Definition 2.5. Let X be a set, R a binary relation on X. A partition
$\mathcal {U}$
of X is said to be R-tuned, if for every
$U,V\in \mathcal {U}$
,
$$ \begin{align} \exists a\in U \exists b\in V \, (aR b) \,\Rightarrow\, \forall a\in U \exists b\in V \, (aR b). \end{align} $$
Let
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
be an
$\mathrm {A}$
-frame. A partition
$\mathcal {U}$
of X is said to be tuned in F, if it is
$R_\lozenge $
-tuned for every
$\lozenge \in \mathrm {A}$
. The frame F is said to be tunable, if for every finite partition
$\mathcal {V}$
of F there exists a finite tuned refinement
$\mathcal {U}$
of
$\mathcal {V}$
. A class
$\mathcal {F}$
of
$\mathrm {A}$
-frames is called f-tunable for a function
$f:\omega \to \omega $
, if for every
$F\in \mathcal {F}$
, for every finite partition
$\mathcal {V}$
of F there exists a refinement
$\mathcal {U}$
of
$\mathcal {V}$
such that
$|\mathcal {U}|\leq f(|\mathcal {V}|)$
and
$\mathcal {U}$
is tuned in F. A class
$\mathcal {F}$
is uniformly tunable, if it is f-tunable for some
$f:\omega \to \omega $
.
In [Reference Segerberg29], tuned partitions were used in a proof of Bull’s theorem (see the definition of Franzen’s filtration in [Reference Segerberg29]). In [Reference Blok11, Corollary 3.3], it was observed that a tuned partition on a frame F induces a subalgebra of the algebra
$\mathop {\mathrm {Alg}}{F}$
; see Proposition 2.6 below.
In [Reference Shapirovsky and Shehtman35], it was shown that a modal logic is locally tabular iff it is the logic of a uniformly tunable class of frames; below we explain how this result follows from Maltsev’s criterion, Theorem 2.2.
It is immediate from the above definition that
$$ \begin{align} \textstyle \mathcal{U}\text{ is }R\text{-tuned} \text{ iff } \forall V\in\mathcal{U}\,\exists \mathcal{S}\subseteq \mathcal{U} \; (R^{-1}[V]=\bigcup \mathcal{S}). \end{align} $$
Proposition 2.6. Let
$\mathcal {U}$
be a partition of a frame F. Then
$\mathcal {U}$
is tuned in F iff the family
$\{\bigcup \mathcal {S}\mid \mathcal {S}\subseteq \mathcal {U}\}$
forms a subalgebra of the modal algebra
$\mathop {\mathrm {Alg}}{F}$
.
Proof. Let
$\mathcal {T}=\{\bigcup \mathcal {S}\mid \mathcal {S}\subseteq \mathcal {U}\}$
, R one of the relations of F.
Assume that
$\mathcal {U}$
is tuned in F. Clearly,
$\mathcal {T}$
is closed under the Boolean operations. For
$\mathcal {S} \subseteq \mathcal {U}$
, we have
$R^{-1}[\bigcup \mathcal {S}]=\bigcup \{R^{-1}[V]\mid V\in \mathcal {S}\}$
, so it follows from (9) that
$R^{-1}[\bigcup \mathcal {S}]\in \mathcal {T}$
. Hence,
$\mathcal {T}$
is closed under operations of
$\mathop {\mathrm {Alg}}{F}$
.
Conversely, assume that
$\mathcal {T}$
forms a subalgebra of
$\mathop {\mathrm {Alg}}{F}$
. Then for every
$V\in \mathcal {U}$
,
$R^{-1}[V]\in \mathcal {T}$
. Hence,
$R^{-1}[V]$
is the union of some elements of
$\mathcal {U}$
. By (9),
$\mathcal {U}$
is R-tuned.
Proposition 2.7. Let
$k<\omega $
,
$\mathcal {V}$
the partition induced by subsets
$P_0,\ldots , P_{k-1}$
of a frame F, B the subalgebra of
$\mathop {\mathrm {Alg}}{F}$
generated by these sets.
-
(1) If B is finite, then the partition
$\mathcal {U}$
of F induced by the elements of B is a tuned refinement of
$\mathcal {V}$
. -
(2) If
$\mathcal {U}$
is a tuned refinement of
$\mathcal {V}$
, then every element of B is the union of some elements of
$\mathcal {U}$
.
Proof. (1) All sets
$P_i$
belong to B, so
$\sim _{\mathcal {U}}\;\subseteq \;\sim _{\mathcal {V}}$
, and so
$\mathcal {U}$
refines
$\mathcal {V}$
. Since B is finite, the partition
$\mathcal {U}$
is the set of atoms of B (here B considered as a Boolean algebra), and the domain of B is the family
$\{\bigcup \mathcal {S}\mid \mathcal {S}\subseteq \mathcal {U}\}$
. By Proposition 2.6,
$\mathcal {U}$
is tuned.
(2) By Proposition 2.6, the family
$\{\bigcup \mathcal {S}\mid \mathcal {S}\subseteq \mathcal {U}\}$
forms a subalgebra C of
$\mathop {\mathrm {Alg}}{F}$
. Since
$\mathcal {U}$
refines
$\mathcal {V}$
, all
$P_i$
are in C, and hence C contains B.
Let
$k<\omega $
. For a k-valuation
$\theta $
in an
$\mathrm {A}$
-frame F, let
$\sim _\theta $
be the equivalence on
$\mathop {\mathrm {dom}}{F}$
induced by all k-formulas in the model
$(F,\theta )$
. In terms of Kripke models,
$\sim _\theta $
is the set of pairs
$(a,b)\in \mathop {\mathrm {dom}}{F}\times \mathop {\mathrm {dom}}{F}$
such that for every k-formula
$\varphi $
,
$$ \begin{align*}(F,\theta), a\vDash \varphi \Leftrightarrow (F,\theta), b\vDash \varphi. \end{align*} $$
Proposition 2.8. If the algebra
$\mathop {\mathrm {Alg}}{F}$
is locally finite, then for every
$k<\omega $
and every k-valuation
$\theta $
in F, the partition
$\mathop {\mathrm {dom}}{F}{/}{\sim _\theta }$
is finite and tuned in F.
Proof. Consider the algebra B generated in
$\mathop {\mathrm {Alg}}{F}$
by the sets
$\theta (p_0), \ldots , \theta (p_{k-1})$
. Then
$\mathop {\mathrm {dom}}{F}{/}{\sim _\theta }$
is the partition of F induced by the elements of B. Now the statement follows from Proposition 2.7(1).
Theorem 2.9 [Reference Shapirovsky and Shehtman35].
-
(1) The algebra of a frame F is locally finite iff F is tunable.
-
(2) Let
$k<\omega $
. The logic of a class
$\mathcal {F}$
of
$\mathrm {A}$
-frames is k-finite iff there exists
$n<\omega $
such that for every
$F\in \mathcal {F}$
, for every partition
$\mathcal {V}$
of F with
$|\mathcal {V}|\leq 2^k$
there exists a finite tuned refinement
$\mathcal {U}$
of
$\mathcal {V}$
with
$|\mathcal {U}|\leq n$
. -
(3) The logic of a class
$\mathcal {F}$
of
$\mathrm {A}$
-frames is locally tabular iff
$\mathcal {F}$
is uniformly tunable.
Proof. (1) The “only if” direction follows from Proposition 2.7(1), the “if” direction from Proposition 2.7(2).
(2) By Maltsev’s criterion provided in Theorem 2.2(2),
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is k-finite iff there exists
$l<\omega $
such that for every
$F\in \mathcal {F}$
, the cardinality of every subalgebra of
$\mathop {\mathrm {Alg}}{F}$
generated by k subsets of F in not greater than l.
Assume that
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is k-finite. Let
$\mathcal {V}$
be a partition of
$F\in \mathcal {F}$
such that
$|\mathcal {V}|\leq 2^k$
. Then there are k subsets
$P_0,\ldots , P_{k-1}$
that induce
$\mathcal {V}$
(consider an injection
$f:\mathcal {V}\to \mathcal {P}(k)$
, and put
$P_i=\bigcup \{V\in \mathcal {V}\mid i\in f(V)\}$
). Let B be the subalgebra of
$\mathop {\mathrm {Alg}}{F}$
generated by these sets, and let
$\mathcal {U}$
be the partition of F induced by the elements of B. By Proposition 2.7(1),
$\mathcal {U}$
is a tuned refinement of
$\mathcal {V}$
. Since B is finite,
$|B|=2^{|\mathcal {U}|}$
. So if
$|B|\leq l$
, then
$2^{|\mathcal {U}|}\leq l$
.
For the other direction, consider a frame
$F\in \mathcal {F}$
and a subalgebra B of
$\mathop {\mathrm {Alg}}{F}$
generated by subsets
$P_0,\ldots , P_{k-1}$
of F. Let
$\mathcal {V}$
be the partition induced by these sets; clearly,
$|\mathcal {V}|\leq 2^k$
. For some fixed n,
$\mathcal {V}$
has a finite tuned refinement
$\mathcal {U}$
of size not greater than n. By Proposition 2.7(2),
$|B|\leq 2^n$
. This completes the proof of the second statement.
The third statement readily follows from the second.
In [Reference Shapirovsky and Shehtman35], this theorem was used to generalize the finite height criterion (3) for certain families of non-transitive logics.
Note that the first statement of this theorem does not imply that
$\mathop {\mathrm {Log}}(F)$
is locally tabular. However, Theorem 2.9(1) can be a useful tool for proving the finite model property of a semantically defined logic. For example, consider the logic of a direct power
$F=(\omega ,\leq )^n$
of
$(\omega ,\leq )$
, where
$0<n<\omega $
. This logic is not locally tabular, since F is not of finite height. On the other hand, F is tunable [Reference Shapirovsky32], so the algebra of F is locally finite, and so the logic of F has the finite model property.
3 Local tabularity and subframes
For a class
$\mathcal {F}$
of
$\mathrm {A}$
-frames, put
$$ \begin{align*}\mathop{\mathrm{Sub}}{\mathcal{F}}=\{F{\upharpoonright} Y\mid F\in \mathcal{F} \text{ and } Y\subseteq \mathop{\mathrm{dom}}{F}\}.\end{align*} $$
3.1 k-finiteness and subframes
Proposition 3.1. If the logic of a class
$\mathcal {F}$
of
$\mathrm {A}$
-frames is k-finite for some positive
$k<\omega $
, then the logic of
$\mathop {\mathrm {Sub}}{\mathcal {F}}$
is
${(k{-}1)}$
-finite.
Proof. Via Theorem 2.9. Let Y be a subset of a frame
$F\in \mathcal {F}$
, and
$\mathcal {V}$
be a finite partition of Y,
$|\mathcal {V}|\leq 2^{k-1}$
. Consider the partition
$\mathcal {V}'=\mathcal {V}\cup \{\mathop {\mathrm {dom}}{F}{\setminus } Y\}$
of F (if
$Y=\mathop {\mathrm {dom}}{F}$
, put
$\mathcal {V}'=\mathcal {V}$
). Then
$\mathcal {V}'\leq 2^k$
, and since
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is k-finite, by Theorem 2.9(2) there exists a finite tuned refinement
$\mathcal {U}$
of
$\mathcal {V}'$
with
$|\mathcal {U}|\leq n$
, for some fixed finite n. Consider the partition
$\mathcal {U}_\prime =\{V\in \mathcal {U}\mid V\subseteq Y\}$
of Y. It is straightforward that
$\mathcal {U}_\prime $
refines
$\mathcal {V}$
, is tuned in
$F{\upharpoonright } Y$
, and
$|\mathcal {U}_\prime |\leq n$
. Using Theorem 2.9(2) again, we conclude that
$\mathop {\mathrm {Log}}{\mathop {\mathrm {Sub}}{\mathcal {F}}}$
is
${(k{-}1)}$
-finite.
Corollary 3.2. The logic of
$\mathcal {F}$
is locally tabular iff the logic of
$\mathop {\mathrm {Sub}}{\mathcal {F}}$
is.
Proof. The “if” direction is immediate:
$\mathcal {F}\subseteq \mathop {\mathrm {Sub}}{\mathcal {F}}$
, so
$\mathop {\mathrm {Log}}{\mathop {\mathrm {Sub}}{\mathcal {F}}}\subseteq \mathop {\mathrm {Log}}{\mathcal {F}}$
. The “only if” direction follows from Proposition 3.1.
An analogous statement holds for algebras. Namely, if the algebra of a frame F is locally finite, then for every
$Y\subseteq \mathop {\mathrm {dom}}{F}$
, the algebra of the frame
$F{\upharpoonright } Y$
is locally finite (same argument as in the proof of Proposition 3.1, via Theorem 2.9(1)). In particular, it follows that all logics
$\mathop {\mathrm {Log}}{F{\upharpoonright } Y}$
have the finite model property.
Proposition 3.3. If the logic of a class
$\mathcal {F}$
of frames is 2-finite, then there exist
$m,h<\omega $
such that for every
$F\in \mathop {\mathrm {Sub}}{\mathcal {F}}$
, the frame F is m-transitive, and the height of F is not greater than h.
Proof. If
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is 2-finite, then logic
$\mathop {\mathrm {Log}}{\mathop {\mathrm {Sub}}{\mathcal {F}}}$
is 1-finite by Proposition 3.1. Now the statement follows from Theorem 2.4 and equivalences (5) and (6).
While in the unimodal transitive case, 1-finiteness of a modal logic implies local tabularity (7), this is not true in general. The followings example was given in [Reference Shapirovsky33]. Let L be the logic of the frame
$F=(\omega +1,R)$
, where
$$ \begin{align*}aRb \text{ iff } a\leq b \textrm{ or }a=\omega.\end{align*} $$
The restriction of F to
$\omega $
is the frame
$(\omega ,\leq )$
, so L is not 2-finite by Proposition 3.3. On the other hand, for every 2-element partition
$\mathcal {V}$
of F, there exists its tuned refinement
$\mathcal {U}$
with
$|\mathcal {U}|\leq 3$
. Indeed, let
$\mathcal {V}=\{V_0,V_1\}$
. W.l.o.g., let
$V_0\subseteq \omega $
. It is immediate that if
$V_0$
is infinite, then
$\mathcal {V}$
is tuned in F. Otherwise, let n be the greatest element of
$V_0$
,
$U_1=\{x\mid n<x<\omega \}$
,
$U_2$
the complement of
$V_0\cup U_1$
in F. It is straightforward from Definition 2.5 that
$\{V_0,U_1,U_2\}$
is a tuned refinement of
$\mathcal {V}$
. By Theorem 2.9(2), the logic of F is 1-finite.
In fact, there are 1-finite but not locally tabular logics above the logic 
of reflexive and symmetric relations. Namely, consider the logic L of the following, reflexive and symmetric, structure
$F=(\mathbb {Z},R)$
:
$$ \begin{align*}aRb \text{ iff } |a-b|\neq 1.\end{align*} $$
Let
$F_0$
be the restriction of F on the set of natural numbers. Then the subalgebra of
$\mathop {\mathrm {Alg}}(F_0)$
generated by the singleton
$\{0\}$
contains all singletons
$\{a\}$
,
$a\in \omega $
(simple induction on a). Hence,
$\mathop {\mathrm {Alg}}(F_0)$
is not 1-finite. By Proposition 3.1, L is not 2-finite. On the other hand, we claim that L is 1-finite. To show it, consider a 2-element partition
$\mathcal {V}=\{V_0,V_1\}$
of
$\mathbb {Z}$
, and let
$|V_0|\leq |V_1|$
. It is easy to verify that if
$a,b\in V_0$
for some distinct
$a,b\in \mathbb {Z}$
with
$|a-b|\neq 2$
, then
$\mathcal {V}$
is tuned in F. In the remaining cases,
$|V_0|\leq 2$
, and we have
$V_0=\{a\}$
or
$V_0=\{a-1,a+1\}$
for some
$a\in \mathbb {Z}$
. In both cases, the three element partition
$\mathcal {U}$
that contains
$\{a\}$
and
$\{a-1,a+1\}$
is a tuned refinement of
$\mathcal {V}$
. By Theorem 2.9(2), L is 1-finite. This proves
Theorem 3.4. There exists a unimodal 1-finite logic above 
, which is not locally tabular.
Hence, in the non-transitive case, 1-finiteness does not imply local tabularity. We do not know if k-finiteness of a modal logic implies its local tabularity for some fixed finite k.Footnote 3
3.2 Relativized height and relativized pretransitivity
Let
$M=(F,\theta )$
be a k-model,
$V\subseteq \mathop {\mathrm {dom}} F$
. The restriction
$M{\upharpoonright } V$
of M to V is the k-model
$(F{\upharpoonright } V,\theta {\upharpoonright } V)$
, where
$\theta {\upharpoonright } V(p_i)=\theta (p_i)\cap V$
for all
$i<k$
.
The following relativization argument was proposed in [Reference Spaan39].Footnote
4
Let
$k\leq \omega $
,
$\xi $
a k-formula. By induction on the structure of a k-formula
$\varphi $
, we define
${\left [\varphi \right ]}{\upharpoonright }{\xi }$
:
${{\left [\bot \right ]}{\upharpoonright }{\xi }=\bot} $
,
${\left [p\right ]}{\upharpoonright }{\xi }=p$
for variables,
${\left [\psi _1\rightarrow \psi _2\right ]}{\upharpoonright }{\xi }={\left [\psi _1\right ]}{\upharpoonright }{\xi }\rightarrow {\left [\psi _2\right ]}{\upharpoonright }{\xi }$
, and
${\left [\lozenge \psi \right ]}{\upharpoonright }{\xi }= \lozenge (\xi \wedge {\left [\psi \right ]}{\upharpoonright }{\xi })$
for
$\lozenge \in \mathrm {A}$
.
Proposition 3.5. Let
$M=(F,\theta )$
be a k-model,
$\xi $
a k-formula, and
$V=\bar {\theta }(\xi )$
. Then for every
$a\in V$
, for every k-formula
$\varphi $
,
$$ \begin{align*}M{\upharpoonright} V,a\vDash \varphi \text{ iff } M,a\vDash {\left[\varphi\right]}{\upharpoonright}{\xi}\end{align*} $$
Proof. By induction on the structure of
$\varphi $
.
Proposition 3.6. Let
$\mathcal {F}$
be a class of
$\mathrm {A}$
-frames,
$\varphi $
a formula in the language of
$\mathrm {A}$
, and q a variable not occurring in
$\varphi $
. Then
$$ \begin{align*}\mathcal{F}\vDash q\rightarrow {\left[\varphi\right]}{\upharpoonright}{q} \text{ iff }\mathop{\mathrm{Sub}}{\mathcal{F}}\vDash\varphi. \end{align*} $$
Proof. Follows from Proposition 3.5.
For a binary relation R on a set X and
$V\subseteq X$
, let
$R_V$
denote the restriction of R to V, and let
$R^*_V$
be the transitive reflexive closure of
$R_V$
, that is:
$$ \begin{align*}R^*_V=\{(a,a)\mid a\in V\}\cup (R_V) \cup (R_V)^2 \cup \ldots \end{align*} $$
A formula is said to be Boolean, if it is build using only Boolean connectives.
Proposition 3.7. Assume that the logic of an
$(l+1)$
-frame
$F=(X,R,R_1,\ldots ,R_l)$
is
$2$
-finite. Then there is
$m<\omega $
such that for every k-model
$M=(F,\theta )$
, for every k-formula
$\xi $
, for every Boolean k-formula
$\varphi $
, for all
$a\in V=\bar {\theta }(\xi )$
, we have:
$$ \begin{align} M,a\vDash {\left[\Box_0^{\leq m} \varphi\right]}{\upharpoonright}{\xi} \text{ iff } R_{V}^*(a)\subseteq \bar{\theta}(\varphi). \end{align} $$
Proof. Observe that
${\left [\varphi \right ]}{\upharpoonright }{\xi }$
is
$\varphi $
. By a straightforward induction on i we obtain:
$$ \begin{align*}M,a\vDash {\left[\lozenge_0^{i}\varphi\right]}{\upharpoonright}{\xi}\text{ iff } \exists b\;( (a,b)\in R_{V}^i\,\&\,M,b\vDash \varphi ).\end{align*} $$
It follows that
$$ \begin{align*}M,a\vDash {\left[\lozenge_0^{\leq i}\varphi\right]}{\upharpoonright}{\xi}\text{ iff } \exists b\;( (a,b)\in R_{V}^{\leq i}\,\&\,M,b\vDash \varphi ).\end{align*} $$
Since the logic of F is 2-finite, the logic of the frame
$(X,R)$
is 2-finite as well. By Proposition 3.3, there is
$m <\omega $
such that for every
$Y\subseteq X$
, the frame
$(X,R){\upharpoonright } Y$
is m-transitive, and so
$(R{\upharpoonright } V)^{\leq m}=R^*_V$
. Hence we have:
$$ \begin{align*}M,a\vDash {\left[\lozenge_0^{\leq m} \varphi\right]}{\upharpoonright}{\xi}\text{ iff } \exists b\;( (a,b)\in R_{V}^*\,\&\, M,b\vDash \varphi ),\end{align*} $$
and so (10) follows.
We conclude this section with a two-variable analog of Theorem 2.4.
Theorem 3.8. Assume that a logic L is
$2$
-finite. Then there exists
$m<\omega $
such that:
-
(1)
$L\vdash q\rightarrow {\left [\lozenge _{\mathrm {A}}^{m+1}p\rightarrow \lozenge _{\mathrm {A}}^{\leq m} p\right ]}{\upharpoonright }{q}$
, and -
(2) if also L is Kripke complete, then there exists h such that
$L\vdash q\rightarrow {\left [B^{[m]}_{h}\right ]}{\upharpoonright }{q}$
.
Proof. The first statement follows from the same argument as in Theorem 2.4. Namely, the 2-canonical frame F of L is finite. The case when L is inconsistent is trivial. Otherwise, F is non-empty. Put
$m=|\mathop {\mathrm {dom}}{F}|-1$
. Then every subframe of F is m-transitive, and so
$\lozenge _{\mathrm {A}}^{m+1}p\rightarrow \lozenge _{\mathrm {A}}^{\leq m}$
is valid there by (5). By Proposition 3.6,
$\varphi =q\rightarrow {\left [\lozenge _{\mathrm {A}}^{m+1}p\rightarrow \lozenge _{\mathrm {A}}^{\leq m} p\right ]}{\upharpoonright }{q}$
is valid in F. Since
$\varphi $
is a formula in two variables,
$L\vdash \varphi $
by the Canonical Model Theorem (Proposition 2.1).
Now assume that L is Kripke complete and that
$\mathcal {F}$
is the class of L-frames. By Proposition 3.3, there exist
$h,m<\omega $
such that the formulas
$\lozenge _{\mathrm {A}}^{m+1} p \rightarrow \lozenge _{\mathrm {A}}^{\leq m} p$
and
$B_h^{[m]}$
are valid in
$\mathop {\mathrm {Sub}}{\mathcal {F}}$
, and so the corresponding relativizations are valid in
$\mathcal {F}$
by Proposition 3.6.
We conjecture that the second statement remains true for Kripke incomplete logics.
4 Local tabularity and reflexivity
For a frame
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})$
, let
$F^{\mathrm {r}}$
be the frame
$(X,(R_\lozenge ^{\mathrm {r}})_{\lozenge \in \mathrm {A}})$
, where
$R_\lozenge ^{\mathrm {r}}$
is the reflexive closure
$R_\lozenge \cup \{(a,a)\mid a\in X\}$
of
$R_\lozenge $
. For a class
$\mathcal {F}$
of frames,
$\mathcal {F}^{\mathrm {r}}=\{F^{\mathrm {r}}\mid F\in \mathcal {F}\}$
.
We will show that
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is locally tabular iff
$\mathop {\mathrm {Log}}{\mathcal {F}^{\mathrm {r}}}$
is. Once the “only if” direction is straightforward, the “if” direction is non-trivial and is based on the following crucial lemma.
Lemma 4.1. Let
$F=(X,R,R_1,\ldots , R_{l})$
be an
$(l{+}1)$
-frame,
$G=(X,R^{\mathrm {r}},R_1,\ldots R_{l})$
, and
$\mathop {\mathrm {Log}}{G}$
locally tabular. Then for every
$k<\omega $
, every k-generated subalgebra of
$\mathop {\mathrm {Alg}}{F}$
is contained in a
$(k+3)$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{G}$
.
Proof. Assume that a subalgebra A of
$\mathop {\mathrm {Alg}}{F}$
is generated by
$P_0,\ldots P_{k-1}\subseteq X$
. We will construct three sets
$$ \begin{align*}Q,E,S\subseteq X\end{align*} $$
such that A is contained in the subalgebra of
$\mathop {\mathrm {Alg}}{G}$
generated by
$P_0,\ldots P_{k-1}, Q,E,S$
. This construction requires a number of technical steps, and we will split it into the following parts: definition of Q; auxiliary constructions; definitions of E and S; embedding the algebras.
Defining
$\boldsymbol {Q}$
. Let
$U\subseteq X$
,
$c\in U$
. We say that c is a defect of U, if
$aRb$
for some
$a,b\in U$
, and
$cRd$
for no d in U. The set of all defects of U is denoted by
$\mathop {\mathrm {Def}}{U}$
. A set is defective, if it contains a defect.
Claim 4.1.1. Let
${\sim }$
be an equivalence on X such that
$X{/}{\sim }$
is tuned in G. If there are no defective
$\sim $
-classes, then
$X{/}{\sim }$
is also tuned in F.
Proof. We only need to check that
$X{/}{\sim }$
is R-tuned. Assume that
$U,V\in X{/}{\sim }$
,
$a R b$
for some
$a\in U$
and
$b\in V$
. Let
$a'\in U$
. We need to show that
$a'R b'$
for some
$b'\in V$
.
Assume that
$U\neq V$
. Since
$X{/}{\sim }$
is tuned in G, there is
$b'\in V$
such that
$a'R^{\mathrm {r}}b'$
. Since
$a'\neq b'$
, we get
$a'Rb'$
.
If
$U=V$
, then, since
$aRb$
,
$a,b\in U$
, and U is not defective, we have
$a'Rb'$
for some
$b'\in U$
.
Consider the k-valuation
$\theta :\{p_0,\ldots ,p_{k-1}\}\to \mathcal {P}(X)$
,
$\theta (p_i)=P_i$
for
$i<k$
.
By recursion, we define a sequence of equivalences on X
$$ \begin{align} \sim_0\;\supseteq\;\sim_1\;\supseteq\;\sim_2\;\supseteq\;\ldots, \end{align} $$
and subsets
$Q_0,Q_1,Q_2\ldots $
of X.
Let
$\sim _0$
be the equivalence induced by all formulas in variables
$p_0,\ldots ,p_{k-1}$
in the model
$(G,\theta )$
. Let
$Q_0$
be the set
$\bigcup \{\mathop {\mathrm {Def}}{U}\mid U\in X{/}{\sim _0}\}$
of defects occurring in
$\sim _0$
-classes.
To define
$\sim _{n+1}$
and
$Q_{n+1}$
, we consider the
$(k{+}n{+}1)$
-model
$(G,\theta _n)$
such that
$\theta _n: \{p_0,\ldots ,p_{k-1},q_0,\ldots ,q_{n}\}\to \mathcal {P}(X)$
extends
$\theta $
and
$\theta _n(q_0)=Q_0$
, …,
$\theta _n(q_n)=Q_n$
. Let
$\sim _{n+1}$
be the equivalence induced by all formulas in variables
$p_0,\ldots ,p_{k-1},q_0,\ldots ,q_{n}$
in the model
$(G,\theta _n)$
. Let
$Q_{n+1}=\bigcup \{\mathop {\mathrm {Def}}{U}\mid U\in X{/}{\sim _{n+1}}\}$
.
We put
$$ \begin{align*}Q=\bigcup_{n<\omega} Q_n.\end{align*} $$
Preliminaries for defining
$\boldsymbol {E}$
and
$\boldsymbol {S}$
. The role of E and S is to “distinguish” subsets
$Q_n$
of Q. To define E and S, we need some preliminary observations about the constructed partitions.
Claim 4.1.2. All quotient sets
$X{/}{\sim _n}$
are finite and tuned in G.
Proof. Since the logic of the frame G is locally tabular, its algebra is locally finite. Now the claim follows from Proposition 2.8.
For
$a\in X$
, let
$[a]_n$
denote the
$\sim _n$
-class of a.
Claim 4.1.3. If
$U\in X{/}{\sim _{n}}$
,
$a\in \mathop {\mathrm {Def}}{U}$
and
$m>n$
, then
$[a]_{m}\subseteq \mathop {\mathrm {Def}} U$
and
$[a]_{m}$
is not defective.
Proof. We have
$a\in Q_n\cap U$
. By the definition of
$\sim _{n+1}$
,
$[a]_{n+1}\subseteq Q_{n}\cap U= \mathop {\mathrm {Def}} U$
. Since
$m\geq n+1$
,
$[a]_m\subseteq [a]_{n+1}$
by (11). So
$[a]_m$
is contained in
$\mathop {\mathrm {Def}}{U}$
. It follows that
$bRc$
for no
$b,c\in [a]_m$
, and so
$[a]_m$
is not defective.
Claim 4.1.4. All sets
$Q_n$
are disjoint.
Proof. Assume
$a\in Q_n$
for some n. Then
$a\in \mathop {\mathrm {Def}}{U}$
, where
$U=[a]_n$
. For every
$m>n$
, the
$\sim _{m}$
-class of a is not defective by Claim 4.1.3. Hence,
$a\notin Q_m$
.
By Claim 4.1.4, for any
$a\in Q$
there exists a unique n, the index of a, such that
$a\in Q_n$
; we denote such an n by
$\mathop {\mathrm {ind}}{a}$
.
Claim 4.1.5. Let
$U\in X{/}{\sim _{n}}$
,
$a\in U\cap Q$
, and
$\mathop {\mathrm {ind}}{a}> n$
. Then
$aRc$
for some
$c\in U$
.
Proof.
a is a defect of some
$V\in X{/}{\sim _m}$
with
$m> n$
. Then
$V\subseteq U$
; by the definition of a defective set,
$b R c$
for some
$b,c\in V$
. So
$b,c \in U$
, and since a is not a defect of U,
$aRd$
for some d in U.
Let
$\mathcal {A}$
be the union of all quotients
$X{/}{\sim _n}$
:
$$ \begin{align*}\mathcal{A}=\bigcup\{X{/}{\sim_n}\mid n<\omega\}.\end{align*} $$
Let
$\mathcal {D}$
denote the set of all defective sets in
$\mathcal {A}$
:
$$ \begin{align*}\mathcal{D}=\{V\in \mathcal{A}\mid \mathop{\mathrm{Def}}{V}\neq \varnothing\}. \end{align*} $$
Let
$V\in \mathcal {D}$
. It is immediate that there exists a unique n such that
$V\in X{/}{\sim _n}$
; this n is called the index of V, in symbols
$\mathop {\mathrm {ind}}{V}$
. It is also immediate that if
$a\in \mathop {\mathrm {Def}}{V}$
, then
$\mathop {\mathrm {ind}}{a}=\mathop {\mathrm {ind}}{V}$
.
Claim 4.1.6. If
$a\in V\cap Q$
for some
$V\in \mathcal {D}$
, then
$\mathop {\mathrm {ind}}{a}\geq \mathop {\mathrm {ind}}{V}$
.
Proof. If
$m>\mathop {\mathrm {ind}}{a}$
, then
$[a]_m$
is not defective by Claim 4.1.3. Since V is defective,
$V=[a]_m$
for some
$m\leq \mathop {\mathrm {ind}}{a}$
.
Defining
$\boldsymbol {E}$
. For
$U\in \mathcal {A}$
, put
$$ \begin{align*}\Sigma(U)=\{V\in\mathcal{A} \mid U\subset V\}.\end{align*} $$
Clearly, for all
$U,U'$
in
$\mathcal {A}$
, we have
$$ \begin{align} U\subseteq U'\text{ or } U'\subseteq U \text{ or } U'\cap U=\varnothing. \end{align} $$
Hence,
$\Sigma (U)$
is a
$\subseteq $
-chain. We put
$$ \begin{align*}{\Sigma}^\uparrow(U)=\{V\in \Sigma(U)\mid \exists a \in U \, \exists b\in \mathop{\mathrm{Def}}{V} \;aRb\}. \end{align*} $$
Claim 4.1.7. For
$U\in \mathcal {A}$
,
${\Sigma }^\uparrow (U)=\{V\in \Sigma (U)\mid \forall a \in U \, \exists b\in \mathop {\mathrm {Def}}{V} \;aRb\}.$
Proof. Let us check that
${\Sigma }^\uparrow (U)\subseteq \{V\in \Sigma (U)\mid \forall a \in U \, \exists b\in \mathop {\mathrm {Def}}{V} \;aRb\}.$
Assume that
$V\in {\Sigma }^\uparrow (U)$
. We have
$U\in X{/}{\sim _n}$
for some n. Then
$U\subset V\in X{/}{\sim _i}$
for some
$i<n$
, and we have
$aRb$
for some
$a \in U$
,
$b\in \mathop {\mathrm {Def}}{V}$
. We have
$U=[a]_n\subseteq [a]_{i+1}$
. Let
$a'\in U$
. Since
$X{/}{\sim _{i+1}}$
is tuned in G, there is
$b'\in [b]_{i+1}$
with
$a'R^{\mathrm {r}}b'$
. By Claim 4.1.3,
$b'\in \mathop {\mathrm {Def}}{V}$
. It remains to observe that
$a'\neq b'$
: indeed, since
$a'\sim _{i+1} a$
and a is not a defect of V, by Claim 4.1.3 we conclude that
$a'$
is not a defect of V as well. Hence,
$a'Rb'$
.
The other inclusion is trivial, since U is non-empty.
Claim 4.1.8. If
$U, U'\in \mathcal {A}$
,
$U'\subseteq U$
, then
${\Sigma }^\uparrow (U')\supseteq {\Sigma }^\uparrow (U)$
.
Proof. Immediate from Claim 4.1.7.
The cardinality of
${\Sigma }^\uparrow (U)$
is called the rank of U and is denoted by
$\mathop {\mathrm {rk}}{U}$
.
Claim 4.1.9. Assume that for
$U\in \mathcal {A}$
,
${\Sigma }^\uparrow (U)=\{V_{\mathop {\mathrm {rk}}{U}-1},\ldots , V_0\}$
with
$V_{\mathop {\mathrm {rk}}{U}-1}\subset \ldots \subset V_0$
. Then for each
$j<\mathop {\mathrm {rk}}{U}$
we have
${\Sigma }^\uparrow (V_j)=\{V_{j-1},\ldots , V_0\}$
and so
$\mathop {\mathrm {rk}}{V_j}=j$
.
Proof. Take
$j<\mathop {\mathrm {rk}}{U}$
. By Claim 4.1.8,
${\Sigma }^\uparrow (V_j) \subseteq \{V_{\mathop {\mathrm {rk}}{U}-1},\ldots , V_0\}$
. Since
${\Sigma }^\uparrow (V_j)\subseteq \Sigma (V_j)$
,
$V_i \in {\Sigma }^\uparrow (V_j)$
only if
$i<j$
. So
${\Sigma }^\uparrow (V_j) \subseteq \{V_{j-1},\ldots , V_0\}$
. If
$i<j$
, then
$V_i\in {\Sigma }^\uparrow (V_j)$
by the definition of
${\Sigma }^\uparrow $
, since
$U\subset V_j\subset V_i$
and
$V_i\in {\Sigma }^\uparrow (U)$
.
For
$a\in Q$
, the rank of a,
$\mathop {\mathrm {rk}}{a}$
, is defined as the rank of the
$\sim _{\mathop {\mathrm {ind}}{a}}$
-class of a:
$$ \begin{align*}\mathop{\mathrm{rk}}{a}=\mathop{\mathrm{rk}}{([a]_{\mathop{\mathrm{ind}}{a}})}. \end{align*} $$
Claim 4.1.10. Let
$V\in \mathcal {D}$
,
$a \in Q\cap V$
. Then:
-
(i)
$\mathop {\mathrm {rk}}{a}\geq \mathop {\mathrm {rk}}{V}$
; -
(ii) If
$\mathop {\mathrm {rk}}{a}> \mathop {\mathrm {rk}}{V}$
, then there exists
$b\in V\cap Q$
such that
$aRb$
and
$\mathop {\mathrm {rk}}{b}=\mathop {\mathrm {rk}}{a}-1$
.
Proof. Let
$n=\mathop {\mathrm {ind}}{V}$
, that is
$V\in X{/}{\sim _n}$
. Since
$V=[a]_n$
is defective,
$n\leq \mathop {\mathrm {ind}}{a}$
by Claim 4.1.6. Let
$V'=[a]_{\mathop {\mathrm {ind}}{a}}$
. Is follows that
$V'\subseteq V$
. By Claim 4.1.8, we have
${\Sigma }^\uparrow (V')\supseteq {\Sigma }^\uparrow (V)$
. Now the first statement follows.
Let
$\mathop {\mathrm {rk}}{a}> \mathop {\mathrm {rk}}{V}$
. In this case
${\Sigma }^\uparrow (V')\supset {\Sigma }^\uparrow (V)$
. So we have for some
$V_{\mathop {\mathrm {rk}}{a}-1}\subset \ldots \subset V_0$
:
$$ \begin{align} {\Sigma}^\uparrow(V')=\{V_{\mathop{\mathrm{rk}}{a}-1},\ldots, V_{\mathop{\mathrm{rk}}{V}-1},\ldots, V_0\},\quad {\Sigma}^\uparrow(V)=\{V_{\mathop{\mathrm{rk}}{V}-1},\ldots, V_0\}. \end{align} $$
By Claim 4.1.7, there exists
$b\in \mathop {\mathrm {Def}}{V_{\mathop {\mathrm {rk}}{a}-1}}$
with
$aRb$
. We have
$V_{\mathop {\mathrm {rk}}{a}-1}=[b]_{\mathop {\mathrm {ind}}{b}}$
, and so
$\mathop {\mathrm {rk}}{b}=\mathop {\mathrm {rk}}{V_{\mathop {\mathrm {rk}}{a}-1}}$
, and hence
$\mathop {\mathrm {rk}}{b}=\mathop {\mathrm {rk}}{a}-1$
by Claim 4.1.9.
It remains to show that
$b\in V$
. By (13),
$V_{\mathop {\mathrm {rk}}{a}-1}\notin {\Sigma }^\uparrow (V)$
. It follows that
$V_{\mathop {\mathrm {rk}}{a}-1}\notin \Sigma (V)$
, since we have
$a \in V$
,
$aRb$
,
$b\in \mathop {\mathrm {Def}}{V_{\mathop {\mathrm {rk}}{a}-1}}$
. Hence, V is not a proper subset of
$V_{\mathop {\mathrm {rk}}{a}-1}$
. Since
$a\in V\cap V_{\mathop {\mathrm {rk}}{a}-1}$
, by (12) we have
$V_{\mathop {\mathrm {rk}}{a}-1}\subseteq V$
. Hence
$b\in V$
.
Let E be the set of
$a\in Q$
of even rank:
$$ \begin{align*}E=\{a\in Q\mid \mathop{\mathrm{rk}}{a} \text{ is even}\}. \end{align*} $$
Defining
$\boldsymbol {S}$
. For
$V\in \mathcal {D}$
, put
$$ \begin{align} \overline{V}&=(V\setminus Q_{\mathop{\mathrm{ind}}{V}})\cap Q, \end{align} $$
$$ \begin{align} G_V&=(\overline{V},(R{\upharpoonright} \overline{V})^*).\qquad \end{align} $$
Let
$\mathop {\mathrm {Cl}}{V}$
be the set of all maximal clusters in the preordered set
$G_V$
,
$$ \begin{align*} \mathcal{C}=\{C\in \bigcup\{\mathop{\mathrm{Cl}}{V}\mid V\in \mathcal{D}\}\mid |C|>1\}. \end{align*} $$
Claim 4.1.11.
-
(i) If
$C\in \mathop {\mathrm {Cl}}{V}$
,
$C'\in \mathop {\mathrm {Cl}}{V'}$
for some
$V,V'\in \mathcal {D}$
,
$C\cap C'\neq \varnothing $
, and
$\mathop {\mathrm {ind}}{V'}\leq \mathop {\mathrm {ind}}{V}$
, then
$C\subseteq C'$
. -
(ii) For all
$C,C'\in \mathcal {C}$
, we have
$C\subseteq C'\text { or } C'\subseteq C \text { or } C\cap C'=\varnothing $
; -
(iii) For any
$C\in \mathcal {C}$
,
$\{C'\in \mathcal {C}\mid C\subset C'\}$
is a finite
$\subseteq $
-chain.
Proof. To prove the first statement, take c in
$C\cap C'$
. Let
$n=\mathop {\mathrm {ind}}{V},~n'=\mathop {\mathrm {ind}}{V'}$
. Then
$$ \begin{align*}V=[c]_n\subseteq [c]_{n'}=V'.\end{align*} $$
It follows that
$\overline {V}\subseteq \overline {V'}$
: indeed, if
$a\in \overline {V}$
, then
$\mathop {\mathrm {ind}}{a}>n$
by Claim 4.1.6 and the definition of
$\overline {V}$
, and so
$\mathop {\mathrm {ind}}{a}>n'$
, which implies
$a\in \overline {V'}$
. Hence, the relation
$R{\upharpoonright } \overline {V}$
is included in the relation
$R{\upharpoonright } \overline {V'}$
. Assume
$c'\in C$
. Then we have
$(c,c') \in (R{\upharpoonright } \overline {V})^*$
, so
$(c,c') \in (R{\upharpoonright } \overline {V'})^*$
; the latter means that
$c'\in C'$
, since
$C'$
is maximal in
$G_{V'}$
. Hence
$C\subseteq C'$
, which completes the proof of the first statement.
The second statement is immediate from the first one: if there is c in
$C\cap C'$
, consider
$V,V'\in \mathcal {D}$
such that
$C\in \mathop {\mathrm {Cl}}{V}$
and
$C'\in \mathop {\mathrm {Cl}}{V'}$
, and compare
$\mathop {\mathrm {ind}}{V}$
and
$\mathop {\mathrm {ind}}{V'}$
.
That
$\{C'\in \mathcal {C}\mid C\subset C'\}$
is a chain follows from (ii). Let
$$ \begin{align*}\Delta=\{V'\in\mathcal{D}\mid \exists C'\in \mathop{\mathrm{Cl}}{V'}\, (C\subset C')\}.\end{align*} $$
Notice that every
$V'$
from
$\Delta $
includes C, so by (12),
$\Delta $
is a
$\subseteq $
-chain. We have
$C\in \mathop {\mathrm {Cl}}{V}$
for some
$V\in \mathcal {D}$
. By (i),
$\mathop {\mathrm {ind}}{V'}<\mathop {\mathrm {ind}}{V}$
for every
$V'\in \Delta $
, so the chain
$\Delta $
is finite. Observe that for every
$V'\in \Delta $
, there is a unique
$C'\in \mathop {\mathrm {Cl}}{V'}$
such that
$C\subset C'$
: indeed, distinct clusters are disjoint; define
$f(V')=C'$
. So f is a function from the finite set
$\Delta $
to
$\{C'\in \mathcal {C}\mid C\subset C'\}$
. By the definition of
$\mathcal {C}$
and
$\Delta $
, f is surjective, which completes the proof.
Consider the poset
$(\mathcal {C},\subseteq )$
. Let
$\mathcal {C}_{\min }$
be the set of all minimal elements of
$(\mathcal {C},\subseteq )$
, and
$$ \begin{align*}\mathcal{C}_0=\{C\in \mathcal{C}\mid \exists C'\in\mathcal{C}_{\min} \, (C'\subseteq C) \}, \quad \mathcal{C}_1=\mathcal{C}{\setminus}\mathcal{C}_0. \end{align*} $$
Claim 4.1.12. There exist pairwise disjoint subsets
$T^+$
,
$T^-$
,
$S^+$
,
$S^-$
of X such that:
-
(a) for every
$C\in \mathcal {C}_0$
, the sets
$C\cap T^+$
and
$C\cap T^-$
are non-empty, and
$T^+\cup T^-\subseteq \bigcup \mathcal {C}_{\min }$
; -
(b) for every
$C\in \mathcal {C}_1$
, the sets
$C\cap S^+$
and
$C\cap S^-$
are non-empty, and
$S^+\cup S^-\subseteq \bigcup \mathcal {C}_1$
.
Proof. First, we show existence of
$T^+$
and
$T^-$
. For C in
$\mathcal {C}_{\min }$
, let
$t^+(C)$
and
$t^-(C)$
be two distinct elements of C (recall that C has at least two elements). Put
$T^+=\{t^+(C)\mid C\in \mathcal {C}_{\min }\}$
and
$T^-=\{t^-(C)\mid C\in \mathcal {C}_{\min }\}$
. Every
$C'\in \mathcal {C}_0$
includes some
$C\in \mathcal {C}_{\min }$
, and so we have
$C'\cap T^+\neq \varnothing $
and
$C'\cap T^-\neq \varnothing $
. Every two distinct elements of
$\mathcal {C}_{\min }$
are disjoint by Claim 4.1.11(ii), and so
$T^+$
and
$T^-$
are disjoint as well: indeed,
$t^+(C)=t^-(C')$
would imply
$C'\neq C$
and at the same time
$C'\cap C\neq \varnothing $
.
Now we define
$S^+$
and
$S^-$
. For C in
$\mathcal {C}_1$
, let
$d(C)$
be the cardinality of the set
$\Delta (C)=\{C'\in \mathcal {C}_1\mid C\subset C'\}$
. By Claim 4.1.11(iii),
$\Delta (C)$
is finite. By recursion on
$d(C)$
we define elements
$a^+(C)$
,
$a^-(C)$
of
$C\in \mathcal {C}_1$
. Notice that C is infinite, since
$C\notin \mathcal {C}_0$
. If
$d(C)=0$
, let
$a^+(C),a^-(C)$
be two distinct elements in C. Otherwise consider the set
$$ \begin{align*}C\setminus (\{ a^+(C')\mid C'\in\Delta(C)\}\cup \{a^-(C')\mid C'\in\Delta(C)\}).\end{align*} $$
Clearly, this set is infinite; let
$a^+(C),a^-(C)$
be two distinct elements in this set. By the construction, we have
$$ \begin{align} \forall C'\in\Delta(C) \,(a^+(C)\neq a^-(C') \;\&\; a^-(C)\neq a^+(C') ). \end{align} $$
Put
$$ \begin{align*}S^+=\{a^+(C)\mid C\in \mathcal{C}_1\},~ S^-=\{a^-(C)\mid C\in \mathcal{C}_1\}.\end{align*} $$
Since
$a^+(C),a^-(C)\in C$
for every C in
$\mathcal {C}_1$
, the sets
$C\cap S^+$
,
$C\cap S^-$
are non-empty and
$S^+$
and
$S^-$
are subsets of
$\bigcup \mathcal {C}_1$
.
Let us check that
$S^+$
and
$S^-$
are disjoint. For the sake of contradiction, assume that they are not. Then there are
$C,C'\in \mathcal {C}_1$
such that
$a^+(C)=a^-(C')$
. Hence
$C\neq C'$
. Since
$a^+(C)\in C$
and
$a^-(C')\in C'$
, if follows that
$C\cap C'\neq \varnothing $
. By Claim 4.1.11(ii), we have that
$C\subset C'$
or
$C'\subset C$
. Both cases contradict (16): indeed, in the first case
$C'\in \Delta (C)$
, and in the second case
$C\in \Delta (C')$
. This contradiction proves that
$S^+$
and
$S^-$
are disjoint.
Notice that
$$ \begin{align} (\bigcup \mathcal{C}_{\min})\cap (\bigcup \mathcal{C}_1)=\varnothing; \end{align} $$
indeed, if
$c\in C\in \mathcal {C}_{\min }$
and
$c\in C'\in \mathcal {C}_1$
, then by Claim 4.1.11(ii),
$C\subseteq C'$
or
$C'\subset C$
; but the first implies that
$C'\in \mathcal {C}_0$
, which contradicts the definition of
$\mathcal {C}_1$
, and the latter contradicts the minimality of C in
$(\mathcal {C},\subseteq )$
.
It follows from (17) that
$T^+$
,
$T^-$
,
$S^+$
,
$S^-$
are pairwise disjoint.
Consider sets
$T^+, T^-, S^+, S^-$
satisfying the above claim. Put
$$ \begin{align*}S=T^+\cup S^+.\end{align*} $$
By the above claim,
$C\cap (S^+\cup T^+) \neq \varnothing $
and
$C\cap (S^-\cup T^-) \neq \varnothing $
for every
$C\in \mathcal {C}$
. Since
$X{\setminus }S\supseteq T^-\cup S^-$
, we have:
$$ \begin{align} \forall C\in\mathcal{C}\, (C\cap S\neq \varnothing\, \&\, C\cap (X{\setminus}S) \neq \varnothing). \end{align} $$
Embedding algebras. Since the logic of
$G=(X,R^{\mathrm {r}},R_1,\ldots R_{l})$
is locally tabular, the logic of the frame
$(X,R^{\mathrm {r}})$
is locally tabular as well. By Proposition 3.3, there is
$h<\omega $
such that for every subset V of X, the height of
$(V,R^{\mathrm {r}}{\upharpoonright } V)$
is not greater than h. In particular, we have:
Claim 4.1.13. For all
$V\in \mathcal {D}$
, the height of
$G_V$
is finite.
Recall that for a set
$V\subseteq X$
,
$R_V$
denotes the restriction of R to V, and
$R_V^*$
denotes its transitive reflexive closure.
The following claim is the key step towards expressing
$Q_n$
in terms of
$Q,E,S$
.
Claim 4.1.14. Let
$V\in \mathcal {D}$
,
$n=\mathop {\mathrm {ind}}{V}$
. For every
$a\in V$
, we have:
$a\in Q_n$
iff
$$ \begin{align} &R_V^*(a)\subseteq Q,\text{ and} \end{align} $$
$$ \begin{align} &(R_V^*(a) \subseteq E\text{ or }R_V^*(a) \subseteq X{\setminus}E)\text{, and } \end{align} $$
$$ \begin{align} &(R_V^*(a) \subseteq S\text{ or }R_V^*(a) \subseteq X{\setminus}S). \end{align} $$
Proof. “Only if”. Assume that
$a\in Q_n$
. We have
$R_V(a)=\varnothing $
by the definition of a defect, so
$R^*_V(a)$
is the singleton
$\{a\}$
, which implies (19), (20), and (21).
“If”. Assume (19), (20), and (21) hold. From (19) we have
$a\in Q$
. By Claim 4.1.6,
$\mathop {\mathrm {ind}}{a}\geq n$
.
For the sake of contradiction, assume that
$\mathop {\mathrm {ind}}{a}>n$
, and show that
$$ \begin{align} \text{there exist }c,c'\in R_{\overline{V}}^*(a)\text{ such that }c\in S\text{ and }c'\notin S. \end{align} $$
Observe that
$R_{\overline {V}}\subseteq R_V$
. Since
$\mathop {\mathrm {ind}}{a}>\mathop {\mathrm {ind}}{V}$
, a belongs to
$G_V$
. Since the height of
$G_V$
is finite (Claim 4.1.13),
$R_{\overline {V}}^*(a)$
includes a maximal in
$G_V$
cluster C. Consider
$b\in C$
. By Claim 4.1.10,
$\mathop {\mathrm {rk}}{b}\geq \mathop {\mathrm {rk}}{V}$
, and if
$\mathop {\mathrm {rk}}{b}>\mathop {\mathrm {rk}}{V}$
, then
$bRb'$
for some
$b'\in V\cap Q$
such that
$bRb'$
and
$\mathop {\mathrm {rk}}{b'}=\mathop {\mathrm {rk}}{b}-1$
. The latter is impossible due to (20), since both b and
$b'$
are in
$R_V^*(a)$
, but exactly one of them is in E. Hence,
$$ \begin{align} \mathop{\mathrm{rk}}{b}=\mathop{\mathrm{rk}}{V}. \end{align} $$
Since
$b\in \overline {V}$
,
$\mathop {\mathrm {ind}}{b}>n$
, and so there exists
$b'\in V$
with
$bRb'$
by Claim 4.1.5. By Claim 4.1.8,
$\Sigma ^\uparrow ([b]_{\mathop {\mathrm {ind}}{b}})\supseteq \Sigma ^\uparrow (V)$
, and so by (23) we obtain
$\Sigma ^\uparrow ([b]_{\mathop {\mathrm {ind}}{b}})=\Sigma ^\uparrow (V)$
. It follows that
$V\notin \Sigma ^\uparrow ([b]_{\mathop {\mathrm {ind}}{b}})$
, and so
$b'$
is not a defect of V. Hence,
$b'$
is not in
$Q_n$
; due to (19),
$b'\in Q$
and so
$b'\in \overline {V}$
. Since
$b\in Q$
,
$(b,b)\notin R$
. It follows that
$b'\neq b$
. Since C is maximal in
$G_V$
,
$b'\in C$
. Since C is not a singleton,
$C\in \mathcal {C}$
. Now (22) follows from (18).
Since
$R_{\overline {V}}\subseteq R_V$
, (22) contradicts (21), which completes the proof of the claim.
Consider the valuation
$\theta ':\{p_0,\ldots ,p_{k-1}, q,e,s\}\to \mathcal {P}(X)$
such that
$\theta '$
extends
$\theta $
and
$\theta '(q)=Q$
,
$\theta '(e)=E$
,
$\theta '(s)=S$
. Let
$\sim $
be the equivalence induced in
$(G,\theta ')$
by all formulas in variables
$\{p_0,\ldots ,p_{k-1}, q,e,s\}$
.
Claim 4.1.15. There exist formulas
$\{{\psi _{n}}\mid n<\omega \}$
in variables
$\{p_0,\ldots ,p_{k-1}, q,e,s\}$
such that
$$ \begin{align} (G,\theta'),a\vDash {\psi_{n}} \text{ iff } a\in Q_n. \end{align} $$
Proof. By induction on n. Assume that
${\psi _{i}}$
are defined for all
$i<n$
.
Let
$V\in X/{\sim _n}$
. Since
$X/{\sim _n}$
is finite (Claim 4.1.2), there is a formula
$\varphi (V)$
in variables
$p_0,\ldots ,p_{k-1}$
and
$q_{i}$
with
$i<n$
such that
$$ \begin{align*}(G,\theta_n),a\vDash \varphi(V) \text{ iff } a\in V.\end{align*} $$
By induction hypothesis, there is a formula
$\psi (V)$
in variables
$p_0,\ldots ,p_{k-1},q,e,s$
such that
$$ \begin{align} (G,\theta'),a\vDash \psi(V) \text{ iff } a\in V. \end{align} $$
By Proposition 3.7, there is
$m<\omega $
such that for every
$a\in V$
we have:
$$ \begin{align*} (G,\theta'),a \vDash {\left[\Box_0^{\leq m}q\right]}{\upharpoonright}{\psi(V)} &\text{ iff } R_V^*(a)\subseteq Q, \\ (G,\theta'),a\vDash {\left[\Box_0^{\leq m}e\right]}{\upharpoonright}{\psi(V)} \vee {\left[\Box_0^{\leq m}\neg e\right]}{\upharpoonright}{\psi(V)} &\text{ iff } (R_V^*(a) \subseteq E \text{ or } R_V^*(a) \subseteq X{\setminus}E),\\ (G,\theta'),a\vDash {\left[\Box_0^{\leq m} s\right]}{\upharpoonright}{\psi(V)} \vee {\left[\Box_0^{\leq m}\neg s\right]}{\upharpoonright}{\psi(V)} & \text{ iff } (R_V^*(a) \subseteq S \text{ or }R_V^*(a) \subseteq X{\setminus}S). \end{align*} $$
Let
$\chi (V)$
be the conjunction of the three modal formulas mentioned in the above equivalences. By Claim 4.1.14, for every
$V\in \mathcal {D}$
with
$\mathop {\mathrm {ind}}{V}=n$
, for every
$a\in V$
,
$$ \begin{align} (G,\theta'),a\vDash \chi(V) \text { iff } a\in Q_n. \end{align} $$
Let
$\mathcal {V}$
be the set of defective sets in
$X{/}{\sim _n}$
. By Claim 4.1.2,
$\mathcal {V}$
is finite. Put
$$ \begin{align*}{\psi_{n}}=\bigvee\{\psi(V)\wedge\chi(V)\mid V\in \mathcal{V}\}.\end{align*} $$
We have
$Q_n=\bigcup \{\mathop {\mathrm {Def}}{V} \mid V\in \mathcal {V}\}$
, and so (24) follows from (25) and (26).
From Claim 4.1.15, it follows that all
$Q_n$
belong to the subalgebra B of
$\mathop {\mathrm {Alg}}{G}$
generated by
$P_0,\ldots P_{k-1}, Q,E,S$
. The algebra B is finite due to the local finiteness of
$\mathop {\mathrm {Alg}}{G}$
. Since all
$Q_n$
are disjoint (Claim 4.1.4), it follows that there is
$N<\omega $
such that
$Q_N=\varnothing $
. The partition
$X{/}{\sim }_N$
is finite and tuned in G by Claim 4.1.2, and since there are no defective N-classes, it is tuned in F due to Claim 4.1.1.
Finally, consider the initial algebra A, the subalgebra of
$\mathop {\mathrm {Alg}}{F}$
generated by
$P_0,\ldots , P_{k-1}$
. By Proposition 2.7(2), every element of A is the union of some
$\sim _N$
-classes. Every such union is in B, so
$ \mathop {\mathrm {dom}}{A}\subseteq \mathop {\mathrm {dom}}{B}. $
Lemma 4.2. If the logic of an
$\mathrm {A}$
-frame
$F^{\mathrm {r}}$
is locally tabular, then for every
$k<\omega $
, every k-generated subalgebra of
$\mathop {\mathrm {Alg}}{F}$
is contained in a
$(k+3|\mathrm {A}|)$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{F^{\mathrm {r}}}$
.
Proof. Consider an
$(n+m)$
-frame
$F=(X,(R_i)_{i<n},(S_i)_{i<m})$
such that all
$S_i$
are reflexive, and
$\mathop {\mathrm {Log}}{F^{\mathrm {r}}}$
is locally tabular. By induction on n, we show that every k-generated subalgebra of
$\mathop {\mathrm {Alg}}{F}$
is contained in a
$(k+3n)$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{F^{\mathrm {r}}}$
. Basic
$n=0$
is trivial. Let
$n>0$
. Consider the frame
$G=(X,(R_i)_{i<n-1},R_n^{\mathrm {r}},(S_i)_{i<m})$
. Notice that
$G^{\mathrm {r}}=F^{\mathrm {r}}$
. By induction hypothesis, every k-generated subalgebra of
$\mathop {\mathrm {Alg}}{G}$
is contained in a
$(k+3(n-1))$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{F^{\mathrm {r}}}$
. In particular, it follows that
$\mathop {\mathrm {Log}}{G}$
is locally tabular. By Lemma 4.1, every k-generated subalgebra of
$\mathop {\mathrm {Alg}}{F}$
is contained in a
$(k+3)$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{G}$
, and consequently, in a
$(k+3n)$
-generated subalgebra of
$\mathop {\mathrm {Alg}}{F^{\mathrm {r}}}$
. This completes the proof of the induction step.
To complete the proof of the lemma, put
$m=0$
.
Theorem 4.3. Let
$\mathcal {F}$
be a class of
$\mathrm {A}$
-frames. Then
$\mathop {\mathrm {Log}}{\mathcal {F}}$
is locally tabular iff
$\mathop {\mathrm {Log}}{\mathcal {F}^{\mathrm {r}}}$
is locally tabular.
Proof. The ‘only if’ direction is clear due to the following well-known translation: put
${[\bot ]}_{\mathrm {r}}=\bot $
,
${[p]}_{\mathrm {r}}=p$
for variables,
${[\varphi \rightarrow \psi ]}_{\mathrm {r}}={[\varphi ]}_{\mathrm {r}}\rightarrow {[\psi ]}_{\mathrm {r}}$
, and
${[\lozenge \psi ]}_{\mathrm {r}}= \lozenge {[\psi ]}_{\mathrm {r}}\vee {[\psi ]}_{\mathrm {r}}$
for
$\lozenge \in \mathrm {A}$
. It is straightforward that
$$ \begin{align*}\mathcal{F}\vDash{[\varphi]}_{\mathrm{r}} \text{ iff } \mathcal{F}^{\mathrm{r}}\vDash\varphi.\end{align*} $$
So the local tabularity of
$\mathop {\mathrm {Log}}{\mathcal {F}}$
implies the local tabularity of
$\mathop {\mathrm {Log}}{\mathcal {F}^{\mathrm {r}}}$
.
The ‘if’ part follows from Lemma 4.2 and Theorem 2.2(1). Namely, since
$\mathop {\mathrm {Log}}{\mathcal {F}^{\mathrm {r}}}$
is locally tabular, the class
$\mathcal {C}$
of algebras
$\{\mathop {\mathrm {Alg}}{F}\mid F\in \mathcal {F}^{\mathrm {r}}\}$
is uniformly locally finite, that is there exists a function
$f:\omega \to \omega $
such that the cardinality of a subalgebra of any
$A\in \mathcal {C}$
generated by
$k<\omega $
elements does not exceed
$f(k)$
. It follows that the class
$\mathcal {D}=\{\mathop {\mathrm {Alg}}{F}\mid F\in \mathcal {F}\}$
is uniformly locally finite as well: for every algebra B in
$\mathcal {D}$
, the size of its subalgebra generated by k elements is bounded by
$f(k+3|A|)$
, according to Lemma 4.2.
We do not know if an analogous result holds for the case of locally finite algebras. Finite height was crucial in the proof of Lemma 4.1 (see Claim 4.1.13). However, local finiteness of an algebra does not imply this property, because, for example, the algebra of the frame
$(\omega ,\leq )$
is locally finite (follows easily from Theorem 2.9(1)).
5 Transfer results
For disjoint alphabets of modalities
$\mathrm {A}$
and
$\mathrm {B}$
, and logics
$L_1$
in the language of
$\mathrm {A}$
and
$L_2$
in the language of
$\mathrm {B}$
, the fusion
$L_1*L_2$
of
$L_1$
and
$L_2$
is the smallest logic in the language of
$\mathrm {A}\cup \mathrm {B}$
that contains
$L_1\cup L_2$
. In the case of consistent
$L_1$
and
$L_2$
, the fusion is a conservative extension of
$L_1$
and of
$L_2$
[Reference Thomason40], and hence local tabularity of
$L_1$
and
$L_2$
is a necessary condition for local tabularity of the fusion. But it is not sufficient. While it is known that Kripke completeness, finite model property, and decidability of logics are preserved under this operation [Reference Fine and Schurz15, Reference Kracht and Wolter22, Reference Wolter, Kracht, de Rijke, Wansing and Zakharyaschev41], this is not the case for local tabularity. For example, let
$\mathrm {A}=\{\lozenge _a\}$
,
$\mathrm {B}=\{\lozenge _b\}$
; it is straightforward that the fusion 
of two instances of a locally tabular logic 
is not even 1-finite (one can easily construct a non-pretransitive frame of 
). Notice however that every proper extension of the logic 
is locally tabular [Reference Bezhanishvili9]. This gives examples of locally tabular products of modal logics [Reference Gabbay and Shehtman17]. Another family of locally tabular modal products was identified in [Reference Shehtman38], see also [Reference Shehtman37]. For related systems, intuitionistic modal logics (considered in the sense of [Reference Gabbay, Kurucz, Wolter and Zakharyaschev16, Section 10.3]), certain locally tabular families were identified in [Reference Bezhanishvili5], [Reference Bezhanishvili and Grigolia7], and [Reference Bezhanishvili6].Footnote
5
While the product of two modal logics inherits both pretransitivity and finite height, the local tabularity is not preserved in general.Footnote
6
Below we consider operations on frames and on logics which preserve local tabularity.
5.1 First semantic transfer result
Definition 5.1. Consider an
$\mathrm {A}$
-frame
$I=(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}})$
and a family
$(F_i)_{i\in Y}$
of
$\mathrm {A}$
-frames
$F_i=(X_i,(R_{i,\lozenge })_{\lozenge \in \mathrm {A}})$
. The sum
${\textstyle \sum _{I}{F_i}}$
of the family
$(F_i)_{i\in Y}$
over I is the
$\mathrm {A}$
-frame
$(\bigsqcup _{i \in Y} X_i, (R^\Sigma _\lozenge )_{\lozenge \in \mathrm {A}})$
, where
$\bigsqcup _{i\in Y}{X_i}=\bigcup _{i\in Y}(\{i\}\times X_i)$
is the disjoint union of sets
$X_i$
, and
$$ \begin{align*}(i,a)R^\Sigma_\lozenge (j,b) \quad \text{ iff } \quad (i = j \,\&\,a R_{i,\lozenge} b) \text{ or } (i\neq j \,\&\, iS_\lozenge j).\end{align*} $$
For classes
$\mathcal {I}$
,
$\mathcal {F}$
of
$\mathrm {A}$
-frames, let
${\textstyle \sum _{\mathcal {I}}{\mathcal {F}}}$
be the class of all sums
${\textstyle \sum _{I}{F_i}}$
such that
$I \in \mathcal {I}$
and
$F_i\in \mathcal {F}$
for every i in I.
A typical example of sum is a preorder, which is, up to an isomorphism, the sum of its clusters over its skeleton.
According to the definition, the relations
$R^\Sigma _\lozenge $
are independent of reflexivity of the relations
$S_\lozenge $
:
$$ \begin{align} {\textstyle \sum_{I}{F_i}}={\textstyle \sum_{I^{\mathrm{r}}}{F_i}}={\textstyle \sum_{I^{\mathrm{ir}}}{F_i}}, \end{align} $$
where
$I^{\mathrm {ir}}=(Y,(S_\lozenge ^{\mathrm {ir}})_{\lozenge \in \mathrm {A}})$
,
$S_\lozenge ^{\mathrm {ir}}=S_\lozenge {\setminus }\{(a,a)\mid a\in Y\}$
.
Theorem 5.2. Let
$\mathcal {F}$
and
$\mathcal {I}$
be classes of
$\mathrm {A}$
-frames. If the modal logics
$\mathop {\mathrm {Log}}{\mathcal {F}}$
and
$\mathop {\mathrm {Log}}{\mathcal {I}}$
are locally tabular, then the logic
$\mathop {\mathrm {Log}}{{\textstyle \sum _{\mathcal {I}}{\mathcal {F}}}}$
is locally tabular as well.
Proof. Let
$\mathcal {I}_1=\{I^{\mathrm {ir}}\mid I\in \mathcal {I}\}$
. By (27),
${\textstyle \sum _{\mathcal {I}}{\mathcal {F}}}={\textstyle \sum _{\mathcal {I}_1}{\mathcal {F}}}$
. Since
$\mathcal {I}^{\mathrm {r}}=(\mathcal {I}_1)^{\mathrm {r}}$
, it follows from Theorem 4.3 that
$\mathop {\mathrm {Log}}{\mathcal {I}_1}$
is locally tabular.
Let
$\mathcal {F}_1$
be the class of all frames of the logic
$\mathop {\mathrm {Log}}{\mathcal {F}}$
. By Theorem 2.9(3),
$\mathcal {F}_1$
and
$\mathcal {I}_1$
are uniformly tunable, that is, there are functions
$f,g:\omega \to \omega $
such that
$\mathcal {F}_1$
is f-tunable and
$\mathcal {I}_1$
is g-tunable. Without loss of generality, we can assume that f and g are monotone. We will show that the class
${\textstyle \sum _{\mathcal {I}_1}{\mathcal {F}}}$
is uniformly tunable.
Consider a sum
${\textstyle \sum _{I}{F_i}}$
, where all
$F_i=(X_i,(R_{i,\lozenge })_{\lozenge \in \mathrm {A}})$
are in
$\mathcal {F}$
,
$I=(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}})\in \mathcal {I}_1$
. Then
$\bigsqcup _{i\in Y}{X_i}$
is the domain of
${\textstyle \sum _{I}{F_i}}$
. Let
$\mathcal {V}_0$
be a finite partition of
$\bigsqcup _{i\in Y}{X_i}$
. Since all
$F_i$
are in
$\mathcal {F}$
, the disjoint sum
$\bigsqcup _{i\in Y} F_i$
is in
$\mathcal {F}_1$
. Hence, there exists a refinement
$\mathcal {V}$
of
$\mathcal {V}_0$
such that
$\mathcal {V}$
is tuned in
$\bigsqcup _{i\in Y}{F_i}$
and
$$ \begin{align} |\mathcal{V}|\leq f(|\mathcal{V}_0|). \end{align} $$
Consider the following function
$t: Y\to \mathcal {P}(\mathcal {V})$
: for
$i\in Y$
, put
$$ \begin{align*}t(i)=\{V\in\mathcal{V}\mid \exists a\in X_i\, (i,a)\in V\}.\end{align*} $$
On Y, put
$$ \begin{align*}i\sim j \text{ iff } t(i)=t(j),\end{align*} $$
and let
$\mathcal {U}_0$
be the quotient
$Y{/}{\sim }$
. By the construction,
$$ \begin{align} |\mathcal{U}_0|\leq 2^{|\mathcal{V}|}. \end{align} $$
Since
$\mathcal {I}_1$
is g-tunable, there exists a finite refinement
$\mathcal {U}$
of
$\mathcal {U}_0$
such that
$\mathcal {U}$
is tuned in I and
$$ \begin{align} |\mathcal{U}|\leq g(|\mathcal{U}_0|). \end{align} $$
Let
$\mathcal {S}$
be the quotient of
$\bigsqcup _{i\in I}{X_i}$
by the following equivalence:
$$ \begin{align*}(i,a)\sim_{\mathcal{S}} (i',a') \text{ iff } (i,a)\sim_{\mathcal{V}} (i',a') \text{ and } i\sim_{\mathcal{U}} i'.\end{align*} $$
Clearly,
$\mathcal {S}$
refines
$\mathcal {V}_0$
, and also we have
$$ \begin{align} |\mathcal{S}|\leq |\mathcal{V}|\times |\mathcal{U}|. \end{align} $$
Define the function
$h:\omega \to \omega $
as follows:
$$ \begin{align*}h(n)=f(n)\cdot g(2^{f(n)}).\end{align*} $$
According to (31), (28), (29), and (30), we have
$$ \begin{align} |\mathcal{S}|\leq h(|\mathcal{V}_0|). \end{align} $$
We claim that
$\mathcal {S}$
is tuned in
${\textstyle \sum _{I}{F_i}}$
. Assume that
$(i,a)\sim _{\mathcal {S}} (i',a')$
and
$(i,a)R^\Sigma _\lozenge (j,b)$
. We need to show that there exists
$(j',b')$
such that
$$ \begin{align} (i',a')R^\Sigma_\lozenge (j',b') \text{ and }(j,b)\sim_{\mathcal{S}} (j',b'). \end{align} $$
Consider two cases.
Case 1. Assume that
$i\neq j$
. Then we have
$i S_\lozenge j$
. Since
$(i,a)\sim _{\mathcal {S}} (i',a')$
, we have
$i\sim _{\mathcal {U}} i'$
. Since
$\mathcal {U}$
is tuned in I, we have
$i'S_\lozenge j'$
and
$j\sim _{\mathcal {U}} j'$
for some
$j'$
. Since
$\mathcal {U}$
refines
$\mathcal {U}_0$
, we have
$t(j)=t(j')$
. Let V be the element of
$\mathcal {V}$
that contains
$(j,b)$
. Then
$V\in t(j')$
, and thus there is
$b'$
in
$X_{j'}$
such that
$(j',b')\in V$
. It follows that
$(j,b)\sim _{\mathcal {S}} (j',b')$
. Since
$i'S_\lozenge j'$
and
$S_\lozenge $
is irreflexive, we have
$i'\neq j'$
. Thus
$(i',a')R^\Sigma _\lozenge (j',b')$
, and so (33) follows.
Case 2. Assume that
$i=j$
. Since
$(i,a)\sim _{\mathcal {S}} (i',a')$
, we have
$(i,a)\sim _{\mathcal {V}} (i',a')$
. By the definition of
$R^\Sigma _\lozenge $
, we have
$a R_{i,\lozenge } b $
. Since
$\mathcal {V}$
is tuned in
$\bigsqcup _{i\in Y}{F_i}$
, we have
$(i,b)\sim _{\mathcal {V}} (i',b')$
and
$a'R_{i',\lozenge } b'$
for some
$b'$
in
$X_{i'}$
. Also, we have
$i\sim _{\mathcal {U}} i'$
. Put
$j'=i'$
. By the definition of
$R^\Sigma _\lozenge $
, we get
$(i',a')R^\Sigma _\lozenge (j',b')$
, which proves (33).
It follows that
$\mathcal {S}$
is tuned. According to (32),
${\textstyle \sum _{\mathcal {I}_1}{\mathcal {F}}}$
is uniformly tunable.
The construction in the above proof also shows the following.
Corollary 5.3. Let
$I=(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}})$
be an
$\mathrm {A}$
-frame where all
$S_\lozenge $
are irreflexive. If
$(F_i)_I$
is a family of
$\mathrm {A}$
-frames, and two algebras
$\mathop {\mathrm {Alg}}{\bigsqcup _{i\in Y} F_i}$
and
$\mathop {\mathrm {Alg}}{I}$
are locally finite, then
$\mathop {\mathrm {Alg}}{{\textstyle \sum _{I}{F_i}}}$
is locally finite and hence the logic of
${\textstyle \sum _{I}{F_i}}$
has the finite model property.
We do not know if this corollary remains true without the irreflexivity condition.
5.2 Second semantic transfer result
The sum operation given above does not change the signature. The following sum-like operation combines modal languages. Let
$\mathrm {A}$
and
$\mathrm {B}$
be finite disjoint sets. Elements of
$\mathrm {A}$
and
$\mathrm {B}$
will be addressed as vertical and horizontal modalities, respectively.
In this and the following subsection we always assume that
$L_1$
and
$L_2$
are logics in the alphabets of
$\mathrm {A}$
and
$\mathrm {B}$
, respectively.
Definition 5.4. Let
$I=(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}})$
be an
$\mathrm {A}$
-frame,
$(F_i)_{i\in Y}$
a family of
$\mathrm {B}$
-frames,
$F_i=(X_i,(R_{i,\lozenge })_{\lozenge \in \mathrm {B}})$
. The lexicographic sum
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{I}{F_i}}$
is the
$(\mathrm {A}\cup \mathrm {B})$
-frame
$\left (\bigsqcup _{i \in Y} X_i, (S^\oplus _\lozenge )_{\lozenge \in \mathrm {A}}, (R_\lozenge )_{\lozenge \in \mathrm {B}}\right )$
, where
$$ \begin{align*} \text{for }\lozenge\in\mathrm{A},& (i,a) S^\oplus_\lozenge (j,b) \text{ iff } i S j;\\ \text{for }\lozenge\in\mathrm{B},& (i,a) R_\lozenge (j,b) \text{ iff } i = j \;\&\;a R_{i,\lozenge} b. \end{align*} $$
For a class
$\mathcal {I}$
of
$\mathrm {A}$
-frames and a class
$\mathcal {F}$
of
$\mathrm {B}$
-frames,
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{\mathcal {I}}{\mathcal {F}}}$
denotes the class of all sums
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{I}{F_i}}$
, where
$I \in \mathcal {I}$
and all
$F_i$
are in
$\mathcal {F}$
. For modal logics
$L_1$
and
$L_2$
, let
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
be the logic of the class
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{\mathcal {F}_1}{\mathcal {F}_2}}$
, where
$\mathcal {F}_i$
is the class of all frames of the logic
$L_i$
.
In the case when all summands are equal, this operation is the lexicographic product of frames; lexicographic products of modal logics were introduced in [Reference Balbiani, Ghilardi and Sebastiani2].
According to the following observation, lexicographic sum can be considered as a particular case of sum in the sense of Definition 5.1. Let
$(\varnothing )_{\mathrm {B}}$
denote the sequence of length
$\mathrm {B}$
consisting of empty sets.
Proposition 5.5. Let
$I=(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}})$
be an
$\mathrm {A}$
-frame,
$(F_i)_{i\in Y}$
a family of
$\mathrm {B}$
-frames, where
$F_i=(X_i,(R_{i,\lozenge })_{\lozenge \in \mathrm {B}})$
. Then
$$ \begin{align*}\textstyle {\textstyle {\sum\limits^{\mathrm{lex} }}_{I}{F_i}}\; = \;{\textstyle \sum_{I'}{(X_i, (T_{i,\lozenge})_{\lozenge\in\mathrm{A}}, (R_{i,\lozenge})_{\lozenge\in \mathrm{B}})}}, \end{align*} $$
where
$I'$
is the
$(\mathrm {A}\cup \mathrm {B})$
-frame
$(Y,(S_\lozenge )_{\lozenge \in \mathrm {A}},(\varnothing )_{\mathrm {B}})$
, and for
$\lozenge \in \mathrm {A}$
,
$i\in Y$
, we put
$T_{i,\lozenge }=X_i\times X_i$
whenever
$(i,i)\in S_\lozenge $
, and
$T_{i,\lozenge }=\varnothing $
otherwise.
Proposition 5.6. Let
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {B}})$
and
$F'=(X,(T_\lozenge )_{\lozenge \in \mathrm {A}},(R_\lozenge )_{\lozenge \in \mathrm {B}})$
be frames, and
$T_\lozenge =\varnothing $
or
$T_\lozenge =X\times X$
for every
$\lozenge \in \mathrm {A}$
. If a partition
$\mathcal {V}$
of X is tuned in F, then
$\mathcal {V}$
is tuned in
$F'$
.
Proof. Every partition is tuned with respect to the empty relation, and with respect to the relation
$X\times X$
.
Theorem 5.7. If the logics
$L_1$
and
$L_2$
are locally tabular, then the logic
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
is locally tabular as well.
Proof. Let
$\mathcal {I}$
and
$\mathcal {F}$
be the classes of frames of the logics
$L_1$
and
$L_2$
, respectively, L denote the logic
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
. Let
$$ \begin{align*} \mathcal{I}' = \{(Y,(S_\lozenge)_{\lozenge\in\mathrm{A}},(\varnothing)_{\mathrm{B}})\mid (Y,(S_\lozenge)_{\lozenge\in\mathrm{A}})\in \mathcal{I}\}, \end{align*} $$
and let
$\mathcal {F}'$
be the class of frames
$(X, (T_{\lozenge })_{\lozenge \in \mathrm {A}}, (R_{\lozenge })_{\lozenge \in \mathrm {B}})$
such that
$(X, (R_{\lozenge })_{\lozenge \in \mathrm {B}})$
is in
$\mathcal {F}$
, and for all
$\lozenge \in \mathrm {A}$
,
$T_{\lozenge }=\varnothing $
or
$T_{\lozenge }= X\times X$
. By Proposition 5.5,
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{\mathcal {I}}{\mathcal {F}}}\;\subseteq \;{\textstyle \sum _{\mathcal {I}'}{\mathcal {F}'}}.$
By Theorem 2.9(3), classes
$\mathcal {I}$
and
$\mathcal {F}$
are uniformly tunable. Hence, by Proposition 5.6, classes
$\mathcal {I}'$
and
$\mathcal {F}'$
are uniformly tunable as well. By Theorem 5.2, the logic
$L'$
of the class
${\textstyle \sum _{\mathcal {I}'}{\mathcal {F}'}}$
is locally tabular. Since
$L'\subseteq L$
, the statement follows.
5.3 Axiomatic transfer result
Let
$\Phi (\mathrm {A},\mathrm {B})$
be the set of all formulas
$$ \begin{align} {\lozenge^{\mathrm{h}}} {\lozenge^{\mathrm{v}}} p\to {\lozenge^{\mathrm{v}}} p, \; {\lozenge^{\mathrm{v}}}{\lozenge^{\mathrm{h}}} p\to {\lozenge^{\mathrm{v}}} p, \;{\lozenge^{\mathrm{v}}} p\to \Box^{\mathrm{h}} {\lozenge^{\mathrm{v}}} p \end{align} $$
with
${\lozenge ^{\mathrm {v}}}$
in
$\mathrm {A}$
and
${\lozenge ^{\mathrm {h}}}$
in
$\mathrm {B}$
. The corresponding frame conditions are the following:
$(X,(R_\lozenge )_{\lozenge \in \mathrm {A}\cup \mathrm {B}})\vDash \Phi (\mathrm {A},\mathrm {B})$
iff for all
${\lozenge ^{\mathrm {v}}}$
in
$\mathrm {A}$
and
${\lozenge ^{\mathrm {h}}}$
in
$\mathrm {B}$
,
$$ \begin{align} R_{\lozenge^{\mathrm{h}}}\circ R_{\lozenge^{\mathrm{v}}} &\subseteq R_{\lozenge^{\mathrm{v}}}, \end{align} $$
$$ \begin{align} R_{\lozenge^{\mathrm{v}}}\circ R_{\lozenge^{\mathrm{h}}} &\subseteq R_{\lozenge^{\mathrm{v}}}, \end{align} $$
$$ \begin{align} {(R_{\lozenge^{\mathrm{h}}})}^{-1}\circ R_{\lozenge^{\mathrm{v}}} &\subseteq R_{\lozenge^{\mathrm{v}}}. \end{align} $$
The formulas
$\Phi (\mathrm {A},\mathrm {B})$
were considered in [Reference Balbiani, Ghilardi and Sebastiani2] in connection with axiomatization problems of lexicographic products, and also in [Reference Beklemishev4] in the context of polymodal provability logic.
Proposition 5.8 (Follows from [Reference Balbiani, Ghilardi and Sebastiani2]).
For a class
$\mathcal {I}$
of
$\mathrm {A}$
-frames and a class
$\mathcal {F}$
of
$\mathrm {B}$
frames,
$$ \begin{align*}{\textstyle {\sum\limits^{\mathrm{lex} }}_{\mathcal{I}}{\mathcal{F}}}\vDash \Phi(\mathrm{A},\mathrm{B}).\end{align*} $$
Proof. By Definition 5.4.
Let
$L_1\oplus L_2$
be the extension of the fusion of
$L_1$
and
$L_2$
with the axioms
$\Phi (\mathrm {A},\mathrm {B})$
:
$$ \begin{align} L_1\oplus L_2 = L_1 * L_2+\Phi(\mathrm{A},\mathrm{B}). \end{align} $$
In many cases, we have
$$ \begin{align} {\textstyle {\sum\limits^{\mathrm{lex} }}_{L_1}{L_2}}=L_1\oplus L_2. \end{align} $$
For example, (39) holds for the logic 
(where 
is the Gödel-Löb logic) [Reference Beklemishev4] and, as follows from [Reference Balbiani, Ghilardi and Sebastiani2], for 
.
Let
$F=(X,(R_\lozenge )_{\mathrm {A}})$
and
$G=(Y,(S_\lozenge )_{\mathrm {A}})$
be frames. Recall that
$f:X\to Y$
is called a p-morphism from F to G, if the following holds for all
$\lozenge \in \mathrm {A}$
:
$$ \begin{align} &\text{for all }a,b\in X, \text{ if }aR_\lozenge b, \text{ then }f(a)S_\lozenge f(b), \text{ and } \end{align} $$
$$ \begin{align} &\text{for all }a\in X, u\in Y, \text{ if }f(a)S_\lozenge u, \text{ then }aR_\lozenge a'\text{ and }f(a')=u\text{ for some }a'\in X. \end{align} $$
The notation
$f:F\twoheadrightarrow G$
means that G is the image of F under a p-morphism f; in this case
$\mathop {\mathrm {Log}}{F}\subseteq \mathop {\mathrm {Log}}{G}$
(see, e.g., [Reference Blackburn, De Rijke and Venema10, Theorem 3.14(iii)]).
For a in F, we put
${F}\!\left <a\right>= F{\upharpoonright } R^*_F(a)$
; we say that
${F}\!\left <a\right>$
is rooted and a is a root of F.
Lemma 5.9. If
$L_1\oplus L_2$
is Kripke complete, then
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}\subseteq L_1\oplus L_2$
.
Proof. Let
$F=(X,(R_\lozenge )_{\lozenge \in \mathrm {A}\cup \mathrm {B}})$
be a frame with a root r,
$F\vDash L_1\oplus L_2$
.
Put
$I={(X,(R_\lozenge )_{\lozenge \in \mathrm {A}})}\!\left <r\right>$
. For i in I, put
$F_i={(X,(R_\lozenge )_{\lozenge \in \mathrm {B}})}\!\left <i\right>$
. Finally, put
$$ \begin{align*}F^\oplus={\textstyle {\sum\limits^{\mathrm{lex} }}_{I}{F_i}}.\end{align*} $$
Observe that
$I\vDash L_1$
and
$F_i\vDash L_2$
for all i in I. Hence,
$F^\oplus $
validates
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
.
We will show that F is a p-morphic image of
$F^\oplus $
. Consider the unions of vertical and of horizontal relations in F:
$$ \begin{align*} \textstyle V=\bigcup_{\lozenge\in\mathrm{A}} R_\lozenge, \quad H =\bigcup_{\lozenge\in\mathrm{B}} R_\lozenge. \end{align*} $$
Notice that we have the following inclusions between relations in F for every vertical modality
$\lozenge \in \mathrm {A}$
:
$$ \begin{align} H^*\circ R_\lozenge &\subseteq R_\lozenge, \end{align} $$
$$ \begin{align} R_\lozenge\circ H^* &\subseteq R_\lozenge, \end{align} $$
$$ \begin{align} {H^*}^{-1}\circ R_\lozenge &\subseteq R_\lozenge. \end{align} $$
Indeed, (42) easily follows from (35), (43) from (36), and (44) from (37).
Let us check that
$$ \begin{align} (V\cup H)^*=V^*\circ H^*. \end{align} $$
That
$(H\cup V)^*\supseteq H^*\circ V^*$
is immediate. To prove the converse inclusion, by induction on n we show that
$(H\cup V)^{n}\subseteq H^*\circ V^*$
for every
$n\geq 0$
. The case
$n=0$
is trivial. By the induction hypotheses,
$$ \begin{align*} (V\cup H)^{n}\circ (V\cup H)&\subseteq (V^*\circ H^*) \circ (V\cup H)\\&= ((V^*\circ H^*) \circ V)\cup ((V^*\circ H^*) \circ H).\end{align*} $$
By (42),
$H^* \circ V\subseteq V$
. So we have
$(V^*\circ H^*) \circ V=V^*\circ (H^* \circ V)\subseteq V^*$
, and hence
$$ \begin{align*}(V\cup H)^{n+1}\subseteq V^*\cup (V^*\circ (H^* \circ H)) = V^*\circ H^*,\end{align*} $$
which proves (45).
For
$(i,a)$
in
$F^\oplus $
, put
$$ \begin{align*}f(i,a)= a.\end{align*} $$
Let us show that f is surjective. Suppose
$a\in X$
. Since r is a root of F,
$r (V\cup H )^* a$
. By (45), we have
$rV^*iH^*a$
for some i. Then i is in I, a is in
$F_i$
, and so
$(i,a)$
is in
$F^\oplus $
.
Let us show that f is a p-morphism. Fix the following notation:
$$ \begin{align*} I=(Y,(S_\lozenge)_{\lozenge\in\mathrm{A}}),\quad F^\oplus=(X^\oplus, (S^\oplus_\lozenge)_{\lozenge\in\mathrm{A}},(R^\oplus_\lozenge)_{\lozenge\in\mathrm{B}}). \end{align*} $$
By the construction, the frame
$(X^\oplus , (R^\oplus _\lozenge )_{\lozenge \in \mathrm {B}})$
is the disjoint sum of a family of generated subframes of
$(X,(R_\lozenge )_{\lozenge \in \mathrm {B}})$
. It follows that
$$ \begin{align} f:(X^\oplus, (R^\oplus_\lozenge)_{\lozenge\in\mathrm{B}}) \twoheadrightarrow (X,(R_\lozenge)_{\lozenge\in\mathrm{B}}). \end{align} $$
Let us check that for every
$\lozenge \in \mathrm {A}$
,
$$ \begin{align} f:(X^\oplus, S^\oplus_\lozenge)\twoheadrightarrow (X,R_\lozenge). \end{align} $$
To check (40), assume that
$(i,a)S^\oplus _\lozenge (j,b)$
. Then
$iR_\lozenge j$
,
$iH^*a$
, and
$jH^*b$
. Thus
$a ({H^*}^{-1} \circ R_\lozenge \circ H^* )b$
. We have
${H^*}^{-1}\circ R_\lozenge \subseteq R_\lozenge $
by (44), and
$R_\lozenge \circ H^*\subseteq R_\lozenge $
by (43), so
$aR_\lozenge b$
. To check (41), consider
$(i,a)\in X^\oplus $
and suppose
$a R_\lozenge b$
. Then we have
$i H^* a R_\lozenge b$
. By (42),
$i R_\lozenge b$
. It follows that b is in I. Clearly, b is in
$F_b$
, so
$(b,b)$
is in
$F^\oplus $
. By the definition of lexicographic sum, we get
$(i,a)S^\oplus _\lozenge (b,b)$
. Hence we have (47). From (46) and (47), we obtain that
$f:F^\oplus \twoheadrightarrow F$
.
So every rooted frame F of
$L_1\oplus L_2$
is a p-morphic image of a frame of
${{\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
, which proves the lemma.
Theorem 5.10. Let
$L_1$
and
$L_2$
be locally tabular logics. If
$L_1\oplus L_2$
is Kripke complete, then it is locally tabular.
Proof. By Lemma 5.9,
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}\subseteq L_1\oplus L_2$
. By Theorem 5.7, the logic
${\textstyle {\sum \limits ^{\mathrm {lex} }}_{L_1}{L_2}}$
is locally tabular, and so
$L_1\oplus L_2$
is.
Formulas (34) are Sahlqvist formulas (see, e.g., [Reference Chagrov and Zakharyaschev14, Section 10.3]). It follows that if the logics
$L_1$
and
$L_2$
are canonical (in the sense that they are valid in their
$\omega $
-canonical frames), then
$L_1\oplus L_2$
is canonical, and so is Kripke complete.
Corollary 5.11. If
$L_1$
and
$L_2$
are canonical locally tabular logics, then
$L_1\oplus L_2$
is locally tabular.
Notice that there are non-canonical locally tabular logics [Reference Goldblatt19, Section 6].
Acknowledgments
I am grateful to the reviewer for multiple useful suggestions on an earlier version of the manuscript.
Funding
The work on this paper was partially supported by the NSF Grant DMS-2231414.
