# untangled_a_complete_dynamic_topological_logic__aa434e68.pdf

Untangled: A Complete Dynamic Topological Logic

David Fern andez-Duque1*and Yo av Montacute2*

1ICS of the Czech Academy of Sciences Ghent University 2University of Cambridge fernandez@cs.cas.cz, yoav.montacute@cl.cam.ac.uk

Dynamical systems are general models of change or movement over time with a broad area of applicability to many branches of science, including computer science and AI. Dynamic topological logic (DTL) is a formal framework for symbolic reasoning about dynamical systems. DTL can express various liveness and reachability conditions on such systems, but has the drawback that the only known axiomatisation requires an extended language. In this paper, we consider dynamic topological logic restricted to the class of scattered spaces. Scattered spaces appear in the context of computational logic as they provide semantics for provability and enjoy definable fixed points. We exhibit the first sound and complete dynamic topological logic in the original language of DTL. In particular, we show that the version of DTL based on the class of scattered spaces is finitely axiomatisable, and that the natural axiomatisation is sound and complete.

Introduction In a nutshell, dynamical systems are mathematical models of movement in space over time. The interaction between space and time is a fundamental aspect of reality, making such models ubiquitous in many scientific disciplines, ranging from physics to economics. Artificial intelligence is no exception, which should not be surprising given the temporal aspect of processes and the deep connections between topology and computation, as demonstrated by abstract models of computation such as the well-known Scott domains (Scott 1982). There are many recent examples from pure and applied work in artificial intelligence involving dynamical systems. Lin and Antsaklis (2014) use hybrid dynamical systems in the research of artificial intelligence and computer-aided verification. Brunton and Kutz (2019) proposed approaching data-related problems and machine learning through dynamical systems, and Weinan (2017) suggested modelling nonlinear functions implemented in machine learning using dynamical systems. Mortveit and Reidys s (2007) sequential dynamical systems generalise cellular automata and provide a framework for studying dynamical processes in graphs.

*These authors contributed equally. Copyright 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

Dynamical systems are also found in their linear form in the shape of Markov chains, linear recurrence sequences and linear differential equations. It is therefore not surprising that connections have been established between dynamical systems and algorithms. Such links can be found for example in the work of Hanrot, Pujol and Stehl e (2011), and in the work of Chu (2008). Dynamical reasoning can also be found in the study of Modal Logic in, for example, spatiotemporal knowledge representation (Galton 2009) and in the study of liveness (Alpern and Schneider 1985), relating some algorithmic properties to topology and hints at formal languages. This list is by no means exhaustive. The applications above warrant the need for an effective formal reasoning framework about topological dynamics, i.e. the action of a (typically continuous) function on a topological space. Modal logic was first suggested to serve that purpose in the 1990s by Artemov et al. (1997), who envisioned dynamic topological logic as a bimodal logic for reasoning about topological dynamics. They defined the logic S4C and showed that it possesses desirable properties such as a natural axiomatisation and the finite model property. Kremer and Mints (2005) suggested that including a third modality, henceforth from linear temporal logic (LTL), would lead to a logic powerful enough to reason about the asymptotic behaviour of dynamical systems, possibly leading to applications in automated theorem proving. They dubbed the resulting system dynamic topological logic (DTL). They proposed a natural axiomatisation for DTL and conjectured it to be sound and complete for the class of dynamical systems. However, the situation turned out to be much more intricate than that of S4C, as DTL is not finitely axiomatisable (Fern andez-Duque 2014). Instead, Fern andez-Duque proposed an extension of DTL, denoted by DTL , which enriches the original language with topological fixed points known as tangled operators; given subsets A1, . . . , An of a topological space X, their tangled closure, c {A1, . . . , An}, is the largest subspace of X within which every Ai is dense. Fern andez-Duque (2012) showed that DTL has a natural infinite axiomatisation. In order to overcome this difficulty, we restrict our attention to a specific class of dynamical systems, namely, those based on scattered spaces. Scattered spaces are topological spaces where every nonempty subspace has an isolated point. They have gathered attention lately in the context of

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

computational logic, as they may be used to model provability in formal theories (Abashidze 1985), leading to applications in characterising their provably total computable functions (Beklemishev 2004). Modal logic on scattered spaces enjoys definable fixed points (Sambin and Valentini 1982), connecting it to the topological µ-calculus (Baltag, Bezhanishvili, and Fern andez-Duque 2021). The latter is particularly relevant to us, as the expressive power gained by topological fixed points, including the tangled operators of DTL , is absent in this setting. As the logic of scattered spaces is the G odel-L ob modal logic GL, we refer to the dynamic topological logic of scattered spaces as dynamic G odel-L ob logic (DGL). Moreover, we base our semantics on the Cantor derivative rather than the topological closure, since the former is known to be more expressive (Kudinov and Shehtman 2014). Our goal is to demonstrate that the standard finite axiomatisation of DGL is sound and complete, leading to the first completeness result of this kind, as well as the first such logic combining the Cantor derivative with the infinitary henceforth from LTL. The proof of completeness employs various advanced techniques from modal logic, including an application of Kruskal s theorem in the spirit of the work of Gabelaia et al. (2006).

