A sound and complete axiomatization for Dynamic Topological Logic

Dynamic Topological Logic (DTL) 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 DTL 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 DTL over this extended language, and prove that it is complete. The polyadic modality is used in an essential way in our proof.