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.

monadicsecond-order ($\Pi^1_1$) sentence, or am I missing something? $\endgroup$ – Emil Jeřábek Dec 15 '16 at 13:20