Lattices of Subframe Logics A Survey(Non-Classical Logics and Their Kripke Semantics)

Lattices of Subframe

Logics

A

Survey

Frank

Wolter

School of Information Science

JAIST

Tatsunokuchi, Ishikawa

923-12

Japan

October

16,

1995

1

Introduction

Besides ofinvestigating the intrinsic propertiesofa logic, like decidability or completeness,

it is desirable to relate it to its neighbors. While in general it is far from clear what the

neighbors ofa logic are, modal logicians traditionally take the lattice of all modal logics

or some principle filter within this lattice. Thus, for a modal logic $\Lambda$, relating it to its

neighbors meant investigatingthe structure ofthe lattice of modallogics. However, in the

late $70\mathrm{s}$it has become clear that the lattice of normal modal logics is extremely complex.

Let us mentiononly theembeddingof second order logicintomodal logic duetoThomason

[32] and the results of Blok (cf. [4], [5],

[6],

and below) about the structure of this lattice.

Without any restriction as

concerns

the class of modal logics under consideration no

positive result is available. And, as concerns the lattice structure, discrimination between

(interesting) logics via there position within the lattice is not possible. (For instance,

intuitively the theory of the reflexive frames, $\mathrm{T}=\mathrm{K}+\square parrow p$, should $\mathrm{h}\mathrm{a}\mathrm{v}.\mathrm{e}$ a specific

position with in the lattice of normal modal logics, simply because it has such a simple

geometric meaning. However, it just behaves like nearly all the others).

In this situation it is one of the basic questions to find and describe interesting proper

sublattices of the lattice of modal logics, which allow a more detailed treatment and thus

lead to finer tuned theory with more discriminative power. The object of this paper is

to show that the lattice of subframe logics as defined here is such a lattice, and that

the natural neighbors of a subframe logic can be found within the lattice of subframe

logics. It will turn out that from the perspective of this lattice we observe many subtle

and interesting differences between logics which seemed to behave similar if taken in the

whole lattice.

This paper gives a survey of$\mathrm{t}\mathrm{h}\mathrm{e}_{r}\mathrm{r}_{\xi}\mathrm{S}\mathrm{u}\mathrm{l}\mathrm{t}_{\mathrm{S}}[33]$ and [37] on lattices ofsubframe logics. If

a proposition is stated without proof and reference then the proofcan always be found in

[33] or [37].

Definition

of subframe

logics.

is a sequence of binary relations on $h$ and $A\subseteq 2^{h}$ is non-empty, closed under the boolean

operations $\cap$ and -, and under

$\square _{i}a=\{X\in g:(\forall y\in g)(_{X}\triangleleft_{iy}\Rightarrow y\in a)\}$,

for $1\leq\dot{i}\leq n$. $\mathrm{n}$-frames form a natural semanticsfor normal modal logics in the

proposi-tional language $\mathcal{L}_{n}$ with _$n$ modal operations $\coprod_{i},$$1\leq i\leq n$

.

The logic Th$\mathcal{H}$ of a frame $\mathcal{H}$

is the set of formulas which are valid in $\mathcal{H}$; we write _{$\mathcal{H}|=\phi$} if a formula $\phi$ is valid in $\mathcal{H}$.

For a class $\mathrm{M}$ offrames put

$\mathrm{T}\mathrm{h}\mathrm{M}=\cap\{\mathrm{T}\mathrm{h}\mathcal{H} :\mathcal{H}\in \mathrm{M}\}$

.

Conversely, for a modal logic $\Lambda$, call a frame

7#

a $\Lambda$-frame, in symbols 7-?

$|=\Lambda$, if all

formulas $\phi\in\Lambda$ are valid in $\mathcal{H}$

.

The class of A-frames is denoted by $\mathrm{G}\mathrm{f}\mathrm{r}\Lambda$. The mapping

$\Lambda\mapsto \mathrm{G}\mathrm{f}\mathrm{r}\Lambda$ is an anti-isomorphism (with respect toinclusion) between the lattice ofmodal

logics (in the language $\mathcal{L}_{n}$) and classes of$\mathrm{n}$-frames of the form $\mathrm{G}\mathrm{f}\mathrm{r}\Lambda$ (cf. [29]).

For each $\mathrm{n}$-frame $\mathcal{H}$ and each $b\in A$ with $b\neq\emptyset$, the structure

$\mathcal{H}_{b}=\langle b, \langle\triangleleft_{i}\cap(b\mathrm{x}b) : 1\leq\dot{i}\leq n\rangle, \{a\cap b : a \in A\}\rangle$

is a$\mathrm{n}$-frame as well, and we callit a

subframe

of$\mathcal{H}$

.

A normal modal logic A is a

subframe

logic iff$\mathrm{G}\mathrm{f}\mathrm{r}\Lambda$ is is closed under forming subframes. Let us introduce the operation Sf on

the class of all frames

Gfr

by putting

$\mathrm{S}\mathrm{f}\mathrm{M}=$ the class of isomorphic copies of subframes of frames in $\mathrm{M}$,

for $\mathrm{M}\subseteq$ Gfr. The notion ofa subframe of a frame has at least two roots. Call a frame $\mathcal{H}=\langle h, \triangleleft, A\ranglearrow$ a Kripke

frame

if$A=2^{h}$. In this case we shall write $\langle h, \triangleleft\ranglearrow$, or simply $h$

instead of$\langle h, \triangleleft, A\ranglearrow$; the class of Kripke framesisdenoted by Fr andweput $\mathrm{F}\mathrm{r}\Lambda=\mathrm{G}\mathrm{f}\mathrm{r}\Lambda\cap \mathrm{F}\mathrm{r}$

.

Now, at the level of Kripke-frames $\langle h, \triangleleft\ranglearrow$ the set ofsubframes coincides with the set of

substructures of the relationalstructure $\langle h, \triangleleft\ranglearrow$, in thesenseofclassical model theory. One

can show (cf. [33]) that a completelogic $\Lambda$, i.e. alogic A with

$\Lambda=\mathrm{T}\mathrm{h}(\mathrm{F}\mathrm{r}\Lambda)$, is asubframe logic iff $\mathrm{S}\mathrm{f}(\mathrm{F}\mathrm{r}\Lambda)\subseteq \mathrm{F}\mathrm{r}\Lambda$. Hence, restricted to complete logics $\Lambda$, we are dealing precisely

with those logics whose Kripke frames are closed under substructures. At the level ofthe

Boolean algebra $\langle A, \cap, -, h\rangle$ forming the subframes is a natural extension offorming the

relativization to

an

element $b\in A$, already discussed in the context of cylindric algebras

(cf. [20]). Subframe logics containing $\mathrm{K}4=\mathrm{K}+\square parrow\square \square p$ (the logic of the transitive

frames) havebeen introduced by K. Fine in [15] by using splittings. Such adefinition was

available because of the following fundamental result in [15].

Theorem 1.1 All

_subframe

logics containing K4 have the

_finite

model property.

A syntactic criterion.

Given anatural semantic definition the $\mathrm{q}\dot{\mathrm{u}}$estion arises whether

we

can describe subframe

logicsbymeans of syntactic closure conditions. Fortunately, thisisthecase. For aformula

$\phi$ and a variable

$p$, define $\phi\downarrow p$ inductively via

$q\downarrow p$ $=$ $q\wedge p$

($\phi$A $\psi$) $\downarrow p$ $=$ $(\phi\downarrow p)$ A $(\psi\downarrow p)$ $(\neg\phi)\downarrow p$ $=$ $\neg(\phi\downarrow p)$ A_$p$ $(\square _{i}\phi)\downarrow p$ $=$ $\coprod_{i}(parrow\phi\downarrow p)$ A

Put $\phi^{\mathrm{r}\mathrm{e}\mathrm{I}}=\phi\downarrow p$, for a variable

$p$ not in $\phi$, and put $\phi^{\mathrm{S}\mathrm{f}}=parrow\phi^{\mathrm{r}\mathrm{e}\mathrm{I}}$

.

It is shown in [33]

that a normal modal logic is a subframe logic if and only ifit is closed under the rule

$\phi/\phi^{\mathrm{S}\mathrm{f}}$

.

In acertain sense this characterization corresponds to the result of classical model theory

that the models of a first order theory $\mathrm{T}$ are closed under substructures if and only if $\mathrm{T}$

is axiomatizable by universal sentences.

A complete sublattice.

The basic observation for a lattice theoretic treatment of subframe logics is that they

form a complete sublattice of the lattice of modal logics (cf. [33]). For a subframe logic

A denote by $S\Lambda$ the lattice of subframe logics containing A. We

can

say

a

bit

more.

Consider a complete sublattice $D$ of a complete lattice $\mathcal{F}$

.

Then, for $a\in \mathcal{F}$, the upward

projection$a\uparrow D$ and downward projection$a\downarrow D$ of$a$ in $D$ are defined by

$a\uparrow_{D}=\wedge\langle b\in D:b\geq a\rangle$ and $a\downarrow_{D}=\langle b\in D:b\leq a\rangle$,

respectively. Denote, for a modal logic $\Lambda$, by A$\uparrow$ the upward projection and by $\Lambda\downarrow \mathrm{t}\mathrm{h}\mathrm{e}$

downward projection of A in $S\mathrm{K}_{n}$

.

Here, $\mathrm{K}_{n}$ denotes the smallest normal modal logic in

the language $\mathcal{L}_{n}$

.

By $\Lambda+\Gamma$ denote the smallest modal logic containing an $\mathrm{n}$-modal logic

A and $\Gamma\subseteq \mathcal{L}_{n}$

.

Assume that $\Lambda=\mathrm{K}_{n}+\Gamma$

.

Then

A$\uparrow=\mathrm{K}_{n}+\Gamma^{\mathrm{S}\mathrm{f}}$, where $\mathrm{r}^{\mathrm{S}\mathrm{f}}=\{\phi^{\mathrm{S}\mathrm{f}} :\phi\in\Gamma\}$

.

It follows that the upward projections of effectively axiomatizable logics are effectively

axiomatizable, as well. For the downward projection we have

A$\downarrow=\mathrm{T}\wedge(\mathrm{s}\mathrm{f}\mathrm{M})$, if $\Lambda=\mathrm{T}\mathrm{h}(\mathrm{M})$, for a class offrames M.

Examples.

Certainly the logics already introduced, $\mathrm{K}_{n},$ $\mathrm{T}$, and K4, are subframe logics. The basic

logic interpreting the provability predicate in arithmetic, namely

$\mathrm{G}=\mathrm{K}4+\square (\square parrow p)arrow\square p$,

is a subframe logic. This logic is characterized by the transitive Kripke frames without

infinite ascending chains (cf. [8]). On the other hand, the most natural modal logics in

which intuitionistic logic is embeddable via G\"odel’s translation, i.e.

$\mathrm{S}4=\mathrm{K}4+\square parrow p$,

Grz $=\mathrm{S}4+\square (\square (parrow\square p)arrow p)arrow p))$,

are

subframe logics. Grz is the logic characterized bythe transitive and reflexive

