Question regarding inexpressibility results over finite models using compactness and the Löwenheim–Skolem theorem

Question

In the book Elements of finite model theory by Leonid Libkin, they show that the parity query for structures over an empty vocabulary is not first order definable.

They do this by constructing two countable infinite models $\mathcal{A}$ and $\mathcal{B}$ using the compactness theorem and the Löwenheim–Skolem theorem. Since both models are countable infinite they are isomorphic and hence all first order sentences agree on both models. The compactness theorem however implies that the parity query disagrees on those two structures. Hence the parity query is not first order definable.

Now my question: they say that this also implies that the parity query is not first order definable over finite models. I think this is because the parity query only makes sense over finite models. Is this correct?

Then they prove the following lemma: For every finite structure $\mathcal{A}$, there is a sentence $\psi_\mathcal{A}$ such that $\mathcal{B} \models \psi_\mathcal{A}$ if and only if $\mathcal{B} \cong \mathcal{A}$.

And claim that this implies that the technique used to show that the parity query is not first order definable cannot be extended to prove more inexpressibility results over finite models.

I know why it does not always suffice to only consider two structures, since some non first order definable queries are expressible for every finite set structures, e.g., graph connectivity. I however do not see that that lemma implies what they claim.

P.S. If needed I can include both proofs.

Answer 1

Note that Libkin says the following (pp.25-26):

As an introduction to these tools, let us revisit the proof of Proposition 3.3 [$\mathsf{even}$ is not FO-definable over an empty signature]. In the proof, we constructed two models, $\mathfrak{A}_1$ and $\mathfrak{A}_2$, that agree on all FO sentences (since they are isomorphic), and yet compactness tells us that they disagree on $\Phi$, which we assumed to define $\mathsf{even}$ — hence $\mathsf{even}$ is not first-order.

Can we extend this technique to prove inexpressibility results over finite models? The most straightforward attempt to do so fails due to the following.

Lemma 3.4. For every finite structure $\mathfrak{A}$, there is a sentence $\Phi_\mathfrak{A}$ such that $\mathfrak{B} \models \Phi_\mathfrak{A}$ iff $\mathfrak{B} \cong \mathfrak{A}$.

...

In particular, every two finite structures that agree on all FO sentences are isomorphic, and hence agree on any Boolean query (as Boolean queries are closed under isomorphism).

Since the technique he wants to extend appears to be that of constructing elementary equivalent models which give different answers to the given query, Lemma 3.4 does say that a straightforward extension of this technique cannot work in the domain of finite models, since any two elementary equivalent finite models are isomorphic (and will thus give the same answer to any Boolean query).

In the case of a Boolean query like $\mathsf{even}$ this becomes clear: if $\mathfrak{A}, \mathfrak{B}$ were finite models such that $\mathfrak{A} \models \mathsf{even}$ and $\mathfrak{B} \models \neg \mathsf{even}$, then $\mathfrak{A} \not\cong \mathfrak{B}$, and so by Lemma 3.4 $\mathfrak{A} \not\equiv \mathfrak{B}$, and a priori there is no reason why a sentence $\Phi$ such that $\mathfrak{A} \models \Phi$ and $\mathfrak{B} \models \neg \Phi$ cannot be a defining formula for $\mathsf{even}$ over finite models.

Note that this is similar to the failed attempt at proving that $\mathsf{even}$ is not FO-definable over ordered structures. Even though compactness of Löwenheim–Skolem resulted in two countably infinite (ordered) models $\mathfrak{A}_1, \mathfrak{A}_2$ satisfying $\mathsf{even}$ and $\neg \mathsf{even}$, respectively, since there was no way to guarantee that $\mathfrak{A}_1$ and $\mathfrak{A}_2$ are elementarily equivalent we couldn't achieve the much desired contradiction.