Axiomatic systems and topological semantics for intuitionistic temporal logic

TL;DR

This paper introduces four new axiomatic systems for intuitionistic linear temporal logic, establishing their soundness over Kripke and topological structures, and explores their semantic differences and equivalences.

Contribution

It presents novel axiomatic systems and a topological semantics for intuitionistic linear temporal logic, including a new interpretation of the 'henceforth' modality.

Findings

Four distinct axiomatic systems are sound for different classes of structures.

A new topological interpretation of the 'henceforth' modality is proposed.

Validity sets coincide for relational and topological semantics in the 'henceforth'-free fragment.

Abstract

We propose four axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. Our topological semantics features a new interpretation for the `henceforth' modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the four logics obtained from the axiomatic systems are distinct. Finally, we show that when the language is restricted to the `henceforth'-free fragment, the set of valid formulas for the relational and topological semantics coincide.