# dynamic_tangled_derivative_logic_of_metric_spaces__c891417e.pdf Dynamic Tangled Derivative Logic of Metric Spaces David Fern andez-Duque1*and Yo av Montacute2* 1University of Barcelona 2University of Cambridge fernandez-duque@ub.edu, yoav.montacute@cl.cam.ac.uk Dynamical systems are abstract models of interaction between space and time. They are often used in fields such as physics and engineering to understand complex processes, but due to their general nature, they have found applications for studying computational processes, interaction in multiagent systems, machine learning algorithms and other computer science related phenomena. In the vast majority of applications, a dynamical system consists of the action of a continuous transition function on a metric space. In this work, we consider decidable formal systems for reasoning about such structures. Spatial logics can be traced back to the 1940 s, but our work follows a more dynamic turn that these logics have taken due to two recent developments: the study of the spatial (or topological ) µ-calculus, and the integration of linear temporal logic with logics based on the Cantor derivative. In this paper, we combine dynamic spatial logics based on the Cantor derivative and the next point in time operators with an expressively complete fixed point operator to produce a combination of the spatial µ-calculus with linear temporal logic. We show that the resulting logics are decidable and have a natural axiomatisation. Moreover, we prove that these logics are complete for interpretations on the Cantor space, the rational numbers, and subspaces thereof. Introduction Our planet is orbited by a myriad of man-made satellites, whose movement must be predicted and controlled to e.g. avoid collision with other objects. To this end, their position over time is modelled using our knowledge of physics, and the mathematical structure governing this behaviour is known as a dynamical system (Figure 1). Given the initial position and momentum of a satellite, one may predict the path it will take: it may be periodic, diverge into space or crash into the earth. In such models, both space and time are continuous, i.e. given by Euclidean spaces; however, they can be approximated discretely for a better computational treatment, or even be represented via finite relational structures (Example 1 and Figure 5). One can thus imagine satellites moving one tick of the clock at a time, for a suitably small time interval. *These authors contributed equally. Copyright 2024, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. Figure 1: Orbits around a centre of gravity Reasoning about dynamical systems is highly relevant to AI. We mention a few examples: Qualitative spatial reasoning is a branch of AI that aims to capture basic relations between regions in space in a way that is computationally efficient and thus suitable for applications (see (Cohn and Renz 2008; Stell 2019) for overviews). The region connection calculus (RCC8) (Egenhofer and Franzosa 1991; Randell, Cui, and Cohn 1992) was introduced for geolocalisation applications, and is closely connected to modal logic (Wolter and Zakharyaschev 2000). Modern-day applications such as self-driving cars require the combination of dynamic and spatial reasoning (for examples, see (Gabelaia et al. 2005)), modelled via dynamical systems (see (Dickmanns, Mysliwetz, and Christians 1990; Hua et al. 2022)). As models of space , we will work in the setting of metric spaces, which are sets of points whose mutual distance is measurable. These spaces generalise the plane, or other Euclidean spaces, but also include some more unusual examples such as the Cantor set.1 Formally, these are structures X = X, δ , where X is any set and δ: X X [0, ) is the distance map satisfying δ(x, x) = 0, δ(x, y) = δ(y, x) and δ(x, z) δ(x, y) + δ(y, z). A discrete time dynamical system is a metric space equipped with a transition function, representing movement. Two recent developments have taken spatial logic into a more dynamic direction. The first is the development of the spatial (or topological ) µ-calculus (Baltag, Bezhanishvili, and Fern andez-Duque 2021; Goldblatt and Hodkin- 1One can work in the even more general class of topological spaces, as in e.g. (Fern andez-Duque and Montacute 2023), but metric spaces are normally more adequate for applications regarding physical space. The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) son 2017), which enriches the usual spatial operators with fixed points and has applications in formal epistemology (Baltag, Bezhanishvili, and Fern andez-Duque 2022). The second, following a suggestion of Saveliev, is equipping temporal logic with the Cantor derivative (Fern andez-Duque and Montacute 2022), obtaining a more expressive version of Dynamic Topological Logic (DTL) (Artemov, Davoren, and Nerode 1997). If X, d is a metric space, the Cantor derivative d(A) of a set A X is its set of limit points, i.e. x d(A) if the distance between x and A \ {x} is zero. This allows one to reason about e.g. dense-in-themselves spaces, which are of relevance for example in chaos theory (Devaney 2018). Our goal is to combine the expressive power of these two proposals and produce DTLs with spatial fixed points. We are specifically interested in dynamical systems based on metric spaces, as these are the spaces used in most applications. Here we build on Fern andez-Duque and Montacute (2022), who consider a bi-modal language with interpreted as Cantor derivative and # as next point in time . In order to enrich this logic with spatial fixed points, we follow Goldblatt and Hodkinson (2017), who utilised results of Dawar and Otto (2009) to represent the spatial µ-calculus via its relatively simple but expressively complete tangled fragment (Fern andez-Duque 2011a,b). The latter augments modal logic with a polyadic modality , in which Γ holds in the largest perfect subspace where each φ Γ is dense. This grants us the full power of the spatial µ-calculus while working within a formal language that is relatively tame from a combinatorial perspective. We thus obtain the logic K4C (and various other extensions) which plays the role of the standard dynamic spatial logic S4C (Kremer and Mints 2005). Despite the additional expressive power due to the Cantor derivative and definability of spatial fixed points, we show that K4C enjoys the same desirable properties of S4C: it is naturally axiomatisable and decidable over the class of all metric spaces. Moreover, we extend a result of Mints and Zhang (2005) which states that S4C is complete for the Cantor space, by showing that K4DC (the extension of K4C with the seriality axiom) is sound and complete both for the Cantor set and for the set of rational numbers. We also consider the logics K4I and K4DI for dynamical systems where the transition function is an immersion (i.e. it preserves the Cantor derivative). All of these logics are decidable, each logic with the D axiom is shown to be complete for the Cantor space and for the rational numbers, and logics without D for subspaces of these two metric spaces. Working with the µ-calculus is notoriously challenging, and despite the simplicity gained by the tangled fragment, there are still many hurdles. In order to deal with fixed points, we follow techniques pioneered by Fine (1974) based on final points, already shown by Bezhanishvili et al. (2021) to be useful for working with the spatial µ-calculus. In our work, we further refine these techniques in order to deal with the interactions between the metric and the transition function. Completeness for the Cantor space and the rational numbers is obtained via the technique of dynamic pmorphisms. To apply it in our setting, we employ Kripke frames with limits, as used by Kremer and Mints (2007), along with the world-duplication construction from derivational modal logic (see e.g. (Baltag, Bezhanishvili, and Fern andez-Duque 2021)). Our general method uniformly yields results for these two metric spaces and their closed subspaces. The current work is essential for the axiomatisation of DTL with the Cantor derivative, which currently has only been achieved in the setting of scattered spaces; see (Fern andez-Duque and Montacute 2023). Preliminaries In this section we introduce the notation and definitions required for understanding this paper. We work with the general notion of derivative spaces: Derivative spaces are a special case of derivative algebras introduced by Esakia (2004), where (X) is replaced by an arbitrary Boolean algebra. We moreover work with transitive derivative algebras, so that the definition is stronger than that of e.g. (Baltag, Bezhanishvili, and Fern andez-Duque 2021). When working with more than one metric space, we may denote the Cantor derivative of the space X, δ by d X. Given subsets A, B X, it is not difficult to verify that d satisfies the following properties: 1. d( ) = ; 2. d(A B) = d(A) d(B); 3. dd(A) d(A). Definition 1. A derivative space is a pair X = X, ρ , where X is a set and ρ: (X) (X) is a map satisfying properties 1-3 above, where d = ρ. If X = X, δ is a metric space and d is the Cantor derivative on X, then X, d is a derivative space. However, there are other examples of derivative spaces. The standard closure of a subset A of points in a metric space can be defined as c(A) = A d(A). Then, X, c is also a derivative space, which satisfies the additional property A c(A); we call such derivative spaces closure spaces. More generally, if X, ρ is an arbitrary derivative space, we define ρ(A) := A ρ(A). Another example of derivative spaces comes from transitive Kripke frames. For the sake of succinctness, we call these frames derivative frames. Below and throughout the text, we write x = y φ instead of x(y < x φ), and adopt a similar convention for the universal quantifier and other relational symbols. Definition 2. A derivative frame is a pair F = W, < where W is a non-empty set and < is a transitive relation on W. Denote the reflexive closure of < by . We also write w v if w v and v w; the equivalence class of w under is called the cluster of w and is denoted C(w). Given A W, we define < as a map < : (W) (W) such that <(A) = {w W : v = w(v A)}. Lemma 1. If W, < is a derivative frame, then W, < is a derivative space. Dynamical derivative systems consist of a derivative space equipped with a continuous function. Recall that if X, δX and Y, δX are metric spaces and f : X Y , then f is continuous if for every x X and every ε > The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) 0 there exists η > 0 such that δX(x, x ) < η implies δY (f(x), f(x )) < ε. It is well known (and not difficult to check) that f is continuous iff c Xf 1(A) f 1c Y (A) for all A Y . We thus arrive at the following general definition. Definition 3. Let X, ρX and Y, ρY be derivative spaces. We say that f : X Y is continuous if for all A Y , ρXf 1(A) f 1 ρY (A). We say that f is an immersion if it satisfies the stronger condition ρXf 1(A) f 1ρY (A). Finally, f is a homeomorphism if it is a bijection satisfying ρXf 1(A) = f 1ρY (A). We are particularly interested in the case where X = Y , which leads to the notion of dynamic derivative system. Definition 4. A dynamic derivative system is a triple S = X, ρ, f , where X, ρ is a derivative space and f : X X is a continuous map. If S = X, ρ, f is such that ρ is the Cantor derivative associated with a metric δ, we say that S is a dynamic metric system and identify it with the triple X, δ, f . If ρ = < for some transitive relation <, we say that S is a dynamic Kripke frame and identify it with the triple X, <, f . It will be convenient to characterise dynamic Kripke frames in terms of <. Definition 5 (monotonicity and strict monotonicity). Let W, < be a derivative frame. A function f : W W is monotonic if w v implies f(w) f(v), and strictly monotonic if w < v implies f(w) < f(v). Lemma 2. If W, < is a derivative frame and f : W W, then 1. if f is monotonic, then it is continuous with respect to <, and 2. if f is strictly monotonic, then it is an immersion with respect to <. Next we will discuss the tangle operators, which are important in spatial modal logic, as they are expressively equivalent to the µ-calculus over the class of transitive Kripke frames, as shown by Dawar and Otto (2009). In the spatial context, the tangled closure was introduced by Fern andez Duque (2011b) and the tangled derivative was introduced by Goldblatt and Hodkinson (2017), who observed that Dawar and Otto s result holds for metric spaces as well. Definition 6 (tangled derivative). Let X, ρ be a derivative space and let S (X). Given A X, we say that S is tangled in A if for all S S, A ρ(S A). We define the tangled derivative of S as ρ (S) := [ {A X : S is tangled in A}. The tangled closure is then the special case of the tangled derivative where ρ is a closure operator, and we denote it by ρ (or c when working with a metric space). Dynamic Topological Logics In this section we discuss dynamic spatial (or topological ) logic in the general setting of dynamic derivative systems. Given a non-empty set PV of propositional variables, the language L is defined recursively as follows: φ ::= p | φ φ | φ | φ | Φ | #φ, where p PV and Φ is a finite sequence of formulas in L . It consists of the Boolean connectives and , the temporal modality #, the modality for the derivative operator, and the tangled derivative modality . As usual, := is the dual of . The closure and interior modalities may be defined by φ := φ φ and φ := φ φ. Following (Goldblatt and Hodkinson 2017), we define Φ := V Φ Φ. Definition 7 (semantics). A dynamic derivative model (DDM) is a quadruple M = X, ρ, f, ν where X, ρ, f is a dynamic derivative system and ν : PV (X) is a valuation function assigning a subset of X to each propositional letter in PV. Given φ, ψ L , we define the truth set φ X of φ inductively as follows: p = ν(p); φ = X \ φ ; φ ψ = φ ψ ; φ = ρ( φ ); {φ1, . . . , φn} = ρ ({ φ1 , . . . , φn }); #φ = f 1( φ ). We write M, x |= φ if x φ , and M |= φ if φ = X. We may write M or ν instead of when working with more than one model or valuation. The notion of validity is defined as usual; if X is a dynamic derivative system and φ is a formula, we write X |= φ if X, ν |= φ for every valuation ν on X. Similarly, if Ωis a class of dynamical systems or models, we write Ω|= φ and say φ is valid on Ωif A |= φ for every A Ω. We define other connectives (e.g. , ) as abbreviations in the usual way. The fragment of L that includes only will be denoted by L . In order to align with the familiar axioms of modal logic, it is convenient to discuss the semantics of . Accordingly, we define the dual of the derivative, called the co-derivative. Definition 8 (co-derivative). Let X, ρ be a derivative space. For each S X we define ˆρ(S) := X\ρ(X\S) to be the co-derivative of S. It can readily be checked that for every dynamic derivative model X, ρ, f, ν and every formula φ, φ = ˆρ( φ ). The co-derivative can be used to define the standard interior of a set, given by i(A) = A ˆρ(A) for each A X. Let us list the axiom schemes and rules that we will consider in this paper. Below, if Φ = {φ1, . . . , φn} is a set of formulas then #Φ := {#φ1, . . . , #φn}, and | { , }. Taut := All propositional tautologies K := (φ ψ) ( φ ψ) 4 := φ φ Next := #φ # φ MP := φ φ ψ The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) Next := #(φ ψ) #φ #ψ C| := |#φ #|φ Fix := Φ V φ Φ (φ Φ) Ind := θ V φ Φ (φ θ) (θ Φ) CTan|:= | #Φ #| Φ The base modal logic over L is given by K := Taut+ K + MP + Nec . However, we are mostly interested in proper extensions of K. Let Λ, Λ be logics over languages L and L . We say that Λ extends Λ if L L and all the axioms and rules of Λ are derivable in Λ. A logic over L is normal if it extends K. If Λ is a logic and φ is a formula, we denote by Λ + φ the least extension of Λ which contains every substitution instance of φ as an axiom. We write Λ φ when φ is a theorem of Λ, or simply φ when Λ is clear from context. Recall that a logic Λ is sound for Ωif every theorem of Λ is valid on Ω, and complete if whenever Ω|= φ, it follows that Λ φ. We then define K4 := K + 4, K4D = K4 + D, and S4 := K4 + T. These logics are well known and characterise certain classes of spaces and Kripke frames which we review below. For a logic Λ, Λ denotes the logic Λ + Fix + Ind over L . For a logic Λ over L , ΛF is the logic over L given by ΛF := Λ + Next + Next + Nec#, i.e. by adding axioms of linear temporal logic to Λ, which hold whenever # is interpreted using a function. In order to reason about continuous functions, we define ΛC := ΛF + C ΛC := Λ C + CTan ΛI := ΛF + C3 ΛI := Λ I + CTan3. As we will see, these correspond to derivative spaces with a continuous function or an immersion, respectively; accordingly, logics that include C3 are immersive. Theorem 1. S4 is the logic of all closure spaces, the logic of all transitive, reflexive derivative frames, and the logic of the real line with the standard closure (Mc Kinsey and Tarski 1944), and K4 is the logic of all (finite) derivative frames (i.e., transitive Kripke frames) and of all (countable) metric spaces (Bezhanishvili and Lucero-Bryan 2012). Logics with the C axioms correspond to classes of dynamical systems. Lemma 3. If Λ is sound for a class of derivative spaces Ω, then: 1. ΛC is sound for the class of dynamic derivative systems X, ρ, f , where X, ρ Ωand f is continuous. 2. ΛI is sound for the class of dynamic derivative systems X, ρ, f , where X, ρ Ωand f is an immersion. The above lemma is easy to verify from the definition of a continuous function in the context of derivative spaces (Definition 3). Note that #Φ # Φ is not valid over the class of dynamic derivative spaces with a continuous function (see Example 3). Applications to Dynamical Systems Our logical framework is designed for the specification and formal reasoning about dynamical systems, especially those based on metric spaces. In many applications, the spaces used have the additional property that they are crowded, or dense-in-themselves i.e., they have no isolated points. This property is expressed by the axiom D, i.e. . In the introduction, we mentioned an example involving satellites orbiting a centre of gravity. Let us revisit this example with our formal language in mind. Example 1 (centre of gravity). In Figure 1, we illustrate a model of bodies orbiting a centre of gravity on a plane. We may model this as R2 with a transition function f : R2 R2 corresponding to the movement of a body over a fixed time interval of ε seconds. We may then describe various properties of this system using dynamic spatial logic. First, observe the region P. Points in this region will return to P after completing a full orbit (say, in time n), but not before that. This corresponds to the expression P #n P Wn 1 i=1 #i P. Conversely, the region Q is a unsafe zone which none of the three orbits indicated in the figure intersect. Accordingly, P Vm i=0 #i Q holds in our model for every m; note that Q means that we are inside the region Q, not on the boundary. This is important in a spatial safety condition, since it means that we are guaranteed not to be in the unsafe region even if there is a small error in measurement. This is a basic example of a dynamical system arising from a metric space which is influenced by a force, in this case gravity. Such forces can initiate different phenomena such as chaos in the system. Given a dynamical system X = X, τ, f , we say that f : X X is topologically transitive if for every nonempty open sets U, V τ there exists n 0 such that f n(U) V = . This is an important property that together with the set of periodic points of f being dense implies that X is a chaotic dynamical system (Devaney 2018); in a seminal result, Banks et al. (1992) showed that such systems exhibit sensitive dependence on initial conditions, i.e. the butterfly effect . Example 2. Consider the dynamical system in Figure 2. Suppose that starting at each of the black points the function reaches the area P within n steps. Then the formula Wn i=1 #i P captures the fact that each open neighbourhood of the red point contains a point reaching P after some amount of time bounded by n. The existence of such n is guaranteed by topological transitivity. Figure 2: A system exhibiting topological transitivity, the orbit of each open set intersects every other open set. The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) Let us now turn our attention to spatial fixed points. We denote the language of the µ-calculus by Lµ. Dawar and Otto (2009) showed that the bisimulation-invariant fragment of monadic second order logic (MSO) is expressively equivalent to L over the class of finite K4 frames. As a corollary, we obtain that for every φ Lµ, there is φ L such that φ φ is valid over the class of metric spaces (Goldblatt and Hodkinson 2017). Thus no generality is lost when replacing Lµ with L . When enriched with #, we obtain a logic where all spatial fixed points can be expressed, but not those defined in terms of #, such as until . As an important special case, we consider the unary tangle {P} which represents the perfect core of P, i.e. the largest subset of ν(P) without isolated points (Baltag, Bezhanishvili, and Fern andez-Duque 2021). Example 3. In Figure 3, we see two dynamical systems based on linear transformations on the plane: on the left a rotation, and on the right, a trivial system that maps the entire plane to 0. The system on the left is an immersion (in fact, a homeomorphism), but the one on the right is not. Let P be the top square on the left-hand figure (including both the interior and the boundary), and let Q be the bottom square. It should be clear that {P} = P, since P = d(P) = d(P P). In other words, P is perfect, i.e. it is closed and contains no isolated points. Similarly, points in Q satisfy {#P}, since every point of Q satisfies #P and Q is also perfect. Moreover, these points also satisfy # {P}, so {#P} # {P} holds; this is an instance of the axiom CTan . In contrast, let us consider the figure on the right, and let O be the singleton containing the origin; Q is as above. As before, we have that every point of Q satisfies #O, hence since Q is perfect, then {#O}. However, the origin is an isolated point, i.e. not perfect, so it does not satisfy {O}. It follows that points of Q satisfy {#O} # {O}, and CTan fails. However, the map is still continuous, so we expect CTan to hold; and, indeed, we observe that {O} holds on the origin, since O c(O). It readily follows that {#O} # {O} is true in the model on the right, i.e. CTan is valid. Figure 3: Two dynamical systems on the plane. Relational Completeness In this section we show that the logics K4C , K4DC , K4I , and K4DI have the finite model property by constructing finite models and truth preserving maps from these models to the canonical model. The first step in our completeness proof is to define the standard canonical model MΛ c = W, <, g, ν . This is done in a standard way, based on the set of maximal consistent theories, and has the following properties (see (Fern andez Duque and Montacute 2022)). Lemma 4. 1. If Λ extends K4C, then the canonical model of Λ is transitive and monotonic. 2. If Λ extends K4I, then the canonical model of Λ is transitive and strictly monotonic. 3. If Λ extends K4D, then the canonical model of Λ is serial with respect to < (i.e., for all w Wc, there is v = w). Unfortunately, the standard truth lemma fails for the canonical model, so it is only a stepping stone in our proof and we must consider some related finite structures called moments . To define these, if < is a transitive relation on A, A, < is called tree-like if whenever a c and b c, it follows that a b or b a. Moments record the static information at a point. Definition 9 (moment). Fix Λ {K4, K4D}. A Λmoment is a structure m = |m|, 0 and y f S[|Si 1|]. The key is that dynamic Φ-morphism π preserves the truth of formulas of suitable #-depth. Lemma 6 (truth preservation). Let S be a story of duration I and let x |S0|. Let π be a dynamic Φ-morphism into the canonical model of some normal logic Λ extending K4C . Suppose that φ Φ is a formula of #-depth at most I, and either Λ and S are immersive or π is distinguished. Then, φ π(x) iff x φ S. The final ingredient in our completeness proof is the fact that every point in the canonical model is a dynamic Φmorphic image of a suitable story. Proposition 1. Let Λ be any of K4C , K4DC , K4I , or K4DI . Given I < ω and w Wc, there is a story S of duration I and a dynamic Φ-morphism π: |S| Wc with w = π(r S), such that either Λ and S are immersive or π is distinguished. This proposition is proven via a step-by-step construction. First, we build a story of duration 1 by constructing the first moment. Then, we iteratively add a new moment in such a way that the required transition function always exists between one moment and the next. It follows that every satisfiable formula is also satisfiable on a finite story, hence satisfiable on a finite model. We obtain Kripke completeness for our logics, where soundness follows from Lemma 3. Theorem 2. The logics K4C , K4DC , K4I and K4DI are sound and complete for their respective classes of finite dynamic Kripke frames. From completeness and FMP, we obtain decidability. Corollary 1. Each of the logics K4C , K4DC , K4I and K4DI is decidable. The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) Metric Completeness Next we lift Theorem 2 to metric spaces. We first need to prepare our stories for this procedure. First, we assume that if w is any reflexive point then there is w = w such that w w and π(w) = π(w ); i.e., there are at least two copies of each reflexive point in each cluster. This is not a problem, since every model is bisimilar to one with this property. Second, following Kremer and Mints (Kremer and Mints 2007), we need to add limits to our Kripke models. Definition 13. Let F = W, <, g be a finite dynamic Kripke frame. A path through F is an infinite sequence w = (wi) i=0 such that wi wi+1. A finite path is defined similarly but has finitely many elements. The set of (infinite) paths is denoted W. For a path w = (wi) i=0, we define g( w) = (g(wi)) i=0. A limit assignment is a function lim assigning to each w W an element lim w W such that lim w occurs infinitely often in w, and such that lim g( w) = g(lim w). Every story admits a limit assignment. The key observation is then that the paths on a Kripke frame form a metric space. Definition 14. Let F = W, <, g be a finite dynamic Kripke frame with a limit assignment. We define a metric δ on W such that δ( w, v) = 0 if w = v, and otherwise δ( w, v) = 2 n for the least n such that wn = vn. Proposition 2. Let F = W, <, g be a finite story such that every reflexive cluster has at least two elements, and let lim be a limit assignment on F. The structure F = ( W, δ, g) is a dynamic metric system, and lim: W W is a dynamic p-morphism. Moreover, if g is immersive, then so is g. We wish to show that W is in fact homeomorphic to a subset of the Cantor space. For this we use the following two results. Theorem 3 (Brouwer, see e.g. (van Mill 2001)). A metric space is a Cantor space if and only if it is non-empty, perfect, compact, and totally disconnected. In particular, it is well known that the set of branches on the infinite binary tree is homeomorphic to the Cantor set. It is not hard to see that this binary tree is of the form W, where W is a two-element cluster. More generally, W is always a Cantor set, provided some mild conditions are satisfied. Completeness for the Cantor space then follows (see Theorem 4 below). Finally, we prove completeness for subspaces of the rational numbers, using the following. Proposition 3 (Sierpinski 1920). Every two perfect countable metric spaces are homeomorphic to each other. For this, we focus our attention on a countable subspace of W; namely, those sequences that are eventually constant. Given a frame W, < , define W0 to be the set of all w W such that there is n N such that wn = wm for all n > m. Clearly, W0 is countable if W is finite, and it inherits the metric (which we denote δ0) from W. The space W0 is always homeomorphic to a subset of Q, and completeness for the rationals follows. Theorem 4. Let X be either Q or the Cantor set. 1. K4C is complete for the class of dynamic metric systems based on a closed subspace of X. 2. K4I is complete for the class of immersive dynamic metric systems based on a closed subspace of X. 3. K4DC is complete for the class of dynamic metric systems based on X. 4. K4DI is complete for the class of immersive dynamic metric systems based on X. Conclusion We have developed dynamic spatial logics based on the spatial µ-calculus, in its tangled presentation, and introduced various axiomatic systems that are sound and complete for their intended interpretations over dynamical systems based on a metric space. We showed that these completeness results in particular apply to the Cantor space and the rational numbers two canonical metric spaces. One may also consider interpretations based on the real line, or on Euclidean spaces in general. Fern andez Duque (2007) showed that S4C is complete for the plane, but we cannot expect similar results for K4DC , in view of results by Lucero-Bryan (2013) and Shehtman (1990). However, it may well be possible to define extensions of K4DC that are complete for Euclidean spaces. Determining the dynamic derivational logics of Euclidean spaces remains a challenging direction for future research. Even in the setting of closure semantics, the dynamic spatial logic of the real line is a long-standing open problem (Nogin and Nogin 2008). Finally, there is the issue of extending our language to include the henceforth operator. It is our expectation that the Cantor-derivative logic of all dynamic metric systems may be axiomatised using the tangled derivative, much as the tangled closure was used to provide an axiomatisation of the closure-based DTL (Fern andez-Duque 2012). Fern andez Duque showed how the tangled closure is essential in axiomatising DTL with the henceforth operator, and in future work we plan to show how the same can be done for DTL with the Cantor derivative. This follows the work of Fern andez-Duque and Montacute who provided a complete axiomatisation for DTL with the Cantor derivative and henceforth for the class of scattered spaces (Fern andez Duque and Montacute 2023). In this context, we are specifically interested in axiomatising the class of chaotic systems. We believe that the present work is an important step towards achieving this goal. References Artemov, S.; Davoren, J.; and Nerode, A. 1997. Modal Logics and Topological Semantics for Hybrid Systems. Technical Report MSI 97-05. Baltag, A.; Bezhanishvili, N.; and Fern andez-Duque, D. 2021. The Topological Mu-Calculus: completeness and decidability. 1 13. Baltag, A.; Bezhanishvili, N.; and Fern andez-Duque, D. 2022. The Topology of Surprise. In Kern-Isberner, G.; Lake- The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24) meyer, G.; and Meyer, T., eds., Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, KR 2022, Haifa, Israel. July 31 - August 5, 2022. Banks, J.; Brooks, J.; Cairns, G.; Davis, G.; and Stacey, P. 1992. On Devaney s Definition of Chaos. Am. Math. Monthly, 99(4): 332 334. Bezhanishvili, G.; and Lucero-Bryan, J. 2012. More on d Logics of Subspaces of the Rational Numbers. Notre Dame J. Formal Log., 53(3): 319 345. Cohn, A.; and Renz, J. 2008. Qualitative Spatial Representation and Reasoning. In van Harmelen, F.; Lifschitz, V.; and Porter, B., eds., Handbook of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, 551 596. Elsevier. Dawar, A.; and Otto, M. 2009. Modal characterisation theorems over special classes of frames. Ann. Pure Appl. Log., 161(1): 1 42. Devaney, R. L. 2018. An introduction to chaotic dynamical systems. CRC press. Dickmanns, E.; Mysliwetz, B.; and Christians, T. 1990. An integrated spatio-temporal approach to automatic visual guidance of autonomous vehicles. IEEE Transactions on Systems, Man, and Cybernetics, 20(6): 1273 1284. Egenhofer, M.; and Franzosa, R. 1991. Point-set topological spatial relations. International Journal of Geographical Information Systems, 5(2): 161 174. Esakia, L. 2004. Intuitionistic logic and modality via topology. Ann. Pure Appl. Log., 127(1-3): 155 170. Fern andez-Duque, D. 2011a. On the Modal Definability of Simulability by Finite Transitive Models. Stud Logica, 98(3): 347 373. Fern andez-Duque, D. 2011b. Tangled Modal Logic for Spatial Reasoning. In Walsh, T., ed., IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, 857 862. IJCAI/AAAI. Fern andez-Duque, D.; and Montacute, Y. 2022. Dynamic Cantor Derivative Logic. In Manea, F.; and Simpson, A., eds., 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G ottingen, Germany (Virtual Conference), volume 216 of LIPIcs, 19:1 19:17. Schloss Dagstuhl - Leibniz-Zentrum f ur Informatik. Fern andez-Duque, D.; and Montacute, Y. 2023. Untangled: A Complete Dynamic Topological Logic. In Williams, B.; Chen, Y.; and Neville, J., eds., Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, 6355 6362. AAAI Press. Fern andez-Duque, D. 2007. Dynamic Topological Completeness for R2. Logic Journal of the IGPL, 15(1): 77 107. Fern andez-Duque, D. 2012. A sound and complete axiomatization for Dynamic Topological Logic. The Journal of Symbolic Logic, 77(3): 947 969. Fine, K. 1974. Logics containing K4. I. J. Symbolic Logic, 39: 31 42. Gabelaia, D.; Kontchakov, R.; Kurucz, A.; Wolter, F.; and Zakharyaschev, M. 2005. Combining Spatial and Temporal Logics: Expressiveness vs. Complexity. J. Artif. Intell. Res., 23: 167 243. Goldblatt, R.; and Hodkinson, I. 2017. Spatial logic of tangled closure operators and modal mu-calculus. Annals of Pure and Applied Logic, 168(5): 1032 1090. Hua, H.; Li, D.; Li, R.; Zhang, P.; Renz, J.; and Cohn, A. 2022. Towards Explainable Action Recognition by Salient Qualitative Spatial Object Relation Chains. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5): 5710 5718. Kremer, P.; and Mints, G. 2005. Dynamic Topological Logic. Annals of Pure and Applied Logic, 131: 133 158. Kremer, P.; and Mints, G. 2007. Dynamic Topological Logic. In Aiello, M.; Pratt-Hartmann, I.; and van Benthem, J., eds., Handbook of Spatial Logics, 565 606. Springer. Lucero-Bryan, J. G. 2013. The d-logic of the real line. J. Log. Comput., 23(1): 121 156. Mc Kinsey, J.; and Tarski, A. 1944. The algebra of topology. Annals of Mathematics, 2: 141 191. Mints, G.; and Zhang, T. 2005. Propositional logic of continuous transformations in Cantor space. Arch. Math. Log., 44(6): 783 799. Nogin, M.; and Nogin, A. 2008. On Dynamic Topological Logic of the Real Line. Journal of Logic and Computation, 18(6): 1029 1045. Randell, D.; Cui, Z.; and Cohn, A. 1992. A Spatial Logic Based on Regions and Connection. In Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning, KR 92, 165 176. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc. Shehtman, V. B. 1990. Derived sets in euclidean spaces and modal logic. ILLC Preprints and Publications, X-1990-05. Sierpinski, W. 1920. Sur une propri et e topologique des ensembles d enombrables denses en soi. Fund. Math., 1: 11 16. Stell, J. 2019. Qualitative Spatial Representation for the Humanities. International Journal of Humanities and Arts Computing, 13(1-2): 2 27. van Mill, J. 2001. The infinite-dimensional topology of function spaces. Amsterdam. Wolter, F.; and Zakharyaschev, M. 2000. Spatial Reasoning in RCC-8 with Boolean Region Terms. In Horn, W., ed., ECAI, 244 250. IOS Press. The Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)