monthyeardate[], MnLargeSymbols’036 MnLargeSymbols’043

# An expressively complete tangle operator for the topological $\mu$-calculus

David Fernández-Duque1 2
Konstantinos Papafilippou1
1Gent University, Gent, Belgium
2University of Barcelona, Barcelona, Spain
<EMAIL_ADDRESS>
<EMAIL_ADDRESS>
###### Abstract

The topological $\mu$-calculus has gathered attention in recent years as a
powerful framework for representation of spatial knowledge. In particular,
spatial relations can be represented over finite structures in the guise of
weakly transitive ($\sf wK4$) frames. In this paper we show that the
topological $\mu$-calculus is equivalent to a simple fragment based on a
variant of the ‘tangle’ operator. Similar results were proven for more
restricted classes of frames by Anuj Dawar and Martin Otto, using modal
characterisation theorems for the corresponding classes of frames. However,
since the $\mu$-calculus is not equivalent to the bisimulation invariant
fragment of FOL or of MSO over wK4 frames, we use a different method to prove
our results; namely, the notion of finality which was also employed in the
proof of completeness and FMP of the $\mu$-calculus over wK4 frames. As a
corollary we obtain a new proof of an existing result showing the collapse of
the alternation hierarchy over wK4 frames.

##  1 Introduction

In knowledge representation, modal logic ($\sf ML$) provides an appealing
alternative to more powerful systems such as first order logic ($\sf FOL$) or
monadic second order logic ($\sf MSO$), largely due to so-called modal
characterization theorems [JvBThesis], which state that $\sf ML$ is the
bisimulation-invariant fragment of $\sf FOL$, while its extension to the modal
$\mu$-calculus is the bisimulation-invariant fragment of $\sf MSO$ [JW]. For
many applications of logic to computer science, it is natural to consider
bisimulation-invariant properties, as bisimular structures essentially
represent equivalent programs or computations. Given that modal logics are
simpler in terms of complexity, often enjoying decidable satisfiability
problems and efficient model-checking, modal characterization theorems show
that these benefits come without sacrificing expressive power.

Dawar and Otto [DO] showed that modal characterization theorems extend to many
classes of frames, but the situation for finite, transitive frames is subtle.
In this setting, the bisimulation-invariant fragments of $\sf FOL$ and $\sf
MSO$ coincide, but are stronger than modal logic. They are in fact equal to
the $\mu$-calculus, but this in turn can be greatly simplified to its tangled
fragment, which adds expressions of the form
$\diamond^{\infty}\\{\varphi_{1},\ldots,\varphi_{n}\\}$, stating that there is
an accessible cluster of reflexive points where each $\varphi_{i}$ is
satisfied.

Finite, transitive frames are especially interesting for representation of
spatial properties, since their logic is that of metric spaces (such as
Euclidean spaces or the rational numbers) [Lucero-Bryan13, GH17], and thus
complex geometric relations can be represented in finite graphs. However, for
the more general setting of topological spaces, one must consider a wider
class of frames called weakly transitive frames: a relation $\sqsubset$ is
weakly transitive if $x\sqsubset y\sqsubset z$ implies $x\sqsubseteq z$. The
modal logic of finite, weakly transitive frames is precisely that of all
topological spaces [esakia-derivative], and this result extends to the full
$\mu$-calculus [Baltag2021TheTM]. In this spatial setting, Dawar and Otto’s
tangled operator becomes the tangled derivative, the largest subspace in which
two or more sets are dense: for example, the tangle of $\mathbb{Q}$ and
$\mathbb{R}\setminus\mathbb{Q}$ is the full real line, since the rationals and
the irrationals are both dense in $\mathbb{R}$. In the set of a single subset
$A$, $\Diamond^{\infty}\\{A\\}$ is the perfect core of $A$, i.e. its largest
perfect subset, a notion useful in describing the limit of learnability after
iterated measurements [SurpriseKR].

Alas, the tangled derivative is no longer expressively complete over the class
of all topological spaces [Baltag2021TheTM], and moreover the $\mu$-calculus
is no longer expressively complete, so Dawar and Otto’s result fails.
Nevertheless, Gougeon [Quent21] has proposed a more expressive operator, which
here we simply dub the tangle and denote by ∞, which coincides with the
tangled derivative over metric spaces (and other spaces satisfying a
regularity property known as $T_{D}$ spaces), but is strictly more expressive
over the class of arbitrary topological spaces. While this tangle operator
cannot be as expressive as the bisimulation-invariant fragment of $\sf MSO$,
it was still conjectured to be as expressive as the full $\mu$-calculus, thus
providing a streamelined framework for representing spatial properties
relevant for the learnability framework considered in [SurpriseKR]. This
conjecture is supported by the recent result stating that the topological
$\mu$-calculus collapses to its alternation-free fragment [alternation].

In this paper we give an affirmative answer to this conjecture. Moreover,
since we cannot use games for $\sf FOL$ to establish our results, our proof
uses new methods which have the advantage of providing an explicit translation
of the $\mu$-calculus into tangle logic. Among other things we provide an
upper bound on formula size, which is doubly exponential, which cannot be
greatly improved given the exponential lower bounds of [Iliev].

It is worth remarking that, despite the spatial motivation for the
$\mu$-calculus over $\sf wK4$, the results of [Baltag2021TheTM] allow us to
work entirely within the class of weakly transitive frames; since their logic
is that of all topological spaces, our expressivity results lift to that
context as well. The upshot is that background in topology is not needed to
follow the rest of the text.

### Layout

In Section 2 we review the syntax and semantics of the $\mu$-calculus, present
Gougeon’s tangle operator and some basic semantic notions that allow us to
characterize path-finite wK4 frames. Section 3 serves as a small introduction
to the notion of finality and some relevant definitions we will find useful.
More information of the applications of finality in wK4 frames can be found in
[Baltag2021TheTM].

In Section 4 are our main results, on important properties of
$\Sigma$-finality for particular sets of formulae $\Sigma$, that serve as a
foundation for the remainder of the paper. In Section 5 we construct some
formulae in the tangle logic that peer into the structure of a given Kripke
model. Then due to the theorems of section 4, we get an equivalence between
the $\mu$-calculus and the tangle logic as well as other concluding remarks.

##  2 Preliminaries

First let us recall the basic definitions of the $\mu$-calculus over weakly
transitive frames. As is often the case when working with $\mu$-calculi, it
will be conveninent to define the $\mu$-calculus with each of the positive
operations, including $\nu x.\phi$, as primitive, and with negation being only
subsequently defined.

######  Definition 1.

The language of the modal $\mu$-calculus $\mathcal{L}_{\mu}$ is defined by the
following syntax:

$\displaystyle\varphi::=\top\,|\,x\,|\,p\,|\,\neg
p\,|\,\varphi\wedge\varphi\,|\,\varphi\vee\varphi\,|\,\Diamond\varphi\,|\,\Box\varphi\,|\,\nu
x.\varphi(x)\,|\,\mu x.\varphi(x)$

where free variables $x$ will be treated as constants $p$ and when specified,
as sets or constants with a specific valuation possibly depending on the
model. Under this presentation of the language, the formulas are said to be in
_negation normal form_. We write $\mathbb{P}$ to denote the set of
propositional constants.
Negation is defined classically as usual with:

  * •

$\neg\nu x.\varphi(x):=\mu x.\neg\varphi(\neg x)$

  * •

$\neg\mu x.\varphi(x):=\nu x.\neg\varphi(\neg x)$.

We also write $\diamonddot\varphi:=\varphi\vee\Diamond\varphi$ and similarly
$\boxdot\varphi:=\varphi\wedge\Box\varphi$.

######  Definition 2.

A Kripke frame is a tuple $\mathcal{F}=\langle M,\sqsubset_{M}\rangle$ where
${\sqsubset_{M}}\subseteq M\times M$.
A Kripke model is a triple $\mathcal{M}=\langle
M,\sqsubset_{M},\|\cdot\|_{M}\rangle$ where $\langle M,\sqsubset_{M}\rangle$
is a Kripke frame with a valuation
$\|\cdot\|_{M}:\mathbb{P}\to\mathcal{P}(M)$. In the sequel, we will use
$\mathcal{M}$ and $M$ interchangeably. We denote by $\sqsubseteq_{M}$ the
reflexive closure of $\sqsubset_{M}$.
Given $A\subseteq M$, we denote the irreflexive and reflexive upsets of $A$ as
$A{\uparrow_{M}}:=\\{w\in M:\exists v\in A\ v\sqsubset_{M}w\\}$ and
$A{\uparrow^{*}_{M}}:=A{\uparrow_{M}}\cup A$ respectively. The downsets are
similarly denoted as $A{\downarrow_{M}}:=\\{w\in M:\exists v\in A\
w\sqsubset_{M}v\\}$ and $A{\downarrow^{*}_{M}}:=A{\downarrow_{M}}\cup A$
respectively. We will omit the $M$ in the subscript when we will be only
referring to a single model.

The valuation $\|\cdot\|=\|\cdot\|_{M}$ is defined as usual on Booleans with:

  * •

$\|\Diamond\varphi\|:=\|\varphi\|{\downarrow}$

  * •

$\|\mu x.\varphi(x)\|:=\bigcap\\{X\subseteq M:X=\|\varphi(X)\|\\}$

  * •

$\|\nu x.\varphi(x)\|:=\bigcup\\{X\subseteq M:X=\|\varphi(X)\|\\}$

Given a Kripke model $M$ and a world $w\in M$ we say a formula $\varphi$ is
satisfied by $M$ at the world $w$ and write $w\vDash_{M}\varphi$ iff
$w\in\|\varphi\|_{M}$.