Preliminaries Before recalling the definition of dynamic topological logic, let us review some notions from topology and dynamical systems, including the Cantor derivative in a topological space.

Topology Definition 1 (topological space). A topological space is a pair X = (X, τ) where X is a set of points and τ (X) is a subset satisfying the following conditions:

1. X, τ; 2. If U, V τ then U V τ; 3. If U τ then S U τ.

The elements of τ are called open sets and τ is called a topology on X. Complements of open sets are called closed sets. If x U τ, we say that U is a neighbourhood of x.

We can view partial orders (posets) of the form (X, ) as topological spaces with the downset topologies, where each set of the form x := {y : y x}, for some x X, is a basic open set (as usual, denotes the reflexive closure of ). Equivalently, a set U X is open iff it is downward closed under . Topologies of this form are Alexandroff topologies, which have the property that arbitrary intersections of open sets are open. Note that in this paper we represent posets via their strict ordering, i.e. with a transitive, irreflexive relation , since it better accommodates our semantics. Topological spaces can be viewed as an abstract representation of space. Indeed, the Euclidean spaces Rn are the most standard examples of topological spaces. Here, open sets are all U Rn for which every x U has ε > 0 such that d(x, y) < ε implies y U, where d(x, y) denotes the Euclidean distance.

A topology on X allows us to define concepts related to limits. In particular, x is a limit point of A X if every neighbourhood of x, with respect to the topology on X, contains at least one point a A distinct from x. This leads to the notion of the Cantor derivative of a subset of X.

Definition 2 (Cantor derivative). Let X = (X, τ) be a topological space. Given A X, the Cantor derivative of A is the set d(A) of all limit points of A. Given subsets A, B X, the Cantor derivative satisfies the following properties:

1. d( ) = ; 2. d(A B) = d(A) d(B); 3. dd(A) A d(A).

Note that if X is a topological space and A X, we do not always have that A d(A); elements of A \ d(A) are called isolated points of A. Cantor observed that if we iteratively remove isolated points of X, we eventually reach the largest subspace X X without isolated points. The subspace X may be empty: spaces with this property are known as scattered spaces. They can be defined without reference to X as follows:

Definition 3 (scattered space). A topological space (X, τ) is scattered if every nonempty subset has an isolated point.

Movement in space over discrete time can be modelled by equipping topological spaces with a transition function, which is assumed to be continuous. Recall that if (X, τX) and (Y, τY ) are topological spaces, then f : X Y is continuous if whenever U Y is open, then f 1(U) is open.

Definition 4 (dynamic topological system). A dynamic topological system is a triple S = (X, τ, f), where (X, τ) is a topological space and f : X X is a continuous function.

In this paper, we will mostly be concerned with dynamic topological systems based on a scattered space (or scattered dynamical systems for short). It is useful to observe that if (X, ) is a poset, then f : X X is continuous iff x y implies f(x) f(y). The class of all topological spaces will be denoted by TOP and the class of all dynamical systems by CTOP. In addition, the class of scattered spaces will be denoted by SCT and the class of all scattered dynamical systems by CSCT. Our goal is to axiomatise the dynamic topological logic of the systems in CSCT, as defined in the following subsection. It would be useful to share some of the motivation for discussing dynamic topological systems based on scattered spaces by providing two examples; the second of which will come later in the paper, after we establish some basic results.

Example 1 (first example of scattered dyanmics). Consider an algorithm that computes a number (say pi) with some degree of precision input by the user. This algorithm is guaranteed to terminate, but the actual computation time is determined by the initial input. This can be modelled using a scattered dynamical system as follows: Consider the ordinal ω + 1. This is the natural numbers with a limit point at infinity. The continuous predecessor function takes the predecessor of n + 1, and is the identity on 0 and ω. The initial state of the algorithm is ω, which jumps to some

value n after the user s input. Computations of this algorithm are modelled by our dynamical system, where each orbit x, f(x), f(f(x)), . . . is a computation.

In addition, there are some specific applications of scattered spaces to AI. For instance, in (Luo and Schulte 2006) it is shown that a class of languages is mind-change bounded (a notion related to learning theory) iff it is scattered in a suitable topology. Another example related to learning theory is the use of scattered spaces in situations where an agent can be surprised , i.e. learn unexpected information (Baltag, Bezhanishvili, and Fern andez Duque 2022). Constructive reasoning is another avenue where scattered spaces are used. Intuitionistic logic enjoys topological semantics and can be seen as a subsystem of either S4 or GL. Moreover, full intuitionistic LTL has not been axiomatised. Our framework embeds systems like Maier s (2004) in a way that has a more natural axiomatisation than S4, providing a better modal companion for such logics.

