Bisimulations for intuitionistic temporal logics

TL;DR

This paper develops bisimulations for an intuitionistic temporal logic, demonstrating that certain temporal operators cannot be defined in terms of others, highlighting the logic's expressive limitations.

Contribution

It introduces bisimulations for $ITL^e$, an intuitionistic temporal logic, and proves non-definability results among key temporal operators.

Findings

'Eventually' cannot be defined by 'next' and 'henceforth'

'Henceforth' cannot be defined by 'next' and 'until'

Results hold even over here-and-there models

Abstract

We introduce bisimulations for the logic $ITL^e$ with `next', `until' and `release', an intuitionistic temporal logic based on structures equipped with a partial order used to interpret intuitionistic implication and a monotone function used to interpret the temporal modalities. Our main results are that `eventually', which is definable in terms of `until', cannot be defined in terms of `next' and `henceforth', and similarly that `henceforth', definable in terms of `release', cannot be defined in terms of `next' and `until', even over the smaller class of here-and-there models.