A formula $\varphi$ is valid over a class of models $\Omega$ if for every
$M\in\Omega$, $\|\varphi\|_{M}=M$.

We note that $\mu x.\varphi(x)$ and $\nu x.\varphi(x)$ are the least and
grteatest fixed points, respectively, of the operator $X\mapsto\varphi(X)$.

######  Example 1.

Consider a simple frame $\mathcal{F}$ consisting of two irreflexive points
$\\{0,1\\}$ such that $0\sqsubset 1$ and $1\sqsubset 0$; this frame is weakly
transitive since $x\sqsubset y\sqsubset z$ implies $x=z$, but it is not
transitive since e.g. $0\sqsubset 1\sqsubset 0$ but $0\not\sqsubset 0$. To
extend this frame into a model, we need to assign subsets of $\\{0,1\\}$ to
each propositional variable. Assume that our set of variables is $e$ (even),
$o$ (odd), $p$ (positive) and $i$ (integer). Then we readily obtain a
valuation $\|\cdot\|$ if we let $\|e\|=\\{0\\}$, $\|o\|=\\{1\\}$,
$\|p\|=\\{1\\}$, and $\|i\|=\\{0,1\\}$. Then for example it can be checked
that $\|o\vee\Diamond p\|=\\{0,1\\}$, since every element of our model is
either odd or has an accessible positive point. We may say that this formula
is valid in our model.

######  Definition 3.

Given $P\subseteq\mathbb{P}$ a $P$-bisimulation is a relation $\iota\subseteq
M\times N$ satisfying the conditions:

If $\langle u,v\rangle\in\iota$ then $w\vDash_{M}p\,\Leftrightarrow
v\vDash_{M}p$ for all $p\in P$;

forth

If $\langle u,v\rangle\in\iota$ and there is some $u\sqsubset_{M}u^{\prime}$,
then there is $v\sqsubset_{N}v^{\prime}$ such that $\langle
u^{\prime},v^{\prime}\rangle\in\iota$;

back

If $\langle u,v\rangle\in\iota$ and there is some $v\sqsubset_{N}v^{\prime}$,
then there is $u\sqsubset_{M}u^{\prime}$ such that $\langle
u^{\prime},v^{\prime}\rangle\in\iota$;

global

$dom(\iota)=M$ and $rng(\iota)=N$.

Two models are called $P$-bisimilar and we write $M\rightleftharpoons_{P}N$ if
there is some $P$-bisimulation relation between them. Given subsets
$A\subseteq M$ and $B\subseteq N$, we write $A\rightleftharpoons_{P}B$ when
$M\upharpoonright A\rightleftharpoons_{P}N\upharpoonright B$, where
$\upharpoonright$ denotes the usual restriction to a subset of the domain.

In the sequel we will omit the $P$ in the subscript and assume it to be the
set of constants occurring in a determined set of formulae.

Bisimulations are useful because they preserve the truth of all $\mu$-calculus
formulas, i,e. if $\langle w,v\rangle\in\iota$ and $\varphi$ is any formula
then $w\in\|\varphi\|$ iff $v\in\|\varphi\|$.

######  Definition 4.

A relation $R$ is weakly transitive iff for all $a,b,c$ where $a\neq c$, if
$aRb$ and $bRc$ then $aRc$. ${\sf wK4}$-frames are precisely those whose
accessibility relation $\sqsubset$ is weakly transitive.

From this point on, we will only be concerning ourselves with wK4 frames.

Interest in weakly transitive frames arises because the set of valid formulas
over these frames is precisly the set of valid formulas over the class of
topological spaces [Baltag2021TheTM]. We will not review these in detail here,
but recall that a topological space is a pair $\langle X,\mathcal{T}\rangle$,
where $\mathcal{T}$ is a family of subsets of $X$ (called the open sets) which
is closed under finite interscetsions and arbitrary unions. For $A\subset X$
we define $d(A)$ to be the set of points $x\in X$ such that whenever $x\in U$
and $U$ is open, there is $y\in A\cap U\setminus\\{x\\}$; this is the set of
limit points of $A$. The topological semantics for the $\mu$-calculus is
obtained by modifying Definition 2 by setting
$\|\Diamond\varphi\|=d\|\varphi\|$. This semantics is the basis to the modal
approach to spatial KR, but [Baltag2021TheTM] allows us to reduce it entirely
to weakly transitive frames.

######  Definition 5 ($\mu$-wK4).

The logic of $\mu$-wK4 is defined as the least set of formulas of
$\mathcal{L}_{\mu}$ containing the following axioms and closed under the
following rules (for all formulae $\varphi,\psi$ and $\theta(x)$ where $x$
occurs only positively in $\theta$):

All instances of axioms and rules of propositional logic closed under
substitution for formulas in $\mathcal{L}_{\mu}$;

Necessitation rule

$\dfrac{\varphi}{\Box\varphi}$;

Distribution axiom(K)

$\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi)$;

Weak Transitivity

$\Diamond\Diamond\varphi\to\diamonddot\varphi$;

Fixed point axiom

$\nu x.\theta(x)\to\theta(\nu x.\theta(x))$;

Induction rule

$\dfrac{\varphi\to\theta(\varphi)}{\varphi\to\nu x.\theta(x)}$

######  Theorem 1 (Completeness, FMP).

$\mu$-$\sf wK4$ is weakly complete for the class of weakly transitive frames.
It also has the finite model property with respect to weakly transitive
frames.

###### Proof.

See [Baltag2021TheTM]. ∎

As a result we will be working exclusively with finite frames.

Next we recall Gougeon’s tangle operator [Quent21].

######  Definition 6.

Given a finite multiset of formulae $\Gamma\subseteq\mathcal{L}_{\mu}$, the
tangle modality is defined as follows:

${}^{\infty}\Gamma=\nu
x.\bigvee_{\varphi_{i}\in\Gamma}\big{(}\diamonddot(\varphi_{i}\wedge
x)\vee\bigwedge_{\genfrac{}{}{0.0pt}{}{\varphi_{j}\in\Gamma}{j\neq
i}}\Diamond(\varphi_{j}\wedge x)\big{)},$

where $x$ does not appear free in any $\varphi_{i}\in\Gamma$.
We can then define the tangle logic $\mathcal{L}_{{}^{\infty}}$ whose language
is defined by the syntax:

$\varphi::=\top\,|\,p\,|\,\neg\varphi\,|\,\varphi\wedge\varphi\,|\,\varphi\vee\varphi\,|\,\Diamond\varphi\,|\,\Box\varphi\,|\,{}^{\infty}\Gamma,$

for $\Gamma\subseteq_{fin}\mathcal{L}_{{}^{\infty}}$.

######  Definition 7.

A cluster $C$ of a model $\mathcal{M}=\langle M,\sqsubset,\|\cdot\|\rangle$ is
a subset of $M$ such that $\forall u,v\in C\,u\sqsubseteq v$. A cluster of $w$
in $M$ is the set $C_{w}=\bigcup\\{C:C\text{ is a cluster of M and }w\in
C\\}$.
Given $A,B\subseteq M$, we write:

  * •

$A\prec B$ iff $\forall v\in B\,\exists u\in A\,u\sqsubset v\not\sqsubset u$

  * •

$A\preceq B$ iff $\forall v\in B\,\exists u\in A\,u\sqsubseteq v$.

In the sequel, $A,B$ will usually be nonempty clusters, in that case, the
above definitions will be equivalent to $\forall u\in A\,\forall v\in
B\,u\sqsubset v\not\sqsubset u$ and similarly for $\preceq$. In the case when
say $A=\\{w\\}$, we will write $w\sqsubset B$ and similarly for $B=\\{w\\}$.
Given $P\subseteq\mathbb{P}$ and clusters $C$and $C^{\prime}$ from models
$\mathcal{M}=\langle M,\sqsubset_{\mathcal{M}},\|\cdot\|_{\mathcal{M}}\rangle$
and $\mathcal{N}=\langle
N,\sqsubset_{\mathcal{N}},\|\cdot\|_{\mathcal{N}}\rangle$ respectively, we
write $C\subsetpluseq_{P}C^{\prime}$ to mean that there is some
$C^{\prime\prime}\subseteq C^{\prime\prime\prime}$ such that
$C^{\prime}\rightleftharpoons_{P}C^{\prime\prime}$. Similarly $C\subsetplus
C^{\prime}$ is defined for when additionally
$C\not\rightleftharpoons_{P}C^{\prime}$. As with the bisimilarity notation,
the $P$ subscript is omitted in the sequel.

######  Lemma 1.

Given multiset $\Gamma$ and a finite pointed model $(M,w)$, then
$w\vDash_{M}{}^{\infty}\Gamma$ iff there is a cluster $C$ of $M$ such that
$w\sqsubseteq C$ and a map $\varphi_{\cdot}\colon C\to\Gamma$ such that
$w\in\|\varphi_{w}\|$ and whenever $\varphi\in\Gamma$ is such that
$\varphi\neq\varphi_{w}$ (possibly because the latter is undefined), then
there is $v\in C$ such that $w\sqsubset v\in C$.

######  Example 2.

Recall the model of Example 1, consisting of an irreflexive cluster
$\\{0,1\\}$ with $\|e\|=\\{0\\}$, $\|o\|=\\{1\\}$, $\|p\|=\\{1\\}$, and
$\|i\|=\\{0,1\\}$. We then have that ${}^{\infty}\\{e,o\\}=\\{0,1\\}$, since
each point is either even and has an accessible point that is odd, or vice-
versa. On the other hand, ${}^{\infty}\\{o,p\\}=\varnothing$, since we cannot
assign any atom $\varphi_{1}\in\\{o,p\\}$ to $1$ in such a way that $1$
satisfies $\diamonddot a\wedge\Diamond a^{\prime}$, where $a^{\prime}$ is the
complementary atom to $a$. Thus it is not enough for each element of $\Gamma$
to be satisfied in a cluster in order to make ${}^{\infty}\Gamma$ true:
instead, each point $w$ must have an accessible world satisfying all but
possibly one element $\varphi_{w}$ of $\Gamma$, in which case it must also
satisfy $\varphi_{w}$.