Dynamic Topological Logic We introduce the language with which we will be working with throughout the paper. Given a nonempty set PV of propositional variables, the language of the logic DGL is defined recursively as follows:

φ ::= p | φ φ | φ | φ | φ | φ,

where p PV. It consists of the Boolean connectives and , the temporal modalities next and eventually with its dual henceforth := , and the spatial modality for the Cantor derivative with its dual the co-derivative := . We define other connectives (e.g. , ) in the usual way. This language will be denoted from this point onward by L while the language without the henceforth operator, the language of the logic GLC (G odel-L ob logic with Continuity), will be denoted by L .

Definition 5 (semantics). A dynamic topological model is a tuple M = (X, τ, f, ν), where (X, τ, f) is a dynamic topological system and ν : PV (X) is a valuation function. Given φ L , we define the truth set JφK X of a formula φ as follows:

Jp K = ν(p); J φK = X\JφK; Jφ ψK = JφK JψK;

J φK = d(JφK); J φK = f 1(JφK); J φK = S n 0 f n(JφK).

We write M, x |= φ if x JφK and M |= φ if JφK = X. We may also denote a specific truth assignment by J KM or J Kν if we deal with more than one possible model or valuation.

Axiomatisation It was shown by Esakia (1981) and Simmons (1975) that the logic GL, whose characteristic axiom is ( φ φ) φ, is the logic of all scattered spaces with respect to the topological semantics where is interpreted as the Cantor

derivative operation. Aside from this change and a modified continuity axiom, our axiomatisation of DGL is very similar to Kremer and Mints axiomatisation (2005) and consists of the following axiom schemes: Taut := All propositional tautologies K := (φ ψ) ( φ ψ) L := ( φ φ) φ Next := φ φ Next := (φ ψ) φ ψ C := ( φ φ) φ K := (φ ψ) ( φ ψ) Fix := φ (φ φ) Ind := (φ φ) (φ φ) It also has the following inference rules:

MP := φ φ ψ

We write DGL φ or simply φ if φ is derivable using these rules and axioms. Given a dynamic topological system S = (X, τ, f), the intuition behind the axioms above can be stated briefly as follows: the axiom L expresses transitivity and wellfoundedness (Segerberg 1971), and in the case of a topology τ, it expresses that τ is a scattered space (Esakia 1981). Lemma 6. A topological space X = (X, τ) is scattered if and only if X |= L. The two operators Next and Next express the functionality of the map f : X X, and the axiom C expresses that f is continuous. Finally, the two axioms Fix and Ind express the properties of fixed-point and successor induction of , which dictate the behaviour of the henceforth operation. Each of these axioms is proven sound in either (Kremer and Mints 2005) or (Fern andez-Duque and Montacute 2022), yielding the following: Proposition 7 (soundness). The axiomatisation above is sound for the class of scattered dynamical systems. The logic GLC is the same as DGL, but as its language lacks the henceforth operator the corresponding axioms are omitted. When a formula φ is derivable in GLC we may write GLC φ, although, as mentioned, without a specified logic refers to derivability in DGL. Nevertheless, our proof of completeness will use the following result by Fern andez-Duque and Montacute (2022). Theorem 8 (GLC completeness). The logic GLC is complete and has the finite model property with respect to the class of scattered dynamical systems. In particular, note that every validity in GLC is syntactically derivable. This will become very useful in our proof of completeness for DGL, which can be stated as follows: Theorem 9 (completeness). CSCT |= φ implies φ, i.e all formulas valid on the class of scattered dynamical system are syntactically derivable in DGL.

