The intuitionistic temporal logic of dynamical systems

Abstract

A dynamical system is a pair $(X,f)$, where $X$ is a topological space and $f:X\to X$ is continuous. Kremer observed that the language of propositional linear temporal logic can be interpreted over the class of dynamical systems, giving rise to a natural intuitionistic temporal logic. We introduce a variant of Kremer's logic, which we denote $\mathsf{IT}{\mathsf{L}}^{\mathsf{c}}$, and show that it is decidable. We also show that minimality and Poincaré recurrence are both expressible in the language of $\mathsf{IT}{\mathsf{L}}^{\mathsf{c}}$, thus providing a decidable logic expressive enough to reason about non-trivial asymptotic behavior in dynamical systems.

References in corpus (1)

• A Decidable Intuitionistic Temporal Logic

Cited by in corpus (2)

• An intuitionistic axiomatization of `eventually'
• Exploring the Jungle of Intuitionistic Temporal Logics