🌕

# Dynamic Cantor Derivative Logic

David Fernández-Duque  Yoàv Montacute

###### Abstract

Topological semantics for modal logic based on the Cantor derivative operator
gives rise to derivative logics, also referred to as $d$-logics. Unlike logics
based on the topological closure operator, $d$-logics have not previously been
studied in the framework of dynamical systems, which are pairs $(X,f)$
consisting of a topological space $X$ equipped with a continuous function
$f\colon X\to X$.

We introduce the logics $\bf{wK4C}$, $\bf{K4C}$ and $\bf{GLC}$ and show that
they all have the finite Kripke model property and are sound and complete with
respect to the $d$-semantics in this dynamical setting. In particular, we
prove that $\bf{wK4C}$ is the $d$-logic of all dynamic topological systems,
$\bf{K4C}$ is the $d$-logic of all $T_{D}$ dynamic topological systems, and
$\bf{GLC}$ is the $d$-logic of all dynamic topological systems based on a
scattered space. We also prove a general result for the case where $f$ is a
homeomorphism, which in particular yields soundness and completeness for the
corresponding systems $\bf{wK4H}$, $\bf{K4H}$ and $\bf{GLH}$.

The main contribution of this work is the foundation of a general proof method
for finite model property and completeness of dynamic topological $d$-logics.
Furthermore, our result for $\bf{GLC}$ constitutes the first step towards a
proof of completeness for the trimodal topo-temporal language with respect to
a finite axiomatisation – something known to be impossible over the class of
all spaces.

##  1 Introduction

Dynamic (topological) systems are mathematical models of processes that may be
iterated indefinitely. Formally, they are defined as pairs
$\langle\mathfrak{X},f\rangle$ consisting of a topological space
$\mathfrak{X}=\langle X,\tau\rangle$ and a continuous function $f\colon X\to
X$; the intuition is that points in the space $\mathfrak{X}$ ‘move’ along
their orbit, $x,f(x),f^{2}(x),\ldots$ which usually simulates changes in time.
Dynamic topological logic ($\bf DTL$) combines modal logic and its topological
semantics with linear temporal logic (see Pnueli [ltl]) in order to reason
about dynamical systems in a decidable framework.

Due to their rather broad definition, dynamical systems are routinely used in
many pure and applied sciences, including computer science. To cite some
recent examples, in data-driven dynamical systems, data-related problems may
be solved through data-oriented research in dynamical systems as suggested by
Brunton and Kutz [brunton2019data]. Weinan [weinan2017proposal] proposes a
dynamic theoretic approach to machine learning where dynamical systems are
used to model nonlinear functions employed in machine learning. Lin and
Antsaklis’s [hybrid] hybrid dynamical systems have been at the centre of
research in control theory, artificial intelligence and computer-aided
verification. Mortveit and Reidys’s [sequential] sequential dynamical systems
generalise aspects of systems such as cellular automata, and also provide a
framework through which we can study dynamical processes in graphs. Another
example of dynamical systems and computer science can be found in the form of
linear dynamical systems, i.e. systems with dynamics given by a linear
transformation. Examples of such systems in computer science include Markov
chains, linear recurrence sequences and linear differential equations.
Moreover, there are known strong connections between dynamical systems and
algorithms. This may be found for example in the work of Hanrot, Pujol and
Stehlé [hanrot2011analyzing], and in the work of Chu [chu2008linear].

Such applications raise a need for effective formal reasoning about
topological dynamics. Here, we may take a cue from modal logic and its
topological semantics. The study of the latter dates back to McKinsey and
Tarski [Tarski], who proved that the modal logic $\bf S4$ is complete for a
wide class of spaces, including the real line. Artemov, Davoren and Nerode
[artemov] extended $\bf S4$ with a ‘next’ operator in the spirit of $\bf LTL$,
producing the logic $\mathbb{S4C}$. They proved that this logic is sound and
complete with respect to the class of all dynamic topological systems. The
system $\mathbb{S4C}$ was enriched with the ‘henceforth’ tense by Kremer and
Mints, who dubbed the new logic dynamic topological logic ($\mathbb{DTL}$).
Later, Konev et al. [konev] showed that $\mathbb{DTL}$ is undecidable, and
Fernández-Duque [david] showed that it is not finitely axiomatisable on the
class of all dynamic topological spaces.

The aforementioned work on dynamic topological logic interprets the modal
operator $\lozenge$ as a closure operator. However, McKinsey and Tarski had
already contemplated semantics that are instead based on the Cantor derivative
[Tarski]: the Cantor derivative of a set $A$, usually denoted by $d(A)$, is
the set of points $x$ such that $x$ is in the closure of $A\setminus\\{x\\}$
(see Section 2). This interpretation is often called $d$-semantics and the
resulting logics are called $d$-logics. These logics were first studied in
detail by Esakia, who showed that the $d$-logic $\mathbb{wK4}$ is sound and
complete with respect to the class of all topological spaces [Esakia2]. It is
well-known that semantics based on the Cantor derivative are more expressive
than semantics based on the topological closure. For example, consider the
property of a space $\mathfrak{X}$ being dense-in-itself, meaning that
$\mathfrak{X}$ has no isolated points (see Section 3.2). The property of being
dense-in-itself cannot be expressed in terms of the closure operator, but it
can be expressed in topological $d$-semantics by the formula $\lozenge\top$.

Logics based on the Cantor derivative appear to be a natural choice for
reasoning about dynamical systems. However, there are no established results
of completeness for such logics in the setting of dynamical systems, i.e. when
a topological space is equipped with a continuous function. Our goal is to
prove the finite Kripke model property, completeness and decidability of
logics with the Cantor derivative operator and the ‘next’ operator $\bc$ over
some prominent classes of dynamical systems: namely, those based on arbitrary
spaces, on $T_{D}$ spaces (spaces validating the $4$ axiom $\square
p\to\square\square p$) and on scattered spaces (see Section 3.2 for
definitions). The reason for considering scattered spaces is to circumvent the
lack of finite axiomatisability of $\mathbb{DTL}$ by restricting to a suitable
subclass of all dynamical systems. In the study of dynamical systems and
topological modal logic, one often works with dense-in-themselves spaces. This
is a sensible consideration when modelling physical spaces, as Euclidean
spaces are dense-in-themselves. However, as we will see in Section 3.2, some
technical issues that arise when studying $\mathbb{DTL}$ over the class of all
spaces disappear when restricting our attention to scattered spaces, which in
contrast have many isolated points. Further, we consider dynamical systems
where $f$ is a homeomorphism, i.e. where $f^{-1}$ is also a continuous
function. Such dynamical systems are called invertible.

The basic dynamic $d$-logic we consider is $\mathbb{wK4C}$, which consists of
$\mathbb{wK4}$ and the temporal axioms for the continuous function $f$. In
addition, we investigate two extensions of $\mathbb{wK4C}$: $\mathbb{K4C}$ and
$\mathbb{GLC}$. As we will see, $\mathbb{K4C}$ is the $d$-logic of all $T_{D}$
dynamical systems, and $\mathbb{GLC}$ is the $d$-logic of all dynamical
systems based on a scattered space. Unlike the generic logic of the trimodal
topo-temporal language $\mathcal{L}^{\circ*}_{\lozenge}$, we conjecture that a
complete finite axiomatisation for $\mathbb{GLC}$, extended with axioms for
the ‘henceforth’ operator, will not require changes to the trimodal language.
This logic is of special interest to us as it would allow for the first finite
axiomatisation and completeness results for a logic based on the trimodal
topo-temporal language.

#### Outline.

This paper is structured as follows: in Section 2 we give the required
definitions and notations necessary to understand the paper. In Section 3 we
provide some background on prior work on the topic of dynamic topological
logics. Moreover, we motivate our interest in $\mathbb{GLC}$, the most unusual
logic we work with.

In Section 4 we present the canonical model, and in Section 5 we construct a
‘finitary’ accessibility relation on it. Both are then used in Section 6 in
order to develop a proof technique that, given the right modifications, would
work for many $d$-logics above $\mathbb{wK4C}$. In particular, we use it to
prove the finite model property, soundness and completeness for the $d$-logics
$\mathbb{wK4C}$, $\mathbb{K4C}$ and $\mathbb{GLC}$, with respect to the
appropriate classes of Kripke models.

In Section 7 we prove topological $d$-completeness of $\mathbb{K4C}$,
$\mathbb{wK4C}$ and $\mathbb{GLC}$ with respect to the appropriate classes of
dynamical systems. In Section 8 we present logics for systems with
homeomorphisms and provide a general completeness result which, in particular,
applies to the $d$-logics $\mathbb{wK4H}$, $\mathbb{K4H}$ and $\mathbb{GLH}$.
Finally, in Section 9 we provide some concluding remarks.

##  2 Preliminaries

In this section we review some basic notions required for understanding this
paper. We work with the general setting of derivative spaces, in order to
unify the topological and Kripke semantics of our logics.

######  Definition 2.1 (topological space).

A topological space is a pair $\mathfrak{X}=\langle X,\tau\rangle$, where $X$
is a set and $\tau$ is a subset of $\wp(X)$ that satisfies the following
conditions:

  * •

$X,\varnothing\in\tau$;

  * •

if $U,V\in\tau$, then $U\cap V\in\tau$;

  * •

if $\mathcal{U}\subseteq\tau$, then $\bigcup\mathcal{U}\in\tau$.

The elements of $\tau$ are called open sets, and we say that $\tau$ forms a
topology on $X$. A complement of an open set is called a _closed_ set.

The main operation on topological spaces we are interested in is the Cantor
derivative.

######  Definition 2.2 (Cantor derivative).

Let $\mathfrak{X}=\langle X,\tau\rangle$ be a topological space. Given
$S\subseteq X$, the _Cantor derivative_ of $S$ is the set $d(S)$ of all limit
points of $S$, i.e. $x\in d(S)\iff\forall U\in\tau$ s.t. $x\in U,\;(U\cap
S)\backslash\\{x\\}\neq\varnothing$. We may write $d(S)$ or $dS$ indistinctly.

When working with more than one topological space, we will often denote the
Cantor derivative of the topological space $\langle X,\tau\rangle$ by
$d_{\tau}$. Given subsets $A,B\subseteq X$, it is not difficult to verify that
$d=d_{\tau}$ satisfies the following properties:

  1. 1.

$d(\varnothing)=\varnothing$;

  2. 2.

$d(A\cup B)=d(A)\cup d(B)$;

  3. 3.

$dd(A)\subseteq A\cup d(A)$.

In fact, these conditions lead to a more general notion of derivative
spaces:111Derivative spaces are a special case of derivative algebras
introduced by Esakia [EsakiaAlgebra], where $\wp(X)$ is replaced by an
arbitrary Boolean algebra.

######  Definition 2.3.

A derivative space is a pair $\langle X,\rho\rangle$, where $X$ is a set and
$\rho\colon\wp(X)\to\wp(X)$ is a map satisfying properties 1-3 (with $\rho$ in
place of $d$).

Accordingly, if $\mathfrak{X}=\langle X,\tau\rangle$ is a topological space
and $d_{\tau}$ is the Cantor derivative on $\mathfrak{X}$, then $\langle
X,d_{\tau}\rangle$ is a derivative space. However, there are other examples of
derivative spaces. The standard topological closure may be defined by
$c(A)=A\cup d_{\tau}(A)$. Then, $\langle X,c\rangle$ is also a derivative
space, which satisfies the additional property $A\subseteq c(A)$ (and, a
fortiori, $cc(A)=c(A)$); we call such derivative spaces closure spaces. For
convenience, we denote the closure of the topological space $\langle
X,\tau\rangle$ by $c_{\tau}$.

Another example of derivative spaces comes from weakly transitive Kripke
frames. For the sake of succinctness, we call these frames derivative frames.
Below and throughout the text, we write $\exists x\sqsupset y\ \varphi$
instead of $\exists x(y\sqsubset x\wedge\varphi)$, and adopt a similar
convention for the universal quantifier and other relational symbols.

######  Definition 2.4.

A derivative frame is a pair $\mathfrak{F}=\langle W,\sqsubset\rangle$ where
$W$ is a non-empty set and $\sqsubset$ is a weakly transitive relation on $W$,
meaning that $w\sqsubset v\sqsubset u$ implies that $w\sqsubseteq u$, where
$\sqsubseteq$ is the reflexive closure of $\sqsubset$.

We chose the notation $\sqsubset$ because it is suggestive of a transitive
relation, but remains ambiguous regarding reflexivity, as there may be
irreflexive and reflexive points. Note that $\sqsubset$ is weakly transitive
iff $\sqsubseteq$ is transitive. Given $A\subseteq W$, we define
${\downarrow_{\sqsubset}}$ as a map
${\downarrow_{\sqsubset}}\colon\wp(W)\to\wp(W)$ such that

${\downarrow_{\sqsubset}}(A)=\\{w\in W:\exists v\sqsupset w(v\in A)\\}.$

The following is then readily verified:

######  Lemma 2.5.

If $\langle W,\sqsubset\rangle$ is a derivative frame, then $\langle
W,{\downarrow_{\sqsubset}}\rangle$ is a derivative space.

There is a connection between derivative frames and topological spaces. Given
a derivative frame $\langle W,\sqsubset\rangle$, we define a topology
$\tau_{\sqsubset}$ on $W$ such that $U\in\tau_{\sqsubset}$ iff $U$ is upwards
closed under $\sqsubset$, in the sense that if $w\in U$ and $v\sqsupset w$
then $v\in U$. Topologies of this form are Aleksandroff topologies. The
following is well known and easily verified.

######  Lemma 2.6.

Let $\langle W,\sqsubset\rangle$ be a derivative frame and
$\tau=\tau_{\sqsubset}$. Then, $d_{\tau}={\downarrow_{\sqsubset}}$ iff
$\sqsubset$ is irreflexive and $c_{\tau}={\downarrow_{\sqsubset}}$ iff
$\sqsubset$ is reflexive.

Dynamical systems consist of a topological space equipped with a continuous
function. Recall that if $\langle X,\tau\rangle$ and $\langle
Y,\upsilon\rangle$ are topological spaces and $f\colon X\to Y$, then $f$ is
continuous if whenever $U\in\upsilon$, it follows that $f^{-1}(U)\in\tau$. The
function $f$ is open if $f(V)$ is open whenever $V$ is open, and $f$ is a
homeomorphism if $f$ is continuous, open and bijective. It is well known (and
not hard to check) that $f$ is continuous iff $c_{\tau}f^{-1}(A)\subseteq
f^{-1}c_{\upsilon}(A)$ for any $A\subseteq Y$. By unfolding the definition of
the closure operator, this becomes $f^{-1}(A)\cup d_{\tau}f^{-1}(A)\subseteq
f^{-1}(A)\cup f^{-1}d_{\upsilon}(A)$, or equivalently,
$d_{\tau}f^{-1}(A)\subseteq f^{-1}(A)\cup f^{-1}d_{\upsilon}(A)$. We thus
arrive at the following definition.