The rest of the paper is devoted to this result. It involves several elements, so it will be useful to sketch their role in the proof. The general idea is to adapt a proof of completeness for linear temporal logic (Lichtenstein and Pnueli 2000). For readers familiar with completeness proofs of LTL, we recall two standard approaches. The first is to construct the (infinite) canonical model and then perform filtration to obtain a finite model. Filtration is needed since in the canonical model the relation used for interpreting is not necessarily the real transitive, reflexive closure of the successor function. While this property does hold in the filtrated model (obtained by taking a suitable quotient), the drawback is that after filtration, the modality is no longer interpreted via a function. We remedy this by unwinding ; that is, choosing a path [w0], [w1], . . . of elements of the filtrated model, where [w] denotes the equivalence class of w. In the terminology of the present paper, such a path is a realising path. This approach does not work in our setting since filtration destroys the continuity condition (which does hold in the canonical model of DGL). Instead, we follow something closer to the second approach, where we begin with a structure that looks like the final filtrated model, but might include too many points. To this end, fix a finite set Σ of DGL-formulas closed under subformulas and single negations (typically, the subformulas of some target formula φ). In the LTL setting, a point of this model would be a type Θ, i.e. a subset of Σ respecting Booleans: in particular, ψ Θ iff ψ / Θ, for ψ Σ. Other conditions may be imposed on types, e.g. ψ Θ implies ψ Θ. Let TΣ denote the set of all Σ-types. Using the truth conditions of the tenses and , we may define a successor relation SΣ on the set of Σ-types, so that for example if Θ SΣ and ψ Θ, then ψ . As was the case with the canonical model, ψ Θ does not necessarily imply that there is n and such that Θ Sn Σ and ψ . But in this case, rather than a quotient, we should take a subset of TΣ. Say that a type Θ is consistent if χ(Θ) := V Θ is consistent with respect to the axioms and rules of LTL. Let WΣ be the restriction of (TΣ, SΣ) to the set of consistent types. Then, much as was the case for the filtrated canonical model, WΣ does interpret correctly, but SΣ is not functional. As before, we obtain a proper LTL model by choosing a realising path on WΣ. Our proof of completeness of DGL grosso modo follows this second proof sketch. The biggest change is that types must be replaced by more complex objects. Conceptually, we may think of types as describing the state of affairs (relative to Σ) at a given moment in time. However, in the setting of dynamical systems, this involves not only stating which propositions hold, but also describing the local topological structure. As the purely topological fragment of DGL is just GL (i.e. the logic of scattered spaces), and GL is sound and complete for finite (strict) posets, we will let Σ-states be finite posets labelled by types: formally, a Σ-state is a structure w = (|w|, w, ℓw, 0w), where (|w|, w) is a strict, finite poset with a root 0w, and ℓw assigns a Σ-type ℓw(w) to each w |w|, satisfying some constraints to mimic the semantics of . The set of all Σ-states forms a structure which we denote

by UΣ, and plays the role of (TΣ, SΣ) in the LTL completeness proof. As was the case in the LTL proof, UΣ contains too many points, and so we must eliminate those Σstates that are inconsistent . This involves describing a Σstate w within our formal language. It is well known that finite frames can be described up to bisimulation in the modal language, but as it turns out, we need to describe states up to simulation (rather than bisimulation). The simulation formula for w is denoted by Sim(w) and plays the role of χ(Θ) in the LTL completeness proof. The existence of the formulas Sim(w) is precisely where the scatteredness assumption plays a role. In general topological spaces such formulas do not exist in the basic modal language and require tangled operators (Fern andez-Duque 2011). However, such operators are modally definable over the class of scattered spaces since the logic GL enjoys definable fixed points (Sambin and Valentini 1982). Thus our completeness proof can be entirely carried out in the original trimodal language of DTL. With this, we define WΣ, the restriction of UΣ to the set of consistent Σ-states, i.e. those Σ-states w such that Sim(w) is consistent with our axiomatisation of DGL. The structure WΣ does satisfy the required properties to ensure satisfiability. To be precise, WΣ is a quasimodel, a labelled strict poset which, aside from having a non-deterministic transition relation rather than a function, respects all semantic clauses of L . Quasimodels are quite general, with WΣ being only a special case, and as such they are defined much earlier. As it was in the case of LTL, a proper model may be obtained by extracting realising paths from any quasimodel Q. The major difference in our setting is that now we must simultaneously consider all realising paths and transform a quasimodel into a model via an unwinding procedure (Fern andez-Duque 2009). By defining the topology of Q in the right way, we in fact obtain a scattered dynamical system satisfying all formulas that were already satisfied in Q. As a final remark, note that contrary to the LTL setting, the structure WΣ for DGL is not finite. As we often need to consider disjunctions or conjunctions of formulas of the form Sim(w), and formulas are finite objects, this is a delicate issue when adapting the LTL proof. Fortunately, at each point in the proof, we may restrict our attention to finite sets of Σ-states: this is a deep fact that relies on an application of Kruskal s theorem pioneered by Gabelaia et al. (2006). This will come into play when we show that WΣ indeed respects the semantics of . As the treatment of quasimodels does not depend on the construction of UΣ and WΣ, we postpone it until later in the paper and first focus our attention on a general treatment of quasimodels.

Quasimodels

In this section, we introduce quasimodels, which are similar to scattered dynamical systems based on an Aleksandroff space (represented as the downset topology induced by a strict partial order). The only difference is that the transition function of quasimodels is replaced with a non-deterministic relation. These structures will be useful in our completeness

proof, as quasimodels are easier to construct than proper models. In order to maintain the validity of expressions such as (p q) p q, we equip each quasimodel Q with a labelling function ℓQ that assigns a type to each point. In the main result of this section we show that every formula satisfiable on a quasimodel Q is satisfiable on a scattered dynamical model. Given a formula φ, we denote by S(φ) the set of subformulas of φ, and we define S (φ) = S(φ) { ψ : ψ S(φ)}.

