Dynamic Topological Logic

Origin. Two 1997 starting points. Sergei Artemov, Jennifer Davoren, and Anil Nerode, "Modal Logics and Topological Semantics for Hybrid Systems" (Technical Report MSI 97-05, Cornell University, 1997), introduced the bimodal system S4C and proved it finitely axiomatizable, decidable, and with the finite model property; Philip Kremer and Grigori Mints announced the program in the Bulletin of Symbolic Logic 3 (1997) — Kremer and Mints, "Dynamic Topological Logic" (371–372), Kremer, "Temporal Logic over S4: An Axiomatizable Fragment of Dynamic Topological Logic" (375–376), and Kremer, Mints, and Rybakov, "Axiomatizing the Next-Interior Fragment of Dynamic Topological Logic" (376–377). The full paper is Kremer and Mints, "Dynamic Topological Logic" (Annals of Pure and Applied Logic 131, 2005, 133–158), which added the henceforth operator and proposed an axiomatization of the trimodal logic, conjectured complete. The negative results are Boris Konev, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev, "Dynamic Topological Logics over Spaces with Continuous Functions" (Advances in Modal Logic 6, 2006, 299–318) and "On Dynamic Topological and Metric Logics" (Studia Logica 84, 2006, 129–160); the positive ones are David Fernández-Duque's, chiefly "A Sound and Complete Axiomatization for Dynamic Topological Logic" (Journal of Symbolic Logic 77(3), 2012, 947–969) and "Non-Finite Axiomatizability of Dynamic Topological Logic" (ACM Transactions on Computational Logic 15(1), 2014).

Models. A dynamic topological system is a topological space with a continuous function f on it, and the logic speaks about orbits x, f(x), f²(x), … — the long-term behaviour of iteration, topological recurrence included. The language joins the two readings this collection records separately: the McKinsey–Tarski topological semantics of S4 (see Spatial Logic), with □ as interior, and the next and henceforth operators of linear temporal logic (see Temporal Logic), read along the orbit. The motivation was specification of hybrid systems — liveness and safety for systems mixing discrete steps with continuous state spaces. The finding, after two decades, is that the combination behaves far worse than either half: S4 is decidable, LTL is PSPACE-complete, and full DTL is undecidable and not finitely axiomatizable in its own language.

Formalism.

Language and semantics: □ (interior), ○ (next), * (henceforth), over ⟨X, f⟩ with f continuous: ⟦□φ⟧ = Int ⟦φ⟧ ⟦○φ⟧ = f⁻¹ ⟦φ⟧ ⟦*φ⟧ = ⋂ₙ f⁻ⁿ ⟦φ⟧ over all n ≥ 0 Valid: ⟦φ⟧ = X in every system.

Continuity: The axiom ◇○p → ○◇p, valid because f is continuous: the preimage of an open set is open. With f a homeomorphism more is valid, and the system S4H captures it (Kremer and Mints 2005).

The next-interior fragment (□, ○): S4C: finitely axiomatizable, decidable, finite model property (Artemov, Davoren, and Nerode 1997). The same logic over arbitrary spaces and over Aleksandrov spaces. Complete for ℝ² (Fernández-Duque, Logic Journal of the IGPL 15(1), 2007, 77–107); the case of ℝ posed as open by Konev–Kontchakov–Wolter–Zakharyaschev (2006). S4H, the homeomorphism variant: complete for the homeomorphism systems (Kremer and Mints 2005); over arbitrary spaces, Aleksandrov spaces, and each ℝⁿ the validities coincide, with the finite model property and decidability.

The shallow fragment: No temporal operator inside a topological one: axiomatized by Kremer and Mints (2005), decidable, and insensitive to the choice among arbitrary spaces, Aleksandrov spaces, and ℝⁿ, continuous functions or homeomorphisms.