Kripke-frameswithout infinite strictly ascending chains (cf. [11]). The finite width logics $\mathrm{K}.\mathrm{I}_{n}=$

$\mathrm{K}+\mathrm{I}_{n},$$n>0$, where

$\mathrm{I}_{n}=\wedge\langle \mathrm{O}p_{i}|1\leq\dot{i}\leq n+1\ranglearrow\vee\langle$$\mathrm{O}$(

$pi$A $(p_{j}\vee \mathrm{O}p_{j})$)$|i\neq j_{i},j\leq n+1\rangle$$)$,

are subframe logics. They are, for $n>0$, characterized by the Kripke frames in which

.3, and corresponds to the condition known as right linearity. Hence K4.3 and S4.3 are well-known subframe logics (cf. $[9]\rangle$

.

The logics K.$\mathrm{A}\mathrm{l}\mathrm{t}_{n}=\mathrm{K}+\mathrm{a}\mathrm{l}\mathrm{t}_{n},$ $n>0$ , are also

subframe logics, where

$\mathrm{a}\mathrm{l}\mathrm{t}_{n}=\wedge\langle 0_{p_{i}}|1\leq i\leq n+1\ranglearrow\langle$$<>(p_{i}$ A$p_{j}$)$|i\neq j\rangle$

.

Those logics are, for $n>0$, characterized by the Kripke frames in which no point has

more than $\mathrm{n}$ successors (cf. [1] and [31]). Let us now turn to polymodal logics. Here we

find the minimal modal logics with $\mathrm{n}$ operators so that

$\mathrm{a}\mathrm{i}\mathrm{l}$

operators are conjugated, i.e.,

the logics $\mathrm{K}_{n}+\mathrm{c}\mathrm{n}_{\pi}$, where _{$\pi:\{1, \ldots n\}arrow\{1, \ldots, n\}$} with $\pi 0\pi=Id$ and

$\mathrm{c}\mathrm{n}_{\pi}=\{parrow\square _{i^{\langle>}\pi}(i)p:1\leq\dot{i}\leq n\}$ (1.1)

$\mathrm{K}_{n}+\mathrm{c}\mathrm{n}_{\pi}$ is characterized by the Kripke frames $\langle g,\vec{R}\rangle$ satisfying

$R_{i}=R_{\pi(}^{-1}1i)’\leq\dot{i}\leq n$. (1.2)

Examples are the selfconjugate logic $\mathrm{K}.\mathrm{B}_{1}=\mathrm{K}+\mathrm{c}\mathrm{n}_{Id}$, which, if added to S4 gives S5,

and the minimal tense logic $\mathrm{K}.t=\mathrm{K}_{2}+\mathrm{c}\mathrm{n}_{\pi}$ with $\pi(1)=2$ and $\pi(2)=1$ (consult [10]

and [17]$)$

.

We denote this mapping $\pi$ by $t$

.

Call a logic A a logic with conjugates if it

contains a $\mathrm{K}_{n}+\mathrm{c}\mathrm{n}_{\pi}$

.

The followingsimple construction from [23] and [16] gives us more

subframe logics. Consider $n$ monomodal logics $\Lambda_{i},$$1\leq i\leq n$, and suppose that $\Lambda_{i}$ is

formulated in the language with $\coprod_{i},$$1\leq i\leq n$. Then the

fusion

of $\langle\Lambda_{i} : 1 \leq i\leq n\rangle$,

$\otimes\langle\Lambda_{i} :1 \leq\dot{i}\leq n\rangle$, is the smallest modal logic in $\mathcal{L}_{n}\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}\cup\{\Lambda_{i} :1 \leq\dot{i}\leq n\}$

.

If all

the $\Lambda_{i}$ are subframe logics then the fusion is a subframe logic, as well. In fusions there

is no connection between different modal operators. A number of interesting subframe

logics is available by adding axioms to fusions, e.g., ifA is a monomodal subframe logic,

then

$\Lambda.t=(\Lambda\otimes \mathrm{K})+\mathrm{C}\mathrm{n}t$

is a subframe logic, as well, known as the minimal tense extension of A (cf. [34] and [35]).

Motivation, the history, and tools.

We shall now discuss in which properties of lattices of subframe logics we are interested

and why. The most important lattice theoretic concept we deal with is the notion of a

splittingofacomplete lattice of modal logics. Take acomplete lattice $D=\langle D, , \wedge, 0,1\rangle$

.

Then we say that $p_{0}\in D$ splits $D$ if there exists a $p_{1}\in D$ such that $\langle p_{0},p_{1}\rangle$ devides

the lattice into two disjoint parts, the filter $\mathcal{E}p_{1}=\{d\in D : d\geq p_{1}\}$ and the ideal

$\mathcal{I}p_{0}=\{d\in D : d\leq p_{0}\}$

.

In this case $p_{1}$ is uniquely determined by $p_{0}$ and we say that $p_{1}$ is the splitting-companion of$p_{0}$

.

$p_{1}$ is denoted by $D/p_{0}$

.

The pair $\langle p_{0},p_{1}\rangle$ is called a

splitting-pair. If$p_{1}$ is the splitting-companion of some $p_{0}$ then we simply say that $p_{1}$ is

a splitting of $D$. Another way to introduce splittings is the following. Call an element

$d$ (strongly) prime in $D$ if, for $d\geq\wedge\langle d_{i}|i\in I\rangle$, there always is an $i\in I$ with $d\geq d_{i}$

.

$\mathrm{M}\mathrm{c}\mathrm{K}\mathrm{e}\mathrm{n}\mathrm{z}\mathrm{i}\mathrm{e}[25].\mathrm{s}\mathrm{h}\mathrm{o}\mathrm{w}\mathrm{s}$ that $d$ is prime in $D$ iff$d$ splits $D$. Hence splittings can be visualized

1. Kripke-separation

A logic A has the Kripke separation property in $D$ ifthere is no other logic $\Theta\in D$

with $\mathrm{F}\mathrm{r}\Theta=\mathrm{F}\mathrm{r}\Lambda$. (Mostly this property is

called strict completeness, e.g. in $[4]$)$.\mathrm{T}\mathrm{h}\mathrm{e}$

problem is whether A has the Kripke separation property in $D$

.

2. Finite Kripke separation

A logic A has the finite Kripke separation property in $D$ ifthere is no other logic

$\Theta\in D$ with $\mathrm{f}\mathrm{F}\mathrm{r}\Theta=\mathrm{f}\mathrm{F}\mathrm{r}\Lambda$, where $\mathrm{f}\mathrm{F}\mathrm{r}\Theta$ denotes the set of finite $\Theta$-frames. The

question is whether A has the finite Kripke seperation property in $D$

.

3. Lower covers

A logic $\Theta\neq$ A is a lower

cover

of A in $D$ iff

{

$\Theta_{1}\in D$ : C) $\subseteq\Theta_{1}\subseteq\Lambda$

}

$=\{\Theta, \Lambda\}$

.

Which logics are the lower covers ofA in $D$, ifthere are any?

4.

Axiomatization

problem

Let us

assume

that there is a recursive set $\mathcal{L}_{D}$ offormulas which is complete for _$D$, i.e. (1) $\mathrm{K}_{n}+\phi\in D$, for all $\phi\in \mathcal{L}_{D}$, and (2) if A _{$\in D$} then _{$\Lambda=\mathrm{K}_{n}+\Gamma$}, for a set

offormulas $\Gamma\subseteq \mathcal{L}_{D}$

.

Is the axiomatization problem for A (relativeto _$D$) decidable?

In other words, is $\{\phi\in \mathcal{L}_{D} : \mathrm{K}_{n}+\phi=\Lambda\}$ a recursive set?

Certainly the interest of the problems above depends on the lattice 7) _{and on A. We}

shall have a look at a simple example and summarize (a small part of) the research on

splittings in modal logic in the $70\mathrm{s}$. Take for A the logic S5. Denote by $\mathcal{E}\Theta$ the lattice of

normal logics containing a normal logic $\Theta$

.

Then, tradionally one would take

$D$ to be one

of the lattices $\mathcal{E}\mathrm{S}4,$ $\mathcal{E}\mathrm{K}4$, or $\mathcal{E}\mathrm{K}$

.

We first have a look at $\mathcal{E}$S4. Here all those

problems

are solved by the observation that S5 is a splitting of $\mathcal{E}\mathrm{S}4$. The pair

$\langle \mathrm{T}\wedge(rightarrow\bullet), \mathrm{S}5\rangle$

is the required splitting pair in $\mathcal{E}$S4 (cf. [28]). (We draw frames

$\langle g, S\rangle$ in such a way

that $\mathrm{x}$ denotes an irreflexive point and

$\bullet$ denotes a reflexive point). Using the figure on

splittings this

means