######  Definition 2.7.

Let $\langle X,\rho_{X}\rangle$ and $\langle Y,\rho_{Y}\rangle$ be derivative
spaces. We say that $f\colon X\to Y$ is continuous if for all $A\subseteq Y$,
$\rho_{X}f^{-1}(A)\subseteq f^{-1}(A)\cup f^{-1}\rho_{Y}(A)$. We say that $f$
is a homeomorphism if it is bijective and
$\rho_{X}f^{-1}(A)=f^{-1}\rho_{Y}(A)$.

It is worth checking that these definitions coincide with their standard
topological counterparts.

######  Lemma 2.8.

If $\langle X,\tau\rangle$, $\langle Y,\upsilon\rangle$ are topological spaces
with Cantor derivatives $d_{\tau}$ and $d_{\upsilon}$ respectively, and
$f\colon X\to Y$, then

  1. 1.

if $f$ is continuous as a function between topological spaces, it is
continuous as a function between derivative spaces, and

  2. 2.

if $f$ is a homeomorphism as a function between topological spaces, it is a
homeomorphism as a function between derivative spaces.

We are particularly interested in the case where $X=Y$, which leads to the
notion of dynamic derivative system.

######  Definition 2.9.

A dynamic derivative system is a triple $\mathfrak{S}=\langle
X,\rho,f\rangle$, where $\langle X,\rho\rangle$ is a derivative space and
$f\colon X\to X$ is continuous. If $f$ is a homeomorphism, we say that
$\mathfrak{S}$ is invertible.

If $\mathfrak{S}=\langle X,\rho,f\rangle$ is such that $\rho=d_{\tau}$ for
some topology $\tau$, we say that $\mathfrak{S}$ is a dynamic topological
system and identify it with the triple $\langle X,\tau,f\rangle$. If
$\rho={\downarrow_{\sqsubset}}$ for some weakly transitive relation
$\sqsubset$, we say that $\mathfrak{S}$ is a dynamic Kripke frame and identify
it with the triple $\langle X,\sqsubset,f\rangle$.

It will be convenient to characterise dynamic Kripke frames in terms of the
relation $\sqsubset$.

######  Definition 2.10 (monotonicity and weak monotonicity).

Let $\langle W,\sqsubset\rangle$ be a derivative frame. A function $f\colon
W\to W$ is monotonic if $w\sqsubset v$ implies $f(w)\sqsubset f(v)$, and
weakly monotonic if $w\sqsubset v$ implies $f(w)\sqsubseteq f(v)$.

The function $f$ is persistent if it is a bijection and for all $w,v\in W$,
$w\sqsubset v$ if and only if $f(w)\sqsubset f(v)$. We say that a Kripke frame
is invertible if it is equipped with a persistent function.

######  Lemma 2.11.

If $\langle W,\sqsubset\rangle$ is a derivative frame and $f\colon W\to W$,
then

  1. 1.

if $f$ is weakly monotonic then it is continuous with respect to
$\downarrow_{\sqsubset}$, and

  2. 2.

if $f$ is persistent then it is a homeomorphism with respect to
$\downarrow_{\sqsubset}$.

Our goal is to reason about various classes of dynamic derivative systems
using the logical framework defined in the next section.

##  3 Dynamic Topological Logics

In this section we discuss dynamic topological logic in the general setting of
dynamic derivative systems. Given a non-empty set $\mathsf{PV}$ of
propositional variables, the language $\mathcal{L}_{\lozenge}^{\circ}$ is
defined recursively as follows:

$\varphi::=p\;|\;\varphi\wedge\varphi\;|\;\neg\varphi\;|\;\lozenge\varphi\;|\;\bc\varphi,$

where $p\in\mathsf{PV}.$ It consists of the Boolean connectives $\wedge$ and
$\neg$, the temporal modality $\bc$, and the modality $\lozenge$ for the
derivative operator with its dual $\square:=\neg\lozenge\neg$. The interior
modality may be defined by $\boxdot\varphi:=\varphi\wedge\square\varphi$.

######  Definition 3.1 (semantics).

A _dynamic derivative model_ (DDM) is a quadruple $\mathfrak{M}=\langle
X,\rho,f,\nu\rangle$ where $\langle X,\rho,f\rangle$ is a dynamic derivative
system and $\nu:\mathsf{PV}\rightarrow\wp(X)$ is a valuation function
assigning a subset of $X$ to each propositional letter in $\mathsf{PV}$. Given
$\varphi\in\mathcal{L}_{\lozenge}^{\circ}$, we define the truth set
$\|\varphi\|\subseteq X$ of $\varphi$ inductively as follows:

  * •

$\|p\|=\nu(p)$;

  * •

$\|\neg\varphi\|=X\setminus\|\varphi\|$;

  * •

$\|\varphi\wedge\psi\|=\|\varphi\|\cap\|\psi\|$;

  * •

$\|\lozenge\varphi\|=\rho(\|\varphi\|)$;

  * •

$\|\bc\varphi\|=f^{-1}(\|\varphi\|)$.

  *

We write $\mathfrak{M},x\models\varphi$ if $x\in\|\varphi\|$, and
$\mathfrak{M}\models\varphi$ if $\|\varphi\|=X$. We may write
$\|\cdot\|_{\mathfrak{M}}$ or $\|\cdot\|_{\nu}$ instead of $\|\cdot\|$ when
working with more than one model or valuation.

We define other connectives (e.g. $\vee,\rightarrow$) as abbreviations in the
usual way. The fragment of $\mathcal{L}_{\lozenge}^{\circ}$ that includes only
$\lozenge$ will be denoted by $\mathcal{L}_{\lozenge}$. Since our definition
of the semantics applies to any derivative space and a general operator
$\rho$, we need not differentiate in our results between $d$-logics, logics
based on closure semantics and logics based on relational semantics. Instead,
we indicate the specific class of derivative spaces to which the result
applies.

In order to keep with the familiar axioms of modal logic, it is convenient to
discuss the semantics of $\square$. Accordingly, we define the dual of the
derivative, called the _co-derivative_.

######  Definition 3.2 (co-derivative).

Let $\langle X,\rho\rangle$ be a derivative space. For each $S\subseteq X$ we
define $\hat{\rho}(S):=X\backslash\rho(X\backslash S)$ to be the co-derivative
of $S$.

The co-derivative satisfies the following properties, where $A,B\subseteq X$:

  1. 1.

$\hat{\rho}(X)=X$;

  2. 2.

$A\cap\hat{\rho}(A)\subseteq\hat{\rho}\hat{\rho}(A)$;

  3. 3.

$\hat{\rho}(A\cap B)=\hat{\rho}(A)\cap\hat{\rho}(B)$.

It can readily be checked that for any dynamic derivative model $\langle
X,\rho,f,\nu\rangle$ and any formula $\varphi$,
$\|\square\varphi\|=\hat{\rho}(\|\varphi\|)$. The co-derivative can be used to
define the standard interior of a set, given by $i(A)=A\cap\hat{\rho}(A)$ for
each $A\subseteq X$. This implies that $U\subseteq\hat{\rho}(U)$ for each open
set $U$, but not necessarily $\hat{\rho}(U)\subseteq U$. Next, we discuss the
systems of axioms that are of interest to us. Let us list the axiom schemes
and rules that we will consider in this paper:

Taut $:=\text{All propositional tautologies}$

K $:=\square(\varphi\to\psi)\to(\square\varphi\to\square\psi)$

T $:=\square\varphi\to\varphi$

w4 $:=\varphi\wedge\square\varphi\to\square\square\varphi$

L $:=\square(\square\varphi\rightarrow\varphi)\rightarrow\square\varphi$

4 $:=\square\varphi\to\square\square\varphi$

${\rm Next}_{\neg}$ $:=\neg\bc\varphi\leftrightarrow\bc\neg\varphi$

${\rm Next}_{\wedge}$
$:=\bc(\varphi\wedge\psi)\leftrightarrow\bc\varphi\wedge\bc\psi$

C $:=\bc\varphi\wedge\bc\square\varphi\to\square\bc\varphi$

H $:=\square\bc\varphi\leftrightarrow\bc\square\varphi$

MP $:=\dfrac{\varphi\ \ \varphi\to\psi}{\psi}$

${\rm Nec}_{\square}$ $:=\dfrac{\varphi}{\square\varphi}$

${\rm Nec}_{\bc}$ $:=\dfrac{\varphi}{\bc\varphi}$

The ‘base modal logic’ over $\mathcal{L}_{\lozenge}$ is given by

$\mathbf{K}:={\rm Taut}+{\rm K}+{\rm MP}+{\rm Nec}_{\square},$

but we are mostly interested in proper extensions of $\mathbf{K}$. Let
$\Lambda,\Lambda^{\prime}$ be logics over languages $\mathcal{L}$ and
${\mathcal{L}}^{\prime}$. We say that $\Lambda$ extends $\Lambda^{\prime}$ if
$\mathcal{L}^{\prime}\subseteq\mathcal{L}$ and all the axioms and rules of
$\Lambda^{\prime}$ are derivable in $\Lambda$. A logic over
$\mathcal{L}_{\lozenge}$ is normal if it extends $\mathbf{K}$. If $\Lambda$ is
a logic and $\varphi$ is a formula, $\Lambda+\varphi$ is the least extension
of $\Lambda$ which contains every substitution instance of $\varphi$ as an
axiom.

We then define $\mathbf{wK4}:=\mathbf{K}+{\rm w4}$,
$\mathbf{K4}:=\mathbf{K}+{\rm 4}$, $\mathbf{S4}:=\mathbf{K4}+{\rm T}$ and
$\mathbf{GL}:=\mathbf{K4}+{\rm L}$. These logics are well known and
characterise certain classes of topological spaces and Kripke frames which we
review below. In addition, for a logic $\Lambda$ over
$\mathcal{L}_{\lozenge}$, $\Lambda\mathbf{F}$ is the logic over
$\mathcal{L}^{\circ}_{\lozenge}$ given by222Logics of the form
$\Lambda\mathbf{F}$ correspond to dynamical systems with a possibly
discontinuous function. We will not discuss discontinuous systems in this
paper; see [artemov] for more information.

$\Lambda\mathbf{F}:=\Lambda+{\rm Next}_{\neg}+{\rm Next}_{\wedge}+{\rm
Nec}_{\bc}.$

This simply adds axioms of linear temporal logic to $\Lambda$, which hold
whenever $\bc$ is interpreted using a function. Finally, we define
$\Lambda{\bf C}:=\Lambda\mathbf{F}+\rm C$ and $\Lambda{\bf
H}:=\Lambda\mathbf{F}+\rm H$, which as we will see correspond to derivative
spaces with a continuous function or a homeomorphism respectively. The
following is well known and dates back to McKinsey and Tarski [Tarski].

######  Theorem 3.3.

$\mathbf{S4}$ is the logic of all topological closure spaces, the logic of all
transitive, reflexive derivative frames, and the logic of the real line with
the standard closure.

The logic $\mathbb{K4}$ includes the axiom $\square p\to\square\square p$,
which is not valid over the class of all topological spaces. The class of
spaces satisfying this axiom is denoted by $T_{D}$, defined as the class of
spaces in which every singleton is the result of an intersection between an
open set and a closed set. Moreover, Esakia showed that this is the logic of
transitive derivative frames [EsakiaAlgebra].

######  Theorem 3.4.

$\mathbf{K4}$ is the logic of all $T_{D}$ topological derivative spaces, as
well as the logic of all transitive derivative frames.

Many familiar topological spaces, including Euclidean spaces, satisfy the
$T_{D}$ property, making $\mathbf{K4}$ central in the study of topological
modal logic. A somewhat more unusual class of spaces, which is nevertheless of
particular interest to us, is the class of scattered spaces.

######  Definition 3.5 (scattered space).

A topological space $\langle X,\tau\rangle$ is scattered if for every
$S\subseteq X$, $S\subseteq d(S)\text{ implies }S=\varnothing.$

This is equivalent to the more common definition of a scattered space where a
topological space is called scattered if every non-empty subset has an
isolated point. Scattered spaces are closely related to converse well-founded
relations. Below, recall that $\langle W,\sqsubset\rangle$ is converse well-
founded if there is no infinite sequence $w_{0}\sqsubset w_{1}\sqsubset\ldots$
of elements in $W$.

######  Lemma 3.6.

If $\langle W,\sqsubset\rangle$ is an irreflexive frame, then $\langle
W,\tau_{\sqsubset}\rangle$ is scattered iff $\sqsubset$ is converse well-
founded.

######  Theorem 3.7 (Simmons [simmons] and Esakia [esakia]).

$\mathbf{GL}$ is the logic of all scattered topological derivative spaces, as
well as the logic of all converse well-founded derivative frames and the logic
of all finite, transitive, irreflexive derivative frames.

Aside from its topological interpretation, the logic $\mathbf{GL}$ is of
particular interest as it is also the logic of provability in Peano
arithmetic, as was shown by Boolos [boolo]. Meanwhile, logics with the $\rm C$
and $\rm H$ axioms correspond to classes of dynamical systems.

######  Lemma 3.8.

  1. 1.

If $\Lambda$ is sound for a class of derivative spaces $\Omega$, then
$\Lambda{\bf C}$ is sound for the class of dynamic derivative systems $\langle
X,\rho,f\rangle$, where $\langle X,\rho\rangle\in\Omega$ and $f$ is
continuous.

  2. 2.

If $\Lambda$ is sound for a class of derivative spaces $\Omega$, then
$\Lambda{\bf H}$ is sound for the class of dynamic derivative systems $\langle
X,\rho,f\rangle$, where $\langle X,\rho\rangle\in\Omega$ and $f$ is a
homeomorphism.

The above lemma is easy to verify from the definitions of continuous functions
and homeomorphisms in the context of derivative spaces (Definition 2.7).

###  3.1 Prior Work

The study of dynamic topological logic originates with Artemov, Davoren and
Nerode, who observed that it is possible to reason about dynamical systems
within modal logic. They introduced the logic $\bf S4C$ and proved that it is
decidable, as well as sound and complete for the class of all dynamic closure
systems (i.e. dynamic derivative systems based on a closure space). Kremer and
Mints [kremer] considered the logic $\bf S4H$, and also showed it to be sound
and complete for the class of dynamic closure systems where $f$ is a
homeomorphism.

The latter also suggested adding the ‘henceforth’ operator, $*$, from Pnueli’s
linear temporal logic ($\bf LTL$) [ltl], leading to the language we denote by
$\mathcal{L}^{\circ*}_{\lozenge}$. The resulting trimodal system was named
dynamic topological logic ($\bf DTL$). Kremer and Mints offered an
axiomatisation for $\bf DTL$, but Fernández-Duque proved that it is
incomplete; in fact, $\bf DTL$ is not finitely axiomatisable [david].
Fernández-Duque also showed that $\bf DTL$ enjoys a natural axiomatisation
when extended with the tangled closure [david3]. In contrast, Konev et al.
established that $\bf DTL$ over the class of dynamical systems with a
homeomorphism is non-axiomatisable [KonevMetric].

