| Popis: |
Correspondence theory systematically investigates the relationship between modal and classical logic. Bisimulations and standard translation are the two tools we need to understand modal expressivity. Van Benthem’s characterization theorem shows that modal languages correspond to the bisimulation invariant fragment of first–order languages, which is established by classical methods of first–order model theory. Perkov and Vuković proved that a first–order formula is equivalent to the standard first–order translation of some formula of interpretability logic with respect to Veltman models if and only if it is invariant under bisimulations between Veltman models. In order to prove that, they used bisimulation games on Veltman models for interpretability logic and an appropriate notion of model unravelling, somewhat analogous to the usual tree unravelling. Since for the standard definition of bisimulations (and their finite approximations called n-bisimulations) the basic result that two worlds are n-bisimilar if and only if they are n-equivalent (i.e. they satisfy the same IL-formulas of modal depth up to n) does not hold, we have defined in [3] a new notion of bisimulations for Verbrugge semantics called w- bisimulations. In this talk we will present that new definition and show that two worlds are n-equivalent if and only if they are n-w- bisimilar. In order to do that we will define Verbrugge model comparison games called w- games and show that wbisimulation relations may be understood as descriptions of winning strategies for one player in a w-game. Finally, we will present the appropriate notion of saturated bisimilar companion to Verbrugge models. |
