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, ⬛ 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. f can be thought of in temporal terms, moving the points of the topological space 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, ○ (next) and ∗ (henceforth), both interpreted using the continuous function f. In particular, ○ expresses f 's action on X from one moment to the next, and ∗ expresses the asymptotic behaviour of f.