Definition 10 (type). A set Φ L is a type if the following conditions are satisfied:

1. There is no formula φ such that φ Φ and φ Φ; 2. If φ Φ then φ Φ; 3. If φ ψ Φ then φ, ψ Φ; 4. If (φ ψ) Φ then φ Φ or ψ Φ; 5. If φ Φ then φ Φ.

The set of all types is denoted by T. If Σ is a set of formulas closed under subformulas and single negations, we say that Φ is a Σ-type if Φ Σ and, for every φ Σ, either φ Φ or φ Φ (identifying φ with its double negation as needed). We denote by TΣ the set of all Σ-types. Often we will assume that Σ is finite: when Σ L is finite and closed under subformulas and single negations, we write Σ L .

Definition 11 (labelled poset). A labelled poset is a triple A = (|A|, A, ℓA), where |A| is a set of points, A is a strict partial order on |A|, and ℓA : |A| TΣ is a labelling function such that

φ ℓA(w) implies v(v w & φ ℓA(v)). φ ℓA(w) implies v(v w φ ℓA(v)).

If Σ is a set of formulas and the range of ℓA is contained in TΣ, we say that A is a Σ-labelled poset.

In the context of posets, a relation S |A| |B| between orders A and B is called continuous if it satisfies the forward-confluence property, i.e. if w A w and w Sv, then there is v such that w Sv and v B v .

Definition 12 (sensibility). Suppose that Φ, Ψ T. The ordered pair (Φ, Ψ) is sensible if

1. φ Φ implies that φ Ψ and φ Φ implies that φ Ψ; 2. φ Φ implies that φ Φ or φ Ψ; 3. φ Φ implies that φ Ψ.

Accordingly, a pair of points (w, v) in a labelled poset A is sensible if (ℓ(w), ℓ(v)) is sensible. A continuous relation S |A| |A| is sensible if every pair in S is sensible. Moreover, S is ω-sensible if it is serial and whenever φ ℓ(w), there is n 0 and there is a point v such that w Snv and φ ℓ(v).

We now have everything we need in order to provide the definition of a quasimodel. Below, a poset (W, ) is locally finite if w is finite for all w W.

Definition 13 (quasimodel). A weak quasimodel is a tuple Q = (|Q|, Q, SQ, ℓQ), where (|Q|, Q, ℓQ) is a locally

finite labelled poset and SQ |Q| |Q| is a sensible relation. If in addition SQ is ω-sensible, then Q is said to be a quasimodel, and if the range of ℓQ is contained in TΣ, we say that Q is a Σ-quasimodel (or weak Σ-quasimodel, if Q is not ω-sensible). We adopt the general convention that subscripts in e.g. Q or ℓQ will be dropped when this does not lead to confusion. Nevertheless, the subscripts will be useful when multiple structures are involved. Example 2. Let φ = ( p p) p. The following structure is a quasimodel, under the labelling given by ℓQ(w) = { p, . . .}, ℓQ(v) = { p p, p, . . .} and ℓQ(u) = { ( p p), p, φ, . . .} (where . . . indicates formulas omitted for simplicity).

This quasimodel falsifies φ at u, but it is known that the formula φ is valid on every Aleksandroff topological space (Kremer and Mints 2005). We will see that the quasimodel above witnesses that φ is not a theorem of GLC. Example 3. Quasimodels generalise dynamic poset models (i.e. dynamic topological models with the downset topology) in the following sense: Suppose that M is such a model, and let Σ be any set of formulas closed under subformulas. For w |M|, let ℓΣ(w) = {φ Σ : w JφKM}. Then, it is not hard to check that (|M|, M, SM, ℓΣ) is indeed a (deterministic) Σ-quasimodel. Henceforth, we will tacitly identify dynamic poset models with their associated quasimodel. Theorem 14. Every formula satisfiable on a quasimodel is satisfiable on a scattered dynamical model. We can now discuss a second example for a dynamic topological system based on a scattered space. Example 4 (second example of scattered dynamics). This example is reminiscent of the dynamical systems considered by Mortveit and Reidys (2008). An AI agent is presented with a DNA sample, and it must answer Yes or No , according to whether it matches the culprit s. After answering, the program runs one of two deterministic procedures (a criminal prosecution or an acquittal). This is modelled in a quasimodel with three states, yes , no , maybe , and the dynamical system itself consists of the computation paths through the automaton. Our strategy for the remainder of the completeness proof will therefore be to show that if φ is consistent, then it is satisfiable on a quasimodel: from Theorem 14, this suffices to ensure that it is indeed satisfiable on the class of scattered dynamical systems.

