# Bisimulations for intuitionistic temporal logics

arXiv: https://arxiv.org/abs/1803.05078 · HTML: https://mlsanity.com/paper/1803.05078/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Mar 2018.

## Built on by (most cited first, 1 of 1)

- [G"odel-Dummett linear temporal logic](https://mlsanity.com/paper/2306.15805/) (2023)

## Abstract (arXiv)

We introduce bisimulations for the logic ITLe 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.