Complete Intuitionistic Temporal Logics in Topological Dynamics

TL;DR

This paper axiomatizes and proves completeness for intuitionistic temporal logic over topological dynamics, extending the understanding of its decidability and applicability to various spaces.

Contribution

It provides a formal axiomatization and completeness results for intuitionistic temporal logic in topological dynamics, including specific fragments and spaces.

Findings

Decidability of the logic established by Fernández-Duque

Axiomatization of the logic and its fragments provided

Completeness proven for several familiar topological spaces

Abstract

The language of linear temporal logic can be interpreted over 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\'andez-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.