Bisimulations for intuitionistic temporal logics

Philippe Balbiani, Joseph Boudou, Marín Diéguez, David Fernández-Duque

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.

arrow_drop_up