###  3.2 The tangled closure on scattered spaces

Our interest in considering the class of scattered spaces within dynamic
topological logic is motivated by results of Fernández-Duque [david3]. He
showed that the set of valid formulas of $\mathcal{L}^{\circ*}_{\lozenge}$
over the class of all dynamic closure systems is not finitely axiomatisable.
Nevertheless, he found a natural (yet infinite) axiomatisation by introducing
the _tangled closure_ and adding it to the language of $\bf DTL$
[FernandezTangled]. Here, we use the more general tangled derivative, as
defined by Goldblatt and Hodkinson [Goldblatt2017Spatial].

######  Definition 3.9 (tangled derivative).

Let $\langle X,d\rangle$ be a derivative space and let
$\mathcal{S}\subseteq\wp(X)$. Given $A\subseteq X$, we say that $\mathcal{S}$
is tangled in $A$ if for all $S\in\mathcal{S}$, $A\subseteq d(S\cap A)$. We
define the _tangled derivative_ of $\mathcal{S}$ as

$\mathcal{S}^{*}:=\bigcup\\{A\subseteq X:\mathcal{S}\text{ is tangled in
}A\\}.$

The tangled closure is then the special case of the tangled derivative where
$d$ is a closure operator. Fernández-Duque’s axiomatisation is based on the
extended language
$\mathcal{L}^{\circ*}_{\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}}$.
This language is obtained by extending $\mathcal{L}^{\circ*}_{\lozenge}$ with
the following operation.

######  Definition 3.10 (tangled language).

We define
$\mathcal{L}^{\circ*}_{\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}}$
by extending the recursive definition of $\mathcal{L}^{\circ*}_{\lozenge}$ in
such a way that if
$\varphi_{1},\ldots,\varphi_{n}\in\mathcal{L}^{\circ*}_{\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}}$,
then
$\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}\\{\varphi_{1},\ldots,\varphi_{n}\\}\in\mathcal{L}^{\circ*}_{\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}}$.
The semantic clauses are then extended so that on any model $\mathfrak{M}$,

$\|{\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}\\{\varphi_{1},\ldots,\varphi_{n}\\}}\|=\\{\|\varphi_{1}\|,\ldots,\|\varphi_{n}\|\\}^{*}.$

The logic $\mathbb{DGL}$ is an extension of $\mathbb{GLC}$ that includes the
temporal operator $*$. Unlike the complete axiomatisation of $\mathbf{DTL}$
that requires the tangled operator, in the case of $\mathbb{DGL}$, we should
be able to avoid this and use the original spatial operator $\lozenge$ alone.
This is due to the following:

theoremscatteredlozenge Let $\mathfrak{X}=\langle X,\tau\rangle$ be a
scattered space and $\\{\varphi_{1},\dots,\varphi_{n}\\}$ a set of formulas.
Then

$\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}\\{\varphi_{1},\dots,\varphi_{n}\\}\equiv\bot.$

###### Proof.

Let $\nu$ be a valuation on $\mathfrak{X}$,
$\mathfrak{M}=\langle\mathfrak{X},\nu\rangle$, and suppose that
$\mathfrak{M},x\models\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}\\{\varphi_{1},\dots,\varphi_{n}\\}$
for some $x\in X$. Then by definition there exists $S\subseteq X$ s.t. $x\in
S$ and $S\subseteq d(S\cap[\\![\varphi_{i}]\\!])$, for all $i\leq n$. It
follows that $S\subseteq d(S)$. Since $\mathfrak{X}$ is scattered, then
$S=\varnothing$ in contradiction. It follows that
$\mathfrak{M},x\not\models\stackMath\mathbin{\stackinset{c}{0ex}{c}{0ex}{\ast}{\lozenge}}\\{\varphi_{1},\dots,\varphi_{n}\\}$
for all $x\in X$. ∎

This leads to the conjecture that the axiomatic system of Kremer and Mints
[kremer], combined with $\mathbf{GL}$, will lead to a finite axiomatisation
for $\mathbf{DGL}$. While such a result requires techniques beyond the scope
of the present work, the completeness proof we present here for $\mathbf{GLC}$
is an important first step. Before proving topological completeness for this
and the other logics we have mentioned, we show that they are complete and
have the finite model property for their respective classes of dynamic
derivative frames.

##  4 The Canonical Model

The first step in our Kripke completeness proof will be a fairly standard
canonical model construction. A _maximal $\Lambda$-consistent set_
($\Lambda$-MCS) $w$ is a set of formulas that is $\Lambda$-consistent, i.e.
$w\not\vdash_{\Lambda}\bot$, and every set of formulas that properly contains
it is $\Lambda$-inconsistent.

Given a logic $\Lambda$ over $\mathcal{L}^{\circ}_{\lozenge}$, let
$\mathfrak{M}^{\Lambda}_{\rm c}=\langle W_{\rm c},\sqsubset_{\rm c},g_{\rm
c},\nu_{\rm c}\rangle$ be the canonical model for $\Lambda$, where

  1. 1.

$W_{\rm c}$ is the set of all $\Lambda$-MCSs;

  2. 2.

$w\sqsubset_{\rm c}v$ iff for all formulas $\varphi$, if $\square\varphi\in
w$, then $\varphi\in v$;

  3. 3.

$g_{\rm c}(w)=\\{\varphi:\bc\varphi\in w\\}$;

  4. 4.

$\nu_{\rm c}(p)=\\{w:p\in w\\}$.

It can easily be verified that $\mathbb{wK4C}$ defines the class of all weakly
transitive Kripke models with a weakly monotonic map. Moreover, $\mathbb{K4C}$
defines the class of all transitive Kripke models with a weakly monotonic map.
We call these models $\mathbb{wK4C}$ models and $\mathbb{K4C}$ models
respectively.

lemmacanonical If $\Lambda$ extends $\mathbb{wK4C}$, then the canonical model
for $\Lambda$ is a $\mathbb{wK4C}$ model. If $\Lambda$ extends $\mathbb{K4C}$,
then the canonical model of $\Lambda$ is a $\mathbb{K4C}$ model.

###### Proof.

Let $\mathfrak{M}^{\Lambda}_{\rm c}=\langle W,\sqsubset,g,\nu\rangle$. Suppose
that $\Lambda$ extends $\mathbb{wK4C}$. We prove that $g$ is weakly monotonic.
Suppose $w\sqsubset v$ and $g(w)\neq g(v)$. Since $g(w)\neq g(v)$, there
exists $\varphi$ such that $\varphi\in g(w)$ and $\varphi\notin g(v)$. We
consider an arbitrary $\square\psi\in g(w)$ then clearly
$\square(\psi\vee\varphi)\in g(w)$ and $(\psi\vee\varphi)\in g(w)$. In
particular, $\bc\square(\psi\vee\varphi)\in w$ and $\bc(\psi\vee\varphi)\in
w$. Since $(\bc\square p\wedge\bc p)\rightarrow\square\bc p\in\mathbb{wK4C}$,
then $\square\bc(\varphi\vee\psi)\in w$. Since $w\sqsubset v$, then
$\bc(\varphi\vee\psi)\in v$ and $(\varphi\vee\psi)\in g(v)$. Since
$\varphi\notin g(v)$, then $\psi\in g(v)$ and because $\square\psi$ is
arbitrary, then $g(w)\sqsubset g(v)$, as required. Hence $g$ is weakly
monotonic.

We prove that $\sqsubset$ is weakly transitive. Suppose $w\sqsubset v\sqsubset
u$ and $w\neq u$. From $w\neq u$ it follows that there exists $\varphi$ such
that $\varphi\in w$ and $\varphi\notin u$. We consider an arbitrary
$\square\psi\in w$, then clearly $\square(\psi\vee\varphi)\in w$ and
$(\psi\vee\varphi)\in w$. Since
$(\varphi\wedge\square\varphi)\rightarrow\square\square\varphi\in\mathbb{wK4C}$,
then $\square\square(\psi\vee\varphi)\in w$. Then $w\sqsubset v\sqsubset u$
implies $(\psi\vee\varphi)\in u$ and as $\varphi\notin u$ we have $\psi\in u$.
Since $\square\psi$ is arbitrary, then $w\sqsubset u$ holds, as required.

It follows that $g$ is weakly monotonic and $\sqsubset$ is weakly transitive
and hence $\mathfrak{M}^{\Lambda}_{\rm c}$ is a $\mathbb{wK4C}$ model.

Suppose that $\Lambda$ extends $\mathbb{K4C}$, then weak monotonicity holds as
before since $\mathbb{K4C}$ extends $\mathbb{wK4C}$. Therefore, we only need
to prove that $\sqsubset$ is transitive. Suppose $w\sqsubset v\sqsubset u$. We
consider an arbitrary $\square\psi\in w$. Since $\square
p\rightarrow\square\square p\in\mathbb{wK4C}$, then $\square\square\psi\in w$.
Then, $w\sqsubset v\sqsubset u$ implies $\psi\in u$ and since $\square\psi$ is
arbitrary, then $w\sqsubset u$, as required.

It follows that $g$ is weakly monotonic and $\sqsubset$ is transitive and thus
$\mathfrak{M}^{\Lambda}_{\rm c}$ is a $\mathbb{K4C}$ model. ∎

It is a well-known fact that the transitivity axiom $\square
p\rightarrow\square\square p$ is derivable in $\mathbb{GL}$ (see [trans]).
Therefore, $\mathbb{GLC}$ extends the system $\mathbb{K4C}$. The proofs of the
following two lemmas are standard and can be found for example in [black].

######  Lemma 4.1 (existence lemma).

Let $\Lambda$ be a normal modal logic and let $\mathfrak{M}^{\Lambda}_{\rm
c}=\langle W_{\rm c},\sqsubset_{\rm c},g_{\rm c},\nu_{\rm c}\rangle$. Then,
for every $w\in W_{\rm c}$ and every formula $\varphi$ in $\Lambda$, if
$\lozenge\varphi\in w$ then there exists a point $v\in W_{\rm c}$ such that
$w\sqsubset_{\rm c}v$ and $\varphi\in v$.

######  Lemma 4.2 (truth lemma).

Let $\Lambda$ be a normal modal logic. For every $w\in W_{\rm c}$ and every
formula $\varphi$ in $\Lambda$,

$\mathfrak{M}^{\Lambda}_{\rm c},w\models\varphi\text{ iff }\varphi\in w.$

######  Corollary 4.3.

The logic $\mathbb{wK4C}$ is sound and complete with respect to the class of
all weakly monotonic dynamic derivative frames, and $\mathbb{K4C}$ is sound
and complete with respect to the class of all weakly monotonic, transitive
dynamic derivative frames.

##  5 A finitary accessibility relation

One key ingredient in our finite model property proof will be the construction
of a ‘finitary’ accessibility relation $\sqsubset_{\Phi}$ on the canonical
model. This accessibility relation will have the property that each point has
finitely many successors, yet the existence lemma will hold for formulas in a
prescribed finite set $\Phi$.

We define the $\sqsubset_{\rm c}$-cluster $C(w)$ for each point $w\in W_{\rm
c}$ as

$C(w)=\\{w\\}\cup\\{v:w\sqsubset_{\rm c}v\sqsubset_{\rm c}w\\}.$

######  Definition 5.1 ($\varphi$-final set).

A set $w$ is said to be a $\varphi$-final set (or point) if $w$ is an MCS,
$\varphi\in w$, and whenever $w\sqsubset_{\rm c}v$ and $\varphi\in v$, it
follows that $v\in C(w)$.

Let us write $\sqsubseteq_{\rm c}$ for the reflexive closure of
$\sqsubset_{\rm c}$. It will be convenient to characterise $\sqsubseteq_{\rm
c}$ in the canonical model syntactically. Recall that
$\boxdot\varphi:=\varphi\wedge\square\varphi$.

lemmaextend If $\Lambda$ extends $\mathbb{wK4C}$ and $w,v\in W_{\rm c}$, then
$w\sqsubseteq_{\rm c}v$ if and only if whenever $\boxdot\varphi\in w$, it
follows that $\boxdot\varphi\in v$.

###### Proof.

First assume that $w\sqsubseteq_{\rm c}v$. Obviously if $w=v$ then
$\boxdot\varphi\in w$ implies $\boxdot\varphi\in v$. If $\boxdot\varphi\in w$
then from $\square\varphi\in w$ we obtain $\varphi\in v$ and by $\rm w4$ we
have $\square\square\varphi\in w$ and so $\square\varphi\in v$.

Conversely, assume that $\boxdot\varphi\in w$ implies $\boxdot\varphi\in v$.
If $w=v$, then $w\sqsubseteq_{\rm c}v$. Otherwise, $w\neq v$, and we can find
$\psi\in w\setminus v$. Suppose that $\square\varphi\in w$. Then
$\boxdot(\varphi\vee\psi)\in w$ and so $\boxdot(\varphi\vee\psi)\in v$. It
follows that $\varphi\vee\psi\in v$. But $\psi\not\in v$, so $\varphi\in v$;
since $\varphi$ was arbitrary, then $w\sqsubset_{\rm c}v$, as required. ∎

We are now ready to prove the main result of this section regarding the
existence of the finitary relation $\sqsubset_{\Phi}$. lemmafinitary Let
$\Lambda$ extend $\mathbb{wK4C}$ and $\Phi$ be a finite set of formulas closed
under subformulas. There is an auxiliary relation $\sqsubset_{\Phi}$ on the
canonical model of $\Lambda$ such that:

  1. (i)

$\sqsubset_{\Phi}$ is a subset of $\sqsubset_{\rm c}$;

  2. (ii)

For each $w\in W$, the set ${\sqsubset_{\Phi}}(w)$ is finite;

  3. (iii)

If $\lozenge\varphi\in w\cap\Phi$, then there exists $v\in W$ with
$w\sqsubset_{\Phi}v$ and $\varphi\in v$;

  4. (iv)

If $w\sqsubset_{\rm c}v\sqsubset_{\rm c}w$ then
${\sqsubset_{\Phi}(w)}\subseteq{\sqsubseteq_{\Phi}(v)}$;

  5. (v)

$\sqsubset_{\Phi}$ is weakly transitive. Moreover, if $\Lambda$ extends
$\mathbb{K4C}$ then $\sqsubset_{\Phi}$ is transitive, and if $\Lambda$ extends
$\mathbb{GLC}$ then $\sqsubset_{\Phi}$ is irreflexive.

###### Proof.

Let $C$ be any cluster of points in $W$ and define

${\sqsubset_{\rm c}}(C)=\bigcup\\{{\sqsubset_{\rm c}}(v):v\in C\\}.$