##  3 The finality property

The property of finality will play a key role in allowing us to characterize
the structure of the valuation of $\mathcal{L}_{\mu}$ formulae in a given
model. In the case of finite wK4 frames, we will show in section 4 that it is
a particularly well behaving property. This notion can be traced back to
[Fin74c].

######  Definition 8 ($\Sigma$-final).

Given a model $M$ and a set of formulas $\Sigma$, a world $w\in M$ is
$\Sigma$-final if there is some formula $\varphi\in\Sigma$ such that
$w\vDash_{M}\varphi$ and if $w\sqsubset u$ and $u\vDash_{M}\varphi$, then
$u\sqsubset w$.
A set $A\subseteq M$ will be called $\Sigma$-final iff every $w\in A$ is
$\Sigma$-final. The $\Sigma$-final part of $M$ is the largest $\Sigma$-final
subset of $M$ and we denote by $M^{\Sigma}$. A rooted model $(M,w)$ will be
called $\Sigma$-semifinal if $M\setminus C_{w}$ is $\Sigma$-final.
Given a set of formulas $\Sigma$, models $M,N$ and worlds $u\in M$, $v\in N$,
we write $M,u\equiv_{\Sigma}N,v$ to mean $\forall\varphi\in\Sigma$
$u\vDash_{M}\varphi\Leftrightarrow v\vDash_{N}\varphi$. In case $M=N$, we will
abbreviate this by $u\equiv_{\Sigma}v$

######  Definition 9.

Given a model $M$, a set of formulas $\Sigma$ and a set $A\subseteq M$ we
define the $\Sigma$-depth of $A$ in $M$ as

$\displaystyle
dpt_{\Sigma}^{M}(A)=\sup\big{(}\big{\\{}dpt_{\Sigma}^{M}(B)+1:A\prec B\text{
and }\emptyset\neq B\subseteq M^{\Sigma}\big{\\}}\cup\\{0\\}\big{)}.$

While the depth of $A$ in $M$ is defined as:

$\displaystyle dpt^{M}(A)=\sup\big{(}\big{\\{}dpt_{\Sigma}^{M}(B)+1:A\prec
B\text{ and }\emptyset\neq B\subseteq M\big{\\}}\cup\\{0\\}\big{)}.$

######  Definition 10.

Given a set of formulas $\Sigma\subseteq\mathcal{L}_{\mu}$, define

$\Sigma^{\nu}=\\{\sigma\in\Sigma:\sigma=\nu x.\varphi(x)\text{ or }\sigma=\mu
x.\varphi(x)\text{ for some }\varphi\\}.$

######  Definition 11.

We define the modified subformula operator
$sub^{*}:\mathcal{L}_{\mu}\to\mathcal{P}(\mathcal{L}_{\mu})$ recursively by

  * •

$sub^{*}(r)=\\{r\\}$ if $r=\top,p,x$;

  * •

$sub^{*}(\neg p)=\\{\neg p,p\\}$;

  * •

$sub^{*}(\varphi\ocircle\psi)=\\{\varphi\ocircle\psi\\}\cup
sub^{*}(\varphi)\cup sub^{*}(\psi)$ where $\ocircle=\wedge\text{ or }\vee$ and
$\varphi\ocircle\psi\neq\diamonddot\sigma\text{ or }\boxdot\sigma$ for some
$\sigma$;

  * •

$sub^{*}(\ocircle\psi)=\\{\psi\\}\cup sub^{*}(\psi)$ where
$\ocircle=\Diamond,\Box,\diamonddot$ or ;

  * •

$sub^{*}(\nu x.\varphi)=\\{\varphi(x_{\nu x.\varphi})\\}\cup
sub^{*}(\varphi(x_{\nu x.\varphi}))$ where $x_{\nu x.\varphi}$ is a fresh
propositional variable named after $\nu x.\varphi$;

  * •

$sub^{*}(\mu x.\varphi)=\\{\varphi(x_{\mu x.\varphi})\\}\cup
sub^{*}(\varphi(x_{\mu x.\varphi}))$ where $x_{\mu x.\varphi}$ is a fresh
propositional variable named after $\mu x.\varphi$.

Given a set of formulae $\Sigma$, we can define a partial order on
$sub^{*}[\Sigma]$ by $\varphi<_{sub^{*}}\psi$ iff $\varphi\in sub^{*}(\psi)$
and $\varphi\neq\psi$.

Observe that if $x_{\psi}$ is a free variable of $\varphi$, then
$\varphi<_{sub^{*}}\psi$.

######  Definition 12.

Given a set $\mathbb{X}$, some $Y\subseteq\mathbb{X}$ and a set $\mathcal{A}$
of mappings $a:\mathbb{X}\to\mathcal{P}(\mathbb{X})$, we define the closure of
$Y$ over $\mathbb{X}$ inductively as follows:

  * •

$Cl^{0}_{\mathcal{A}}(Y)=Y$;

  * •

$Cl^{\alpha+1}_{\mathcal{A}}(Y)=Cl^{\alpha}_{\mathcal{A}}(Y)\cup\\{\alpha(x):\alpha\in\mathcal{A}\
\&\,x\in Cl^{\alpha}_{\mathcal{A}}(Y)\\}$;

  * •

$Cl^{\lambda}_{\mathcal{A}}(Y)=\displaystyle\bigcup_{\alpha<\lambda}Cl^{\alpha}_{\mathcal{A}}(Y)$
for $\lambda\in Lim$.

$Cl_{\mathcal{A}}(Y)=Cl^{\alpha}_{\mathcal{A}}(Y)$ where $\alpha$ is any
ordinal such that
$Cl^{\alpha}_{\mathcal{A}}(Y)=Cl^{\alpha+1}_{\mathcal{A}}(Y)$.

For the remainder of the paper, unless stated otherwise, we will be working
with a set of formulae $\Sigma$ such that
$\Sigma=Cl_{\diamonddot,sub^{*},\neg}$. Observe that any such set will be
finite up to modal equivalence of formulae since in $\sf S4$ there are only
finitely many non equivalent modalities and since is an $\sf S4$ modality
[Chagrov1997ModalL].

##  4 Model pruning in accordance to finality

In this section we see that in the case of $\sf wK4$ frames, the value of a
$\mathcal{L}_{\mu}$ formula $\varphi$ in a finite rooted model $(M,w)$ can be
solely determined by restricting our field of view to just $M^{\Sigma}\cup w$
with $\Sigma=Cl_{\diamonddot,sub^{*},\neg}$.

######  Lemma 2.

Given a finite set of formulas $\Sigma$ closed under $sub^{*}$ and some
$\varphi\in\Sigma$, we let $\lfloor\varphi\rfloor$ denote the closed form of
$\varphi$; that is every instance of $x_{\psi}$ is substituted by $\psi$
recursively until there are no free variables left.
Then $\lfloor\varphi\rfloor\in\mathcal{L}_{\mu}$ for each $\varphi\in\Sigma$.

###### Proof.

Inductively on the inverse of $<_{sub^{*}}$.
Suppose $\varphi$ is such that there is no $\psi$ with
$\varphi<_{sub^{*}}\psi$, then it has no free variables of the form $x_{\psi}$
and so $\lfloor\varphi\rfloor=\varphi$.
Now given $\varphi$, assume by our induction hypothesis that
$\lfloor\psi\rfloor\in\mathcal{L}_{\mu}$ for all $\varphi<_{sub^{*}}\psi$.
Since for all $x_{\psi}$ in $\varphi$ it is the case that
$\varphi<_{sub^{*}}\psi$, then
$\lfloor\varphi\rfloor=\varphi[x_{\psi}/\lfloor\psi\rfloor]$ i.e. we
substitute each $x_{\psi}$ showing up in $\varphi$ with $\lfloor\psi\rfloor$.
∎

Observe that additionally $\neg\lfloor\varphi\rfloor$ is equivalent to
$\lfloor\neg\varphi\rfloor$ for all $\varphi\in\Sigma$. In the sequel, given a
model $M$ and a set of formulae $\Sigma$ closed under $sub^{*}$, we will read
$w\vDash_{M}\varphi$ to mean $w\vDash_{M}\lfloor\varphi\rfloor$. In
particular, this means that $w$ is final for $\varphi$ in $M$ iff it is final
for $\lfloor\varphi\rfloor$ in $M$.

######  Definition 13.

Given a finite rooted model $(M,w)$ and a set of formulas $\Sigma$, we will
write

$\displaystyle w\vDash_{M}\overline{\langle
n\rangle}\varphi:\Leftrightarrow\exists v\in M^{\Sigma}\,(v\sqsupseteq w\wedge
dpt_{\Sigma}(v)=n\wedge\,v\vDash_{M}\varphi).$

Since for a given cluster $C$ of $M$ and $u,v\in
C,\,u\vDash_{M}\overline{\langle n\rangle}\varphi\Leftrightarrow
v\vDash_{M}\overline{\langle n\rangle}\varphi$, we will occasionally make an
abuse of notation and write $C\vDash_{M}\overline{\langle n\rangle}\varphi$ to
mean $\exists u\in C\,u\vDash_{M}\overline{\langle n\rangle}\varphi$.

The formulas $\overline{\langle n\rangle}\varphi$ provide all the information
needed to evaluate truth on $C$:

######  Theorem 2.

