Modal vs First-Order Logic on finite models

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

• I don’t understand the second question: the standard translation tells you that every modal property is expressible by a monadic second-order ($\Pi^1_1$) sentence, or am I missing something? – Emil Jeřábek Dec 15 '16 at 13:20
• Yes, you're right. By the "further question" I was hoping to get a formula that has some kind of graph theoretic meaning. For example, it could be saying something about colourability of the graph. (I'll update the question) – Tomáš Jakl Dec 15 '16 at 16:21

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.

• I don't know if complexity theory counts as finite model theory, but here is a funny alternative argument: the frame condition for the McKinsey formula is easily seen to be coNP-complete (under, say, FO reductions) by a reduction from MON-NAE-SAT, hence it is not in AC^0, hence it is not FO definable. (This was unconditional, but further assuming $\mathrm{P\ne NP}$, this implies it is also not definable in stronger logics such as IFP.) – Emil Jeřábek Dec 17 '16 at 9:55
• Wow, that's really interesting. But I don't get the "easily seen" part. Do you have a reference that shows that McKinsey formula is coNP-complete? – Tomáš Jakl Dec 19 '16 at 17:32
• I don’t have a reference, I just noticed it myself. I added an explanation to the answer. Ok, so maybe it is not that easy to see :) – Emil Jeřábek Dec 20 '16 at 13:18