We construct the weakly transitive relation $\sqsubset_{\Phi}$ as follows:
Using Lemma A.2 we use the axiom of choice to choose a function that for each
formula $\varphi$ and each cluster $C$ such that $\lozenge\varphi\in\bigcup
C$, assigns a $\varphi$-final point $w(\varphi,C)$ such that
$w(\varphi,C)\in{\sqsubset_{\rm c}}(C)$. We choose a second point
$w^{\prime}(\varphi,C)$, possibly equal to $w(\varphi,C)$, such that

  * •

if $\lozenge\varphi\in w(\varphi,C)$, then $w^{\prime}(\varphi,C)$ is any
$\varphi$-final point such that $w(\varphi,C)\sqsubset_{\rm
c}w^{\prime}(\varphi,C)$;

  * •

otherwise, $w^{\prime}(\varphi,C)=w(\varphi,C)$.

Set $u\sqsubset_{\Phi}^{0}v$ iff $u\sqsubset_{\rm c}v$ and there exists
$\psi\in\Phi$ such that $\lozenge\psi\in u$ and
$v\in\\{w(\psi,C(u)),w^{\prime}(\psi,C(u))\\}$. Let $\sqsubset_{\Phi}$ be the
weakly transitive closure of $\sqsubset_{\Phi}^{0}$.

It is clear that (i), (iii) and (iv) follow directly from the construction:
(i) follows from the fact that $\sqsubset_{\Phi}$ is the transitive closure of
$\sqsubset^{0}_{\Phi}$; (iii) follows from Lemma 5.1; (iv) follows from the
fact that $v\in C(w)$ and by assuming that $v\sqsubseteq_{\Phi}u$ and
unraveling the definition of $\sqsubseteq_{\Phi}$.

We continue to verify conditions (ii) and (v). For condition (ii), first
observe that ${\sqsubset_{\Phi}^{0}}(u)$ is finite by construction, as it
contains at most two elements for each $\varphi\in\Phi$. Now, if
$u\sqsubset_{\Phi}v$ then there is a sequence

$u\sqsubset_{\Phi}^{0}v_{1}\sqsubset_{\Phi}^{0}\dots\sqsubset_{\Phi}^{0}v_{n}=v.$

By taking a minimal such sequence, we may assume that it is injective.
Consider the tree consisting of all such sequences (ordered by the initial
segment relation). This is a finitely-branching tree, as
${\sqsubset_{\Phi}^{0}}(x)$ is always finite. Moreover, if
${\sqsubset_{\Phi}}(u)$ is infinite, then this tree is infinite. By König’s
lemma, there is an infinite sequence

$u\sqsubset_{\Phi}^{0}v_{1}\sqsubset_{\Phi}^{0}v_{2}\sqsubset_{\Phi}^{0}\dots.$

By definition of $\sqsubset_{\Phi}^{0}$, for each $i\in\omega$ there is
$\varphi_{i}\in\Phi$ such that $v_{i+1}$ is $\varphi_{i}$-final. Since
${\sqsubset_{\Phi}^{0}}\subseteq{\sqsubset_{\rm c}}$, we have that
$v_{i}\sqsubseteq_{\rm c}v_{j}$ whenever $i\leq j$. Since $\Phi$ is finite,
there is some $\theta\in\Phi$ such that $v_{i}$ is $\theta$-final for
infinitely many values of $i$. Let $i_{0}$ be the least such value. If
$i>i_{0}$ is any other such value, $v_{i_{0}}\sqsubset_{\rm c}v_{i}$ together
with $\theta$-finality of $v_{i_{0}}$ yields $v_{i}\sqsubset_{\rm
c}v_{i_{0}}$. Thus $v_{i}\in C(v_{i_{0}})$ and
$v_{i}\sqsubset_{\Phi}^{0}v_{i+1}$, which by definition of
$\sqsubset^{0}_{\Phi}$ yields $v_{i+1}\in{\sqsubset_{\Phi}^{0}}(v_{i_{0}})$.
But ${\sqsubset_{\Phi}^{0}}(v_{i_{0}})$ is finite, contradicting that the
chain is infinite and injective.

Finally, we verify condition (v). The relation $\sqsubset_{\Phi}$ is weakly
transitive by definition, and if $\Lambda$ extends $\mathbf{K4C}$, we have
that $x\sqsubset_{\Phi}y\sqsubset_{\Phi}z$ implies $x\sqsubseteq_{\Phi}z$,
which in the case that $x=z$ implies that $x\sqsubset_{\rm c}x$ and also that
$x,y$ are in the same cluster. This together with $y\sqsubset_{\Phi}z$ implies
that $x\sqsubset_{\Phi}z$, as $\sqsubset_{\Phi}$ is cluster-invariant.

Now let $\Lambda$ extend $\mathbf{GLC}$, and suppose that $w$ is
$\varphi$-final. We claim that $\lozenge\varphi\not\in w$, which immediately
yields $w\neq\sqsubset_{\Phi}w$, as needed. By the contrapositive of $\rm L$,
we have that $\lozenge\varphi\to\lozenge(\varphi\wedge\square\neg\varphi)\in
w$. If $\lozenge\varphi\in w$, then
$\lozenge(\varphi\wedge\square\neg\varphi)\in w$. It follows that there is
$v\sqsupset_{\Phi}w$ with $\varphi\wedge\square\neg\varphi\in v$. But
$\square\neg\varphi\in v$ implies that $v\not\sqsubset_{\Phi}w$, contradicting
the $\varphi$-finality of $w$. So $\lozenge\varphi\notin w$ and $w$ is
irreflexive, as required. ∎

##  6 Stories and $\Phi$-morphisms

In this subsection we show that the logics $\mathbb{wK4C}$, $\mathbb{K4C}$ and
$\mathbb{GLC}$ have the finite model property by constructing finite models
and truth preserving maps from these models to the canonical model.

If $\sqsubset$ is a weakly transitive relation on $A$, $\langle
A,\sqsubset\rangle$ is tree-like if whenever $a\sqsubseteq c$ and
$b\sqsubseteq c$, it follows that $a\sqsubseteq b$ or $b\sqsubseteq a$. We
will use labelled tree-like structures called moments to record the ‘static’
information at a point; that is, the structure involving $\sqsubset$, but not
$f$.

######  Definition 6.1 (moment).

A $\Lambda$-moment is a structure
$\mathfrak{m}=\langle|\mathfrak{m}|,\sqsubset_{\mathfrak{m}},\nu_{\mathfrak{m}},r_{\mathfrak{m}}\rangle$,
where $\langle|\mathfrak{m}|,\sqsubset_{\mathfrak{m}}\rangle$ is a finite
tree-like $\Lambda$ frame with a root $r_{\mathfrak{m}}$, and
$\nu_{\mathfrak{m}}$ is a valuation on $|\mathfrak{m}|$.

In order to also record ‘dynamic’ information, i.e. information involving the
transition function, we will stack up several moments together to form a
‘story’. Below, $\bigsqcup$ denotes a disjoint union.

######  Definition 6.2 (story).

A story (with duration $I$) is a structure
$\mathfrak{S}=\langle|\mathfrak{S}|,\sqsubset_{\mathfrak{S}},f_{\mathfrak{S}},\nu_{\mathfrak{S}},r_{\mathfrak{S}}\rangle$
such that there are $I<\omega$, moments
$\mathfrak{S}_{i}=\langle|\mathfrak{S}_{i}|,\sqsubset_{i},\nu_{i},r_{i}\rangle$
for each $i\leq I$, and functions $(f_{i})_{i<I}$ such that:

  1. 1.

$|\mathfrak{S}|=\bigsqcup_{i\leq I}|\mathfrak{S}_{i}|$;

  2. 2.

$\sqsubset_{\mathfrak{S}}=\bigsqcup_{i\leq I}\sqsubset_{i}$;

  3. 3.

$\nu_{\mathfrak{S}}(p)=\bigsqcup_{i\leq I}\nu_{i}(p)$ for each variable $p$;

  4. 4.

$r_{\mathfrak{S}}=r_{0}$;

  5. 5.

$f_{\mathfrak{S}}={\rm Id}_{I}\cup\bigsqcup_{i<I}f_{i}$ with
$f_{i}\colon|\mathfrak{S}_{i}|\to|\mathfrak{S}_{i+1}|$ being a weakly
monotonic map such that $f_{i}(r_{i})=r_{i+1}$ for all $i<I$ (we say that
$f_{i}$ is root preserving), and ${\rm Id}_{I}$ is the identity on
$|\mathfrak{S}_{I}|$.

$r_{1}$$r_{2}$$r_{I}$$r_{0}$$f_{\mathfrak{S}}$$\sqsubset_{\mathfrak{S}}$

Figure 1: An example of a $\mathbb{GL}$-story. The squiggly arrows represent
the relation $\sqsubset_{\mathfrak{S}}$ while the straight arrows represent
the function $f_{\mathfrak{S}}$. Each vertical slice represents a
$\mathbb{GL}$-moment. In the case of other types of stories, we may also have
clusters besides singletons.

We often omit the subindices $\mathfrak{m}$ or $\mathfrak{S}$ when this does
not lead to confusion. We may also assign different notations to the
components of a moment, so that if we write $\mathfrak{m}=\langle
W,\sqsubset,\nu,x\rangle$, it is understood that $W=|\mathfrak{m}|$,
${\sqsubset}={\sqsubset_{\mathfrak{m}}}$, etc.

Recall that a $p$-morphism between Kripke models is a type of map that
preserves validity. It can be defined in the context of dynamic derivative
frames as follows:

######  Definition 6.3 (dynamic $p$-morphism).

Let $\mathfrak{M}=\langle
W_{\mathfrak{M}},\sqsubset_{\mathfrak{M}},g_{\mathfrak{M}}\rangle$ and
$\mathfrak{N}=\langle
W_{\mathfrak{N}},\sqsubset_{\mathfrak{N}},g_{\mathfrak{N}}\rangle$ be dynamic
derivative frames. Let $\pi\colon W_{\mathfrak{M}}\to W_{\mathfrak{N}}$. We
say that $\pi$ is a dynamic $p$-morphism if $w\sqsubset_{\mathfrak{M}}v$
implies that $\pi(w)\sqsubset_{\mathfrak{N}}\pi(v)$,
$\pi(w)\sqsubset_{\mathfrak{N}}u$ implies that there is
$v\sqsupset_{\mathfrak{M}}w$ with $\pi(v)=u$, and $\pi\circ
g_{\mathfrak{M}}=g_{\mathfrak{N}}\circ\pi$.

It is then standard that if $\pi\colon W_{\mathfrak{M}}\to W_{\mathfrak{N}}$
is a surjective, dynamic $p$-morphism, then any formula valid on
$\mathfrak{M}$ is also valid on $\mathfrak{N}$. However, our relation
$\sqsubset_{\Phi}$ will allow us to weaken these conditions and still obtain
maps that preserve the truth of (some) formulas.

######  Definition 6.4 ($\Phi$-morphism).

Fix a logic $\Lambda$ and let $\mathfrak{M}^{\Lambda}_{\rm c}=\langle W_{\rm
c},\sqsubset_{\rm c},g_{\rm c},\nu_{\rm c}\rangle$ and $\mathfrak{S}$ be a
story of duration $I$. A map ${\pi}:|{\mathfrak{S}}|\rightarrow W_{\rm c}$ is
called a _dynamic $\Phi$-morphism_ if for all $x\in|{\mathfrak{S}}|$ the
following conditions are satisfied:

  1. 1.

$x\in{\nu_{\mathfrak{S}}}(p)\iff p\in{\pi}(x)$;

  2. 2.

If $x\in|\mathfrak{S}_{i}|$ for some $i<I$, then $g_{\rm
c}({\pi}(x))={\pi}(f_{\mathfrak{S}}(x))$;

  3. 3.

If $x\sqsubset_{\mathfrak{S}}y$ then $\pi(x)\sqsubset_{\rm c}\pi(y)$;

  4. 4.

If ${\pi}(x)\sqsubset_{\Phi}v$ for some $v\in W_{\rm c}$, then there exists
$y\in|{\mathfrak{S}}|$ such that $x\sqsubset_{\mathfrak{S}}y\text{ and
}v={\pi}(y).$

If we drop condition 2, we say that $\pi$ is a $\Phi$-morphism.

We now show that a dynamic $\Phi$-morphism $\pi$ preserves the truth of
formulas of suitable $\bc$-depth, where the latter is defined as usual in
terms of nested occurrences of $\bc$ in a formula $\varphi$.

[truth preservation] lemmatruthLet $\mathfrak{S}$ be a story of duration $I$
and $x\in|\mathfrak{S}_{0}|$. Let $\pi$ be a dynamic $\Phi$-morphism to the
canonical model of some normal logic $\Lambda$ over
$\mathcal{L}^{\circ}_{\lozenge}$. Suppose that $\varphi\in\Phi$ is a formula
of $\bc$-depth at most $I$. Then $\varphi\in\pi(x)$ iff
$x\in\|\varphi\|_{\mathfrak{S}}$.

###### Proof.

We prove the more general claim that if $\varphi$ has $\bc$-depth at most
$I-j$ and $x\in|\mathfrak{S}_{j}|$, then $\varphi\in\pi(x)$ iff
$x\in\|\varphi\|_{\mathfrak{S}}$. We proceed by induction on the complexity of
$\varphi$. For the base case, suppose $p\in\pi(x)$. Then by the definition of
a dynamic $\Phi$-morphism we have $x\in\nu_{\mathfrak{S}}(p)$ as required. The
other direction follows similarly, and since the Boolean connectives follow by
standard arguments, then we focus on modalities.

If $\square\varphi\in\pi(x)$ and $y\sqsupset_{\mathfrak{S}}x$ then
$\pi(y)\sqsupset_{\mathrm{c}}\pi(x)$, so $\varphi\in\pi(y)$ and the induction
hypothesis and the fact that $y\in|\mathfrak{S}_{j}|$ (as $\mathfrak{S}_{j}$
is closed under $\sqsubset_{\mathfrak{S}}$) yields
$y\in\|\varphi\|_{\mathfrak{S}}$. Since $y$ was arbitrary,
$x\in\|\square\varphi\|_{\mathfrak{S}}$.

If $\lozenge\varphi\in\pi(x)$ then there exists $v\in W_{\rm c}$ such that
$\pi(x)\sqsubset_{\Phi}v$ and $\varphi\in v$. By the definition of a dynamic
$\Phi$-morphism there exists $v^{\prime}\in|{\mathfrak{S}}|$ such that
$x\sqsubset_{\mathfrak{S}}v^{\prime}$ and $v=\pi(v^{\prime})$. By the
induction hypothesis $v^{\prime}\in\|\varphi\|_{\mathfrak{S}}$ and thus
$x\in\|\lozenge\varphi\|_{\mathfrak{S}}$.

If $\bc\varphi\in\pi(x)$ then $\varphi\in g_{\rm c}(\pi(x))$. By the
definition of a dynamic $\Phi$-morphism we get $g_{\rm
c}(\pi(x))=\pi(f_{\mathfrak{S}}(x))$. Note that
$f_{\mathfrak{S}}(x)\in|\mathfrak{S}_{j+1}|$, but the $\bc$-depth of $\varphi$
is bounded by $I-j-1$. From the induction hypothesis we get
$f_{\mathfrak{S}}(x)\in\|\varphi\|_{\mathfrak{S}}$. Hence by definition
$x\in\|\bc\varphi\|_{\mathfrak{S}}$.