Let $M,N$ be finite rooted models with root clusters $C$ and $C^{\prime}$
respectively. Assume that $dpt_{\Sigma}^{M}(w)=dpt_{\Sigma}^{N}(w)$ and
$\forall\varphi\in\Sigma$ $w\vDash_{M}\overline{\langle
n\rangle}\varphi\Leftrightarrow w\vDash_{N}\overline{\langle n\rangle}\varphi$
for all $n<dpt_{\Sigma}^{M}(w)$, and

  * •

if $C$ is $\Sigma$-final then $C^{\prime}=C$

  * •

if $C$ is not $\Sigma$-final then $C^{\prime}\subseteq C$

then $\forall v\in C^{\prime}\,\forall\varphi\in\Sigma\ v\vDash_{M}\varphi$
iff $v\vDash_{N}\varphi$.

###### Proof.

Let $\vec{X}=(X_{\psi})_{\psi\in\Sigma^{\nu}_{2}}$ and
$\vec{Y}=(Y_{\psi})_{\psi\in\Sigma^{\nu}_{2}}$ be tuples of sets such that
$X_{\psi}\subseteq M$, $Y_{\psi}\subseteq N$, $X_{\psi}\cap(M\setminus
C^{\prime})=\|\lfloor\psi\rfloor\|_{M}\setminus C^{\prime}$,
$Y_{\psi}\cap(N\setminus C^{\prime})=\|\lfloor\psi\rfloor\|_{N}\setminus
C^{\prime}$ and $X_{\psi}\cap
C^{\prime}=(Y_{\psi}\cup\|\psi(\vec{X})\|_{M})\cap C^{\prime}$.111Here more
formally, $\vec{X}$ only contains the $X_{\sigma}$ such that $x_{\sigma}$
occur as free in $\psi$. Observe that the $X_{\psi}$ are well defined. We show
this by induction on the inverse of $<_{sub^{*}}$ on the set $\Sigma^{\nu}$.
$\psi$ is such that there are no $\psi<_{sub^{*}}\sigma$, then
$X_{\psi}=\|\psi\|_{M}\cup Y_{\psi}$ and it is well defined. Suppose that
$\psi$ is such that $X_{\sigma}$ is well defined for all
$\psi<_{sub^{*}}\sigma$, then since the only occurrences of free variables
$x_{\sigma}$ in $\psi$ are for $\psi<_{sub^{*}}\sigma$, and so
$X_{\psi}=\|\psi[x_{\sigma}/X_{\sigma}]\|_{M}\cup Y_{\sigma}$ which is well
defined.

Claim:

For all $\psi\in\Sigma$ and $w\in C^{\prime}$, if $w\vDash_{N}\psi(\vec{Y})$
then $w\vDash_{M}\psi(\vec{X})$.

This is proven by induction on the structure of the form of formulas $\psi$
that have no occurrences of the $\neg$ symbol outside of the atomic cases. The
cases for the set variables, propositional variables and logical connectives
are immediate.
Case for $\varphi=\Diamond\sigma$:
If $w\vDash_{N}\varphi(\vec{Y})$, then $\exists u\in N\ w\sqsubset_{N}u$ such
that $u\vDash_{N}\sigma(\vec{Y})$. If $u\in C^{\prime}$, then by induction
hypothesis $u\vDash_{M}\sigma(\vec{X})$ and since $w\sqsubset_{M}u$, then
$w\vDash_{M}\varphi(\vec{X})$. If $u\not\in C^{\prime}$, then
$u\vDash_{N}\sigma(\vec{Y})$ iff $v\vDash_{N}\lfloor\sigma\rfloor$, so there
is $\Sigma$-final $u\sqsubset_{N}u^{\prime}$ such that
$u^{\prime}\vDash_{N}\lfloor\sigma\rfloor$ and so
$w\vDash_{N}\overline{\langle n\rangle}\lfloor\sigma\rfloor$ for some
$n<dpt_{\Sigma}^{N}(w)$. Thus $w\vDash_{M}\overline{\langle
n\rangle}\lfloor\sigma\rfloor\Rightarrow
w\vDash_{M}\lfloor\varphi\rfloor\Rightarrow w\vDash_{M}\varphi(\vec{X})$.
Case for $\varphi=\Box\sigma$:
If $w\vDash_{N}\varphi(\vec{Y})$ then –as with the $\Diamond$ case– by the
induction hypothesis, for all $w\sqsubset_{N}u$ with $u\in C^{\prime}$ as well
as for all $w\prec_{M}u$ $u\vDash_{M}\sigma(\vec{X})$. In particular, for all
$n<dpt_{\Sigma}^{M}(w)$ $w\not\vDash_{M}\overline{\langle
n\rangle}\neg\lfloor\sigma\rfloor$. In the case where $C\setminus
C^{\prime}\neq\emptyset$, we have that $C$ is not $\Sigma$-final in $M$, then
assume towards a contradiction that for some $u\in C\setminus C^{\prime}$
$u\not\vDash_{M}\sigma(\vec{X})$. Then by monotonicity we get that
$u\not\vDash_{M}\lfloor\sigma\rfloor$ i.e.
$u\vDash_{M}\neg\lfloor\sigma\rfloor$, then since $u$ is not $\Sigma$-final,
there is some $u\sqsubset_{M}u^{\prime}$ such that
$u^{\prime}\vDash_{M}\neg\lfloor\sigma\rfloor$, a contradiction since
$dpt_{\Sigma}^{M}(u^{\prime})<dpt_{\Sigma}^{M}(w)$. Thus in either case
$u\vDash_{M}\sigma(\vec{X})$ for all $w\sqsubset_{M}u$ and so
$w\vDash_{M}\varphi(\vec{X})$.
The cases for the and formulas are mutandis mutatis.
Case for $\varphi=\nu x.\sigma(x)$:
Let $Y_{\varphi}=\|\varphi(\vec{Y})\|_{N}$, then $\|\varphi(\vec{Y})\|_{N}\cap
C^{\prime}=\|\sigma(\vec{Y})\|_{N}\cap C^{\prime}=Y_{\varphi}\cap
C^{\prime}\subseteq X_{\varphi}$. We show that
$X_{\varphi}\subseteq\sigma(\vec{X})$. Let $u\in X_{\varphi}$

Case 1:

$u\in Y_{\varphi}\Leftrightarrow u\in\|\sigma(\vec{Y})\|_{N}\Rightarrow
u\in\|\sigma(\vec{X})\|_{M}$ by the induction hypothesis.

Case 2:

$u\in\|\varphi(\vec{X})\|_{M}=\|\sigma(\varphi(\vec{X}),\vec{X})\|_{M}\subseteq\|\sigma(\vec{X})\|_{M}$
by monotonicity.

Case for $\varphi=\mu x.\sigma(x)$:
Since $C^{\prime}$ is finite222or at least bisimilar to a finite cluster.,
$\|\varphi(\vec{Y})\|_{N}=\|\sigma^{m}(x,\vec{Y})\|_{N}$ for some $m$, where

$\sigma^{0}(x,\vec{Y}):=\|\lfloor\varphi\rfloor\|_{N}\setminus C^{\prime}$;

$\sigma^{n+1}(x,\vec{Y}):=\sigma(\sigma^{n}(x,\vec{Y}),\vec{Y})$.

We show inductively on $n$ that for all
$Y_{\varphi}=\|\sigma^{n}(x,\vec{Y})\|_{N}$ that $C^{\prime}\cap
Y_{\varphi}\subseteq\|\varphi(\vec{X})\|_{M}=X_{\varphi}$. This is trivially
true for $Y_{\varphi}=\|\lfloor\varphi\rfloor\|_{N}\setminus C^{\prime}$. For
the inductive step, suppose it holds for some
$Y_{\varphi}=\|\sigma^{n}(x,\vec{Y})\|_{N}$, then by the original induction
hypothesis, $\|\sigma^{n+1}(x,\vec{Y})\|_{N}\cap
C^{\prime}=\|\sigma(\vec{Y})\|_{N}\cap
C^{\prime}\subseteq\|\sigma(\vec{X})\|_{M}$ and so for
$Y_{\varphi}^{\prime}=\|\sigma^{n+1}(x,\vec{Y})\|_{N}$, we get
$X_{\varphi}^{\prime}=\|\varphi(\vec{X})\|_{M}$.
This proves the Claim. Now, by letting $Y_{\psi}=\|\lfloor\psi\rfloor\|_{N}$
for all $\psi\in\Sigma^{\nu}$, we get by a simple induction on the inverse of
$sub^{*}$ that $X_{\psi}=\|\lfloor\psi\rfloor\|_{M}$, and so combining this
with the claim we get:

$\forall\varphi\in\Sigma\ \|\lfloor\varphi\rfloor\|_{N}\cap
C^{\prime}\subseteq\|\lfloor\varphi\rfloor\|_{M}\cap C^{\prime}.$

Since $\Sigma$ is closed under negation, it is also the case that
$\|\lfloor\neg\varphi\rfloor\|_{N}\cap
C^{\prime}\subseteq\|\lfloor\neg\varphi\rfloor\|_{M}\cap C^{\prime}$, ie
$C^{\prime}\setminus\|\lfloor\varphi\rfloor\|_{N}\subseteq
C^{\prime}\setminus\|\lfloor\varphi\rfloor\|_{M}$ and so
$\|\lfloor\varphi\rfloor\|_{M}\cap
C^{\prime}\subseteq\|\lfloor\varphi\rfloor\|_{N}\cap C^{\prime}$, which proves
the theorem. ∎

As an immediate corrollary, we get:

######  Theorem 3.

Given a finite model $M$, a model $N$ with $M\supseteq N\supseteq M^{\Sigma}$
and any $w\in N$, then $M,w\equiv_{\Sigma}N,w$.

###### Proof.

