A Decidable Intuitionistic Temporal Logic

Abstract

We introduce the logic $\mathsf{IT}{\mathsf{L}}^{\mathsf{e}}$, an intuitionistic temporal logic based on structures $(W,\preccurlyeq ,S)$, where $\preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $\mathsf{IT}{\mathsf{L}}^{\mathsf{e}}$ are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a `persistent' version of the logic, $\mathsf{IT}{\mathsf{L}}^{\mathsf{p}}$, whose models are similar to Cartesian products. We prove that, unlike $\mathsf{IT}{\mathsf{L}}^{\mathsf{e}}$, $\mathsf{IT}{\mathsf{L}}^{\mathsf{p}}$ does not have the finite model property.

Cited by in corpus (4)

• The intuitionistic temporal logic of dynamical systems
• Bisimulations for intuitionistic temporal logics
• Exploring the Jungle of Intuitionistic Temporal Logics
• Intuitionistic Linear Temporal Logics