If $x\in\|\bc\varphi\|_{\mathfrak{S}}$, then
$f_{\mathfrak{S}}(x)\in\|\varphi\|_{\mathfrak{S}}$. The bound on $\bc$-depth
can be checked as above, so from the induction hypothesis it follows that
$\varphi\in\pi(f_{\mathfrak{S}}(x))$ and by the definition of a dynamic
$\Phi$-morphism we get $\pi(f_{\mathfrak{S}}(x))=g_{\rm c}(\pi(x))$. Therefore
$\bc\varphi\in\pi(x)$. ∎

We will next demonstrate that for every point $w$ in the canonical model,
there exists a suitable moment $\mathfrak{m}$ and a $\Phi$-morphism mapping
$\mathfrak{m}$ to $w$. In order to do this, we define a procedure for
constructing new moments from smaller ones.

######  Definition 6.5 (moment construction).

Let $\Lambda\in\\{\mathbb{wK4},\mathbb{K4},\mathbb{GL}\\}$ and
${C}^{\prime}\cup\\{x\\}\subseteq C(x)$ for some $x$ in the canonical model
$\mathfrak{M}^{\Lambda}_{\mathrm{c}}$. Let
$\vec{\mathfrak{a}}=\langle\mathfrak{a}_{m}\rangle_{m<N}$ be a sequence of
moments. We define a structure
${\mathfrak{n}}={{\vec{\mathfrak{a}}}\choose{C^{\prime}}}_{x}$ as follows:

  1. 1.

$|{\mathfrak{n}}|=C^{\prime}\sqcup\bigsqcup_{m<N}|\mathfrak{a}_{m}|;$

  2. 2.

$y\sqsubset_{\mathfrak{n}}z$ if either

     * •

$y,z\in C^{\prime}$, $\Lambda\neq\mathbb{GL}$ and $y\sqsubset_{\rm c}z$,

     * •

$y\in C^{\prime}$ and $z\in|\mathfrak{a}_{m}|$ for some $m$, or

     * •

$y,z\in|\mathfrak{a}^{m}|$ and $y\sqsubset_{\mathfrak{a}_{m}}z$ for some $m$;

  3. 3.

$\nu_{\mathfrak{n}}(p)=\\{x\in C^{\prime}:x\in\nu_{\rm
c}(p)\\}\sqcup\bigsqcup_{m<N}\nu_{\mathfrak{a}_{m}}(p)$;

  4. 4.

$r_{\mathfrak{n}}=x$.

Below, we denote by $C_{\Phi}(w)$ the $\sqsubset_{\Phi}$-cluster of $w$, i.e.

$C_{\Phi}(w)=\\{w\\}\cup\\{v:w\sqsubset_{\Phi}v\sqsubset_{\Phi}w\\}.$

lemmaexistsmoment Given
$\Lambda\in\\{\mathbf{wK4C},\mathbf{K4C},\mathbf{GLC}\\}$, for all $w\in
W_{\mathrm{c}}$ there exists a $\Lambda$-moment ${\mathfrak{m}}$ and a
$\Phi$-morphism $\pi\colon|{\mathfrak{m}}|\to W_{\mathrm{c}}$ such that
$\pi(r_{\mathfrak{m}})=w$.

###### Proof.

We prove the stronger claim, that there is a moment ${\mathfrak{m}}$ and a map
$\pi\colon|{\mathfrak{m}}|\to W_{\rm c}$ that is a $p$-morphism on the
structure $(W_{\rm c},\sqsubset_{\Phi})$ (we will say that $\pi$ is a
$p$-morphism with respect to $\sqsubset_{\Phi}$). Let $\sqsubset_{\Phi}^{1}$
be the strict $\sqsubset_{\Phi}$ successor, i.e. $w\sqsubset_{\Phi}^{1}v$ iff
$w\sqsubset_{\Phi}v$ and $\neg(v\sqsubset_{\Phi}w)$. Since
$\sqsubset_{\Phi}^{1}$ is converse well-founded, we can assume inductively
that for each $v$ such that $w\sqsubset_{\Phi}^{1}v$, there is a moment
${{\mathfrak{m}}_{v}}$ and a $p$-morphism
$\pi_{v}:|{{\mathfrak{m}}_{v}}|\rightarrow W_{\rm c}$ with respect to
$\sqsubset_{\Phi}$ that maps the root of ${{\mathfrak{m}}_{v}}$ to $v$.
Accordingly, we define a moment

${\mathfrak{m}}={\\{{{\mathfrak{m}}}_{v}:v\sqsupset_{\Phi}^{1}w\\}\choose
C_{\Phi}(w)}_{w};$

note that $C_{\Phi}(w)$ is finite and, if $\Lambda=\bf{GLC}$, it is a
singleton, so ${\mathfrak{m}}$ is a $\Lambda$-moment by Lemma A.3.

Next we define a map $\pi:|{\mathfrak{m}}|\rightarrow W$ as

$\pi(x)=\begin{cases}x&\text{if }x\in C_{\Phi}(w),\\\ \pi_{v}(x)&\text{if
}x\in|{\mathfrak{m}}_{v}|.\end{cases}$

We prove that $\pi$ is a $p$-morphism for $\sqsubset_{\Phi}$. First assume
that $\pi(x)\sqsubset_{\Phi}v$; we must show that there is
$y\sqsupset_{\mathfrak{m}}x$ so that $\pi(y)=v$. Either $x\in C_{\Phi}(w)$ or
$x\in|{\mathfrak{m}}_{u}|$ for some $u$. In the first case, we consider two
sub-cases. If $v\in C_{\Phi}(w)$ as well, then $\pi(v)=v$ and we may set
$y:=v$. If not, $\pi(x)\sqsubset_{\Phi}^{1}v$, and by letting $y$ be the root
of ${\mathfrak{m}}_{v}$, we see that $\pi(y)=v$. If instead
$x\in|{\mathfrak{m}}_{u}|$ for some $u$, then by assumption $\pi_{u}$ is a
$p$-morphism, immediately yielding the desired $y$ (also satisfying
$y\in|{\mathfrak{m}}_{u}|$).

Now, suppose $x\sqsubset_{\mathfrak{m}}y$. We check that
$\pi(x)\sqsubset_{\Phi}\pi(y)$. There are two cases to consider: First suppose
that $x\in|{\mathfrak{m}}_{u}|$ for some $u$ and $y\in|{\mathfrak{m}}_{v}|$
for some $v$. Then by the definition of the moment construction operation,
$u=v$. By the induction hypothesis, since $\pi_{u}$ is a $p$-morphism, then
$\pi(x)\sqsubset_{\Phi}\pi(y)$. Otherwise, suppose that $x\in C_{\Phi}(w)$. If
$y\in C_{\Phi}(w)$ we immediately obtain $\pi(x)\sqsubset_{\Phi}\pi(y)$, since
$C_{\Phi}(w)$ is precisely the $\sqsubset_{\Phi}$-cluster of $w$ (with the
same accessibility relation). Otherwise, $y\in|{\mathfrak{m}}_{v}|$ for some
$v$, and we let $y^{\prime}$ be the root of ${\mathfrak{m}}_{v}$, so that
$\pi(y^{\prime})=v$. Then, $\pi(x)\sqsubset_{\Phi}\pi(y^{\prime})$. If
$y=y^{\prime}$ we are done. If $y\neq y^{\prime}$, then since by the induction
hypothesis $\pi_{v}$ is a $p$-morphism with respect to $\sqsubset_{\Phi}$,
then $y^{\prime}\sqsubset y$ implies $\pi(y^{\prime})\sqsubset_{\Phi}\pi(y)$.
By the (weak) transitivity of $\sqsubset_{\Phi}$ we have that either
$\pi(x)\sqsubset_{\Phi}\pi(y)$ and we are done, or if $\Lambda=\bf wK4C$,
possibly $\pi(x)=\pi(y)$. But then, $\pi(y^{\prime})\sqsubset_{\Phi}\pi(x)$,
contradicting that $\pi(x)\sqsubset^{1}_{\Phi}\pi(y^{\prime})$. ∎

We next define the notions of _pre- $\Phi$-morphism_ and _quotient moment_
that will be essential for the rest of the proof.

######  Definition 6.6 (pre-$\Phi$-morphism, $\Lambda$-bottom).

Let ${\mathfrak{m}}$ be a moment and $\pi:|{\mathfrak{m}}|\rightarrow W_{\rm
c}$. We say that $x\in|{\mathfrak{m}}|$ is _at the $\Lambda$-bottom_ for
$\Lambda\in\\{\mathbb{wK4},\mathbb{K4},\mathbb{GL}\\}$ if

  * •

$\Lambda\neq\mathbb{GL}$ and $\pi(x)\in C(\pi(r_{{\mathfrak{m}}}))$, or

  * •

$\Lambda=\mathbb{GL}$ and for all $y\sqsubset_{\mathfrak{m}}x$,
$\pi(y)=\pi(x)$.

We will refer to ‘$\Lambda$-bottom’ simply as ‘bottom’ when this does not lead
to confusion.

We say that $\pi:|{\mathfrak{m}}|\rightarrow W_{\rm c}$ is a _pre-
$\Phi$-morphism_ if it fulfils conditions 1 and 4 of a $\Phi$-morphism
(Definition 6.4), and $x\sqsubset_{\mathfrak{m}}y$ implies that either
$\pi(x)\sqsubset_{\rm c}\pi(y)$ or $x,y$ are at the bottom.

######  Definition 6.7 (quotient moment).

Let $\Lambda\in\\{\mathbb{wK4C},\mathbb{K4C},\mathbb{GLC}\\}$. Let
${\mathfrak{m}}$ be a $\Lambda$-moment and $\pi:|{\mathfrak{m}}|\rightarrow
W_{\mathrm{c}}$ be a pre-$\Phi$-morphism. We define $x\sim y$ if either $x=y$,
or $x,y$ are at the bottom and $\pi(x)=\pi(y)$. Given $y\in|{\mathfrak{m}}|$
we set $[y]=\\{z:z\sim y\\}$.

The _quotient moment_ ${\mathfrak{m}}/\pi$ of ${\mathfrak{m}}$ and its
respective map $[\pi]:|{\mathfrak{m}}/\pi|\rightarrow W_{\rm c}$ are defined
as follows, where $x,y\in|{\mathfrak{m}}|$:

  1. (a)

$|{\mathfrak{m}}/\pi|=\\{[x]:x\in|{{\mathfrak{m}}}|\\}$;

  2. (b)

$[x]\sqsubset_{{\mathfrak{m}}/\pi}[y]$ iff one of the following conditions is
satisfied:

     * •

$x,y$ are at the bottom, $\pi(x)\sqsubset_{\rm c}\pi(y)$, and
$\Lambda\neq\mathbb{GLC}$;

     * •

$x$ is at the bottom and $y$ is not at the bottom;

     * •

$x,y$ are not at the bottom and $x\sqsubset_{\mathfrak{m}}y$;

  3. (c)

$\nu_{{\mathfrak{m}}/\pi}(p)=\\{[x]:x\in{\nu_{\mathfrak{m}}}(p)\\}$;

  4. (d)

$r_{{\mathfrak{m}}/\pi}=[r_{\mathfrak{m}}]$;

  5. (e)

$[\pi]([x])={\pi}(x)$.

The quotient moment and its respective map hold some essential properties for
the derivation of this section’s main result. The idea is that by constructing
a $\Lambda$-moment $m$ with an associated pre-$\Phi$-morphism $\pi$, we get
that ${\mathfrak{m}}/\pi$ is still a $\Lambda$-moment, but now $[\pi]$ is a
proper $\Phi$-morphism. The next few results make this intuition precise.

lemmapremor For $\Lambda\in\\{\mathbb{wK4},\mathbb{K4},\mathbb{GL}\\}$, if
${\mathfrak{m}}$ is any $\Lambda$-moment and $\pi:|{\mathfrak{m}}|\rightarrow
W_{\rm c}$ is a pre-$\Phi$-morphism, then ${\mathfrak{m}}/\pi$ is a
$\Lambda$-moment and $[\cdot]\colon|{\mathfrak{m}}|\to|{\mathfrak{m}}/\pi|$ is
weakly monotonic and root-preserving.

###### Proof.

For the cases where $\Lambda=\mathbb{wK4}$ and $\Lambda=\mathbb{K4}$ it is
easy to verify that $|{\mathfrak{m}}/\pi|$ is weakly transitive and transitive
respectively. For the case where $\Lambda=\mathbb{GL}$ suppose for
contradiction that $[x]\sqsubset_{{\mathfrak{m}}/\pi}[x]$. Then it must be the
case that $x$ is not at the bottom and $x\sqsubset_{\mathfrak{m}}x$ in
contradiction. ∎

propositionwelldefined If ${\mathfrak{m}}$ is a moment and
$\pi\colon|{\mathfrak{m}}|\to W_{\rm c}$ is a pre-$\Phi$-morphism, then the
map $[\pi]$ is a well-defined $\Phi$-morphism.

###### Proof.

To show that $[\pi]$ is well defined, suppose that for some
$x,y\in|{\mathfrak{m}}|$ we have $x\neq y$ and $[x]=[y]$. By definition of
$\sim$ it follows that $\pi(x)=\pi(y)$, as required. It remains to show that
$[x]\sqsubset_{{\mathfrak{m}}/\pi}[y]$ implies $[\pi]([x])\sqsubset_{\rm
c}[\pi]([y])$. Suppose $[x]\sqsubset_{{\mathfrak{m}}/\pi}[y]$. If both $x,y$
are at the bottom, then $[x]\sqsubset_{{\mathfrak{m}}/\pi}[y]$ may only occur
when $\pi(x)\sqsubset_{\rm c}\pi(y)$. If neither $x$ nor $y$ are at the bottom
then $[x]\sqsubset_{{\mathfrak{m}}/\pi}[y]$ may only occur when
$x\sqsubset_{{\mathfrak{m}}}y$, which implies that $\pi(x)\sqsubset_{\rm
c}\pi(y)$ since $\pi$ is a pre-$\Phi$-morphism. The case where $y$ is at the
bottom but $x$ is not is impossible by Lemma A.4. So we are left with the case
where $x$ is at the bottom but $y$ is not. But then
$\pi(x)=\pi(r_{\mathfrak{m}})\sqsubset_{\rm c}\pi(y)$, where
$\pi(r_{\mathfrak{m}})\sqsubset_{\rm c}\pi(y)$ is obtained from the definition
of pre-$\Phi$-morphism, using the fact that
$r_{\mathfrak{m}}\sqsubset_{\mathfrak{m}}y$ and $y$ is not at the bottom. We
conclude that $[\pi]$ satisfies Condition 3 of a $\Phi$-morphism.

