# 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