By induction on the depth of the clusters of $N$. Clusters of depth $0$ are
necessarily $\Sigma$-final and so the claim holds trivially true. Assume that
the claim holds for all upwards closed submodels of $N$ of depth $m\leq n$,
then by the assumption, a cluster of depth $m\leq n$ is then $\Sigma$-final in
$M$ iff it is so in $N$, thus a cluster $C^{\prime}$ of $N$ of depth $n+1$
satisfies the same $\overline{\langle k\rangle}\varphi$ formulae in $N$ as
does its counterpart $C$ in $M$ for
$k<dpt_{\Sigma}^{M}(C)=dpt_{\Sigma}^{N}(C^{\prime})$. An application of
Theorem 2 concludes the proof. ∎

##  5 Structural evaluation

The strategy we will follow to obtain an equivalence is to describe the parts
of the world and the model that are relevant to Theorem 2. In particular we
will define formulae in $\mathcal{L}_{{}^{\infty}}$ equivalent to the
$\overline{\langle n\rangle}\varphi$ formulae, as well as a formula which
approximates the statement “$w$ is $\Sigma$-final".

An alternative approach could have been to instead use only Theorem 3 and
produce a formula that determines the $\Sigma$-final part of a given rooted
model. While this approach would have also worked, it would have resulted in a
super-exponential upper bound on the size of the induced formula (relative to
the size of its equivalent $\mathcal{L}_{\mu}$ formula $\varphi$).

######  Definition 14.

Given a finite model $M$ and a cluster $C$ with $M\cap C=\emptyset$, we denote
by $\left[\genfrac{}{}{0.0pt}{}{M}{C}\right]$ the model $N$ with domain $M\cup
C$, accessibility relation
$\sqsubset_{N}:={\sqsubset_{M}}\cup{\sqsubset_{C}}\cup{(C\times M)}$ and
$\|\cdot\|_{N}:=\|\cdot\|_{M}\cup\|\cdot\|_{C}$.

######  Definition 15.

Given a model $M$ say that $\langle C,\Theta\rangle$ is a semi-satisfaction
pair for $M$ if $\exists w\in M$ such that $C=C_{w}$ and
$\Theta=\\{\overline{\langle m\rangle}\psi:w\vDash_{M}\overline{\langle
m\rangle}\psi$ for $\psi\in\Sigma\wedge m<dpt_{\Sigma}(w)\\}$. A pair $\langle
C,\Theta\rangle$ is called a semi-satisfaction pair if it is a semi-
satisfaction pair for some finite pointed $\Sigma$-semifinal model. A
satisfaction pair for $M$ is a semi-satisfaction pair $\langle
C,\Theta\rangle$ such that $C$ is $\Sigma$-final in $M$.
Given a semi-satisfaction pair $\langle C,\Theta\rangle$ for some model $M$,
we will denote by333Due to Theorem 2, $\Theta^{C}$ is uniquely determined
irrespectively of the chosen model $M$ for which $\langle C,\Theta\rangle$ is
a semi-satisfaction pair.

$\displaystyle\Theta^{C}:=\\{\overline{\langle
m\rangle}\psi:C\vDash_{M}\overline{\langle m\rangle}\psi\text{ for
}\psi\in\Sigma\wedge m\leq dpt_{\Sigma}(C)\\}.$

We extend the definition of $dpt_{\Sigma}$ by saying
$dpt_{\Sigma}(\Theta)=sup\\{n:\overline{\langle n\rangle}\varphi\in\Theta$ for
some $\varphi\in\Sigma\\}$. Let $Sat_{n}$ be the set of satisfaction pairs
$\langle C,\Theta\rangle$ such that $dpt_{\Sigma}(\Theta)=n$ and let
$Sat^{0}_{n},\,Sat^{1}_{n}$ be the first and second projections of $Sat_{n}$
respectively. Similarly, $Sat^{*}_{n},Sat^{*0}_{n},Sat^{*1}_{n}$ are the
corresponding sets for semi-satisfaction pairs. Define
$\vartriangleleft_{n}\,\subseteq Sat_{n}$ by $\langle
C^{\prime},\Theta^{\prime}\rangle\vartriangleleft_{n}\langle C,\Theta\rangle$
iff $C^{\prime}\subsetplus C$ and $\Theta^{\prime}=\Theta$. Let
$\trianglelefteq_{n}$ be the reflexive closure of $\vartriangleleft_{n}$. We
will identify $\vartriangleleft$ and $\trianglelefteq$ to be the appropriate
$\vartriangleleft_{n}$ and $\trianglelefteq_{n}$ respectively.

######  Lemma 3.

For every $\Sigma$-final model $M$ of depth $n$ with a root cluster $C$, there
is some chain $\mathcal{C}=\\{\langle C_{i},\Theta_{i}\rangle\\}_{i\leq n}$
such that

  1. 1.

$C_{n}=C$

  2. 2.

$\langle C_{i},\Theta_{i}\rangle$ is a satisfaction pair for $M$ for each
$i\leq n$

  3. 3.

$C_{i+1}\prec C_{i}$ for each $i<n$

  4. 4.

For all $i<n$, if
$\left[\genfrac{}{}{0.0pt}{}{C_{i}}{C_{i+1}}\right]\rightleftharpoons C_{i}$
then $\Theta_{i+1}\neq\Theta_{i}^{C_{i}}$.

###### Proof.

We need to show that we can always choose a chain as above such that the
clause 4 above holds. Towards a contradiction, let $M$ be a $\Sigma$-final
model with a root cluster $C$ of depth $n+1$ that belongs to a satisfaction
pair $\langle C,\Theta\rangle$ for $M$ and such that for every cluster
satisfaction pair $\langle C^{\prime},\Theta^{\prime}\rangle$ of depth $n$,
then $\left[\genfrac{}{}{0.0pt}{}{C^{\prime}}{C}\right]\rightleftharpoons
C^{\prime}$ and $\Theta=\Theta^{\prime C^{\prime}}$. Then by Theorem 2
$\left[\genfrac{}{}{0.0pt}{}{C^{\prime}{\uparrow^{*}_{M}}}{C}\right]$ and $M$
satisfy the same $\Sigma$ formulae on $C$. However
$\left[\genfrac{}{}{0.0pt}{}{C^{\prime}{\uparrow^{*}_{M}}}{C}\right]\rightleftharpoons
C^{\prime}{\uparrow^{*}_{M}}$ which implies that $C$ is not $\Sigma$-final in
$M$, a contradiction. ∎

######  Definition 16.

We will call a chain such that the above conditions hold for some
$\Sigma$-final model $M$, a witnessing chain of depth $n$ and denote them as
$\mathcal{C},\mathcal{C^{\prime}},\mathcal{C}_{i}$. Let $Chain_{n}$ be the set
of witnessing chains of depth $n$. Define $\vartriangleleft_{n}\subseteq
Chain_{n}\times Chain_{n}$ by
$\mathcal{C}\vartriangleleft_{n}\mathcal{C}^{\prime}$ iff the following hold:

  * •

$\langle C_{i},\Theta_{i}\rangle=\langle
C_{i}^{\prime},\Theta_{i}^{\prime}\rangle$ for $i<n$

  * •

$C_{n}\subsetplus C_{n}^{\prime}$

  * •

$\Theta_{n}=\Theta_{n}^{\prime}$

and let $\trianglelefteq_{n}$ be its reflexive closure. We will identify
$\vartriangleleft$ and $\trianglelefteq$ to be the appropriate
$\vartriangleleft_{n}$ and $\trianglelefteq_{n}$ respectively. Finally, given
$n$ and a formula $\varphi\in\Sigma$, we write

$\displaystyle supp(\overline{\langle
n\rangle}\varphi)=\big{\\{}\mathcal{C}\in Chain_{n}:\exists(M,w)\text{ finite
pointed }\Sigma\text{-final model where
}w\vDash_{M}\varphi\wedge\,C_{n}=C_{w}\,\wedge$
$\displaystyle\mathcal{C}\text{ is a witnessing chain of depth }n\text{ for
}M\big{\\}}.$

The definition of witnessing chains can be further expanded to semifinal
models, however the analogue of Lemma 3 for semi-witnessing chains will not
necessarily hold for any $\Sigma$-semifinal model as we cannot guarantee that
we can always find a chain in that case for which condition 4 will hold for
the root cluster.

######  Definition 17.

Given a $\Sigma$-semifinal model $M$ of depth $n$ with root cluster $C$, a
semi-witnessing chain for $M$ of depth $n$ (if it exists) is some chain
$\mathcal{C}=\\{\langle C_{i},\Theta_{i}\rangle\\}_{i\leq n}$ such that

  1. 1.

$C_{n}=C$

  2. 2.

$\langle C_{i},\Theta_{i}\rangle$ is a semi-satisfaction pair for $M$ for each
$i\leq n$

  3. 3.

$C_{i+1}\prec C_{i}$ for each $i<n$

  4. 4.

For all $i<n$, if
$\left[\genfrac{}{}{0.0pt}{}{C_{i}}{C_{i+1}}\right]\rightleftharpoons C_{i}$
then $\Theta_{i+1}\neq\Theta_{i}^{C_{i}}$.

We will denote by $Chain_{n}^{*}$ the set of all semi-witnessing chains of
depth $n$. For $M$ an arbitrary finite model, a (semi-)witnessing chain on $M$
of depth $n$ will be a (semi-)witnessing chain on the $\Sigma$-(semi)final
part of $w\uparrow^{*}_{M}$ for some $w\in M$. Finally given $\mathcal{C}\in
Chain^{*}_{n}$, let $dpt(\mathcal{C}):=n$ denote its depth.