Simulating States and Simulation Formulas In this section we introduce the notion of Σ-states, which are local descriptions of quasimodels very similar to finite Σ-labelled posets but with a root. The Σ-states form the universe |UΣ| of the universal state space UΣ = (|UΣ|, , 7 , ℓ) of Σ, which will be used in order to establish the connection between our semantic framework and the syntactic derivations in DGL. The structure UΣ is universal in the sense that every model can be simulated by a Σ-state w |UΣ|. Simulations are the correct notion of embedding from the point of view of modal logic, just as bisimulations are the correct notion of isomorphism. In the context of labelled structures, this notion is defined as follows. Definition 15 (labelled simulation). Given two labelled posets A and B, a relation R |A| |B| is strictly forwardconfluent if a A a and a Rb implies that there is b B b such that a Rb . A labelled simulation is a strictly forwardconfluent relation χ |A| |B| such that wχv implies ℓA(w) = ℓB(v). After defining Σ-states, we will show that for each Σ-state w there is a formula Sim(w) defining the property of being simulated by w. We will then prove that certain derivations in regards to Sim(w) are possible whenever some relevant conditions on w hold. This part relies on the completeness and finite model property of GLC (Theorem 8). We later use this information to define the consistent restriction of UΣ and to show that this restriction is a canonical quasimodel.

Simulating States We first define the worlds of our universal structure, which we call states . Definition 16 (state). A state is a tuple

w = (|w|, w, ℓw, 0w),

where (|w|, w, ℓw) is a finite labelled poset and 0w is a distinguished point such that v 0w for all v |w|. If Σ is a set of formulas such that the range of ℓw is contained in TΣ, we say that w is a Σ-state. The set of all states is infinite, but it is essential that each individual state be finite. The following definition provides a useful way to measure the size of each state. Definition 17 (norm). Given a Σ-state w we denote by hgt(w) the maximum length of a -sequence of points in |w|. Moreover, we denote by wdt(w) the maximum N such that there exists w |w| with N daughters which are pairwise -incomparable. The norm of w is then defined as

w = max(hgt(w), wdt(w)).

Being labelled structures, the notion of simulation readily applies to states, with the caveat that all simulations must be root-preserving in this context. Definition 18 (simulations between states). Let w and v be Σ-states. We say that w simulates v if there exists a labelled simulation χ |w| |v| such that 0wχ0v. We write w v if w simulates v.

Note that compositions of simulations are simulations, given that compositions of strictly forward-confluent relations are also strictly forward-confluent. Thus the relation is transitive. Since the identity is a simulation, it is also reflexive. Thus is a quasiorder on the set of states. This relation will be essential in controlling the size of states we must consider, as when w v, it is often the case that v can be replaced by w as far as satisfiability is concerned, even when the latter is much smaller.

The Universal State Space Given a set of formulas Σ, the set of Σ-states forms a weak Σ-quasimodel. In order to see this, we first need to equip the set of Σ-states with a suitable strict partial order. Below, we say that a Σ-state v is a generated substructure of a Σ-state w if |v| is a downward-closed subset of |w| with respect to w, such that v = w (|v| |v|) and ℓv(v) = ℓw(v) for all v |v|. Definition 19 (substate). Let w and v be Σ-states. We call v a substate of w and denote it by v w if 0w = 0v |w| and v is a generated substructure of w. We write w 7 v if there exists a sensible relation R |w| |v| such that 0w R0v. We say that v is a bounded future of w and denote it by w 7 v, if w 7 v and in addition the following inequality is satisfied:

w |w| { φ ℓw(w)} .

Definition 20 (universal state space). Let Σ L and fix K 0. We define |UK Σ | to be the set of all Σ-states w for which w (K + 1) |Σ|. We denote by |UΣ| the union S k<ω |Uk Σ|, and we use it to define the universal state space

UΣ = (|UΣ|, , 7 , ℓ),

where ℓ(w) = ℓw(0w).

Simulation Formulas Next, we introduce the formulas Sim(w), which define the property of being simulated by w. Recall from Example 3 that if M is a model, then for x |M| we defined ℓΣ(x) = {φ Σ : x JφKM}, and that M is thus identified with the corresponding quasimodel. Thus the proposition below applies to both models and (weak) quasimodels. Proposition 21 (simulation formulas). Let w be a Σ-state. Then there exists a formula Sim(w) such that for every scattered dynamic model M and x |M|, we have that

x JSim(w)KM w (M, x).

There are a few important derivable properties that hold in relation to simulation formulas and that should be discussed before we proceed to the main part of the proof. Below, recall that Σ L means that Σ is finite and closed under subformulas and single negations.

Lemma 22. Let Σ L and let w = (|w|, , ℓ, 0w) be a Σ-state. Then the formula Sim(w) satisfies the following properties:

1. If φ ℓ(w), Sim(w) φ; 2. If v w, Sim(w) Sim(v); 3. If v w, Sim(w) Sim(v); 4. If φ Σ, φ _ {Sim(w) : w U0 Σ, φ ℓ(w)};

5. For all w UΣ, Sim(w) _ {Sim(v) : w 7 v}.

