Modal vs First-Order Logic on finite models

Question

It is known that Modal Logic can be interpreted in First-Order logic via Standard translation. However, this translation needs a unary predicate for every propositional variable. It is also known that without these propositional variables certain formulas in ML can't be expressed in FOL. For example:

1. Löb's formula: $\Box (\Box p \to p) \to \Box p$
2. McKinsey's formula: $\Box\Diamond p \to \Diamond \Box p$
3. Grzegorczyk's formula: $\Box((p\to \Box p) \to p) \to p$

In the proofs of this, one usually constructs an infinite counterexample to some property of FOL (for example to Löwenheim-Skolem property in case of McKinsey's formula) [ML book].

My question: Is there a formula $\varphi$ in ML which is not expressible in FOL and we can prove this by tools available in finite model theory only?

Further question: Could $\varphi$ have some kind of graph theoretic meaning?

[ML book] Blackburn, de Rijke, and Venema: Modal logic

Answer 1

On p. 30–31 of Van Benthem’s Notes on modal definability (Notre Dame Journal of Formal Logic 30 (1988), #1, pp. 20–35), you can find a (brief!) sketch of a proof that the modal formula $$(\Diamond\Diamond\top\land\Box(\Diamond\top\to\Diamond p))\to\Diamond(\Diamond\top\land\Box p)$$ is not FO-definable on finite frames. The reason is, essentially, that it defines parity on a certain family of frames, which is impossible in FO by an Ehrenfeucht–Fraïssé argument. I would consider this to use only tools of finite model theory.

In fact, the same argument applies to the McKinsey formula $\Box\Diamond p\to\Diamond\Box p$ itself, if we take the frames in the proof as non-transitive, and make the leaf nodes reflexive. That is, for any $n\in\mathbb N$, let $F_n$ be the Kripke frame with nodes $\{r,u_0,\dots,u_{n-1},v_0,\dots,v_{n-1}\}$ where $r$ sees each $u_i$; $u_i$ sees $v_i$ and $v_{(i+1)\bmod n}$; and $v_i$ sees itself. Then $F_n$ validates the McKinsey formula iff $n$ is odd, but for any given FO sentence $\phi$, all $F_n$ with sufficiently large $n$ agree on the truth of $\phi$ by an Ehrenfeucht–Fraïssé argument (or, using the fact that $F_n$ is interpretable in the undirected $n$-cycle).

---

Finite model theory is closely connected to complexity theory, and one can give an alternative argument that the McKinsey formula is not FO on finite frames by noting that the set of frames it defines is coNP-complete under $\mathrm{AC}^0$ reductions (or even DLOGTIME reductions), whereas all FO properties are decidable in $\mathrm{AC}^0$. (Further assuming $\mathrm{P\ne NP}$, this implies that the McKinsey formula is not expressible even in stronger logics such as IFP.)

This can be conveniently shown by reduction from the NP-complete problem Mon-NAE-SAT (monotone not-all-equal SAT). In a combinatorial formulation, this problem is the following.

Input: A set $S=\{C_1,\dots,C_m\}$ of subsets $C_i\subseteq V=\{1,\dots,n\}$.

Output: Does there exist a set $P\subseteq V$ that splits all sets in $S$, i.e., $C_i\cap P\ne\varnothing$ and $C_i\smallsetminus P\ne\varnothing$ for each $i=1,\dots,m$?

We may assume all $C_i$ to be nonempty.

Now, the reduction goes as follows. We construct a frame $F_S=(W_S,R_S)$, where $W_S=\{r,u_1,\dots,u_m,v_1,\dots,v_n\}$, with the accessibility relation $R_S$ defined so that $r$ is related to each $u_i$; $u_i$ is related to those $v_j$ such that $j\in C_i$; and each $v_j$ is related to itself.

The McKinsey frame condition is: for all $w\in W$ and all $P\subseteq W$, there is a successor $u$ of $w$ such that the successors of $u$ are either all in $P$, or all in $W\smallsetminus P$. It is easy to see that this condition holds in all nodes of $F_S$ except possibly in $r$, and it fails in $r$ iff the original NAE-SAT problem is solvable.

Notice also that if $S=\{\{1,2\},\{2,3\},\dots,\{n-1,n\},\{n,1\}\}$, then $F_S$ is exactly the frame $F_n$ we defined earlier.