Bisimulations for Intuitionistic Temporal Logics.

We introduce bisimulations for the logic ITLe with ◯ (‘next’), U (‘until’) and R (‘release’), an intuitionistic temporal logic based on structures (W, ≼, S), where ≼ is used to interpret intuitionistic implication and S is a ≼-monotone function used to interpret the temporal modalities. Our main results are that ◇ (‘eventually’), which is definable in terms of U, cannot be defined in terms of ◯ and ◻, and similarly that ◻ (‘henceforth’), definable in terms of R, cannot be defined in terms of ◯ and U, even over the smaller class of here-and-there models.

Authors

• Philippe Balbiani
• Joseph Boudou
• Martín Diéguez
• David Fernández-Duque

Keywords

No keywords are indexed for this paper.