Ehrenfeucht-Fraisse games and first order formulas in one free variable

I've been reading lately Martin Otto's proof of Van Benthem - Rosen theorem. This theorem states that first order formula in one free variable $\alpha(x)$ (in vocabulary of Kripke structures, that is: vocabulary $\sigma$ consists of one binary relational symbol $R$ which corresponds to accesibility relation $R$ and countably many unary symbols $(P_{n})_{n\in\mathbb{N}}$ which correspond to propositional letters $(p_{n})_{n\in\mathbb{N}}$) is standard stranslation of some basic modal formula over finite Kripke structures if and only if $\alpha(x)$ is bisimulation invariant. Bisimulation invariance means that for every two bisimilar pointed Kripke structures $(\mathfrak{M},w)$ and $(\mathfrak{M}',w')$ we have $$\mathfrak{M}\models\alpha[w]\Leftrightarrow\mathfrak{M}'\models\alpha[w']$$ In order to prove this theorem, we have to consider EF games. Ehrenfeucht's theorem states that two $\sigma$-structures $\mathfrak{M}$ and $\mathfrak{M}'$ (where $\sigma$ is finite and purely relational) correspond at every first order sentence $\varphi$ whose quantifier rank is less or equal to $q\in\mathbb{N}$ (that is $\mathfrak{M}\models\varphi$ iff $\mathfrak{M}'\models\varphi$ ) if and only if Duplicator has winning strategy in EF game on these structure in $q$ moves. Recall that correspondence at every first order sentence of quantifier rank less or equal to $q$ is also calles $q$-elementary equivalence and is denoted as $\equiv_{q}$.

It is easy to define notions of bisimilarity and modal equivalence (and their finite approximations) for pointed Kripke structures. It is also easy to define elementary equivalence (and $q$-elementary equivalence) for Kripke structures. Problem is that standard translation of simple modal formula has one free variable and, consequently, is not a sentence.

So, after brief introduction, my question would be: does it make sense to talk about $q$-elementary equivalence of pointed Kripke structures $(\mathfrak{M},w)$ and $(\mathfrak{M}',w')$? My notion of such thing would be that two pointed Kripke structures are $q$-elementary equivalent if for every first order formula in one free variable $\alpha(x)$ whose quantifier rank is less or equal than $q$ we have $$\mathfrak{M}\models\alpha[w]\Leftrightarrow\mathfrak{M}'\models\alpha[w']$$ So, my idea is to produce a sentence from $\alpha(x)$ by assigning $w$ and $w'$ to free variable $x$.

Even better question now is: what are the rules of EF game in pointed Kripke structures?

• Have you tried treating pointed Kripke structures as structures for the vocabulary of Kripke structures and one addiitonal constant symbol (to denote the "point" $w$)? – Andreas Blass Aug 18 '18 at 19:21

There should be a natural way to define EF games in the given situation. Take a look at "On the expressive power of CTL" by Moller and Rabinovich. They define bisimulation equivalence, q-bisimilarity and q-elementary equivalence for a general notion of trees. In particular, bisimilarity requires the roots of both trees to be in the bisimulation relation.

It should be possible to naturally translate this notion to pointed Kripke structures.