For Condition 4, suppose that $[\pi]([x])\sqsubset_{\Phi}v$. Since
$[\pi]([x])=\pi(x)$, there is $y\sqsupset_{\mathfrak{m}}x$ such that
$\pi(y)=v$. Inspecting the definition of $\sqsubset_{{\mathfrak{m}}/\pi}$
yields that $[\pi]([x])\sqsubset_{{\mathfrak{m}}/\pi}$, except possibly when
$\Lambda=\bf{GLC}$ and $x,y$ are at the bottom. However, in this case we would
have $v=\pi(x)$, but $\sqsubset_{\Phi}$ is irreflexive, so this is impossible.
We conclude that Condition 4 is also satisfied. ∎

Using these properties, we can prove the existence of an appropriate story
that maps to the canonical model. This is based on the following useful lemma:

######  Lemma 6.8.

Fix $\Lambda\in\\{\mathbf{wK4C},\mathbf{K4C},\mathbf{GLC}\\}$ and let
$\mathfrak{M}^{\Lambda}_{\rm c}=\langle W_{\rm c},\sqsubset_{\rm c},g_{\rm
c},\nu_{\rm c}\rangle$. Let ${\mathfrak{m}}$ be a $\Lambda$-moment and suppose
that there exists a $\Phi$-morphism $\pi\colon|{\mathfrak{m}}|\to W_{\rm c}$.
Then, there exists a moment ${\mathfrak{n}}$, a weakly monotonic map
$f\colon|{\mathfrak{m}}|\to|{\mathfrak{n}}|$, and a $\Phi$-morphism
$\rho\colon|\hat{\mathfrak{n}}|\to W_{\rm c}$ such that $g_{\rm
c}\circ\pi=\rho\circ f$.

###### Proof.

We proceed by induction on the height of ${\mathfrak{m}}$. Let $C$ be the
cluster of $r_{\mathfrak{m}}$ and let
$\vec{\mathfrak{a}}=\langle\mathfrak{a}_{n}\rangle_{n<N}$ be the generated
sub-models of the immediate strict successors of $r_{\mathfrak{m}}$; note that
each $\mathfrak{a}_{n}$ is itself a moment of smaller height. By the induction
hypothesis, there exist moments
$\langle\mathfrak{a}^{\prime}_{n}\rangle_{n<N}$, root-preserving, weakly
monotonic maps $f_{n}\colon|\mathfrak{a}_{n}|\to|\mathfrak{a}^{\prime}_{n}|$,
and $\Phi$-morphism $\rho_{n}\colon|\mathfrak{a}^{\prime}_{n}|\to W_{\rm c}$
such that $g_{\rm c}\circ\pi_{n}=\rho_{n}\circ f_{n}$. Moreover, for each
$v\sqsupset_{\Phi}g_{\rm c}(r_{\mathfrak{m}})$, by Lemma 6 there are
$\mathfrak{b}_{v}$ and a $\Phi$-morphism $\rho_{v}\colon|\mathfrak{b}_{v}|\to
W_{\rm c}$ mapping the root of $\mathfrak{b}_{v}$ to $v$. Let $D=g_{\rm
c}\pi(C)\cup C_{\Phi}(g_{\rm c}(x))$, and let
$\hat{\mathfrak{n}}={\vec{\mathfrak{a}}*\vec{\mathfrak{b}}\choose D}_{g_{\rm
c}(w)}$. It is not difficult to verify that the maps $\rho_{v}$ can be used to
define a pre-$\Phi$-morphism $\hat{\rho}$ from $\hat{\mathfrak{n}}$ to $W_{\rm
c}$. Let

$\hat{f}(w)=\begin{cases}g_{\rm c}(w)&\text{if $w\in C$},\\\ f_{n}(w)&\text{if
$w\in|\mathfrak{a}_{n}|$}.\end{cases}$

It is easy to see that $\hat{f}\colon|{\mathfrak{m}}|\to|\hat{\mathfrak{n}}|$
is weakly monotonic and satisfies $g_{\rm c}\circ\pi=\hat{\rho}\circ\hat{f}$.
Setting ${\mathfrak{n}}=\hat{\mathfrak{n}}/\hat{\rho}$, $f=[\hat{f}]$ and
$\rho=[\hat{\rho}]$, Proposition 6.7 implies that ${\mathfrak{n}}$, $f$ and
$\rho$ have the desired properties.∎

propositionstoryexist Fix
$\Lambda\in\\{\mathbb{wK4C},\mathbb{K4C},\mathbb{GLC}\\}$. Given $I<\omega$
and $w\in W_{\rm c}$, there is a story $\mathfrak{S}$ of duration $I$ and a
dynamic $\Phi$-morphism $\pi\colon|\mathfrak{S}|\to W_{\rm c}$ with
$w=\pi(r_{\mathfrak{S}})$.

###### Proof.

Proceed by induction on $I$. For $I=0$, this is essentially Lemma 6.
Otherwise, by the induction hypothesis, assume that a story
$\hat{\mathfrak{S}}$ of depth $I$ and dynamic $p$-morphism $\hat{\pi}$ exist.
By Lemma A.6, there is a moment $\mathfrak{S}_{I+1}$, map
$f_{I}\colon|\mathfrak{S}_{I}|\to|\mathfrak{S}_{I+1}|$, and $\Phi$-morphism
$\pi_{I+1}\colon|\mathfrak{S}_{I+1}|\to W_{\rm c}$ commuting with $f_{I}$. We
define $\mathfrak{S}$ by adding $\mathfrak{S}_{I+1}$ to $\hat{\mathfrak{S}}$
in order to obtain the desired story. ∎

It follows that any satisfiable formula is also satisfiable on a finite story,
hence satisfiable on a finite model, yielding the main result of this section.

theoremmainkripke The logics $\mathbb{wK4C}$, $\mathbb{K4C}$ and
$\mathbb{GLC}$ are sound and complete for their respective class of finite
dynamic $\Lambda$-frames.

###### Proof.

Soundness follows from Lemma 3.8 and the well known soundness results reviewed
in Section 3. Let $\Lambda\in\\{\mathbb{wK4C},\mathbb{K4C},\mathbb{GLC}\\}$
and suppose $\Lambda\not\vdash\varphi$. Then in the canonical model
$\mathfrak{M}^{\Lambda}_{\rm c}=\langle W,\sqsubset,g,\nu\rangle$, there is
$w\in W$ that refutes $\varphi$. By the previous lemmas, there is a story
$\mathfrak{S}$ and a dynamic $\Phi$-morphism $\pi:|\mathfrak{S}|\rightarrow W$
such that $w=\pi(r)$, where $r$ is a root of $\mathfrak{S}$. It follows that
$\mathfrak{S},r\not\models\varphi$. Recall that $\mathfrak{S}$ is a finite
dynamic derivative frame. In the case of $\mathbb{K4C}$, $\mathfrak{S}$ is
also transitive, and in the case of $\mathbb{GLC}$, also transitive and
irreflexive. Then $\mathbb{wK4C}$ is complete with respect to finite dynamic
derivative frames, $\mathbb{K4C}$ with respect to finite, transitive, dynamic
derivative frames, and $\mathbb{GLC}$ is complete with respect to finite,
irreflexive, transitive dynamic derivative frames. ∎

##  7 Topological $d$-completeness

In this section we establish completeness results for classes of dynamic
topological systems with continuous functions. We begin with the logic
$\mathbb{GLC}$, simply because the topological $d$-completeness for
$\mathbb{GLC}$ is almost immediate, given that a $\mathbb{GLC}$ model is
already a dynamic derivative model based on a scattered space via the standard
up-set topology.

theoremscattered $\mathbb{GLC}$ is the $d$-logic of all dynamic topological
systems based on a scattered space, and enjoys the finite model property for
this class.

###### Proof.

Soundness follows from Theorem 3.7 and Lemma 3.8. For completeness, suppose
that $\not\vdash_{\mathbb{GLC}}\varphi$. Then by Theorem 6.8 there is a finite
model $\mathfrak{M}=\langle W,\sqsubset,g,\nu\rangle$ based on a transitive,
irreflexive dynamic derivative frame such that
$\mathfrak{M}\not\models\varphi$. But by Lemmas 2.6 and 3.6, setting
$\tau=\tau_{\sqsubset}$, we see that $d_{\tau}=d_{\sqsubset}$ and $\langle
W,\tau,f\rangle$ is a scattered dynamic topological system, which is identical
to $\mathfrak{M}$ as a dynamic derivative system and thus also refutes
$\varphi$. ∎

In order to prove topological $d$-completeness for $\mathbb{wK4C}$, we first
provide a definition and some generalisations of known results. We use similar
constructions as in e.g. [EsakiaAlgebra].

######  Definition 7.1.

A dynamic topological space $\mathcal{X}=\langle X,\tau,f\rangle$ is a
topological space $\mathcal{X}=\langle X,\tau\rangle$ with a continuous
function $f:X\rightarrow X$.

######  Definition 7.2.

Let $\mathfrak{F}=\langle W,\sqsubset,g\rangle$ be a $\mathbb{wK4C}$-frame and
let $W^{\mathrm{i}}$ and $W^{\mathrm{r}}$ be the sets of irreflexive and
reflexive points respectively. We define a new frame
$\mathfrak{F}_{\oplus}=\langle
W_{\oplus},\sqsubset_{\oplus},g_{\oplus}\rangle$, where

  1. 1.

$W_{\oplus}=(W^{\rm i}\times\\{0\\})\cup(W^{\rm r}\times\\{0,1\\})$;

  2. 2.

$(w,i)\sqsubset_{\oplus}(v,j)$ iff $w\sqsubset v$ and $(w,i)\neq(v,j)$;

  3. 3.

$g_{\oplus}(w,i)=(g(w),0)$.

The following is standard [EsakiaAlgebra] and easily verified.

######  Proposition 7.3.

If $\mathfrak{F}=\langle W,\sqsubset,g\rangle$ is any dynamic derivative
frame, then $\mathfrak{F}_{\oplus}$ is an irreflexive dynamic derivative frame
and $\pi\colon W_{\oplus}\to W$ given by $\pi(w,i)=w$ is a surjective, dynamic
$p$-morphism.

Proposition 7.3 allows us to obtain topological completeness from Theorem 6.8,
as Lemma 2.6 tells us that irreflexive Kripke frames are essentially Cantor
derivative spaces. We thus obtain the following:

theoremtopowkc $\mathbb{wK4C}$ is the $d$-logic of all dynamic topological
systems, and enjoys the finite model property for this class.

###### Proof.

Soundness follows from Lemma 3.8. For completeness, suppose
$\mathbb{wK4C}\not\vdash\varphi$. Then by Theorem 6.8 there exists a finite
$\mathbb{wK4C}$-frame $\mathfrak{F}=\langle W,\sqsubset,g\rangle$ such that
$\mathfrak{F}\not\models\varphi$. But then, by Proposition 7.3,
$\mathfrak{F}_{\oplus}=\langle
W_{\oplus},\sqsubset_{\oplus},g_{\oplus}\rangle$ is an irreflexive dynamic
derivative system and $\pi\colon W_{\oplus}\to W$ is a surjective, dynamic
$p$-morphism. But by Lemma 2.6 and by setting $\tau=\tau_{\sqsubset}$ we see
that $d_{\sqsubset}=d_{\tau}$, so $\mathfrak{F}_{\oplus}$ can be seen as a
dynamic topological system with the same semantics, also falsifying $\varphi$.
∎

Finally we turn our attention to $\mathbb{K4C}$. Unlike the other two logics,
$\mathbb{K4C}$ (or even $\mathbb{K4}$) does not have the topological finite
model property, despite having the Kripke finite model property. In the case
of Aleksandroff spaces, the class $T_{D}$ is easy to describe.

######  Lemma 7.4.

The Aleksandroff space of a $\mathbb{K4}$-frame $\mathfrak{F}=\langle
W,\sqsubset\rangle$ is $T_{D}$ if and only if $\sqsubset$ is antisymmetric, in
the sense that $w\sqsubset v\sqsubset w$ implies $w=v$.

If we moreover want the Kripke and the $d$-semantics to coincide on
$\mathfrak{F}$, we need $\sqsubset$ to be irreflexive. Thus we wish to
‘unwind’ $\mathfrak{F}$ to get rid of all non-trivial clusters. The following
construction achieves this.

######  Definition 7.5.

Let $\mathfrak{F}=\langle W,\sqsubset,g\rangle$ be a dynamic $\mathbb{K4}$
frame. We define a new frame
$\vec{\mathfrak{F}}=\langle\vec{W},\vec{\sqsubset},\vec{g}\rangle,$ where

  * •

$\vec{W}$ is the set of all finite sequences $(w_{0},\ldots,w_{n})$, where
$w_{i}\sqsubset w_{i+1}$ for all $i<n$;

  * •

$\mathbb{w}\mathrel{\vec{\sqsubset}}\mathbb{v}$ iff $\mathbb{w}$ is a strict
initial segment of $\mathbb{v}$;

  * •

$\vec{g}(w_{0},\ldots,w_{n})$ is the subsequence of
$(g(w_{0}),\ldots,g(w_{n}))$, obtained by deleting every entry that is equal
to its immediate predecessor.

We moreover define a map $\pi\colon\vec{W}\to W$, where
$\pi(w_{0},\ldots,w_{n})=w_{n}$.

In the definition of $\vec{g}$, note that $g$ is only weakly monotonic, so it
may be that, for instance, $g(w_{0})=g(w_{1})$; in this case, we include only
one copy of $g(w_{0})$ to ensure that $\vec{g}(\mathbb{w})\in\vec{W}$.

propositionwind If $\mathfrak{F}=\langle W,\sqsubset,g\rangle$ is any dynamic
$\mathbb{K4}$ frame, then $\vec{\mathfrak{F}}$ is an antisymmetric and
irreflexive dynamic $\mathbb{K4}$ frame. Moreover, $\pi\colon\vec{W}\to W$ is
a surjective, dynamic $p$-morphism.

###### Proof.