$\mathrm{S}5=\cap\{\Lambda\in \mathcal{E}\mathrm{S}4:rightarrow\bullet \#\Lambda\}$.

Note that this splitting pair also shows in

a

nice way the geometrical meaning of S5.

It just says that the frames validating S5 are precisely those quasi ordered sets $\langle g, S\rangle$

figure on splittings shows that the only lower cover of S5 in $\mathcal{E}\mathrm{S}4$ is $\mathrm{S}5\cap \mathrm{T}\mathrm{A}(rightarrow\bullet$ $)$.

(3.) is solved. Now (1.) is solved by the consequence that $rightarrow\bullet|=\Theta$, for each logic $\Theta$

with S4 $\subseteq\Theta$ and S5 $\not\in$ O. So S5 is the only logic containing S4 whose Kripke frames

are

precisely the sets with an equivalence relation. (2.) is solved analogously (by using

that S5 has the finite model property). (4.) is translated into the problem whether

$\{\phi:\mathrm{S}4+\phi=\mathrm{S}5\}$ is recursive. But,

$\{\phi:\mathrm{S}4+\phi=\mathrm{s}5\}=\mathrm{s}5\cap\{\phi : rightarrow\bullet\#\phi\}$,

and the set to the right is certainly recursive. Intuitively, the frame $rightarrow\bullet$ is of more

importance than its logic. So,

we

shall say that $rightarrow\bullet$ splits S4 and

we

shall write

$\mathrm{S}5=\mathrm{S}4/rightarrow\bullet$

We come to $\mathcal{E}\mathrm{K}4$. In this lattice S5 is not a splitting. However, by extending the

notion of a splitting to the notion of a join-splitting we can apply basically the same

technique. An element $p_{1}\in D$ is

a

join-splitting of$D$ by $F\subseteq D$ if all $p_{0}\in F$ split $D$ and

$p_{1}=\vee\langle D/p:p\in F\rangle$

.

$p_{1}$ is denoted by $D/F$. Again for an element $a\in D$ and $F\subseteq \mathcal{E}a$

we call a join-splitting $\mathcal{E}a/F$ a join-splitting of $a$ and denote it by $a/F$

.

The following

proposition states that join-splittings behave quite similar to splittings.

Proposition 1.2 Suppose that$p_{1}=D/F$

.

Then,

for

all $a\in D,$ $a\geq p_{1}$

if

and only

if

$a\not\leq p$,

for

all$p\in F$

.

The following is shown in [28].

$\mathrm{S}5=\mathrm{K}4/\{\mathrm{x}, \mapsto, rightarrow\bullet \}$

.

(We omit writing Th(-)). In completely the same way as in $\mathcal{E}$S4 one may now solve all

the problems stated above for S5 in $\mathcal{E}\mathrm{K}4$

.

It should have become clear why splittings

give us interesting information about logics. In [3], [27], and [28], a lot of other systems

containing K4 are shown to be join.-splittings of $\mathcal{E}\mathrm{K}4$. However, the basic question is

whether we can apply the same technique in order to invest\’igate S5 in the lattice of all

modal logics $\mathcal{E}\mathrm{K}$

.

This is not the

case.

A frame

$g$ is called cyle free if there is no path

oflength $>0$ from a point in $g$ to itself, and a frame is rooted if there is a point $x$ such

that all the other points are endpoints of a path of length $\geq 0$ from $x$

.

The following is

proved in [4].

Theorem 1.3 A logic $0$ splits $\mathcal{E}\mathrm{K}$

if

and only

_if

$\Theta=\mathrm{T}\wedge(\mathcal{G})$,

for

a

finite

and rooted and

cycle

_{free frame}

$\mathcal{G}$

.

This theorem

means

that there

are

nearly no

interesting

join-splittings in $\mathcal{E}\mathrm{K}$

.

This

can

be seen by the observation that

$\mathrm{D}=\mathrm{K}+\theta \mathrm{T}=\mathrm{K}/\mathrm{x}$ (1.3)

is the largest join-splitting of $\mathcal{E}\mathrm{K}$ (cf. [4]). More important in the context of subframe

logics is the following Corollary from [33].

Corollary 1.4 No logic in$S\mathrm{K}$ is a join-splitting

So

we

get none of the basic systems introduced above. But maybe the definition of a

join-splitting is too weak! It might wellbe possible that there are splittings of$\mathcal{E}(\mathrm{K}+\mathrm{O}\mathrm{T})$

which wedo not obtain asjoin-splittings of$\mathcal{E}\mathrm{K}$. So, we call anelement _{$p_{1}\in D$} an iterated

splitting of $D$ by $(F_{1}, \ldots F_{n})$, (here $F_{i}\subseteq D$, for all $1\leq\dot{i}\leq n$), if each $p_{0}\in F_{1}$ splits $D$

and, for $1\leq\dot{i}\leq n-1$, each $p_{0}\in F_{i+1}$ splits $D/F_{1}/F_{2}/\ldots/F_{i}$, and

$p_{1}=D/F_{1}/F_{2}/\ldots/F_{n-1}/F_{n}$.

The following proposition states that iterated splittings behave quite similar to

join-splittings.

Proposition 1.5 Suppose that$p_{1}=D/F_{1}/F_{2}\ldots/F_{n}$

.

Then,

for

all$a\in D,$ $a\geq p_{1}$

if

and

only $\dot{i}fa\not\leq p$,

for

all$p\in F_{1}\cup F_{2}\ldots\cup F_{n}$

.

However, the following crucial result of [4] states that we get only one

new

(not very

exciting) logic.

Theorem 1.6 A logic A $\in \mathcal{E}\mathrm{K}$ is an iterated splitting

of

$\mathcal{E}\mathrm{K}$

if

and only

_if

it is a

join-splitting

_of

$\mathcal{E}\mathrm{K}$ or it is the inconsistent logic.

The conclusionisthat inthe lattice $\mathcal{E}\mathrm{K}$splittings arenot the appropriatetool forstudying

interesting systems. One may ask whether some of the problems stated above have a

positive solution without using splittings. Again, [4] gives

a

negative

answer.

Theorem 1.7

_If

a logic A is not an iterated splitting

_of

$\mathcal{E}\mathrm{K}$ and $not=\mathrm{K}$ then there exist

$2^{\aleph_{0}}$ logics $\Theta$ with $\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}\ominus$

.

Moreover, A has $2^{\aleph_{0}}$ lower covers in $\mathcal{E}\mathrm{K}$.

As concerns the axiomatization problem it is an old problem to show

Conjecture 1.8

_If

afinitely axiomatizable logic A is not an iterated splitting

_of

$\mathcal{E}\mathrm{K}$ and

does not coincide with $\mathrm{K}$ then the axiomatization problem

for

A in$\mathcal{E}\mathrm{K}$ is undecidable.

It is justified to conclude that only via sublattices there is hope to get positive results as

concerns the lattice structure of the lattice of modal logics. So we shall now have a brief

look at lattices of subframe logics. First note that we do not loose splitting pairs when

we take a complete sublattice.

Proposition 1.9 Suppose that $\mathcal{F}$ is a complete sublattice

of

$D$ and that $\langle p_{0},p_{1}\rangle$ is a

splitting pair in D. Then $\langle p_{0}\downarrow_{\mathcal{F},p}1\uparrow \mathcal{F}\rangle$ is a splitting-pair in $F$

.

Quite easily we obtain with (1.3) that

$\langle$Th(x),$\mathrm{T}\rangle$

is a splitting pair in the lattice of subframe logics. First, $\mathrm{T}\Uparrow(\mathrm{x})\downarrow=\mathrm{T}\mathrm{b}(\mathrm{x})$

.

Also, via

simple syntactic manipulation,

$( \mathrm{K}+\mathrm{O}\mathrm{T})\uparrow=\mathrm{K}+(\mathrm{O}\mathrm{T})\mathrm{s}\oint=\mathrm{K}+parrow \mathrm{O}(p\wedge \mathrm{T})=\mathrm{K}+parrow\langle\rangle p=\mathrm{T}$

.

Now we can solve for $\mathrm{T}$, in the lattice $S\mathrm{K}$, all the problems stated above. For instance,

the only lower cover of$\mathrm{T}$ in $S\mathrm{K}$ is $\mathrm{T}\cap \mathrm{T}\mathrm{h}(\mathrm{x})$, in contrast to the result that $\mathrm{T}$ has $2^{\aleph_{0}}$

A be a subframe logic. Then $\Theta\in S\Lambda$ has the $S\mathrm{f}$-separation property

$(\mathrm{S}\mathrm{s}\mathrm{p})$ in $S\Lambda$ iffit has

the Kripke separation propertyin $S\Lambda$. $\Theta$ has the _$Sf$

-finite

separation property $(\mathrm{f}\mathrm{s}\mathrm{p})$ in $S\Lambda$

iff it has the finite Kripke separation property in $S\Lambda$

.

The $Sf$-axiomatization problem is

solvable for $\Theta$ in $S\Lambda$ iff

$\{\phi\sim\phi^{\mathrm{S}} :\Lambda+=\Theta\}\backslash \mathrm{s}\mathrm{t}\mathrm{f}$

is a recursive set. Now $\mathrm{T}$ has ssp and fsp in $S\mathrm{K}$ since $\mathrm{T}$ has the fmp and

$\mathrm{x}|=\Theta$, for

each subframe logic $\Theta$ with $\mathrm{T}\not\in$ O. The

Sf-axiomatization

problem for $\mathrm{T}$ is decidable

since

$\{\phi^{\mathrm{S}\mathrm{f}} :\mathrm{K}+\phi=\mathrm{T}\mathrm{s}\mathrm{f}\}=\mathrm{T}\cap\{\phi \mathrm{s}\mathrm{f}:\mathrm{x}\#\phi^{\mathrm{S}\mathrm{f}}\}$ .

Certainly this example is not surprising. Themain difference if compared with the lattice

$\mathcal{E}\mathrm{K}$, is the fact that there

are

numerous

interesting examples ofiterated splittings in $S\mathrm{K}$

which are _{not join-splittings. Thus, the result} on $\mathrm{T}$ is useful, since now, in

order to prove

that a logic $\Lambda\supseteq \mathrm{T}$ is an iterated splitting of$S\mathrm{K}$ it suffices to show that it is

an iterated

splitting

of

ST.

At the moment we note only the following example.

$\mathrm{S}5=\mathrm{K}/^{\mathrm{S}\mathrm{f}}\mathrm{x}/^{\mathrm{S}\mathrm{f}}rightarrow/^{\mathrm{S}\mathrm{f}}<_{\bullet}^{\bullet}$

.

(Here we omit writing Th(Sf-) $\mathrm{a}\mathrm{n}\mathrm{d}/^{\mathrm{S}\mathrm{f}}$ means splitting in

the lattice ofsubframe logics).

Thus, for S5, all the problems stated above have a positive solution in the lattice of

subframe logics.

2

On

Correspondence

For subframe logics a number of concepts from _{completeness and correspondence theory}

turn out to be equivalent. First recall the following definitions of classes of frames. An

$\mathrm{n}$-frame $\langle h, \triangleleft, A\ranglearrow$ is

refined

if both

$(\forall x, y\in h)(x=y\Leftrightarrow(\forall a\in A)(X\in a\Leftrightarrow y\in a))$,

$(\forall x, y\in h)(_{X\triangleleft_{i}}y\Leftrightarrow(\forall a\in A)(_{X}\in\square _{i}a\Rightarrow y\in a))$

.

See [29] for an _{extensive study of refined frames. The class of refined frames is denoted}

by Rfr. A frame $\mathcal{H}$ is descriptiveifit is refined

$\mathrm{a}\mathrm{n}\mathrm{d}\cap U\neq\emptyset$, for each ultrafilter $U$ in the

boolean

reduct of $\mathcal{H}^{+}$ (consult [18]). We denote the class of finite

Kripke frames by $\mathrm{f}\mathrm{F}\mathrm{r}$

and the class of finite and rooted Kripke frames by $\mathrm{r}\mathrm{F}\mathrm{r}$. Also,

$\mathrm{R}\mathrm{f}\mathrm{r}\Lambda=\mathrm{R}\mathrm{f}\mathrm{r}\cap \mathrm{G}\mathrm{f}\mathrm{r}\Lambda,$ $\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}\cap \mathrm{G}\mathrm{f}\mathrm{r}\Lambda,$ $\mathrm{f}\mathrm{F}\mathrm{r}\Lambda=\mathrm{f}\mathrm{F}\mathrm{r}\cap \mathrm{G}\mathrm{f}\mathrm{r}\Lambda,$ $\mathrm{r}\mathrm{F}\mathrm{r}\Lambda=\mathrm{r}\mathrm{F}\mathrm{r}\cap \mathrm{G}\mathrm{f}\mathrm{r}\Lambda$,

for each logic A. Now we

can

define the concepts which will turn out to be equivalent. A

logic A is compact (alias strongly complete) iff each set $\Gamma\subseteq \mathcal{L}$ which is consistent with

A is satisfiable in a frame in $\mathrm{F}\mathrm{r}\Lambda$. A logic A is

$r$-persistent if $\langle h, \triangleleft^{arrow}\rangle\in \mathrm{F}\mathrm{r}\Lambda$

whenever

$\langle h, \triangleleft, A\ranglearrow\in \mathrm{R}\mathrm{f}\mathrm{r}\Lambda$

.

[13] calls

$r$-persistent logics naturallogics. A is $d$-persistent if $\langle h, \triangleleft\ranglearrow\in$ $\mathrm{F}\mathrm{r}\Lambda$ whenever $\langle h, \triangleleft, A\ranglearrow$ is a descriptive A-frame. Following Goldblatt [19] we call a logic A complex if, for all $\mathcal{G}\in \mathrm{G}\mathrm{f}\mathrm{r}\Lambda$, there exists $\mathcal{H}=\langle h, \triangleleft, A\ranglearrow$ with $\langle h, \triangleleft\rangle\sim\in \mathrm{F}\mathrm{r}\Lambda$ such that

$\mathcal{H}^{+}\simeq \mathcal{G}^{+}$

.

Note that, in general, $\mathrm{r}$-persistency does not imply $\mathrm{d}$-persistency (cf. [13]). Also,

in general, $\mathrm{d}$

logics which are not $\mathrm{d}$-persistent (cf. [38]). A class of Kripke frames

$\mathrm{F}$ is called universal

iffit is definable by a set of universal first order sentences. $\mathrm{F}$ has the

finite

embedding

property if$g\in \mathrm{F}$ ifand only if each finite subframe $f$ of$g$ is in $\mathrm{F}$, for all

$g\in$ Fr.

Theorem 2.1 For a

_subframe

logic A thefollowing conditions are equivalent:

(1) $\mathrm{F}\mathrm{r}\Lambda$ is universal and A is complete.

(2) A is elementary and complete.

(3) A is d-persistent.

(4) A is r-persistent.

(5) A is complex.

(6) A is compact.

(7) $\mathrm{F}\mathrm{r}\Lambda$ has the

finite

embeddingproperty and A is complete.

Later we shall mostly work with $\mathrm{r}$-persistency. However, the finite embedding propertyis

closely related to splittings. Suppose that $\mathrm{F}\subseteq \mathrm{r}\mathrm{F}\mathrm{r}$ and A is a subframe logic. Define

$\mathrm{F}\mathrm{r}\Lambda_{\mathrm{F}}=\{g\in \mathrm{F}\mathrm{r}\Lambda :(\forall f\in \mathrm{F})f\not\in \mathrm{S}\mathrm{f}g\}$

.

We write $\mathrm{F}\mathrm{r}_{\mathrm{F}}$ instead of $(\mathrm{F}\mathrm{r}\mathrm{K}_{n})_{\mathrm{F}}$

.

Corollary 2.2 Suppose that a

_subframe

logic A is complete and elementary. Then there

is a set $\mathrm{F}\subseteq \mathrm{r}\mathrm{F}\mathrm{r}$ such that $\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}_{\mathrm{F}}$