Canonical Quasimodels In this section we focus on constructing a canonical quasimodel for Σ. We denote it by WΣ, which we temporarily dub the canonical structure of Σ. It is the restriction of UΣ to consistent states, i.e. states w for which Sim(w). We prove that WΣ is a quasimodel by showing that 7 is serial and ω-sensible. Once we have all the required results, we can conclude that DGL is complete by showing that every consistent formula φ yields a consistent state w WΣ, where Σ = S (φ). Since WΣ is a quasimodel, QΣ |= φ. Since QΣ is a scattered dynamical model, the logic DGL is complete with respect to such models.

The Canonical Structure We say that a Σ-state w is inconsistent if Sim(w); otherwise it is consistent. The set of consistent Σ-states is denoted by Cons(Σ).

Definition 23 (canonical structure). For a set of formulas Σ, we define the canonical structure of Σ as the quadruple WΣ = (|WΣ|, WΣ, 7 WΣ, ℓWΣ), where

|WΣ| = Cons(Σ); WΣ = UΣ (Cons(Σ) Cons(Σ)); 7 WΣ = 7 UΣ (Cons(Σ) Cons(Σ)); ℓWΣ = ℓUΣ (Cons(Σ) (L )).

Lemma 24. Let Σ L . Then |WΣ| is open in |UΣ| and 7 WΣ is serial.

Efficiency and ω-Sensibility There is a point of tension that we need to address before proceeding. We need to be able to determine when a formula of the form φ will be realised, which becomes difficult as there is an infinite number of Σ-states to consider. We deal with this by showing that it is sufficient to consider a finite set of efficient paths, which allows us to only consider finitely many states when evaluating each instance of φ. In the following, we let w = (wn)n α denote a finite path of Σ-states.

Definition 25 (efficiency). A finite path w is called efficient if the following conditions are satisfied:

1. For all n < α, wn 7 wn+1; 2. For all i < j and states wi, wj in the path w, wi wj.

With this we define a notion of reachability which refines the transitive, reflexive closure of 7 .

Definition 26 (efficient reachability). Let w be a Σ-state. A Σ-state v is efficiently reachable from w if there exists a finite efficient path p = (p0, . . . , pα) of consistent states such that p0 = w and pα = v.

We denote by ϱ(w) the set of states that are efficiently reachable from w. The following is a deep consequence of Kruskal s tree theorem. Lemma 27. For every w |WΣ|, the set ϱ(w) is finite. We will use this result to ensure that the formulas in Lemma 28 and Lemma 29 below have finite disjunctions and hence are well defined. The following derivation is required for showing that 7 WΣ is ω-sensible: Lemma 28. Let w |WΣ|. Then

v ϱ(w) Sim(v) _

v ϱ(w) Sim(v). (1)

We are now ready to prove that 7 WΣ is ω-sensible. Lemma 29 (ω-sensibility). Let w |WΣ| and φ ℓ(w). Then there is v ϱ(w) such that φ ℓ(v). Putting together the above results, we conclude that WΣ is always a quasimodel.

Corollary 30. Given Σ L , the canonical structure WΣ is a quasimodel. We now have all the tools needed to prove completeness for DGL.

Proof of Theorem 9. Recall that a logic Λ is complete if and only if every Λ-consistent formula is satisfied on a Λ-model. Let φ L be a consistent formula, i.e. φ. Let Σ = S (φ). By Proposition 22.4, there must be some w |WΣ| such that φ ℓ(w). By Corollary 30, WΣ is a quasimodel satisfying φ, so that, by Theorem 14, there exists a scattered dynamical model that satisfies φ.

Conclusion We have exhibited the first finitely axiomatisable dynamic topological logic in the original trimodal language. The techniques employed here can be applied to related logics which may or may not be topologically inspired, including expanding products of modal logics (Gabelaia et al. 2006). In particular, dynamic Grzegorczyk logic (DGrz) could be treated in the same fashion, where is interpreted as closure rather than Cantor derivative. Note, however, that the Cantor derivative can define the topological closure, so completeness for DGrz should also follow from embedding it into DGL using proof-translation techniques. In fact, tangle-free logics may be applicable to a wider class of topological spaces by modifying the underlying Boolean algebra. Instead of considering the powerset of X, one may consider subalgebras (i.e. regular open or closed sets). In this setting, the tangled operators could also be trivialised, eliminating the need for such operators without restricting the class of topological spaces at one s disposal. Finally, there is the question of axiomatising the dynamic topological logic of Aleksandroff spaces. Chopoghloo and Moniri (2020) provided an infinitary proof system for this class, and the results of Fern andez-Duque (2014) apply in this setting as well and rule out a finite axiomatisation. However, it is possible that a natural, finitary proof system can be found in this setting (albeit with infinitely many axioms).

Acknowledgements David Fern andez-Duque was supported by RVO 67985807, by the Czech Science Foundation project GA22-01137S, and by the FWO-FWF Lead Agency grant G030620N (FWO)/I4513N (FWF).