It is easy to see that $\vec{\mathfrak{F}}$ is antisymmetric and irreflexive.
In order to show that $\vec{\mathfrak{F}}$ is a dynamic $\mathbb{K4}$ frame we
need to show that it is transitive and $\vec{g}$ is a weakly monotonic
function. Suppose
$\mathbb{w}\vec{\sqsubset}\mathbb{v}\vec{\sqsubset}\mathbb{u}$, then clearly
since $\mathbb{w}$ is an initial segment of $\mathbb{v}$, it is also an
initial segment of $\mathbb{u}$ and therefore
$\mathbb{w}\vec{\sqsubset}\mathbb{u}$ and thus $\vec{\sqsubset}$ is
transitive. The functionality of $\vec{g}$ follows from the functionality of
$g$, and weak monotonicity can be checked from the definitions unsing the weak
monotonicity of $g$. Finally, we show that $\pi$ is a surjective $p$-morphism.
It is clearly surjective. Next, we note that if ${\bf w}\vec{\sqsubset}{\bf
v}$ then transitivity plus $w_{n}=v_{n}$ yields $w_{n}\sqsubset v_{i}$ for all
$i\in(n,m]$, and in particular $w_{n}\sqsubset v_{m}$, that is, $\pi({\bf
w})\sqsubset\pi({\bf v})$. Moreover, if $\pi({\bf w})\sqsubset u$, then
$w_{n}\sqsubset u$ by definition of $\pi$, which means that ${\bf
u}:=(w_{1},\ldots,w_{n},u)\in\vec{W}$ is such that ${\bf
w}\mathrel{\vec{\sqsubset}}{\bf u}$ and $\pi({\bf u})=u$. Furthermore,
$\pi(\vec{g}(w_{0},\dots,w_{n}))=g(w_{n})=g(\pi(w_{0},\dots w_{n}))$ and thus
$\pi$ is a $p$-morphism. ∎

Similar constructions have already appeared in e.g. [konev]. From this we
obtain the following:

theoremtopokc $\mathbb{K4C}$ is the $d$-logic of the class of all dynamic
topological systems based on a $T_{D}$ space, as well as the $d$-logic of the
class of all dynamic topological systems based on an Aleksandroff $T_{D}$
space.

###### Proof.

Soundness follows from soundness for $\mathbb{wK4C}$ and Lemma 7.4. For
completeness, if $\mathbb{K4C}\not\vdash\varphi$, by Theorem 6.8 there is a
$\mathbb{K4C}$ model $\mathfrak{M}=\langle W,\sqsubset,g,V\rangle$ falsifying
$\varphi$. Let $\mathfrak{F}=\langle W,\sqsubset,g\rangle$. But by Proposition
7.5, $\pi\colon\vec{W}\to W$ is a surjective $p$-morphism, which implies that
$\varphi$ is not valid on $\vec{\mathfrak{F}}$. By Proposition 7.5,
$\vec{\sqsubset}$ is antisymmetric, hence by Lemma 7.4, the Aleksandroff
topology of $\vec{\mathfrak{F}}$ is $T_{D}$; moreover, $\vec{\sqsubset}$ is
also irreflexive, so we see that $\varphi$ is falsified on this $T_{D}$
Aleksandroff space as well. ∎

##  8 Invertible Systems

Recall that if $\langle X,\tau\rangle$ is a topological space and $f\colon
X\to X$ is a function, then $f$ is a homeomorphism if it is a bijection and
both $f$ and $f^{-1}$ are continuous.

Unlike in the continuous case, for logics with homeomorphisms, every formula
is equivalent to a formula where all occurrences of $\bc$ are applied to
atoms. More formally, we say that a formula is in $\bc$-normal form if it is
of the form $\varphi(\bc^{k_{0}}p_{0},\ldots,\bc^{k_{n}}p_{n})$, where
$\varphi(p_{0},\ldots,p_{n})$ does not contain $\bc$, the $p_{i}$’s are
variables, and the $k_{i}$’s are natural numbers. It is readily observed that
the axiom H allows us to ‘push’ all instances of $\bc$ to the propositional
level. Thus we obtain the following useful representation lemma:

lemmabcnormal For every logic $\Lambda$ and every formula $\varphi$, there is
a formula $\varphi^{\prime}$ in $\bc$-normal form such that $\Lambda{\bf
H}\vdash\varphi\leftrightarrow\varphi^{\prime}$.

###### Proof.

This is a standard proof by induction on the complexity of $\varphi$. In
particular, note that the axioms $\square\bc p\rightarrow\bc\square p$ and
$\bc\square p\rightarrow\square\bc p$ permit the interchangeability between
$\bc$ and $\square$, thus allow us to push $\bc$ towards the atomic part of
the formula. ∎

As we shall see shortly, $\Lambda{\bf H}$ inherits completeness and the finite
model property almost immediately from $\Lambda$. If $\mathfrak{X}=\langle
X,\rho_{X}\rangle$ and $\mathfrak{Y}=\langle Y,\rho_{Y}\rangle$ are derivative
spaces, then the topological sum is defined as
$\mathfrak{X}\oplus\mathfrak{Y}=(X\oplus Y,\rho_{X}\oplus\rho_{Y})$, where
$X\oplus Y$ is the disjoint union of the two sets, and
$\rho_{X}\oplus\rho_{Y}$ is given by $(\rho_{X}\oplus\rho_{Y})A=\rho_{X}(A\cap
X)\cup\rho_{Y}(A\cap Y)$. We say that a class $\Omega$ of derivative spaces is
closed under sums if whenever $\mathfrak{A},\mathfrak{B}\in\Omega$, it follows
that $\mathfrak{A}\oplus\mathfrak{B}\in\Omega$.

Given a derivative space $\mathfrak{A}=\langle A,\rho\rangle$, we may write
$\mathfrak{A}^{n}$ instead of
$\mathfrak{A}\oplus\mathfrak{A}\oplus\ldots\oplus\mathfrak{A}$ ($n$ times),
and if $\mathfrak{A}$ has domain $A$, we may identify the domain of
$\mathfrak{A}^{n}$ with $A^{n}=A\times\\{0,\ldots,n-1\\}$. It should be clear
that if $\mathfrak{A}\in\Omega$ and $\Omega$ is closed under sums, then
$\mathfrak{A}^{n}\in\Omega$. Let $(m)_{n}$ denote the remainder of $m$ modulo
$n$. We then define a dynamical structure
$\mathfrak{A}^{(n)}=(\mathfrak{A}^{n},f)$, where $f\colon A^{n}\to A^{n}$ is
given by $f(w,i)=(w,(i+1)_{n})$.

lemmainvert Let $\Omega$ be a class of derivative spaces closed under sums.
Then, if $\mathfrak{A}\in\Omega$, it follows that $\mathfrak{A}^{(n)}$ is an
invertible dynamic derivative system based on an element of $\Omega$.

###### Proof.

Suppose $\mathfrak{A}=\langle X,d\rangle\in\Omega$ is a derivative space. Let
$\mathfrak{A}^{(n)}=(X^{n},d^{\prime},f)$. Clearly $f$ is a bijection as it
defines disjoint cycles. If $Y\subseteq X^{n}$, let $Y_{i}=\\{x\in X:(x,i)\in
Y\\}$. Then,
$d^{\prime}f^{-1}Y=\bigcup_{i<n}(dY_{i},(i-1)_{n})=f^{-1}\bigcup_{i<n}(dY_{i},i)=f^{-1}d^{\prime}Y$.
So, $\mathfrak{A}^{(n)}$ is a dynamic derivative frame. ∎

For our proof of completeness, we need the notion of extended valuation.

######  Definition 8.1.

Let $\mathfrak{A}=\langle A,\rho\rangle$ be a derivative space. Let
$\mathsf{PV}^{\bc}$ be the set of all expressions $\bc^{i}p$, where
$i\in\mathbb{N}$ and $p$ is a propositional variable. An extended valuation on
$\mathfrak{A}$ is a relation $\nu\subseteq\mathsf{PV}^{\bc}\times A$.

If $\nu$ is an extended valuation on $\mathfrak{A}$, we define a valuation on
$\mathfrak{A}^{(n)}$ so that for any variable $p$ and $(w,i)\in A^{n}$,
$(w,i)\in\nu^{(n)}(p)$ if and only if $w\in\nu(\bc^{i}p)$.

lemmanpreserve Let $\mathfrak{A}=\langle A,\rho\rangle$ be any derivative
space and $\nu$ be any extended valuation on $\mathfrak{A}$. Let $w\in A$,
$i<n$, and $\varphi$ be any formula in $\bc$-normal form which has $\bc$-depth
less than $n-i$. Then,
$\langle\mathfrak{A}^{(n)},\nu^{(n)}\rangle,(w,i)\models\varphi$ if and only
if $\langle\mathfrak{A},\nu\rangle,w\models\varphi.$

###### Proof.

We start with the right to left direction and we only show the case where
$\varphi=\bc\psi$. Since $\varphi$ is in $\bc$-normal form then it is of the
form $\bc^{j}p$. Since $j<n-i$ and by definition $(w,j)\in\nu^{(n)}p$, then
$\langle\mathfrak{A}^{(n)},\nu^{(n)}\rangle,(w,i)\models\bc^{j}p$. The other
direction follows similarly. The rest of the modalities and connectives follow
by a standard induction on the build of $\varphi$. ∎

It then readily follows that $\varphi$ is consistent if and only if
$\varphi^{\prime}$ is consistent, which implies that $\varphi^{\prime}$ is
satisfiable on $\Omega$. This is equivalent to $\varphi$ being satisfiable on
the class of invertible systems based on $\Omega$. From this, we obtain the
following general result.

theoremtopoh Let $\Lambda$ be complete for a class $\Omega$ of derivative
spaces. Then, if $\Omega$ is closed under sums, it follows that $\Lambda{\bf
H}$ is complete for the class of invertible systems based on $\Omega$.

###### Proof.

Assume that $\Lambda$ and $\Omega$ are as in the statement of the theorem. Let
$\varphi$ be any formula, and using Lemma 8, let $\varphi^{\prime}$ be a
$\Lambda{\bf H}$-equivalent formula in $\bc$-normal form. Let $n$ be the
$\bc$-depth of $\varphi^{\prime}$. If $\varphi$ is consistent, then
$\varphi^{\prime}$ is consistent over $\Lambda$. By the assumption,
$\varphi^{\prime}$ is satisfied on some $\mathfrak{A}=\langle
A,\rho\rangle\in\Omega$. Suppose it is satisfied on a point $w_{*}\in A$. By
Lemma 8, $\mathfrak{A}^{(n)}$ is an invertible system based on an element of
$\Omega$, which by Lemma 8.1 satisfies $\varphi^{\prime}$ on $(w_{*},0)$. But
$\Lambda{\bf H}$ is sound for the class of invertible systems based on
$\Omega$, hence $\varphi$ is also satisfied on $(w_{*},0)$. ∎

######  Corollary 8.2.

  1. 1.

$\bf wK4H$ is sound and complete for

    1. (a)

The class of all finite invertible dynamic $\bf wK4$ frames.

    2. (b)

The class of all finite invertible dynamic topological systems with Cantor
derivative.

  2. 2.

$\bf K4H$ is sound and complete for

    1. (a)

The class of all finite invertible dynamic $\bf K4$ frames.

    2. (b)

The class of all invertible, $T_{D}$ dynamic topological systems with Cantor
derivative.

  3. 3.

$\bf GLH$ is sound and complete for

    1. (a)

The class of all finite invertible dynamic $\bf GL$ frames.

    2. (b)

The class of all finite invertible, scattered dynamic topological systems with
Cantor derivative.

##  9 Conclusion

We have recast dynamic topological logic in the more general setting of
derivative spaces and established the seminal results for the
$\\{\lozenge,\bc\\}$-fragment for the variants of the standard logics with the
Cantor derivative in place of the topological closure. Semantics on the Cantor
derivative give rise to a richer family of modal logics than their
counterparts based on closure. This is evident in the distinction between e.g.
the logics $\mathbf{wKC}$ and $\mathbf{K4C}$, both of which collapse to
$\mathbf{S4C}$ when replaced by their closure-based counterparts. This line of
research goes hand in hand with recent trends that consider the Cantor
derivative as the basis of topological semantics [FernandezIliev, Kudinov].

There are many natural problems that remain open. The logic $\mathbf{S4C}$ is
complete for the Euclidean plane. In the context of $d$-semantics, the logic
of the Euclidean plane is a strict extension of $\mathbf{K4}$, given that
punctured neighbourhoods are connected in the sense that they cannot be split
into two disjoint, non-empty open sets. Thus one should not expect
$\mathbf{K4C}$ to be complete for the plane. This raises the question: what is
the dynamic $d$-logic of Euclidean spaces in general, and of the plane in
particular?

The $d$-semantics also poses new lines of inquiry with respect to the class of
functions considered. We have discussed continuous functions and
homeomorphisms. Artemov et al. [artemov] also considered arbitrary functions,
and we expect that the techniques used by them could be modified without much
issue for $d$-semantics. On the other hand, in the setting of closure-based
logics, the logic of spaces with continuous, open maps that are not
necessarily bijective coincides with the logic of spaces with a homeomorphism.
This is no longer true in the $d$-semantics setting, as the validity of the
$\rm H$ axiom requires injectivity. Along these lines, the $d$-logic of
immersions (i.e. continuous, injective functions) would validate the original
continuity axiom $\bc\square p\to\square\bc p$. Thus there are several classes
of dynamical systems whose closure-based logics coincide, but are split by
$d$-semantics.

Finally, there is the issue of extending our language to the trimodal language
with the ‘henceforth’ operator. It is possible that the $d$-logic of all
dynamic topological systems may be axiomatised using the tangled derivative,
much as the tangled closure was used to provide an axiomatisation of the
closure-based $\mathbf{DTL}$. However, given that the tangled derivative is
made trivial on scattered spaces, we conjecture that the trimodal $d$-logic
based on this class will enjoy a natural, finite axiomatisation. The work
presented here is an important first step towards proving this.

