Dynamic Topological Logic (DFH) is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of DFH over the class of all dynamical systems has proven to be quite elusive. Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different (...) context. We then provide a sound axiomatization for DFH over this extended language, and prove that it is complete. The polyadic modality is used in an essential way in our proof. (shrink)

The language of linear temporal logic can be interpreted on the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${\sf ITL}^{\sf c}_{\Diamond \forall }$, recently shown to be decidable by Fernández-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.