On the modal definability of simulability by finite transitive models (Q763328)

Given a finite, transitive and reflexive Kripke model \(\langle W, \preccurlyeq, [ \mkern-3mu [ \cdot ] \mkern-3mu ] \rangle\) and \(w \in W\), it is shown that the property ``being simulated by \(w\)'' (i.e. lying on the image of a literal-preserving relation satisfying the ``forth'' condition of bisimulation) is modally undefinable within the class of \({\mathsf S4}\) Kripke models (contrary to \({\mathsf K4}\), which is also proved). A minor extension of the language by adding a sequent operator \(\natural\) (``tangle'') which can be interpreted over Kripke models as well as over topological spaces is proposed. In the extended language \({\mathsf L}^+ = {\mathsf L}^{\square \natural}\), being simulated by a point on a finite transitive Kripke model becomes definable, both over the class of arbitrary Kripke models and over the class of topological \({\mathsf S4}\) models. As a consequence it is obtained that any class of finite, transitive models over finitely many propositional variables closed under simulability is also definable in \({\mathsf L}^+\), as well as Boolean combinations of these classes. From this it follows that the \(\mu\)-calculus interpreted over any such class of models is decidable.