## References

  * [1] S. Artemov, J. Davoren, and A. Nerode.  Modal logics and topological semantics for hybrid systems.  Technical Report MSI 97-05, 1997.
  * [2] Patrick Blackburn, Maarten de Rijke, and Yde Venema.  Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Scie.  Cambridge University Press, Cambridge, 2001.
  * [3] George Boolos.  The logic of provability.  The American Mathematical Monthly, 91(8):470–480, 1984.  arXiv:https://doi.org/10.1080/00029890.1984.11971467, doi:10.1080/00029890.1984.11971467.
  * [4] Steven L Brunton and J Nathan Kutz.  Data-driven science and engineering: Machine learning, dynamical systems, and control.  Cambridge University Press, 2019.
  * [5] Moody T Chu.  Linear algebra algorithms as dynamical systems.  Acta Numerica, 17:1–86, 2008.
  * [6] L. Esakia.  Weak transitivity–restitution.  In Nauka, editor, Study in Logic, volume 8, pages 244–254, 2001\.  In Russian.
  * [7] Leo Esakia.  Diagonal constructions, Löb’s formula and Cantor’s scattered spaces.  Studies in logic and semantics, 132(3):128–143, 1981.
  * [8] Leo Esakia.  Intuitionistic logic and modality via topology.  Ann. Pure Appl. Log., 127(1-3):155–170, 2004.  doi:10.1016/j.apal.2003.11.013.
  * [9] D. Fernández-Duque.  Non-finite axiomatizability of dynamic topological logic.  ACM Transactions on Computational Logic, 15(1):4:1–4:18, 2014\.  URL: http://doi.acm.org/10.1145/2489334, doi:10.1145/2489334.
  * [10] David Fernández-Duque.  Tangled modal logic for spatial reasoning.  In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 857–862. IJCAI/AAAI, 2011.  doi:10.5591/978-1-57735-516-8/IJCAI11-149.
  * [11] David Fernández-Duque and Petar Iliev.  Succinctness in subsystems of the spatial $\mu$-calculus.  Journal of Applied Logics, 5(4):827–874, 2018.
  * [12] David Fernández-Duque.  A sound and complete axiomatization for dynamic topological logic.  The Journal of Symbolic Logic, 77(3):947–969, 2012.  doi:10.2178/jsl/1344862169.
  * [13] R. Goldblatt and I. Hodkinson.  Spatial logic of tangled closure operators and modal mu-calculus.  Annals of Pure and Applied Logic, 168(5):1032 – 1090, 2017.
  * [14] Guillaume Hanrot, Xavier Pujol, and Damien Stehlé.  Analyzing blockwise lattice algorithms using dynamical systems.  In Annual Cryptology Conference, pages 447–464. Springer, 2011\.
  * [15] B. Konev, R. Kontchakov, F. Wolter, and M. Zakharyaschev.  Dynamic topological logics over spaces with continuous functions.  In G. Governatori, I. Hodkinson, and Y. Venema, editors, Advances in Modal Logic, volume 6, pages 299–318, London, 2006. College Publications.
  * [16] Boris Konev, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev.  On dynamic topological and metric logics.  Studia Logica, 84(1):129–160, 2006.  doi:10.1007/s11225-006-9005-x.
  * [17] P. Kremer and G. Mints.  Dynamic topological logic.  Annals of Pure and Applied Logic, 131:133–158, 2005.
  * [18] Andrey Kudinov.  Topological modal logics with difference modality.  In Guido Governatori, Ian M. Hodkinson, and Yde Venema, editors, Advances in Modal Logic 6, pages 319–332. College Publications, 2006.  URL: http://www.aiml.net/volumes/volume6/Kudinov.ps.
  * [19] Hai Lin and Panos J. Antsaklis.  Hybrid dynamical systems: An introduction to control and verification.  Found. Trends Syst. Control, 1(1):1–172, March 2014.  doi:10.1561/2600000001.
  * [20] J.C.C. McKinsey and A. Tarski.  The algebra of topology.  Annals of Mathematics, 2:141–191, 1944.
  * [21] Henning S. Mortveit and Christian M. Reidys.  An Introduction to Sequential Dynamical Systems.  Springer-Verlag, Berlin, Heidelberg, 2007.
  * [22] A. Pnueli.  The temporal logic of programs.  In Proceedings 18th IEEE Symposium on the Foundations of CS, pages 46–57, 1977.
  * [23] H. Simmons.  Topological aspects of suitable theories.  Proceedings of the Edinburgh Mathematical Society, 19(4):383–391, 1975.  doi:10.1017/S001309150001049X.
  * [24] Craig Smorynski.  Self-reference and modal logic.  Springer, 1985.
  * [25] E Weinan.  A proposal on machine learning via dynamical systems.  Communications in Mathematics and Statistics, 5(1):1–11, 2017.

##  Appendix A Appendix

######  Lemma A.1 (Zorn’s Lemma).

Let $(A,\leq)$ be a preordered set where $A$ is non-empty. A chain is a subset
$\mathcal{C}\subseteq A$ whose elements are totally ordered by $\leq$. Suppose
that every chain $\mathcal{C}$ has an upper bound in $A$. Then, $A$ has a
$\leq$-maximal element.

######  Lemma A.2.

If $\lozenge\varphi\in w$, then there is $\varphi$-final point $v$ such that
$w\sqsubset_{\rm c}v$.

###### Proof.

Suppose that $\mathcal{C}$ is an $\sqsubseteq_{\rm c}$-chain in
$A:={\sqsubset_{\rm c}}(w)\cap\|\varphi\|$ (where ${\sqsubset_{\rm
c}}(w)=\\{v\in W_{\rm c}:w\sqsubset_{\rm c}v\\}$). We show that there is an
upper bound of $\mathcal{C}$ that belongs to $A$.

Choose a formula $\theta$ as follows: If $w$ is an irreflexive world (i.e.
$w\not\sqsubset_{\rm c}w$), then choose $\theta$ so that
$\square\theta\wedge\neg\theta\in w$. Otherwise, $w$ is reflexive and we
simply set $\theta=\top$. Let $\Gamma$ be the set

$\\{\boxdot\psi:\exists x\in\mathcal{C}(\boxdot\psi\in x)\\}.$

Suppose $\boxdot\psi_{1},\dots,\boxdot\psi_{n}\in\Gamma$. For each $i$ there
is $w_{i}\in\mathcal{C}$ such that $\boxdot\psi_{i}\in w_{i}$. Since
$\mathcal{C}$ is a chain, for some $j$ we have that
$w_{j}=\max_{i=1}^{n}w_{i}$. Then,
$\varphi,\theta,\boxdot\psi_{1},\dots,\boxdot\psi_{n}\in w_{j}$, hence
$\\{\varphi,\theta,\boxdot\psi_{1},\dots,\boxdot\psi_{n}\\}$ is consistent.
Since $\\{\boxdot\psi_{1},\dots,\boxdot\psi_{n}\\}$ is an arbitrary finite
subset of $\Gamma$, we have that $\Gamma\cup\\{\varphi,\theta\\}$ is
consistent.

By the Lindenbaum lemma we can extend $\Gamma\cup\\{\varphi,\theta\\}$ to an
MCS, which we denote by $w^{*}$. Suppose $\boxdot\psi\in v\in\mathcal{C}$,
then by construction $\boxdot\psi\in w^{*}$. It follows by Lemma 5.1 that
$v\sqsubseteq_{\rm c}w^{*}$. Hence $w^{*}$ is an upper bound for
$\mathcal{C}$. Note that the assumption that $\lozenge\varphi\in w$ implies
that there is some $v\sqsupset_{\rm c}w$ such that $\varphi\in v$, that is,
$v\in A$. Hence $w\sqsubset_{\rm c}v\sqsubseteq_{\rm c}w^{*}$, which yields
$w\sqsubseteq_{\rm c}w^{*}$. To see that indeed $w\sqsubset_{\rm c}w^{*}$, if
$w$ is reflexive there is nothing to prove, otherwise since $\theta\in w^{*}$
we have that $w\neq w^{*}$. Moreover $\varphi\in w^{*}$ by construction, so
$w^{*}\in A$.

Thus, by Lemma A.1 we conclude that $A$ contains a maximal element, and this
maximal element is clearly a $\varphi$-final point above $w$. ∎

######  Lemma A.3.

Let $\Lambda\in\\{\mathbb{wK4},\mathbb{K4},\mathbb{GL}\\}$ and
${C}^{\prime}\subseteq C(x)$ for some $x$ in the canonical model
$\mathfrak{M}^{\Lambda}_{\mathrm{c}}$, where $C^{\prime}$ is a singleton if
$\Lambda=\mathbb{GL}$ and finite otherwise. Let
$\vec{\mathfrak{a}}=\langle\mathfrak{a}^{m}\rangle_{m<N}$ be a sequence of
$\Lambda$-moments. Then, ${\vec{\mathfrak{a}}\choose C}_{x}$ is a
$\Lambda$-moment.

###### Proof.

If $\Lambda=\mathbb{wK4}$ then $\sqsubset$ is easily seen to be weakly
transitive since each $\mathfrak{a}_{i}$ is weakly transitive and the root
sees all other points. The transitivity of $\sqsubset$ where
$\Lambda\supseteq\mathbb{K4}$ follows by the same reasoning. The irreflexivity
of $\sqsubset$ where $\Lambda=\mathbb{GL}$ follows from the fact that
$C^{\prime}$ is an irreflexive singleton and each $\mathfrak{a}_{i}$ is
irreflexive. ∎

######  Proposition A.4.

Let ${\mathfrak{m}}$ be a moment and $\pi:|{\mathfrak{m}}|\rightarrow
W_{\mathrm{c}}$ be a pre-$\Phi$-morphism. Let $x,y\in|{\mathfrak{m}}|$. If $x$
is at the $\Lambda$-bottom and $y\sqsubset_{\mathfrak{m}}x$, then $y$ is at
the $\Lambda$-bottom.

###### Proof.

Suppose $\Lambda\neq\mathbb{GLC}$. If $x$ is at the bottom, we have that
$\pi(x)\in C(\pi(r_{\mathfrak{m}}))$. If moreover
$y\sqsubset_{\mathfrak{m}}x$, then since $\pi$ is a pre-$\Phi$-morphism, we
have that either $\pi(y)\sqsubset_{\rm c}\pi(x)$ or $y$ is at the bottom. In
the latter case there is nothing to prove. Otherwise,
$r_{\mathfrak{m}}\sqsubset_{\mathfrak{m}}y\sqsubset_{\mathfrak{m}}x$ and $y$
is not at the bottom. Then $\pi(r_{\mathfrak{m}})\sqsubset_{\rm
c}\pi(y)\sqsubset_{\rm c}\pi(x)$ and hence $\pi(y)\in C(r_{\mathfrak{m}})$.
This is a contradiction and so $y$ is at the bottom.

Suppose $\Lambda=\mathbb{GLC}$. Then by the transitivity of
$\sqsubset_{\mathfrak{m}}$ it follows that $y$ is also at the bottom. ∎

######  Proposition A.5.

Fix $\Lambda\in\\{\mathbf{wK4C},\mathbf{K4C},\mathbf{GLC}\\}$ and let
$\mathfrak{M}^{\Lambda}_{\rm c}=\langle W,\sqsubset,g,\nu\rangle$. Let
${\mathfrak{m}}$ and ${\mathfrak{n}}$ be moments,
$f\colon|{\mathfrak{m}}|\to|{\mathfrak{n}}|$ be root-preserving, weakly
monotonic, and $\pi\colon|{\mathfrak{m}}|\to W$ and
$\rho\colon|{\mathfrak{n}}|\to W$ be such that $\pi$ is a $\Phi$-morphism,
$\rho$ is a pre-$\Phi$-morphism, and $g\circ\pi=\rho\circ f$. Let $[f]$ be
given by $[f](x)=[f(x)]$. Then,
$[f]\colon|{\mathfrak{m}}|\to|{\mathfrak{n}}/\rho|$ is weakly monotonic and
satisfies $g\circ\pi=[\rho]\circ[f]$.

###### Proof.

Checking that $g\circ\pi=[\rho]\circ[f]$ is routine. We show that $[f]$ is
weakly monotonic. Suppose that $x\sqsubset_{{\mathfrak{m}}}y$. Then,
$f(x)\sqsubseteq_{\mathfrak{n}}f(y)$. By Proposition A.4, if $f(y)$ is at the
bottom, so is $f(x)$. Thus in order to prove that
$[f(x)]\sqsubseteq_{{\mathfrak{n}}/\rho}[f(y)]$, there are three cases to
consider. If $f(x),f(y)$ are at the bottom, either $\pi(f(x))=\pi(f(y))$, so
that $[f(x)]=[f(y)]$, or else $\Lambda\neq\mathbf{GLC}$ and
$\pi(f(x))\sqsubset_{\mathrm{c}}\pi(f(y))$, hence
$[f(x)]\sqsubset_{{\mathfrak{n}}/\rho}[f(y)]$ by definition of
$\sqsubset_{{\mathfrak{n}}/\rho}$. If $f(x)$ is at the bottom and $f(y)$ is
not at the bottom, then by definition
$[f(x)]\sqsubset_{{\mathfrak{n}}/\rho}[f(y)]$. If neither is at the bottom,
$f(x)\sqsubset_{{\mathfrak{n}}}f(y)$ yields
$[f(x)]\sqsubset_{{\mathfrak{n}}/\rho}[f(y)]$. In all cases we have that
$[f(x)]\sqsubseteq_{{\mathfrak{n}}/\rho}[f(y)]$. ∎

######  Lemma A.6.

Fix $\Lambda\in\\{\mathbf{wK4C},\mathbf{K4C},\mathbf{GLC}\\}$ and let
$\mathfrak{M}^{\Lambda}_{\rm c}=\langle W,\sqsubset,g,\nu\rangle$. Let
${\mathfrak{m}}$ be a $\Lambda$-moment and suppose that there exists a
$\Phi$-morphism $\pi\colon|{\mathfrak{m}}|\to W$. Then, there exists a moment
${\mathfrak{n}}$, a weakly monotonic map
$f\colon|{\mathfrak{m}}|\to|{\mathfrak{n}}|$, and a $\Phi$-morphism
$\rho\colon|\hat{\mathfrak{n}}|\to W$ such that $g\circ\pi=\rho\circ f$.

###### Proof.

We proceed by induction on the height of ${\mathfrak{m}}$. Let $C$ be the
cluster of $r_{\mathfrak{m}}$ and let
$\vec{\mathfrak{a}}=\langle\mathfrak{a}_{n}\rangle_{n<N}$ be the generated
sub-models of the immediate strict successors of $r_{\mathfrak{m}}$; note that
each $\mathfrak{a}_{n}$ is itself a moment of smaller height. By the induction
hypothesis, there exist moments
$\langle\mathfrak{a}^{\prime}_{n}\rangle_{n<N}$, root-preserving, weakly
monotonic maps $f_{n}\colon|\mathfrak{a}_{n}|\to|\mathfrak{a}^{\prime}_{n}|$,
and $\Phi$-morphism $\rho_{n}\colon|\mathfrak{a}^{\prime}_{n}|\to W$ such that
$g\circ\pi_{n}=\rho_{n}\circ f_{n}$. Moreover, for each
$v\sqsupset_{\Phi}g(r_{\mathfrak{m}})$, by Lemma 6 there are
$\mathfrak{b}_{v}$ and a $\Phi$-morphism $\rho_{v}\colon|\mathfrak{b}_{v}|\to
W$ mapping the root of $\mathfrak{b}_{v}$ to $v$. Let $D=g\pi(C)\cup
C_{\Phi}(g(x))$, and let
$\hat{\mathfrak{n}}={\vec{\mathfrak{a}}*\vec{\mathfrak{b}}\choose D}_{g(w)}$,
with associated map $\hat{\rho}$. It is not hard to check that $\hat{\rho}$ is
a pre-$\Phi$-morphism from $\hat{\mathfrak{n}}$ to $W$. By letting

$\hat{f}(w)=\begin{cases}g(w)&\text{if $w\in C$}\\\ f_{n}(w)&\text{if
$w\in|\mathfrak{a}_{n}|$},\end{cases}$

it is easy to see that $\hat{f}\colon|{\mathfrak{m}}|\to|\hat{\mathfrak{n}}|$
is weakly monotonic and satisfies $g\circ\pi=\hat{\rho}\circ\hat{f}$. Setting
${\mathfrak{n}}=\hat{\mathfrak{n}}/\hat{\rho}$, $f=[\hat{f}]$ and
$\rho=[\hat{\rho}]$, Proposition A.5 implies that ${\mathfrak{n}}$, $f$ and
$\rho$ have the desired properties.∎