$C_{n}$$C_{n-1}$$C_{n-2}$w$\langle n\rangle\phi$$\mathcal{C}$ Figure 1: On the
left, a witnessing chain. On the right, a witnessing chain ensures that the
$\Sigma$-depth of a point where $\langle n\rangle\phi$ holds is at least $n$.

We can now define formulas equivalent to the $``\overline{\langle
n\rangle}\varphi"$ in the language of $\mathcal{L}_{{}^{\infty}}$. This is
done inductively by having the formula $\alpha$ express the existence of a
witnessing chain $\mathcal{C}$ with a satisfaction pair $\langle
C,\Theta\rangle$ underneath it. Then the formulae $\beta$ and $\gamma$ ensure
that the extension $\mathcal{C}^{\frown}\langle C,\Theta\rangle$ is also a
witnessing chain (i.e. the pair $\langle C,\Theta\rangle$ is as high as it can
possibly be while remaining below $\mathcal{C}$). At this point it is
important to note that if we were to simply use satisfaction pairs, we would
run the risk of having the $\Sigma$-depth of worlds satisfying $\langle
n\rangle\phi$ being smaller than $n$; with witnessing chains, we ensure that
the depth does not collapse.

######  Definition 18.

Given $w\in M$ and a set of formulae $\Sigma$ let $\tau_{w}:=\bigwedge_{p\in
P(w)}p\wedge\bigwedge_{p\not\in P(w)}\neg p$, where $p\in\Sigma$. We will as a
convention assume the model as given and the set $\Sigma$ to be the one as
above, so will not include it in the notation.

  * •

$Ir(\mathcal{C}):=\langle C_{n},\Theta_{n}\rangle\trianglelefteq\langle
C_{n-1},\Theta_{n-1}^{C_{n-1}}\rangle\wedge\exists w\in C_{n}\forall u\in
C_{n}\cap w\uparrow\ P(w)\neq P(u)$ where $n=dpt(\mathcal{C})$

  * •

$\displaystyle A(\Theta):=\bigwedge_{\overline{\langle
m\rangle}\psi\in\Theta}\langle m\rangle\psi\wedge\bigwedge_{\overline{\langle
m\rangle}\psi\not\in\Theta}\neg\langle m\rangle\psi$

  * •

$\displaystyle\tau_{w}^{\mathcal{C}}:=\begin{cases}\tau_{w}\wedge
A(\Theta_{dpt(\mathcal{C})})\wedge\Diamond\big{(}\tau_{w}\wedge\delta(\mathcal{C}{\upharpoonright}dpt(\mathcal{C}))\big{)}&\text{
if }Ir(\mathcal{C})\\\ \tau_{w}\wedge
A(\Theta_{dpt(\mathcal{C})})\wedge\Diamond\delta(\mathcal{C}{\upharpoonright}dpt(\mathcal{C}))&\text{
otherwise }\end{cases}$

  * •

$\alpha(\mathcal{C}):={}^{\infty}\\{\tau_{w}^{\mathcal{C}}:w\in
C_{dpt(\mathcal{C})}\\}$

  * •

$\beta(\mathcal{C}):=\Box\big{(}\displaystyle\bigvee_{\mathcal{C}^{\prime}\vartriangleleft\mathcal{C}}\alpha(\mathcal{C}^{\prime})\to\alpha(\mathcal{C})\big{)}$

  * •

$\gamma(\mathcal{C}):=\displaystyle\neg\bigvee_{\mathcal{C}^{\prime}\not\trianglelefteq\mathcal{C}}\alpha(\mathcal{C}^{\prime})$

  * •

$\delta(\mathcal{C}):=\alpha(\mathcal{C})\wedge\beta(\mathcal{C})\wedge\gamma(\mathcal{C})$

  * •

$\langle n\rangle\varphi:=\displaystyle\bigvee_{\mathcal{C}\in
supp(\overline{\langle n\rangle}\varphi)}\diamonddot\delta(\mathcal{C})$

By following step by step the definitions above, we can prove the following
lemma:

######  Lemma 4.

Given a finite model $M$ a set of formulas $\Sigma$ and $w\in M$, then
$w\vDash_{M}\langle n\rangle\varphi\Leftrightarrow
w\vDash_{M}\overline{\langle n\rangle}\varphi$ for all $\varphi\in\Sigma$.

###### Proof.

By induction on $n$.
Assume that the statement holds true for all $m<n$, and let $\mathcal{C}\in
supp(\overline{\langle n\rangle}\varphi)$. We claim the following:

  1. 1.

$w\vDash_{M}\alpha(\mathcal{C})$ iff $\mathcal{C}{\upharpoonright}n$ is a
witnessing chain of depth $n$ for $M$ strictly above $w$ (i.e. $w\prec
C_{n-1}$) and there is some cluster $C=C_{u}$ for some $u\in M$ such that

    1. (a)

$w\preceq C\prec C_{n-1}$;

    2. (b)

$C_{n}\subsetpluseq C$;

    3. (c)

$C\vDash_{M}A(\Theta_{n})$.

  2. 2.

$w\vDash_{M}\diamonddot\delta(\mathcal{C})$ iff $\mathcal{C}$ is a witnessing
chain of depth $n$ for $M$ above $w$ (i.e. $w\preceq C_{n}$).

We prove the claims by the same induction on $n$. From the definition of
$\alpha(\mathcal{C})$ and by the I.H., it should be clear that
$C_{n}\subsetpluseq C$ and $C\vDash_{M}A(\Theta_{n})$ . By Claim 2,
$\mathcal{C}{\upharpoonright}n$ is a witnessing chain of depth $n$ for $M$
above the cluster $C$ of Claim 1 (i.e. $C\preceq C_{n-1}$). We show that it is
strictly above $C$.

  * •

If $C\not\subsetpluseq C_{n-1}$ then by Claim 2 $C\prec C_{n-1}$;

  * •

If $C\subsetpluseq C_{n-1}$ and $C_{n-1}\not\vDash_{M}A(\Theta_{n})$, then
$C\prec C_{n-1}$ as $C\vDash_{M}A(\Theta_{n})$;

  * •

If $C\subsetpluseq C_{n-1}$ and $C_{n-1}\vDash_{M}A(\Theta_{n})$, then let
$N=\left[\genfrac{}{}{0.0pt}{}{C_{n-1}{\uparrow^{*}_{M}}}{C_{n}}\right]$. Then
since $C_{n-1}{\uparrow^{*}_{M}}$ is a model admitting the witnessing chain
$\mathcal{C}{\upharpoonright}n$, then so is $N$ for $\mathcal{C}$. Then it
must be the case that $Ir(\mathcal{C})$ as otherwise $N\rightleftharpoons
C_{n-1}{\uparrow^{*}_{M}}$ which would contradict the $\Sigma$-finality of the
cluster $C_{n}$ in $N$. Then any $v$ witnessing $Ir(\mathcal{C})$ would also
be irreflexive in $C$ in $M$ and so $C\prec C_{n-1}$ from the definition of
$\tau^{\mathcal{C}}_{w}$.

This proves Claim 1. Now observe that in addition to that, if the cluster $C$
of Claim 1 has $dpt_{\Sigma}(C)=n$, then it is a $\Sigma$-final cluster. If
not, then by Theorem 3 the model $N=\big{(}M\setminus(C\setminus
C_{n})\big{)}$ has the cluster $C_{n}$ not be $\Sigma$-final which in turn
contradicts Theorem 2.

Now assume that the representative cluster $C$ for $C_{n}$ is the topmost
cluster in $M$ in which $\alpha(\mathcal{C})$ holds. To prove Claim 2, we
first show that assuming $\diamonddot\delta(\mathcal{C})$, there is no
$\Sigma$-final $C_{v}$ with $C_{n}\prec C_{v}\prec C_{n-1}$ and
$dpt_{\Sigma}(C_{v})=n$. Let
$\mathcal{C}^{\prime}=\mathcal{C}{\upharpoonright}n\cup\langle n,\langle
C_{v},\Theta\rangle\rangle$ for $\Theta$ such that $\mathcal{C}^{\prime}$ is a
witnessing chain of depth $n$ for $M$.

  * •

Assume $\mathcal{C}^{\prime}\vartriangleleft\mathcal{C}$, i.e.
$C_{v}\subsetplus C_{n}$ and $\Theta=\Theta_{n}$. By the clause of
$\beta(\mathcal{C})$, the clause of $\alpha(\mathcal{C})$ must hold above
$C_{v}$. But this contradicts the choice of $C$.

  * •

If $\mathcal{C}^{\prime}\not\trianglelefteq\mathcal{C}$, then we contradict
the clause of $\gamma(\mathcal{C})$.

For the reverse direction, let $\mathcal{C}$ a witnessing chain of depth $n$
for $M$ above $w$. We will show that for given $u\in
C_{n}\,u\vDash_{M}\delta(\mathcal{C})$. It is clear that $\alpha(\mathcal{C})$
holds and additionally since $dpt_{\Sigma}(C_{n})=n$ and $C_{n}$ is
$\Sigma$-final, there are no other eligible witnessing chains
$\mathcal{C}^{\prime}$ with $\mathcal{C}^{\prime}\vartriangleleft\mathcal{C}$
or $\mathcal{C}^{\prime}\trianglelefteq\mathcal{C}$ above $u$ in $M$ and so
$\beta(\mathcal{C})$ and $\gamma(\mathcal{C})$ hold as well.

Finally $w\vDash_{M}\overline{\langle n\rangle}\varphi$ iff there is some
witnessing chain $\mathcal{C}\in supp(\overline{\langle n\rangle}\varphi)$
above $w$ iff $w\vDash_{M}\langle n\rangle\varphi$. ∎

######  Corollary 1.

