Dynamic Topological Logic

Dynamic Topological Logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ (the standard “box” of modal logic) is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system be a topological space X together with a continuous function f. The function f can be thought of in temporal terms, moving the points of the topological space X from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □ (interior), and two temporal modalities, ○ (a circle for ‘next’) and * (an asterisk for ‘henceforth’), both interpreted using the continuous function f. In particular, ○ expresses the action of f action on X from one moment to the next, and * expresses the asymptotic behaviour of f.

Various fragments of DTLs have been axiomatized, and some important DTLs in the trimodal language have been shown to be nonaxiomatizable.

1. Introductory papers

S. Artemov, J. Davoren and A. Nerode 1997, “Modal logics and topological semantics for Hybrid Systems”, Technical Report MSI 97-05, Cornell University.

P. Kremer and G. Mints 2005, “Dynamic topological logic”, Annals of Pure and Applied Logic 131, 133-158.¹

P. Kremer and G. Mints 2007, “Dynamic topological logic”, in M. Aiello, I. Pratt-Harman, and J. van Benthem (eds.), Handbook of Spatial Logics, Springer-Verlag 2007, 565-606.

2. Bimodal next-interior (○, □) fragments

In the bimodal language with the topological modality □ and the temporal modality ○, define the logic S4C by any axioms for classical logic plus the following:

S4 axioms for □: (□A → A), (□A → □□A)

Commutativity of ○ with Boolean connectives:

(○~A ↔ ~○A), (○(A & B) ↔ (○A & ○B)), (○(A ∨ B) ↔ (○A ∨ ○B))

Continuity: (○□A → □○A).

We also add the rules of Modus Ponens and Necessitation for □ and ○. Define the logic S4H, in this language, by adding the following converse of the continuity axiom:

Converse of continuity: (□○A → ○□A)

S4H is sound and complete for homeomorphisms on topological spaces (Kremer and Mints 2005); for homeomorphisms on the real line, R (Kremer and Mints 2005). The methods used to show this second result can easily be extended to show that S4H is sound and complete for homeomorphisms on the rationals, Q; on Cantor space; on Rⁿ, for any n; and on finite topological spaces. S4C is sound and complete for continuous functions on topological spaces and on finite topological spaces (Artemov, Davoren and Nerode 1997). We also have the following results:

2.1. S4C is complete for continuous functions on Cantor space

G. Mints and T. Zhang 2005, “Propositional logic of continuous transformations in Cantor space”, Archive for Mathematical Logic 44, 783-799..

P. Kremer 2006, “The modal logic of continuous functions on Cantor space”, Archive for Mathematical Logic 45, 1021-1032.

2.2. S4C is complete for continuous functions on the following class of topological spaces: {Rⁿ: n > 1}.

S. Slavnov 2005, “On completeness of dynamic topological logic”, Moscow Mathematical Journal 5, 477-492.

2.3. S4C is complete for continuous functions on the real plane, R².

D. Fernández Duque 2005, “Dynamic topological completeness for R²”, Logic Journal of IGPL 15, 77-107.

Note that this is stronger than the result of Slavnov 2005.

2.4. S4C is complete for continuous functions on the rational numbers, Q.

P. Kremer 2007, “The modal logic of continuous functions on rational numbers”, manuscript.

2.5. S4C is not complete for continuous functions on the real line, R.

For one counterexample to the completeness of S4C for the real line see Kremer and Mints 2005; for another, see S. Slavnov (2003), “Two counterexamples in the logic of dynamic topological systems”, Technical Report TR-2003015, Cornell University.

3. Trimodal DTLs.

3.1. Incompleteness of important trimodal DTLs and related results.

3.1.1. B. Konev, R. Kontchakov, F. Wolter and M. Zakharyaschev (2006), “On dynamic topological and metric logics”, Studia Logica 84, 129-160. (The conference version appeared in R. Schmidt, I. Pratt-Hartmann, M. Reynolds, H. Wansing, (editors), Proceedings of AiML 2004, 182-196, September 2004, Manchester, U.K.)

Abstract: We investigate computational properties of propositional logics for dynamical systems. First, we consider logics for dynamic topological systems (W, f), where W is a topological space and f a homeomorphism² on W. The logics come with ‘modal’ operators interpreted by the topological closure and interior, and temporal operators interpreted along the orbits {w, f(w), f²(w), ... } of points w in W. We show that for various classes of topological spaces the resulting logics are not recursively enumerable (and so not recursively axiomatisable). This gives a ‘negative’ solution to a conjecture of Kremer and Mints. Second, we consider logics for dynamical systems (W, f), where W is a metric space and f an isometric function. The operators for topological interior/closure are replaced by distance operators of the form ‘everywhere/somewhere in the ball of radius a’, for a in Q⁺. In contrast to the topological case, the resulting logic turns out to be decidable, but not in time bounded by any elementary function.

3.1.2. B. Konev, R. Kontchakov, F. Wolter and M. Zakharyaschev (2006), “Dynamic topological logics over spaces with continuous functions”, in G. Governatori, I. Hodkinson and Y. Venema (editors), Advances in Modal Logic, vol.6, 299-318, College Publications, London, 2006.

Abstract: Dynamic topological logics are combinations of topological and temporal modal logics that are used for reasoning about dynamical systems consisting of a topological space and a continuous function on it. Here we partially solve a major open problem in the field by showing (by reduction of the ω-reachability problem for lossy channel systems) that the dynamic topological logic over arbitrary topological spaces as well as those over Euclidean spaces Rⁿ, for each n ≥ 1, are undecidable. Actually, we prove this result for the natural and expressive fragment of the full dynamic topological language where the topological operators cannot be applied to formulas containing the temporal eventuality. Using Kruskal’s tree theorem we also show that the formulas of this fragment that are valid in arbitrary topological spaces with continuous functions are recursively enumerable, which is not the case for spaces with homeomorphisms.

3.2. The trimodal DTL of continuous functions on topological spaces is recursively enumerable.

D. Fernández Duque (2007), “Non-deterministic semantics for dynamic topological logic”, manuscript. This paper is now in print as D. Fernández Duque (2009), “Non-deterministic semantics for dynamic topological logic”, Annals of Pure and Applied Logic 157, 110-121.

Fernández Duque closes one of the main open problems in DTL (left open by Konev et al), by showing that the trimodal DTL of continuous functions on topological spaces is recursively enumerable. This contrasts sharply with the results of Konev et al concerning the logic of homeomorphisms (3.1.1, above). In a forthcoming paper, Fernández Duque also shows that this same logic is complete for interpretations on metric spaces.

3.3. Dynamic topological S5

P. Kremer 2007, “Dynamic topological S5”, manuscript.

This paper axiomatizes the following four conservative extensions of S5: the logic of continuous functions on almost discrete topological spaces; of homeomorphisms on almost discrete topological spaces; of continuous functions on trivial topological spaces; and of homeomorphisms on trivial topological spaces.

4. Intuitionistic DTL

The ideas behind modal DTLs can readily be extended to defining intuitionistic DTLs. Completeness results for the fragment with ‘next’ but not ‘henceforth’ can be given along the lines of Kremer and Mints 2005 or Artemov, Davoren and Nerode 1997, above. The axiomatizability question for the intuitionistic DTL in the full language, with both ‘next’ and ‘henceforth’ remains open. One might expect the following principles: (*p → **p), (*p → ○*p), and (*○p → ○*p). But they fail. See P. Kremer 2004, “A small counterexample in intuitionistic dynamic topological logic”.