.

If

A is finitely axiomatizable, then there exists a

finite

set$\mathrm{F}\subseteq \mathrm{r}\mathrm{F}\mathrm{r}$ with $\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}_{\mathrm{F}}$

.

Intuitively, ifwe want to show that a complete and elementary subframe logic A is an

iterated Sf-splitting, then we should take a set $\mathrm{F}\subset \mathrm{r}\mathrm{F}\mathrm{r}$ with

$\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}_{\mathrm{F}}$, and show that $\mathrm{F}$

defines an iterated Sf-splitting such that $\Lambda=\mathrm{K}_{n}/^{\overline{\mathrm{S}}\mathrm{f}}\mathrm{F}$

.

(See the next chapter for

a

precise

definition ofthe right hand side ofthis equation). This is indeed the simple idea behind

many results to follow. Call a class of Kripke frames $\mathrm{F}$

definable

by modal

_formulas

if

there exists a modal logic A with $\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}$

.

Let us note the following characterizations.

Theorem 2.3 A universal class

_of

Kripke

_frames

$\mathrm{F}$ is

definable

by modal

_{formulas iff}

$\mathrm{F}$

is closed with respect to $p$-morphic images and disjoint unions.

Corollary 2.4 For each set $\mathrm{F}\subseteq \mathrm{r}\mathrm{F}\mathrm{r}$, the class $\mathrm{F}\mathrm{r}_{\mathrm{F}}$ is

definable

by modal

formulas iff

$\mathrm{F}\mathrm{r}_{\mathrm{F}}$

is closed under$p$-morphic images.

3

A

Splitting

Lemma

From

now

on we are dealing with lattice theoretic properties of lattices of subframe

logics. Suppose that A and $\Theta$ are subframe logics. $\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{n}\ominus=\mathrm{T}\mathrm{h}\mathcal{G}$, for aframe $\mathcal{G}$

.

Hence, $\Theta=\mathrm{T}\mathrm{h}(\mathrm{S}\mathrm{f}\mathcal{G})$

.

Now suppose that $\Theta$ splits $S\Lambda$

.

Then we shall say that $\mathcal{G}$ Sf-splits A and

weshall denote the splitting $S\Lambda/\Theta$ by$\Lambda/\mathrm{S}\mathrm{f}\mathcal{G}$. Foraset of frames$\mathrm{F}$ suchthat all framesin $\mathrm{F}$ Sf-split A

we

shall denote thejoin-splitting by the theories Th

$(\mathrm{S}\mathrm{f}\mathcal{G}),$$\mathcal{G}\in \mathrm{F}$, by $\Lambda/\mathrm{S}\mathrm{f}_{\mathrm{F}}$

.

By definition, $\Lambda/^{\mathrm{S}\mathrm{f}}\mathrm{F}$ is the smallest

$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{f},\mathrm{r}\mathrm{a}\mathrm{m}\mathrm{e}$ logic

$\Theta$ containing A with _{$\mathcal{G}\#\Theta$}, for all

$\mathcal{G}\in \mathrm{F}$

.

The following Theorem provides a criterion for Sf-splittings. It is also important that

language of polymodal logic with $n$ Boxes $\coprod_{1},$

.

$,$

.

$,$

$\coprod_{n}$. For a formula $\phi\in \mathcal{L}_{n}$ and $m\in\omega$

the formula $\square ^{m}\phi$ is defined as follows.

$\square ^{0}\phi=\phi;\square ^{m+1}\phi=\wedge\langle\square i\square m\phi|1\leq\dot{i}\leq n\rangle$.

Let $\square ^{\mathrm{t}^{m})}\phi=\wedge\langle\square ^{i}\phi|i\leq m\rangle$ and define fora set of formulas $\Gamma$ Notice that the construction of $\square ^{m}\phi$ depends on the language. If

we

want to indicate that $\square ^{m}\phi$ is defined in the

language $\mathcal{L}$

we

write $\square _{\mathcal{L}}^{m}\phi$

.

Consider

a finite frame

$\mathcal{G}=\langle g,\vec{S}\rangle$. Reserve

a

variable

$p_{y}$ for

each $y\in g$. We define aformula $\nabla_{\mathcal{G}}$ by putting

$\nabla_{\mathcal{G}}$ $=$ $\wedge\langle p_{y}arrow \mathrm{O}_{i}p_{z}|yS_{i}z, 1\leq i\leq n\rangle$

A $\wedge\langle p_{y}arrow\square _{i}\neg p_{z}|\neg(ys_{i^{Z}}), 1\leq\dot{i}\leq n\rangle$

A $\wedge\langle p_{y}arrow\urcorner p_{z}|y\neq z\rangle$.

Theorem 3.1 Suppose that $\mathcal{G}=\langle g,\vec{S}\rangle$ is a

finite frame

with root $0$, and A is a

subframe

logic. Then (1) $\mathcal{G}Sf$-splits A

iff

(2) there exists $m\in\omega$ such that

for

all $\mathcal{H}\in \mathrm{G}\mathrm{f}\mathrm{r}\Lambda$

$\coprod^{(m)}\nabla \mathcal{G},p\mathrm{o}$ is

satisfiable

in $\mathrm{S}\mathrm{f}\mathcal{H}\Rightarrow(\forall n\geq m)\coprod^{(n})\nabla \mathcal{G},p_{0}$ is

satisfiable

in $\mathrm{S}\mathrm{f}\mathcal{H}$.

In this case $\Lambda/\mathrm{S}\mathrm{f}\mathcal{G}=\Lambda+(\square (m)\nabla_{Q}arrow\neg p\mathrm{o})\mathrm{S}\mathrm{f}$

.

There exist more general versions of this result. [21] presents a characterization of

split-tingsoflatticesof type$\mathcal{E}\Lambda$for finitelypresentable algebras. In [33] thisresult is generalized

to a characterization ofsplittings of arbitrary complete sublattices ofthe lattice of modal

logics by arbitrary subdirectlyirreducible algebras. However, here

we

shallnot need those

versions. For a large class of subframelogics Ait can be deduced that all finite and rooted

frames Sf-split $S\Lambda$

.

An $\mathrm{n}$-modal subframe logic A is $m$-transitive, $m>0$, if the formula

$\mathrm{t}\mathrm{r}_{m}.=(\coprod_{\mathcal{L}_{n}}p(m)arrow\square _{\mathcal{L}_{n}}^{m+_{p}})^{\mathrm{S}}1\mathrm{f}$

belongs to A. For instance, K4 is 1-transitive. Put $\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}=\mathrm{K}_{n}+\mathrm{t}\mathrm{r}_{m}$

.

By definition,

the logics $\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}$ are subframe logics. A tedious but straightforward proof shows that

$\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}$ is $\mathrm{d}$-persistent, hence complete and elementary. An$\mathrm{n}$-frame

$g$ is a$\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}$-frame

if and only if for each finite path from $x$ to $y$ in $g$ there exists a subpath oflength $\leq m$

from $x$ to $y$ in $g$

.

We get from the Theorem above

Corollary 3.2 Suppose that A is a $m$-transitive

subframe

logic,

for

some $m>0$

.

Then

each$\mathcal{G}\in \mathrm{r}\mathrm{F}\mathrm{r}\Lambda Sf$-splits A and $\Lambda/\mathrm{S}\mathrm{f}\mathcal{G}=\Lambda+\Pi^{(m)}\nabla_{\mathcal{G}}arrow\neg p_{0}$

.

Note that inthis case, for the axiomatization, we don’t need $(\coprod^{(m)}\nabla garrow\neg p_{0})\mathrm{S}\mathrm{f}$

.

Weleave

the proof to the reader since we shall not use this fact. That finite and rooted frames

always Sf-split $\mathrm{m}$-transitive logics A follows also, by Proposition 1.9, from the result

of Rautenberg [28] that those frames already split $\mathcal{E}\Lambda$

.

The deeper reason is that the

corresponding varieties ofmodal algebras have equational definable principle

congruences

(EDPC), consult [7].

We formulate the results as concerns the relation between the concepts we have

intro-duced in the introduction. It will be said that a set $\mathrm{F}$ of finite and rooted frame defines

an iterated Sf-splitting of a subframe logic A if there is a partition $\mathrm{F}_{1}\cup\ldots\cup \mathrm{F}_{n}$ of$\mathrm{F}$ such

