A note on bisimulation and modal equivalence in provability logic and interpretability logic (Q361870)

Interpretability logic is a modal logic for studying interpretability between theories. For detailed definitions see, e.g. [\textit{A. Visser}, CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020); \textit{G. Japaridze} and \textit{D. de Jongh}, Stud. Logic Found. Math. 137, 475--546 (1998; Zbl 0915.03019)]. There are a few semantics for interpretability logic. The basic one is Veltman semantics. \textit{A. Visser}, defined [in: Mathematical logic, Proc. Summer Sch. Conf. Ded. 90th Anniv. Arend Heyting, Chaika/Bulg. 1988, 175--209 (1990; Zbl 0793.03064)] bisimulations between Veltman models. In the paper under review a counterexample for the reverse of the Hennessy-Milner theorem for Veltman semantics is given. The authors use games on Veltman models and prove the basic property of games, i.e.\ the winning strategy for such a game is equivalent to picking out a bisimulation between two models.