Given a finite model $M$, some $w\in M$ and $C\in Chain_{n}^{*}\setminus
Chain_{n}$, then $w\vDash_{M}\alpha(\mathcal{C})$ iff
$\mathcal{C}{\upharpoonright}n$ is a witnessing chain of depth $n$ for $M$
strictly above $w$ (i.e. $w\prec C_{n-1}$) and there is some cluster $C=C_{u}$
for some $u\in M$ such that

  1. (a)

$w\preceq C\prec C_{n-1}$

  2. (b)

$C_{n}\subsetpluseq C$

  3. (c)

$C\vDash_{M}A(\Theta_{n})$

###### Proof.

The proof is as in the lemma above. ∎

Since a completely accurate finality definition is impossible to obtain in
$\mathcal{L}_{\mu}$, we will instead approximate one with the following.

######  Definition 19.

We define formulas

$\displaystyle split(n):=$
$\displaystyle\displaystyle\bigvee_{\mathcal{C},\mathcal{C}^{\prime}\in
Chain_{n}\text{ with }\langle C_{n},\Theta_{n}\rangle\neq\langle
C_{n}^{\prime},\Theta_{n}^{\prime}\rangle}\big{(}\diamonddot\delta(\mathcal{C})\wedge\diamonddot\delta(\mathcal{C}^{\prime})\big{)}$
$\displaystyle\vee\bigvee_{\mathcal{C}_{0}\in Chain_{n+1}^{*}\setminus
Chain_{n+1}}\alpha(\mathcal{C}_{0}).$

At this point, we just need to define the characteristic formula of $\varphi$.
To do so, we first define $eval(\varphi,n)$ to be the set of all triples
$\langle w,\mathcal{C},\Theta\rangle$ for which there exists a rooted
$\Sigma$-semifinal model $(M,w)$ such that

  1. 1.

$w\in M$

  2. 2.

$w\vDash_{M}\varphi$

  3. 3.

$\Theta=\\{\overline{\langle m\rangle}\psi:w\vDash_{M}\overline{\langle
m\rangle}\psi\text{ for }\psi\in\Sigma\wedge m<dpt_{\Sigma}(w)\\}$

  4. 4.

If $w\not\in M^{\Sigma}$ then $dpt_{\Sigma}(\Theta)=n$ and
$\mathcal{C}=\emptyset$

  5. 5.

If $w\in M^{\Sigma}$ then $dpt_{\Sigma}(\Theta)=n-1$ and $\mathcal{C}$ is a
witnessing chain for $M$ of depth $n$ with $\langle
C_{w},\Theta\rangle=\langle C_{n},\Theta_{n}\rangle$.

And let $eval(\varphi):=\displaystyle\bigcup_{n}eval(\varphi,n)$. Now let

$\displaystyle\displaystyle\chi_{0}(w,\mathcal{C},\Theta,n):=\begin{cases}\langle
n\rangle\top\wedge\neg\langle n+1\rangle\top\wedge\\\ \neg
split(n)\wedge\tau_{w}\wedge\diamonddot\delta(\mathcal{C})&\text{if
}\mathcal{C}\neq\emptyset\\\ \langle n\rangle\top\wedge\neg\langle
n+1\rangle\top\wedge\\\ split(n)\wedge\tau_{w}\wedge A(\Theta)&\text{if
}\mathcal{C}=\emptyset\end{cases}.$

Finally, the characteristic formula $\chi(\varphi)$ of $\varphi$ is defined
as:

$\displaystyle\chi(\varphi):=\bigvee_{\langle w,\mathcal{C},\Theta\rangle\in
eval(\varphi)}\chi_{0}\big{(}w,\mathcal{C},\Theta,dpt_{\Sigma}(\Theta)\big{)}.$

######  Lemma 5.

Given a rooted model $(M,w)$ such that $w\vDash_{M}\langle
n\rangle\top\wedge\neg\langle n+1\rangle\top$ then

  1. 1.

If $w\vDash_{M}split(n)$ then $w$ is not $\Sigma$-final in $M$.

  2. 2.

If $w\not\vDash_{M}split(n)$ then for every cluster $C\in M^{\Sigma}$ of depth
$n$ and for $N=w\cup C{\uparrow^{*}_{M}}$, the following hold:

     * •

$\forall\varphi\in\Sigma\ w\vDash_{M}\varphi\Leftrightarrow
w\vDash_{N}\varphi$

     * •

$N\rightleftharpoons C{\uparrow^{*}_{M}}$.

###### Proof.

Claim 1 is derived from the claims proved in Lemma 4 as $split(n)$ holds if
one of the following holds:

  1. (a)

There are two satisfaction pairs in $M$: $\langle C,\Theta\rangle\neq\langle
C^{\prime},\Theta^{\prime}\rangle\in Sat_{n}$ with $C,C^{\prime}$ being above
$w$ and hence $dpt_{\Sigma}(w)>n$.

  2. (b)

There is a semi-witnessing chain $\mathcal{C^{\prime}}$ of $M$ of depth $n+1$
above $w$ and hence $dpt_{\Sigma}(w)\geq n+1$.

For Claim 2 assume that $w$ is not final. Since $w\not\vDash_{M}split(n)$,
none of the above two cases hold, therefore

  * •

Every satisfaction pair of depth $n$ in $M$ is the same.

  * •

For every semi-satisfaction pair $\langle C,\Theta\rangle$ of $M$ above $w$
with $dpt_{\Sigma}(C)=n+1$ and every satisfaction pair $\langle
C^{\prime},\Theta^{\prime}\rangle$ of $M$ with $dpt_{\Sigma}(C^{\prime})=n$
and $C^{\prime}\succ C$, it holds that
$\left[\genfrac{}{}{0.0pt}{}{C^{\prime}}{C}\right]\rightleftharpoons
C^{\prime}$ and $\Theta=\Theta^{\prime C^{\prime}}$.

∎

######  Theorem 4.

Given a formula $\varphi$ and a rooted model $(M,w)$, then
$w\vDash_{M}\varphi\Leftrightarrow w\vDash_{M}\chi(\varphi)$.

###### Proof.

Let $n=dpt_{\Sigma}^{M}(w)$ and $\Theta=\\{\overline{\langle
m\rangle}\psi:w\vDash_{M}\overline{\langle m\rangle}\psi\text{ for
}\psi\in\Sigma\wedge m<dpt_{\Sigma}(w)\\}$. Assume first that
$w\vDash_{M}\varphi$ and consider the following cases.

  1. 1.

Suppose that $w\in M^{\Sigma}$, then $w\vDash_{M}\neg split(n)$ and $w\
\vDash_{M}\langle n\rangle\top\wedge\neg\langle n+1\rangle\top$. Since
$w\vDash_{M}\varphi$ then by the definition of $eval$ and the fact that $w\in
M^{\Sigma}$, we have $\langle w,\mathcal{C},\Theta\rangle\in eval(\varphi,n)$
for some witnessing chain for $M$ rooted at $w$ and so
$w\vDash_{M}\chi_{0}(w,\mathcal{C},\Theta,n)$.

  2. 2.

Assume now that $w\not\in M^{\Sigma}$, then $w\vDash_{M}\langle
n-1\rangle\top\wedge\neg\langle n\rangle\top$ and

    1. (a)

If $w\vDash_{M}split(n-1)$ then $(M,w)$ is a witness of $\langle
w,\emptyset,\Theta\rangle\in eval(\varphi,n)$ and so
$w\vDash_{M}\chi_{0}(w,\emptyset,\Theta,n-1)$.

    2. (b)

If $w\not\vDash_{M}split(n-1)$, let $C$ a $\Sigma$-final cluster with
$dpt_{\Sigma}(C)=n-1$. By Lemma 5, $w$ satisfies the same $\Sigma$-formulae as
some $u\in C$ and since
$u\vDash_{M}\tau_{w}\wedge\diamonddot\delta(\mathcal{C})$ for some
$\mathcal{C}$, then so does $w$.

Assume now that $w\vDash_{M}\chi(\varphi)$ and consider the same cases as
before:

  1. 1.

If $w\in M^{\Sigma}$, then $w\vDash_{M}\chi_{0}(w,\mathcal{C},\Theta,n)$ for
some witnessing chain $C$ and so $C_{w}=C_{n}$ and by Theorem 2
$w\vDash_{M}\varphi$.

  2. 2.

If $w\not\in M^{\Sigma}$, then $w\vDash_{M}\chi_{0}(w,\mathcal{C},\Theta,n-1)$
and

    1. (a)

If $w\vDash_{M}split(n-1)$ then since $\langle w,\emptyset,\Theta\rangle\in
eval(\varphi,n)$, by Theorem 2 $w\vDash_{M}\varphi$.

    2. (b)

If $w\not\vDash_{M}split(n-1)$, then since
$w\vDash\diamonddot\delta(\mathcal{C})$, there is a $\Sigma$-final cluster $C$
above $w$ that is the root of the witnessing chain $\mathcal{C}$ in $M$. By
Lemma 5 $w$ satisfies the same $\Sigma$-formulae as some $u\in C_{n-1}$, and
since $u\vDash\diamonddot\delta(\mathcal{C})$, then $w\vDash_{M}\varphi$.

∎

${}^{\infty}\Gamma$ can be expressed by a first order formula in all path-
finite wK4 frames. Where path-finite means that the ordering $\prec$ is
conversely well-founded. So we get a first order expressibility of
$\mathcal{L}_{\mu}$ in frames analogous to the ones in [DO].

######  Theorem 5.

$\mathcal{L}_{\mu}\equiv\mathcal{L}_{{}^{\infty}}$ over wK4 frames and so
$\mathcal{L}_{\mu}\subset{\sf FOL}{/}{\rightleftharpoons}$ over finite and
path-finite wK4 frames.

###### Proof.