References Abashidze, M. 1985. Ordinal completeness of the G odel L ob modal system. Intensional Logics and the Logical Structure of Theories, 49 73. In Russian. Alpern, B.; and Schneider, F. B. 1985. Defining Liveness. Inf. Process. Lett., 21(4): 181 185. Art emov, S. N.; Davoren, J. M.; and Nerode, A. 1997. Modal Logics and Topological Semantics for Hybrid Systems. Technical report msi 97-05, Cornell University. Baltag, A.; Bezhanishvili, N.; and Fern andez-Duque, D. 2021. The Topological Mu-Calculus: completeness and decidability. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, 1 13. IEEE. Baltag, A.; Bezhanishvili, N.; and Fern andez-Duque, D. 2022. The Topology of Surprise. In Kern-Isberner, G.; Lakemeyer, 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. Beklemishev, L. D. 2004. Provability algebras and prooftheoretic ordinals, I. Ann. Pure Appl. Log., 128(1-3): 103 123. Brunton, S. L.; and Kutz, J. N. 2019. Data-driven science and engineering: Machine learning, dynamical systems, and control. Cambridge University Press. Chopoghloo, S.; and Moniri, M. 2020. An infinitary axiomatization of dynamic topological logic. Logic Journal of the IGPL. Chu, M. T. 2008. Linear algebra algorithms as dynamical systems. Acta Numerica, 17: 1 86. Esakia, L. 1981. Diagonal constructions, L ob s formula and Cantor s scattered spaces. Studies in logic and semantics, 132(3): 128 143. Fern andez-Duque, D. 2009. Non-deterministic semantics for dynamic topological logic. Ann. Pure Appl. Log., 157(23): 110 121. Fern andez-Duque, D. 2011. On the Modal Definability of Simulability by Finite Transitive Models. Studia Logica, 98: 347 373. Fern andez-Duque, D. 2012. A Sound and Complete Axiomatization for Dynamic Topological Logic. Journal of Symbolic Logic, 77(3): 947 969. Fern andez-Duque, D. 2014. Non-finite axiomatizability of dynamic topological logic. ACM Transactions on Computational Logic, 15(1): 4:1 4:18. 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. Gabelaia, D.; Kurucz, A.; Wolter, F.; and Zakharyaschev, M. 2006. Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic, 142(1-3): 245 268. Galton, A. 2009. Spatial and temporal knowledge representation. Earth Sci. Informatics, 2(3): 169 187. Hanrot, G.; Pujol, X.; and Stehl e, D. 2011. Analyzing blockwise lattice algorithms using dynamical systems. In Annual Cryptology Conference, 447 464. Springer. Kremer, P.; and Mints, G. 2005. Dynamic Topological Logic. Annals of Pure and Applied Logic, 131: 133 158. Kudinov, A.; and Shehtman, V. 2014. Derivational Modal Logics with the Difference Modality. In Leo Esakia on Duality in Modal and Intuitionistic Logics, 291 334. Springer. Lichtenstein, O.; and Pnueli, A. 2000. Propositional Temporal Logics: Decidability and Completeness. Logic Jounal of the IGPL, 8(1): 55 85. Lin, H.; and Antsaklis, P. J. 2014. Hybrid Dynamical Systems: An Introduction to Control and Verification. Found. Trends Syst. Control, 1(1): 1 172. Luo, W.; and Schulte, O. 2006. Mind change efficient learning. Inf. Comput., 204(6): 989 1011. Maier, P. 2004. Intuitionistic LTL and a New Characterization of Safety and Liveness. In Marcinkowski, J.; and Tarlecki, A., eds., Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, 295 309. Springer. Mortveit, H. S.; and Reidys, C. M. 2007. An Introduction to Sequential Dynamical Systems. Berlin, Heidelberg: Springer-Verlag. ISBN 0387306544. Mortveit, H. S.; and Reidys, C. M. 2008. An Introduction to Sequential Dynamical Systems. Universitext. Springer. ISBN 978-0-387-30654-4. Sambin, G.; and Valentini, S. 1982. The modal logic of provability. The sequential approach. J. Philos. Log., 11(3): 311 342. Scott, D. S. 1982. Domains for Denotational Semantics. In Nielsen, M.; and Schmidt, E. M., eds., Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings, volume 140 of Lecture Notes in Computer Science, 577 613. Springer. Segerberg, K. 1971. An essay in classical modal logic. Filosofiska F oreningen och Filosofiska Institutionen vid Uppsala Universitet. Simmons, H. 1975. Topological aspects of suitable theories. Proceedings of the Edinburgh Mathematical Society, 19(4): 383 391. Weinan, E. 2017. A proposal on machine learning via dynamical systems. Communications in Mathematics and Statistics, 5(1): 1 11.