that the frames in $\mathrm{F}_{i+1}$ Sf-split $\Lambda/\mathrm{S}\mathrm{f}\mathrm{F}_{1}\ldots/\mathrm{S}\mathrm{f}\mathrm{F}_{i}$, for $0\leq i<n$. The result is denoted by

Proposition 3.3 Suppose $that\ominus\in S\Lambda$, and A a

subframe

logic. Suppose that $\Theta$ is an

iterated $Sf$-splitting

of

A by a set

of

finite

and rooted

frames

F.

$\bullet$

If

$\mathrm{F}$ is

finite

$and\ominus is$ decidable, then the $Sf$-axiomatization problem$for\ominus in$ $S\Lambda$ is

decidable. We have

$\{\phi^{\mathrm{S}\mathrm{f}} :\Lambda+\phi^{\mathrm{S}\mathrm{f}}=\Theta\}=\{\phi^{\mathrm{S}\mathrm{f}} :\phi^{\mathrm{S}\mathrm{f}}\in\Theta, (\forall \mathcal{G}\in \mathrm{F})(\mathcal{G}\#\phi^{\mathrm{S}\mathrm{f}})\}$

$\bullet$

If

$\Theta$ is complete, then $\Theta$ has

$ssp$ in $S\Lambda$

.

$\bullet$

If

$\Theta$ has the$fmp$, $then\ominus has$ $fsp$ in $S\Lambda$.

$\bullet$ The lower covers

of

$\Theta$ in $S\Lambda$ are

{

$\Theta\cap \mathrm{T}\mathrm{h}(\mathrm{S}\mathrm{f}\mathcal{G}):\mathcal{G}\in \mathrm{F},$ $\mathcal{G}$ not subreducible onto another

frame

in $\mathrm{F}$

}.

4

Characterizing Sf-splittings

In this section we characterize the Sf-splittings of basic lattices $S\Lambda$

.

We know already

from Proposition 1.3 and 1.9 that rooted and cycle free finite frames Sf-split $\mathrm{K}_{n}$. On the

other hand, Blok has shown in [6] that only the reflexive point splits $\mathcal{E}\mathrm{T}$

.

The following

result tells us that for $S\mathrm{K}$ the situation is comparable to $\mathcal{E}\mathrm{K}$ while for $S\mathrm{T}$ it is quite

different from $\mathcal{E}\mathrm{T}$

.

Important for later applications is that we also obtain that those

Sf-splittings are $\mathrm{r}$-persistent. Let us recall the definitions.

Cycle

_{free frames.}

An $\mathrm{n}$-frame $\mathcal{G}=\langle g,\vec{R}\rangle$ is cycle

free

if $x_{0}\neq x_{m}$ for any path $\langle x_{j}|0\leq j\leq m\rangle$ in $\mathcal{G}$ with

$0\neq m$

.

$r$-cycle

free frames.

For an $\mathrm{n}$-frame $\mathcal{G}=\langle g,\vec{S}\rangle$ define $\mathcal{G}^{\mathrm{x}}=\langle g, \langle S_{i}-\{(y, y)|y\in g\}|\dot{i}\leq n\rangle\rangle$

.

In other words, we

replace all reflexive points by irreflexive points. Then $\mathcal{G}$ is _$r$-cycle

free

if$\mathcal{G}^{\mathrm{x}}$ is cycle free.

Theorem 4.1 (1) $A$

finite

rooted $n$

-frame

$\mathcal{G}Sf$-splits $\mathrm{K}_{n}$

iff

$\mathcal{G}$ is cycle

free.

In this case

$\mathrm{K}_{n}/\mathrm{S}\mathrm{f}\mathcal{G}=\mathrm{K}_{n}+\square (dp(\mathcal{G}))\nabla_{\mathcal{G}}arrow\neg p_{0}$ .

All$jo\dot{i}n- \mathrm{S}\mathrm{f}$-splittings

of

$\mathrm{K}_{n}$ are r-persistent.

(2) $A$

finite

rooted

frame

$\mathcal{G}\in \mathrm{F}\mathrm{r}(\otimes^{n}\mathrm{T})\mathrm{S}\mathrm{f}- spl\dot{i}ts\otimes^{n}\mathrm{T}$

iff

$\mathcal{G}$ is _$r$-cycle

free.

In this case

$\otimes^{n}\mathrm{T}/\mathrm{S}\mathrm{f}(\mathcal{G}=\otimes^{n}\mathrm{T}+\coprod dp(\mathcal{G}))\nabla_{\mathcal{G}}arrow\neg p_{0}$

.

All$jo\dot{i}n- \mathrm{S}\mathrm{f}- spl\dot{i}ttingsof\otimes^{n}\mathrm{T}$ are r-persistent.

Hence splittings of $\mathcal{E}\Lambda$ are even more sensible to cycles than splittings in $S\Lambda$

.

Let us

note two more characterizations ofsplittings and Sf-splittings ofimportant lattices which

underline this interpretation. Recall that $\mathrm{K}.t$ is

$\mathrm{t}\mathrm{h}\mathrm{e}-\mathrm{l}$ minimal tense logic. Define for

a

2-tree $\mathcal{T}=\langle t, <_{1}, <_{2}\rangle$ the frame $\mathcal{T}^{\mathrm{t}}’=\langle t, <_{1}\cup<_{2} , <_{2}\cup<_{1}^{-1}\rangle$

.

Obviously $\mathcal{T}^{\mathrm{t}}|=\mathrm{K}.t$

.

Also put $\mathcal{T}^{\mathrm{S}5}=\langle t, R_{1}, R_{2}\rangle$, where $R_{i}$ is the reflexive, transitiveand symmetric closure of $<_{i}$, for $i=1,2$

.

In the following theorem item (1) is shown in [22].

Theorem 4.2 (1) $A$

finite

and rooted

frame

$\mathcal{G}$ splits $\mathrm{K}.t$

iff

$\mathcal{G}=\mathrm{x}\mathrm{t}$

.

_{$(\mathit{1}’)A$}

finite

and

rooted

_frame

$\mathcal{G}Sf$-splits $\mathrm{K}.t$

iff

there exists a 2-tree $\mathcal{T}$ with $\mathcal{G}=\mathcal{T}^{\mathrm{t}}$

.

(2) $A$

finite

and

rooted

_frame

$\mathcal{G}$ splits $\mathrm{S}5\otimes \mathrm{S}5\dot{i}ff\mathcal{G}=\mathrm{x}\mathrm{S}5$

.

$(\mathit{2}’)A$

finite

and rooted

frame

$\mathcal{G}$ Sf-splits

5Iterated

splittings by

$\mathcal{T}$

-closed

sets

Now that we know which frames Sf-split $\mathrm{K}_{n}$ we have to find a path to go on. We shall

explain the idea how to do this by a simple example. Put $\mathrm{K}5=\mathrm{K}+\mathrm{O}parrow\square \mathrm{O}p$

.

K5 is

an $\mathrm{r}$-persistent logic such that

$\mathrm{F}\mathrm{r}\mathrm{K}5$ is axiomatized by _{$(\forall x, y, z)$}($XRy$A _{$xRz\Rightarrow yRz$}) (cf.

[26]$)$. How to provethat K5 is aniterated Sf-splitting? Following correspondence theory

it is readily checked that $\mathrm{F}\mathrm{r}\mathrm{K}5=\mathrm{F}\mathrm{r}_{\mathrm{F}}$, where $\mathrm{F}$ consists of the following frames.

$\mathcal{F}_{1}=*arrow \mathrm{x},$ $F_{2}=rightarrow \mathrm{x},$ $F_{3}=*arrow \mathrm{x},$ $F_{4}=$ -$\bullet$ , $F_{5}=rightarrow\bullet$,

$F_{6}=4_{\bullet}^{\bullet}$ $F_{7}=<_{\bullet}^{\bullet}$

.

In order to prove that $\mathrm{F}$ defines an iterated Sf-splitting which coincides with K5 we have

to decide with which frames to $S\mathrm{f}$-split first. It turns out that

$\mathrm{K}5=\mathrm{K}/^{\mathrm{s}\mathrm{f}}F_{1}/\mathrm{s}\mathrm{f}\{F2, \tau 3, F_{6}\}/\mathrm{S}\mathrm{f}_{\mathcal{F}4}/^{\mathrm{S}\mathrm{f}}\mathcal{F}5/^{\mathrm{S}}\mathrm{f}\mathcal{F}_{7}$,

where the right side of the equation is defined. In order to clarify this order we define

Arrow

_subframes.

Suppose that $\mathcal{F}=\langle f,\vec{R}\rangle$ and $\mathcal{G}=\langle g,\vec{S}\rangle$ are finite $\mathrm{n}$-frames and $x\in g$. Then $\mathcal{F}$ is an

$x$

-arrow

subframe

of $\mathcal{G}$, in symbols $F\leq_{x}\mathcal{G}$, if $f=g,$ $R_{i}\subseteq S_{i}$, for $1\leq i\leq n$, and $x$ is a

root ofF. $\mathcal{F}$is a strict

$x$-arrow

subframe

of$\mathcal{G}$, in symbols $\mathcal{F}<_{x}\mathcal{G}$, if$F\leq_{x}\mathcal{G}$ and $F\neq \mathcal{G}$.

In general, for $\mathcal{F}<_{x}\mathcal{G}$, we should first Sf-split with $\mathcal{F}$ and then with $\mathcal{G}$

.

(Above, _{$F_{1}$}

is indeed the only frame in $\mathrm{F}$ which splits $S\mathrm{K}.$) This motivates the order of the frames

$\mathcal{F}_{1}\ldots F_{5}$

.

However, in order to proceed in this way, we need some knowledge about the

intermediate steps. Roughly, we need to know that a $F$ with $\mathcal{F}<_{x}\mathcal{G}$ does not occur in

a frame for A if we want to show that $\mathcal{G}S\mathrm{f}$-splits A. More precisely, we would like to be

sure that

$\bullet$ $\Lambda_{1}=\mathrm{K}/^{\mathrm{S}\mathrm{f}}\mathcal{F}_{1}$ is complete and that

$\mathrm{F}\mathrm{r}\Lambda_{1}=\mathrm{F}\mathrm{r}_{\{\mathcal{F}_{1}\}}$ ,

$\bullet$ $\Lambda_{2}=\Lambda_{1}/^{\mathrm{S}\mathrm{f}}\{F2, F3, F6\}$ is complete and $\mathrm{F}\mathrm{r}\Lambda_{2}=\mathrm{F}\mathrm{r}_{\{f_{1}},\mathcal{F}2,F_{3},F_{6}$

},

$\bullet$ $\Lambda_{3}=\Lambda_{2}/^{\mathrm{S}\mathrm{f}}\tau_{4}$ is complete and

$\mathrm{F}\mathrm{r}\Lambda_{3}=\mathrm{F}\mathrm{r}_{\{\mathcal{F}_{6}}\mathcal{F}_{1},F_{2},F3,\mathcal{F}_{4},$

}.

and so on, for all the other intermediate steps. Often this will be achieved by proving

that those intermediate logics are $\mathrm{r}$-persistent. The frames$F_{6}$ and $F_{7}$ fit intothis scheme

since

$F_{11}=\mathrm{x}<_{\mathrm{X}}^{\mathrm{X}}$

and $F_{12}=\mathrm{x}<_{\bullet}^{\mathrm{x}}$

do not occur as subframes of frames in $\mathrm{F}\mathrm{r}\Lambda_{1}=\mathrm{F}\mathrm{r}_{\{\mathcal{F}_{1}\}}$

.

The argument is similar for $\mathcal{F}_{7}$.

Let us note already that the heuristic ideas above are not valid in general. For instance,

it will be shown (cf. Theorems 5.2 (1.) and 6.4) that $F_{11}$ Sf-splits $\mathrm{K}$ but that

$F_{12}$ does

not Sf-split $\mathrm{K}/\mathrm{S}\mathrm{f}_{\mathcal{F}_{11}}$. On the other hand $<_{\mathrm{X}}^{\mathrm{X}}$

Followingthe idea offorming$x- \mathrm{a}\mathrm{r}\mathrm{r}\mathrm{o}\mathrm{W}-\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{f}\Gamma \mathrm{a}\mathrm{m}\mathrm{e}\mathrm{S}$ we shallfirst investigate Sf-splittings

by sequences of frames from

$T$-closed sets.

Suppose that $\mathcal{T}=\langle t, <\ranglearrow$ is an $\mathrm{n}$-tree with root $0$. Then we put

$\langle \mathcal{T}\rangle=\{\mathcal{F}\in \mathrm{F}\mathrm{r}|\tau\leq 0\mathcal{F}\}$

.

Then $(\langle \mathcal{T}\rangle, \leq 0)$ is a finite partially ordered set with smallest element $\mathcal{T}$ and greatest

element $\langle t, \langle t\cross t:1\leq\dot{i}\leq n\rangle\rangle$. For $\mathcal{F}\in\langle \mathcal{T}\rangle$ we denote by $[\mathcal{T}, F]$ the interval

{

$\mathcal{G}$

:

$\mathcal{T}\leq 0$ $\mathcal{G}\leq 0\mathcal{F}\}$. Also put [$\mathcal{T},$$F[=[\mathcal{T}, \mathcal{F}]-\{\mathcal{F}\}$. A set $\mathrm{F}\subseteq\langle T\rangle$ is $\mathcal{T}$-closed if $\mathcal{F}\in \mathrm{F}$ implies

$[\mathcal{T}, \mathcal{F}]\subseteq \mathrm{F}$

.

n-trees.

Above, and in what follows, a $\mathrm{n}\mathrm{n}$-frame $\mathcal{G}=\langle g,\vec{S}\rangle$ is an $n$-tree if it is cycle free and

rooted and $S_{i}\cap S_{j}=\emptyset$, for all $\dot{i}\neq j$, and each _{$x\in g$} has not more than one predecessor

with respect to the relation $S=\cup\{S_{i}|1\leq i\leq n\}$

.

$1$-trees are called trees.

Since we want to define iterated Sf-splittings by $\mathcal{T}$-closed sets $\mathrm{F}$ it is important to

know whether $\mathrm{F}\mathrm{r}_{\mathrm{F}}$ is a class definable by modal formulas. This can be checked by using

Proposition 2.4. However, it is instructive to have an axiomatization. For a finite n-tree

$\mathcal{T}=\langle t, <\ranglearrow$ and $\mathcal{T}\leq 0\mathcal{G}=\langle g,\vec{S}\rangle$ define

$\nabla_{[\mathcal{T},\mathcal{G}]}$ $=$ $\wedge\langle p_{x}arrow\neg p_{y}|x\neq y\rangle$

$\wedge\wedge\langle p_{y}arrow C^{\rangle}ip_{x}|y<_{i}x\rangle$

$\wedge\wedge\langle p_{y}arrow\neg \mathrm{O}_{ip_{x}}|\neg(xS_{iy)\rangle}$

Proposition 5.1 $\Lambda=\mathrm{K}_{n}+\square (dp(T))\nabla[\tau,\mathcal{G}]arrow\neg p_{0}$ is the $r$-persistent

subframe

logic with

$\mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}_{1^{\mathcal{T},\mathcal{G}}}]$

.

Obviously we get an axiomatization for each logic ofthe form Th$(\mathrm{F}\mathrm{r}_{\mathrm{F}})$, where $\mathrm{F}$ is $\mathcal{T}-$

closed for some $\mathcal{T}$. The formulas

$\nabla_{[\mathcal{I},\mathcal{G}]}$ look quite similar to the formulas axiomatizing

iterated Sf-splittings, but they are not equivalent. This will follow from the fact that

quite often logics of type Th$(\mathrm{F}\mathrm{r}_{\mathrm{F}})$ are not iterated Sf-splittings. The following Lemma is

proved in

a

similar

_wa.y.

We are ready to prove the first general splitting result. In one of

the cases ofthis result the following frames will play a major role. Put, for $m\in\omega$,

$1\mathrm{i}\mathrm{n}\mathrm{e}_{m}=\langle\{0, \ldots, m\}, <\rangle$,

$\mathrm{d}\mathrm{i}.\mathrm{s}\mathrm{c}_{m}=\langle\{0, \ldots, m\}, s\rangle$, where $iSj$ iff$j=\dot{i}+1$,

$\mathrm{H}\mathrm{E}\mathrm{L}\mathrm{P}_{m}=[\mathrm{d}\mathrm{i}_{\mathrm{S}\mathrm{c}_{m}}, 1\mathrm{i}\mathrm{n}\mathrm{e}_{m}]$.

It follows immediately from Theorem 4.1 that $\mathrm{H}\mathrm{E}\mathrm{L}\mathrm{P}_{m}$ defines aniterated Sf-splitting such

that $\mathrm{H}_{m}:=\mathrm{K}/\mathrm{S}\mathrm{f}_{\mathrm{H}\mathrm{E}\llcorner}\mathrm{P}_{m}$ is $\mathrm{r}$-persistent and $\mathrm{F}\mathrm{r}\mathrm{H}_{m}=\mathrm{F}\mathrm{r}_{\mathrm{H}\mathrm{E}\mathrm{L}}\mathrm{p}_{m}$

.

Roughly, in presence of

$\mathrm{H}_{m}$ a lot of frames will Sf-split which do not Sf-split without $\mathrm{H}_{m}$

.

Transitive closure.

For a frame $\mathcal{G}=\langle g,\vec{S}\rangle$ define the transitive closure $\vec{S}^{*}$ of$\vec{S}$

by putting

$x\tilde{S}^{*}y$ iff there is a path oflength _$>0$ from

$x$ to $y$ in $\mathcal{G}$

.

Two classes

_{of frames.}

For an $\mathrm{n}$-tree $\mathcal{T}=\langle t, <\ranglearrow$ define the set $\langle \mathcal{T}\rangle_{\mathrm{R}}$ by

For a $\mathrm{n}$-tree $\mathcal{T}=\langle t, <\ranglearrow$ define the set $\langle \mathcal{T}\rangle_{\mathrm{H}}$ by

$\langle t,\vec{R}\rangle\in\langle \mathcal{T}\rangle_{\mathrm{H}}\Leftrightarrow \mathcal{T}\leq 0\langle t,\vec{R}\rangle$and $R_{i}\subseteq<arrow*\cup\{(x, 0) : x\in t\}\cup\{(x, x) : x\in t\},$ $1\leq i\leq n$

.

Theorem 5.2 Suppose that $\mathcal{G}\in\langle \mathcal{T}\rangle$ and that A is a $r$-persistent

subframe

logic with

$\mathrm{F}\mathrm{r}\Lambda\subseteq \mathrm{F}\mathrm{r}_{[\tau,Q[}$. Suppose that one

of

the following cases holds.

1. $\mathcal{G}\in\langle \mathcal{T}\rangle_{\mathrm{R}}$

.

2. $\mathcal{G}\in\langle \mathcal{T}\rangle_{\mathrm{H}}$ and $\Lambda\supseteq\otimes^{n}\mathrm{T}$

.

3. $\mathcal{G},$$\mathcal{T}$

,

andA are monomodal, $\mathcal{G}\in\langle \mathcal{T}\rangle_{\mathrm{H}}$ and $\Lambda\supseteq \mathrm{K}/\mathrm{S}\mathrm{f}_{\mathrm{H}\mathrm{E}\llcorner}\mathrm{P}_{m}$,

for

an $m\in\omega$

.

4.

A has conjugates, $i.e$. $\Lambda\supseteq \mathrm{K}_{n}+\mathrm{c}\mathrm{n}_{\pi}$ (see the Introduction).

Then $\mathcal{G}Sf$-splits A and $\Lambda/^{\mathrm{S}\mathrm{f}}\mathcal{G}$ is

$r$-persistent with $\mathrm{F}\mathrm{r}(\Lambda/^{\mathrm{s}\oint}\mathcal{G})=\mathrm{F}\mathrm{r}\Lambda\cap \mathrm{F}\mathrm{r}_{\{\mathcal{G}\}}$ .

We proceed with some applications of this Theorem. Often it will be more convenient

to allow Sf-splittings oflogics A by frames $\mathcal{G}$ with $\mathcal{G}\#$ A. In this case we simply put

$\Lambda/\mathrm{S}\mathrm{f}\mathcal{G}=\Lambda$. This mainly applies to iterated Sf-splittings.

Define an $\mathrm{n}$-tree $T$ by putting $\mathcal{T}=\langle\{0\}, \langle\emptyset|1\leq i\leq n\rangle\rangle$. By Theorem 5.2 (1.) $\langle \mathcal{T}\rangle_{\mathrm{R}}$

defines an iterated Sf-splitting of $\mathrm{K}_{n}$ and

$\otimes^{n_{\mathrm{T}=}}\mathrm{K}n/\mathrm{S}\mathrm{f}\langle \mathcal{T}\rangle_{\mathrm{R}}$

.

Corollary 5.3 For all $\pi$ with $\pi 0\pi=id$ the $logics\otimes^{n}\mathrm{T}+\mathrm{c}\mathrm{n}_{\pi}$ are iterated Sf-splittings

of

$\mathrm{K}_{n}$ by

finite frames.

They have the $fsp$, the

$ssp$ and the $Sf$-axiomatization problem is

decidable. Examples are $\mathrm{T}.tand\otimes^{n}\mathrm{T}.\mathrm{B}_{1}$.

For $m>0$ put

$\mathrm{w}\mathrm{d}_{m}=\mathrm{x}\langle_{\mathrm{x}_{\mathrm{m}}}^{\mathrm{X}1}$

$1$ and

$\mathrm{r}\mathrm{w}\mathrm{d}_{m}=\prec_{\bullet}^{\bullet 1}\mathrm{m}$

$1$

.

(7.1)

It isreadily checked that $\mathrm{F}\mathrm{r}_{\mathrm{W}\mathrm{D}_{m}}=\mathrm{F}\mathrm{r}(\mathrm{K}+\mathrm{I}_{m})$, where $\mathrm{W}\mathrm{D}_{m}=[\mathrm{w}\mathrm{d}_{m}, \prime \mathrm{w}\mathrm{d}_{m}]$

.

We also have

$\mathrm{W}\mathrm{D}_{m}\subseteq\langle \mathrm{w}\mathrm{d}_{m}\rangle_{\mathrm{H}}$. So we can apply Theorem 5.2 (3.) to $\mathrm{W}\mathrm{D}_{m}$ and have that $\Lambda+\mathrm{I}_{m}$ is

an iterated Sf-splitting by finite and rooted frames whenever $\Lambda\supseteq \mathrm{H}_{m}$, for some $m\in\omega$.

This applies, for instance, to $\mathrm{T}+\mathrm{I}_{m}$

.

Recall from Proposition 3.2 that the logics $\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}$ play an important role in lattices

ofsubframe since they are those which allow splittings by arbitrary frames in $\mathrm{r}\mathrm{F}\mathrm{r}$

.

So, it

would be nice ifwe could get $\mathrm{K}_{n}.\mathrm{T}\mathrm{r}_{m}$ as an iterated $S\mathrm{f}$-splitting. In the next section we

shall see that this not the case. However, for conjugated logics, more can be said.

Corollary 5.4 $\mathrm{K}.t+\mathrm{t}\mathrm{r}_{n}$ is an iterated $Sf$-splitting

of

$\mathrm{K}.t$ by

finite frames

and has the

$ssp$ in

SK.t.

$\mathrm{T}.t+\mathrm{t}\mathrm{r}_{n}$ is an iterated $Sf$-splitting

of

$\mathrm{K}_{2}$ by

finite

frames

and has

$ssp$ in

$S\mathrm{K}_{2}$

.

(Here, $\mathrm{t}\mathrm{r}_{n}=(\coprod_{\mathcal{L}_{2}}^{(n)}arrow\square _{c_{2}^{n+}}p)^{\mathrm{s}}(1)\mathrm{f}$).

We

see

that Part 4 of Theorem

5.2

is indeed the strongest result so far. We also get the

following result for minimal tense extensions $\Lambda.t$of monomodallogics A. For a monomodal

frame $\langle h, \triangleleft\rangle$ define

and for a set of monomodal Kripke frames $\mathrm{F}$ put

$\mathrm{F}^{t}=\{h^{t} : h\in \mathrm{F}\}$. A straightforward

proof shows

$\mathrm{F}\mathrm{r}(\Lambda.t)=(\mathrm{F}\mathrm{r}\Lambda)^{t}$ and $(\mathrm{F}\mathrm{r}(\Theta.t)=\mathrm{F}\mathrm{r}(\Lambda.t)\Leftrightarrow \mathrm{F}\mathrm{r}\Lambda=\mathrm{F}\mathrm{r}\ominus)$, (7.3)

for all monomodal logics A and $0$

.

The following Corollary follows immediately with

Theorem

5.2

(4.).

Corollary 5.5 Let $\mathcal{T}$ be a tree and $\mathrm{F}\subseteq\langle \mathcal{T}\rangle$ be $\mathcal{T}$-closed. Then $\mathrm{F}^{t}$

defines

an iterated

$S\mathrm{f}$-splitting

of

$\mathrm{K}.t$ such that $\mathrm{K}.t/\mathrm{S}\mathrm{f}_{\mathrm{F}}t$ is _$r$-persistent and $\mathrm{F}\mathrm{r}(\mathrm{K}.t/\mathrm{S}\mathrm{f}_{\mathrm{F}^{t})}=(\mathrm{F}\mathrm{r}_{\mathrm{F}})^{t}$

.

Put, for $m>0$,

$\mathrm{t}\mathrm{r}_{m}=\langle\{0, \ldots, m+1\}, \{(i,j)|j\leq\dot{i}+1\}\rangle$

.

(7.2) It is readily checked that $\mathrm{F}\mathrm{r}_{\mathrm{T}\mathrm{R}_{m}}=\mathrm{F}\mathrm{r}(\mathrm{K}.\mathrm{T}\mathrm{r}_{m})$, for $\mathrm{T}\mathrm{R}_{m}=[\mathrm{d}\mathrm{i}\mathrm{s}\mathrm{c}_{m+m}1, \mathrm{t}\mathrm{r}]$

.

Thus, the

minimal tense extensions (K.$r_{\mathrm{R}_{n}).t}$ as well as $(\mathrm{K}+\mathrm{I}_{n}).t$ are iterated $S\mathrm{f}$-splittings of $\mathrm{K}.t$

by finite frames. We even get $\mathrm{K}4.t$

.

Put

$F_{3}=\rangle-\cross,$ $F_{4}=*arrow\bullet$ .

Now it is not difficult to show that

$\mathrm{K}4.t=(\mathrm{K}.\mathrm{T}_{X_{1}}.\cdot t)/^{\mathrm{s}\mathrm{f}}\mathcal{F}_{3}t/\mathrm{S}\mathrm{f}_{\mathcal{F}_{4}}t$

.

By the previous Corollary $(\mathrm{K}.\mathrm{T}_{\Gamma_{1}}).t=\mathrm{K}.t/\mathrm{S}\mathrm{f}\mathrm{T}\mathrm{R}_{1}t$

.

So we conclude

Corollary 5.6 (1) The logic $\mathrm{K}4.t$ is an iterated $Sf$-splitting

of

$\mathrm{K}.t$ by

finite frames.

$It$

has the $ssp$ and the $fsp$ and the $S\mathrm{f}$-axiomatization problem is decidable in $SK$.t. (2) The

logic $\mathrm{S}4.t$ is an iterated$Sf$-splitting

of

$\mathrm{K}_{2}$ by

finite frames.

It has the

$ssp_{f}$ the$fsp$ and the

$S\mathrm{f}$-axiomatization problem is decidable in$S\overline{\mathrm{K}}_{2}$

.

6

Negative

Results

In this section we deliver some general counterexamples. Denote by G.3 the logic $\mathrm{G}+\mathrm{I}_{1}$.

G.3 has the finite model property and its frames areprecisely thestrict orderings without

infinite ascending chains. Hence

G.3 $=\mathrm{T}\wedge\{1\mathrm{i}\mathrm{n}\mathrm{e}_{n} :n\in\omega\}$

.

Theorem 6.1 Suppose that A is a $r$-persistent

subframe

logic with $1\mathrm{i}\mathrm{n}\mathrm{e}_{m}|=\Lambda$,

for

all

$m\in\omega$ (or, equivalently, $\Lambda\subseteq$ G.3). Suppose that there exists $\mathcal{G}\in \mathrm{r}\mathrm{F}\mathrm{r}\mathrm{T}$ which is

r-cycle-free

and $\mathcal{G}\#$ A. Then A is not

an

iterated $Sf$-splitting

of

$\mathrm{K}$ by

frames

in $\mathrm{r}\mathrm{F}\mathrm{r}$ and A does

not have the $ssp$

.

The Theorem above applies, for instance, for $\mathrm{K}.\mathrm{I}_{n}$ and $\mathrm{K}.\mathrm{T}\mathrm{r}_{n}$ but certainly also to

un-countably many other subframe logics.

Theorem 6.2 Suppose that$\mathrm{K}.\mathrm{T}\mathrm{r}_{n}\subseteq\Lambda\subseteq$ G.3

for

an $n>0$

.

Then A is not a

Recall that all frames in $\mathrm{r}\mathrm{F}\mathrm{r}(\mathrm{K}.\mathrm{T}\mathrm{r}_{n+1})s\mathrm{f}$-splitK.$\mathrm{T}\mathrm{r}_{n+1}$

.

Thus, Theorem 6.2 states that

as long as we do not Sf-split with finite G.3-frames we shall not get a logic containing

$\mathrm{K}.\mathrm{T}\mathrm{r}_{n}$ as a $\mathrm{j}_{\mathrm{o}\mathrm{i}\mathrm{n}-}\mathrm{s}\mathrm{f}$-splitting of $\mathrm{K}.\mathrm{T}_{\Gamma_{n+1}}$; hence not as an iterated $S\mathrm{f}$-splitting of $\mathrm{K}$ by frames in $\mathrm{r}\mathrm{F}\mathrm{r}$

.

Thus, the

following

result _{is just a reformulation of Theorem 6.2.}

Theorem 6.3 Suppose that $\mathrm{F}\subseteq \mathrm{r}\mathrm{F}\mathrm{r}(\mathrm{K}.\mathrm{T}\mathrm{r})n+1$ such that $\mathrm{F}\cap\{1\mathrm{i}\mathrm{n}\mathrm{e}_{m} :m\in\omega\}=\emptyset$ and

$\mathrm{F}\mathrm{r}(\mathrm{K}.\mathrm{T}\mathrm{r}+1)n\mathrm{p}\subseteq \mathrm{F}\mathrm{r}\mathrm{T}\mathrm{r}_{n}$. Then

K.$\mathrm{T}\mathrm{r}_{n+1}/\mathrm{S}\mathrm{f}\mathrm{F}$ is incomplete.

This result showsthat splittings also form apowerful tool forestablishing

numerous

simple

examples of finitely axiomatizable incomplete subframe logics. So far we did not disprove

certain quite plausible conjectures as

concerns

extensions of Theorem 5.2 (1.). Consider a

tree $\mathcal{T}=\langle t, <\rangle$ and a point $x\in t$ without

successors

(i.e. with _{$\{y:x<y\}=\emptyset$}). Denote

by $\mathcal{T}_{r(x)}$ the frame $\langle t, <\cup\{(x, x)\}\rangle$. The followingresult states that with each tree $\mathcal{T}$ with

$|t|>2$ there is associated a strictly _{descending chain of (incomplete) subframe logics} $\Theta_{n}$,

$n\in\omega$, with $\mathrm{F}\mathrm{r}\Theta_{n}=\mathrm{F}\mathrm{r}_{\{\tau,\mathcal{I}_{r()}\}x}$

.

Theorem 6.4 Suppose that $\mathcal{T}=\langle t, <\rangle$ is a tree with $|t|>2$ and _$x$ has no

successors.

Then there is a sequence $\langle k(n):n\in\omega\rangle$ such that,

for

$\Theta_{n}=(\mathrm{K}/\mathrm{s}\mathrm{f})T+(\square (k(n))\nabla_{\mathcal{T},r(x})arrow\neg p\mathrm{o})\mathrm{S}\mathrm{f},$ $n\in\omega$,

1. For all$n\in\omega_{f}\mathrm{F}\mathrm{r}\Theta_{n}=\mathrm{F}\mathrm{r}_{\{\mathcal{T},\mathcal{T}\}r(x)}$ and $\Theta_{n}$ is incomplete.

2. For all $n\in\omega,$ $\Theta_{n}\supset\Theta_{n+1}$

.

3.

$\mathcal{T}_{r(x)}$ does not$Sf$-split$\mathrm{K}/\mathrm{S}\mathrm{f}_{\mathcal{T}}$

.

4.

Th$\mathrm{F}\mathrm{r}_{\{\tau,\tau\}r(x)}$ does not have the _$ssp$ and is not an iterated $S\mathrm{f}$-splitting by

finite

and

rooted

_frames.

7

Subframe Logics

above

K4

The main result of this section is a classification of subframe logics containing K4. In

orderto prove it we have toSf-split witha number offrames. But

some

workwas already

rlnn$\theta.$ in Th$\mathrm{P}\cap \mathrm{r}p\mathfrak{m}.52$

.

Put

$\mathrm{T}\mathrm{R}=[\mathrm{d}\mathrm{i}\mathrm{S}\mathrm{C}2, \mathcal{G}_{1}]\cup\{\mathcal{G}_{2}\cdots \mathcal{G}_{7}\}$

.

Based

on

the

following

two Lemmas one can show the main Theorem.

Lemma 7.2 For all$n\in\omega$,

$\Lambda_{n}:=\mathrm{K}/^{\mathrm{s}}\mathrm{f}||\mathrm{n}\mathrm{e}/n\mathrm{s}\mathrm{f}[\mathrm{d}|\mathrm{s}\mathrm{c}2, \mathcal{G}_{1}]/\mathrm{S}\mathrm{f}\mathrm{s}\mathcal{G}2/\mathrm{f}\ldots/^{\mathrm{S}\mathrm{f}}\mathcal{G}_{7}$

is

_well-defined

and

$\Lambda_{n}=\mathrm{K}+\{(\square (3)\nabla_{\mathcal{G}}arrow p_{0})^{\mathrm{s}\mathrm{f}} : \mathcal{G}\in \mathrm{T}\mathrm{R}\cup\{1\mathrm{i}\mathrm{n}\mathrm{e}_{n}\}\}=\mathrm{K}4/^{\mathrm{S}\mathrm{f}_{\mathrm{l}\mathrm{i}}}\mathrm{n}\mathrm{e}_{n}$.

Theorem 7.3 Suppose that $\mathrm{F}$ is a set

of

finite, transitive and rooted

_frames

and that

$n\geq 2$

.

Then the following conditions are equivalent.

(1) $\mathrm{K}4/\mathrm{S}\mathrm{f}_{\mathrm{F}}$ has

$ssp$ in $S\mathrm{K}$

.

(2) K.$\mathrm{T}\mathrm{r}_{n}/\mathrm{S}\mathrm{f}(\mathrm{T}\mathrm{R}\cup \mathrm{F})=\mathrm{K}4/\mathrm{S}\mathrm{f}\mathrm{F}$

.

(3) $\mathrm{K}.\mathrm{T}\mathrm{r}_{n}/\mathrm{S}\mathrm{f}(\mathrm{T}\mathrm{R}\cup \mathrm{F})$ has_$fmp$. (4) $\mathrm{K}.\mathrm{T}\mathrm{r}n/\mathrm{S}\mathrm{f}(\mathrm{T}\mathrm{R}\cup \mathrm{F})$ is complete. (5) $(\exists m\in\omega)(|_{1}.\mathrm{n}\mathrm{e}m\in \mathrm{F})$

.

(6) $\mathrm{K}4/\mathrm{S}\mathrm{f}_{\mathrm{F}}$ is an iterated _$Sf$-splitting

of

$\mathrm{K}b\dot{y}$

finite

and rooted

frames.

Corollary 7.4 For$\Lambda\in S\mathrm{K}4$ the following conditions

are

equivalent:

(1) $\Lambda\not\subset \mathrm{G}.3$

.

(2) A is an iterated $Sf$-splitting

of

$\mathrm{K}$ by

finite

and rooted

_frames.

(3) A is a$j_{oi-}n\mathrm{S}\mathrm{f}$-splitting

of

K.$\mathrm{T}\mathrm{r}_{2}$ by

finite

and rooted

frames.

(4) A has $ssp$ in$S\mathrm{K}$

.

(5) A has $fsp$ in $S\mathrm{K}$

.

(6) A has $ssp$ in$\mathrm{K}.\mathrm{T}\mathrm{r}_{2}$

.

(7) A has$fsp$ in $\mathrm{K}.\mathrm{T}\mathrm{r}_{2}$

.

Thus, only a minor weakening of transitivity to $\mathrm{t}\mathrm{r}_{2}$ destroys all the nice properties of

subframe logics containing K4. Now, for a logic $\Theta$ without the ssp in $S\Lambda$ one would like

to know the cardinality of the set of logics $\Theta_{1}\in S\Lambda$ with $\mathrm{F}\mathrm{r}\ominus=\mathrm{F}\mathrm{r}\Theta_{1}$

.

Put

$\delta_{S\Lambda}(\Theta)=|\{\Theta_{1}\in S\Lambda$

:

$\mathrm{F}\mathrm{r}\ominus=^{\mathrm{p}_{\mathrm{r}}\ominus\underline{\eta}}1|$

.

The following partial answer for logics containing K4 is delivered in [33].

Theorem 7.5

_If

$\Lambda\in S\mathrm{K}4$ and $\Lambda\subseteq \mathrm{G}$, then $\delta_{S\mathrm{K}.\mathrm{T}\mathrm{r}_{2}}(\Lambda)=2^{\mathrm{N}_{0}}$

.

It is an open (and from a structural point of view interesting) problem whether also

$\delta_{S\mathrm{K}}$(G.3) $=2^{\mathrm{N}_{0}}$

.

We note that is is easy to show with the frames from the last section that $\delta_{S\mathrm{K}}(\mathrm{G}.3)\geq\aleph_{0}$

.

8

The

upper

part

of

$SK_{n}$

Investigating the upper part of a lattice is a classical problem in modal logic (cf. [5],

[12], [24]$)$

. So

it is

interesting

whether the upper part ofthe lattice of subframe logics

behaves

better than the upper part of the lattice of all normal modal logics. Recall from

the Introduction that $\mathrm{K}.\mathrm{A}\mathrm{l}\mathrm{t}_{n}$ is the (mono)-modal theory of all frames

$\langle h, \triangleleft\rangle$ satisfying

$|\{y:x\triangleleft y\}|\leq n$, for all _{$x\in h$}

.

First

we

need the foolowing result

on

the finite model

Theorem 8.1 For all $n,$$m>0$ all

subframe

logics $contain\dot{i}ng\otimes^{n}\mathrm{K}.\mathrm{A}\mathrm{l}\mathrm{t}_{m}$ have the$fmp$.

Based on this result one can show

Theorem 8.2 For all$n,$$l>0$ all

subframe

logics $contain\dot{i}ng\otimes^{n}\mathrm{K}$.Alt$l$ have the $ssp$ and

the $fsp$

.

We note that, in a certain sense, this result is optimal since there exists afinitely

axiom-atizable undecidable monomodal subframe logic such that in all rooted frames only one

point is allowed to have more than 4 successors. (This is not shown in [33] or [37] but

will be shown elsewhere).

Recall that a logic A is called tabular iff A $=$ Th$\mathcal{G}$, for a finite frame $\mathcal{G}$

.

Since each

tabular logic contains $\mathrm{s}\mathrm{o}\mathrm{m}\mathrm{e}\otimes^{n}\mathrm{K}.\mathrm{A}\mathrm{l}\mathrm{t}_{m}$, we conclude

Corollary 8.3 All tabular

_subframe

logics have $ssp$ and$fsp$.

Call a logic A $Sf$-pretabular iff it is a maximal non-tabular subframe logic in $S\mathrm{K}$. By

Zorn’s Lemma, all non-tabular subframe logics are contained in aSf-pretabular subframe

logic. Examples are $\mathrm{K}.\mathrm{A}\mathrm{l}\mathrm{t}_{1}$, G.3, S5 and Grz.3. (Recall that Grz.3 is the reflexive

counterpart of G.3, i.e.

Grz.$3=\mathrm{T}\mathrm{h}\{\mathrm{r}|\mathrm{i}\mathrm{n}\mathrm{e}_{m} :m\in\omega\}$,

where $\mathrm{r}\mathrm{I}\mathrm{i}\mathrm{n}\mathrm{e}_{m}=\langle\{0, \ldots, m\}, \leq\rangle$, for $m\in\omega$, (cf. [15])$)$

.

Nowwe can formulate all desirable

properties of the upper part of$S\mathrm{K}_{n}$

.

The codimension of a logic A in $S\mathrm{K}_{n}$ is the length

of the longest $\subset$-chain in $S\mathrm{K}_{n}$ from A to $\mathcal{L}_{n}$

.

Corollary 8.4 (1) All $S\mathrm{f}$-pretabular logics have

infinite

codimension in $S\mathrm{K}_{n}$

.

(2) $A$

subframe

logic is tabular

_if

and only

_if

it has

_finite

codimension in $S\mathrm{K}_{n}$

.

(3) The

Sf-axiomatization problem in $S\mathrm{K}_{n}\dot{i}S$ decidable,

for

all tabular

subframe

logics. (4) All

Sf-pretabular logics have the$fmp$

.

We shall now restrict attention to monomodal logics. One of the classical problems

of modal logic is the description of the pretabular logics in certain lattices, if possible.

However,

even

for logics containing K4 such a description is not available byBlok’s result

that there

are

$2^{\aleph_{0}}$ pretabular

logics containing K4 (cf. [5]). (On the other hand, there

are precisely 5 pretabular logics containing S4 (cf. [12])$)$

.

The situation is different

for monomodal lattices of

subframe

logics. Here we shall describe those Sf-pretabular

logic which do not contain $\mathrm{K}.\mathrm{A}\mathrm{l}\mathrm{t}_{n}$, for all $n>0$

.

(A description of all monomodal

Sf-pretabular logics seems possible. However, it is readily checked that there exist $\geq\aleph_{0}$ such

logics containing K.$\mathrm{A}\mathrm{l}\mathrm{t}_{3}$). Consider the following sets of frames

$\mathrm{F}^{00}=$ $\{ \mathrm{X}\langle_{\mathrm{x}_{\mathrm{n}}}\mathrm{X}1 1 :n\in\omega\}$ and $\mathrm{G}^{00}=$ $\{ \mathrm{X}\langle_{\mathrm{X}}^{\cross}\mathrm{n}1 1 :n\in\omega\}$

.

From $\mathrm{F}^{00}$ and $\mathrm{G}^{00}$ we obtain sets $\mathrm{F}^{0}$ and $\mathrm{G}^{0}$ by adding

$\{(0,0)\}$ to the relations, and we

obtain $\mathrm{F}^{1}$ and $\mathrm{G}^{1}$ by adding _{$\{(x, x) : 1 \leq x\leq n+1\}$} to

the relations. Finally we obtain

sets$\mathrm{F}^{01}$ and $\mathrm{G}^{01}$ by adding $\{(x, x) : 0\leq x\leq n+1\}$ to the relations. Recall the definition