Complete Intuitionistic Temporal Logics in Topological Dynamics

Abstract

The language of linear temporal logic can be interpreted over the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${{\mathsf{ITL}}^{\mathsf{c}}}_{◊,\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.