Full DTL: Undecidable over arbitrary spaces and over each ℝⁿ, n ≥ 1, by reduction of ω-reachability for lossy channel systems — already for the fragment in which topological operators never apply to formulas containing a temporal eventuality (Konev, Kontchakov, Wolter, Zakharyaschev 2006). Over continuous functions: recursively enumerable (Fernández-Duque, "Non-Deterministic Semantics for Dynamic Topological Logic", Annals of Pure and Applied Logic 157, 2009, 110–121); for the eventuality-restricted fragment this follows from Kruskal's tree theorem (Konev et al. 2006). Over homeomorphisms: the logics of arbitrary spaces, Aleksandrov spaces, and ℝⁿ are pairwise distinct and none is recursively enumerable (Konev et al., Studia Logica 2006) — the negative answer to a Kremer–Mints conjecture. Not finitely axiomatizable, in any language between the trimodal language and the tangled extension; the Kremer–Mints system is incomplete (Fernández-Duque 2014).

The tangled extension: L*: ◇ applies to finite sets of formulas; ⟦◇Γ⟧ = the union of all E such that each ⟦γ⟧, γ ∈ Γ, is dense in E — a greatest fixpoint, the tangled closure. DTL* is sound and complete over L* (Fernández-Duque, JSL 2012). The temporal-free tangled fragment is expressively equal to the bisimulation-invariant fragments of first-order and monadic second-order logic over finite S4 models, and the plain modal fragment is weaker (Dawar and Otto 2009) — the added expressive power the completeness proof uses. In the original trimodal language, completeness holds over scattered spaces (Fernández-Duque and Montacute, "Untangled: A Complete Dynamic Topological Logic", AAAI 2023, 6355–6362).

Metric variant: Interior and closure replaced by "everywhere/somewhere within distance a", a ∈ ℚ⁺, over metric spaces with isometries: decidable, but not in time bounded by any elementary function (Konev et al., Studia Logica 2006).

Symbols.

Metatheory. The next-interior fragment is a well-behaved modal logic — axiomatization, finite model property, decidability, all in Artemov, Davoren, and Nerode (1997) — and the henceforth operator is what breaks it. Konev, Kontchakov, Wolter, and Zakharyaschev (2006) proved full DTL undecidable over arbitrary spaces and over every ℝⁿ by encoding lossy channel systems, and proved the homeomorphism logics not recursively enumerable, refuting the Kremer–Mints conjecture for that case; Fernández-Duque (2009) proved the continuous-function logic recursively enumerable, so an axiomatization exists in principle, and then (2014) proved that no finite one exists in the trimodal language and that the Kremer–Mints system is incomplete. His completeness theorem (2012) holds over the tangled language, whose extra expressive power over finite S4 models is exactly the bisimulation-invariant fragment of first-order and monadic second-order logic (Dawar and Otto 2009); the tangled closure is a greatest fixpoint — a μ-calculus operator rather than a plain modality (see Modal Mu-Calculus). The 2023 Fernández-Duque–Montacute system is the first complete axiomatization in the original language, obtained by restricting to scattered spaces. The □-only fragment is S4 with the McKinsey–Tarski completeness the Spatial Logic entry records.

Applies to. Topological dynamics: statements about orbits, iteration, and recurrence over a space and a continuous map. Specification of hybrid systems — the Artemov–Davoren–Nerode motivation, developed in Davoren's Modal Logics for Continuous Dynamics (PhD thesis, Cornell, 1998). The combination theory of spatial and temporal logics (Gabelaia, Kontchakov, Kurucz, Wolter, Zakharyaschev, Journal of Artificial Intelligence Research 23, 2005), where DTL shows a combination can be harder than either component. Lossy channel systems and well-quasi-order methods, which supply both the undecidability encoding and the Kruskal-based enumerability proof.

Limitations. Full DTL is undecidable over arbitrary spaces and over each ℝⁿ, and over homeomorphisms not even recursively enumerable, so for invertible dynamics there is no proof system at all. In the native trimodal language there is no finite axiomatization even where the validities are recursively enumerable; completeness has been reached only by extending the language with the tangle operator or by restricting to scattered spaces, which exclude ℝⁿ and every dense-in-itself space. The temporal vocabulary is next and henceforth only — no until. The metric variant is decidable but not elementarily so. Whether the next-interior fragment is complete for ℝ was posed as an open problem in 2006. And the undecidability already strikes the fragment that keeps topological operators away from eventualities, so no simple syntactic discipline on the mixing of the two modal families restores decision procedures.

© 2026 Lingenic LLC