Immediate from the above remark, the finite model property of
$\mathcal{L}_{\mu}$ over wK4 frames and from Theorem 4. ∎

In addition to that, we get that formulas of $\mathcal{L}_{\mu}$ are
equivalent to formulae without nested fixed points i.e. formulae that are not
equal to formulae of the form $\rho_{0}x.\phi(\rho_{1}y.\psi)$ with $x$
occurring in $\psi$ and $\rho_{i}$ being $\nu$ or $\mu$. Hence our work has as
a corollary the following result by [alternation]:

######  Theorem 6.

The $\mu$-calculus collapses to its alternation-free fragment over wK4 frames.

In view of [Baltag2021TheTM], these results lift to topological spaces, with
the caveat that $\sf FOL$ does not make sense in this setting.

######  Theorem 7.

$\mathcal{L}_{\mu}\equiv\mathcal{L}_{{}^{\infty}}$ over the class of all
topological spaces.

Since our methods at proving the equivalence of the two calculi over wK4
frames involved constructing an equivalent formula, we can the derive a
succinctness upper bound of formulae between $\mathcal{L}_{\mu}$ and
$\mathcal{L}_{{}^{\infty}}$. Though the upper bound we calculate is rather
crude, it is reasonably close to the known lower bound, which is exponential
[Iliev].

######  Theorem 8.

Let $\varphi\in\mathcal{L}_{\mu}$ and $|\varphi|=n$ be the total number of
symbols that appear in $\varphi$. Then $|\chi(\varphi)|\leq
2^{(14n+1)2^{14n+6}}$. Hence for every formula $\varphi$ of
$\mathcal{L}_{\mu}$ there is a formula of $\mathcal{L}_{{}^{\infty}}$ of size
bounded by a double exponential function on $|\varphi|$ and equivalent to
$\varphi$ over the class of weakly transitive frames as well as the class of
all topological spaces.

###### Proof.

The number of propositional constants that show up in $\varphi$ is
$|P|\leq\lceil\dfrac{n}{2}\rceil\leq n$; and by [Chagrov1997ModalL] we know
that the induced $\Sigma=Cl_{\diamonddot,sub^{*},\neg}(\varphi)$ has
cardinality $|\Sigma|\leq 14n=:m$. Then the number of different propositional
valuations a given world can have is $2^{|P|}\leq 2^{n}$ and thus the number
of different non-bisimilar clusters of $\sf wK4$ frames is $|Sat^{0}_{0}|\leq
3^{2^{|P|}}\leq 3^{2^{n}}$. The number of sets of the form
$\\{\overline{\langle i\rangle}\psi:\psi\in\Sigma\wedge
i<dpt_{\Sigma}(w)\wedge w\vDash_{M}\overline{\langle i\rangle}\psi\\}$ for
$\Sigma$-semifinal rooted finite models $(M,w)$ of depth $k$ is
$|Sat^{*1}_{k}|\leq 2^{m}(k+1)$ and so
$|Sat_{k}|\leq|Sat^{*}_{k}|\leq|Sat^{*0}_{k}||Sat^{*1}_{k}|\leq|Sat^{0}_{0}||Sat^{*1}_{k}|\leq
3^{2^{n}}2^{m}(k+1)$. The number of (semi-)witnessing chains of depth $k$ is
then $|Chain_{k}|\leq|Chain^{*}_{k}|\leq\prod_{0\leq i\leq k}|Sat^{*}_{i}|\leq
3^{(k+1)2^{n}}2^{m(k+1)}(k+1)^{k+1}\leq 2^{2^{m+2}}$.

For the formulas used to define the modal $\langle k\rangle\psi$’s, we will
for the interest of clarity use a slightly modified notation when calculating
the upper bound of the number of symbols showing up. Define $|\langle
k\rangle|:=sup\\{|\langle k\rangle\psi|:\psi\in\Sigma\\}$ and similarly
$|\alpha(k)|:=sup\\{|\alpha(\mathcal{C})|:\mathcal{C}\in Chain^{*}_{k}\\}$ and
$|\delta(k)|:=sup\\{|\delta(\mathcal{C})|:\mathcal{C}\in Chain^{*}_{k}\\}$.
Then for given $k$, the definitions give

  * •

$|\langle k\rangle|\leq 4|Chain_{k}|\cdot|\delta(k)|\leq
2^{2^{m+2}+2}|\delta(k)|$

  * •

$|\alpha(k)|\leq 1+2^{n}\big{(}2^{n+3}+4+\sum_{i<k}(|\langle i\rangle|\cdot
3m)+|\delta(k-1)|\big{)}$

  * •

$\displaystyle\begin{aligned} &|\delta(k)|\leq
3|Chain^{*}_{k}|\cdot|\alpha(k)|\leq 3\cdot 2^{2^{m+2}}|\alpha(k)|\\\ &\leq
3\cdot 2^{2^{m+2}}\cdot
2^{n+1}\big{(}2^{n+3}+2^{2^{m+2}+2}\cdot\sum_{i<k}(|\delta(i)|\cdot
3m)+|\delta(k-1)|\big{)}\\\ &\leq 2^{2^{m+2}}\cdot
2^{n+7}\big{(}2^{2^{m+3}}\cdot(|\delta(k-1)|+1)\big{)}\\\ &\leq 2^{k\cdot
2^{m+4}}\end{aligned}$

Then we can evaluate an upper bound of $|split(k)|\leq
6|Chain_{k+1}^{*}||\delta(k)|\leq 6\cdot 2^{2^{m+1}}\cdot 2^{k\cdot
2^{m+4}}\leq 2^{(k+1)\cdot 2^{m+4}}$ and finally $|\chi(\varphi)|\leq
2^{n}\cdot|\bigcup_{k\leq m}Chain_{k}|\cdot|Sat^{*1}_{m}|\cdot(2|\langle
m+1\rangle|+2^{n+3}+|split(m)|+2|\delta(m)|)\leq 2^{n}\cdot(m+1)\cdot
2^{2^{m+2}}\cdot
2^{m}\cdot(m+1)\cdot(2^{2^{m+4}+2^{m+2}+3}+2^{n+3}+2^{(m+1)\cdot
2^{m+4}}+2^{m\cdot 2^{m+4}})\leq 2^{(m+1)2^{m+6}}$.

∎

##  6 Conclusion

We have shown that the topological $\mu$-calculus is equi-expressive to its
tangled fragment, provided it’s defined in a way that better captures its
intended behaviour on arbitrary topological spaces while retaining its
original value on metric spaces and other ‘nice’ topological spaces. Given the
much more transparent syntax of tangle logic, this suggests that the latter is
more suitable for applications in spatial KR than the full $\mu$-calclus.

In futurte work we will present our proof that the $\mu$-calculus is not as
epxressive as $\sf MSO$ over the class of finite, weakly transitive frames,
hence we do not obtain a modal characterization theorem in the sense of van
Benthem. This begs the question of whether the topological $\mu$-calculus, or
its tangled fragment, can be enriched in a natural way to obtain the full
expressive power of the bisimulation-invariang fragments of $\sf FOL$ or $\sf
MSO$. Perhaps something in the spirit of hybrid logics can bridge this gap,
but at this point the question remains a challenging open problem.

## References

  * [Baltag et al., 2021] Baltag, A., Bezhanishvili, N., and Fernández-Duque, D. (2021).  The topological mu-calculus: completeness and decidability.  2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13.
  * [Baltag et al., 2022] Baltag, A., Bezhanishvili, N., and Fernández-Duque, D. (2022).  The topology of surprise.  In Kern-Isberner, G., Lakemeyer, G., and Meyer, T., editors, Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, KR 2022, Haifa, Israel. July 31 - August 5, 2022.
  * [Chagrov and Zakharyaschev, 1997] Chagrov, A. V. and Zakharyaschev, M. (1997).  Modal logic.  In Oxford logic guides.
  * [Dawar and Otto, 2009] Dawar, A. and Otto, M. (2009).  Modal characterisation theorems over special classes of frames.  Annals of Pure and Applied Logic, 161(1):1–42.
  * [Esakia, 2001] Esakia, L. (2001).  Weak transitivity—a restitution.  Logical investigations, 8:244–245.
  * [Fernández-Duque and Iliev, 2018] Fernández-Duque, D. and Iliev, P. (2018).  Succinctness in subsystems of the spatial $\mu$-calculus.  FLAP, 5(4):827–874.
  * [Fine, 1974] Fine, K. (1974).  Logics containing $K4$. I.  J. Symbolic Logic, 39:31–42.
  * [Goldblatt and Hodkinson, 2017] Goldblatt, R. and Hodkinson, I. (2017).  Spatial logic of tangled closure operators and modal mu-calculus.  Ann. Pure Appl. Log., 168(5):1032–1090.
  * [Gougeon, 2022] Gougeon, Q. (2022).  The expressive power of derivational modal logic.  Master’s thesis, ILLC, University of Amsterdam.
  * [Janin and Walukiewicz, 1996] Janin, D. and Walukiewicz, I. (1996).  On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic.  In Montanari, U. and Sassone, V., editors, CONCUR ’96: Concurrency Theory, pages 263–277, Berlin, Heidelberg. Springer Berlin Heidelberg.
  * [Lucero-Bryan, 2013] Lucero-Bryan, J. G. (2013).  The d-logic of the real line.  J. Log. Comput., 23(1):121–156.
  * [van Benthem, 1976] van Benthem, J. (1976).  Modal Correspondence Theory.  PhD thesis, University of Amsterdam.
  * [Pacheco and Tanaka, 2022] Pacheco, L. and Tanaka, K. (2022).  The alternation hierarchy of the-calculus over weakly transitive frames.  In International Workshop on Logic, Language, Information, and Computation, pages 207–220. Springer.