I'm interested in techniques for proving that given properties are not first-order.
I can think of one such technique, proving that, given a first-order theory $T$ with some property, proving that we can produce a fixed first-order theory that's known to be impossible (in this case, the theory of an equivalence relation with finitely many equivalence classes).
I'm wondering whether there's a logic that's more expressive than FOL that nevertheless still can't express the theory of equivalence relations with finitely many equivalence classes.
Basically, I want to know if there are some kinds of properties where this technique definitely won't work.
I'm also curious whether my argument reducing a theory to a known non-firstorder theory works. I could have made a stupid mistake.
This section contains a link to the lecture notes and a summary of the proof.
On page 32 of Alex Kruckman's lecture notes, there's an example of a class of structures that are not first-order definable. Namely, the connected graphs within the class of graphs with the vocabulary $\{ E \}$ where $E$ has arity $2$. I think that in this setting a graph is any structure with the vocabulary $E$, so the graph is directed and self-edges are allowed.
The method of proof works in an extended signature $\{E, c, d\}$ where $c$ and $d$ are fresh constant symbols.
Kruckman then considers the following sequence of formulas $\Phi$ $(c \neq d); (\lnot E(c, d)); \{ \textit{there is no path of length $n$} \;:\;\; $n$ \in \mathbb{N} \}$.
The argument is then that, if there were a first-order theory $T$ of connected graphs, then $T' := T \cup \Phi$ would be consistent as well by compactness.
Since $T'$ is consistent it has a model $G$, $G$ is a model of $T$ and thus connected by hypothesis, but also the path between its two designated points $c$ and $d$ does not have any finite length, which means $G$ is disconnected. This is a contradiction.
This section contains my attempt to prove the lemma using a different technique, constructing a first-order theory that's known to be impossible
If we know in advance that the theory of an equivalence relation with finitely many equivalence classes is not first-order axiomatizable, then we can construct an alternative argument.
Suppose $T$ is a first-order $L$-theory whose models are precisely the structures in which the relation symbol $E$ is a connected graph.
Consider the theory $W$ built in the following way:
- $\forall x \mathop. R(x, x)$
- $\forall x \forall y \mathop. R(x, y) \to R(y, x)$
- $\forall x \forall y \forall z \mathop. R(x, y) \land R(y, z) \to R(x, z)$
- all the sentences in $T$
- If there's only one equivalence class, then $E$ always holds.
- If there's more than one equivalence class, arrange them cyclically $C_1, C_2, \cdots C_n$, and have $E(a, b)$ hold if and only if $a$ is in the class immediately before the class containing $b$ in cyclic order.
$6$ is the sentence:
$$\textit{If}\;\; (\lnot \forall x \forall y \mathop. R(x, y)) \;\; \textit{then}\\
(\forall x \forall y \mathop. R(x, y) \to \lnot E(x, y)) \land \\
(\forall x \forall y \forall z \mathop. E(x, y) \land R(y, z) \to E(x, z)) \land \\
(\forall x \forall y \forall z \mathop. R(z, x) \land E(x, y) \to E(z, y)) \land \\
(\forall x \forall y \forall z \mathop. E(x, y) \land E(x, z) \to R(y, z)) \land \\
(\forall x \forall y \forall z \mathop. E(y, x) \land E(z, x) \to R(y, z)) \land \\
(\forall x \exists y \mathop. E(x, y))
$$
Suppose $M$ is an $L$-structure.
If $M \models W$, then $[\![R]\!]_M$ is an equivalence relation with finitely many equivalence classes.
For any given equivalence relation with finitely many equivalence classes $X$, we can construct a model $M$ where $[\![R]\!]_M$ is isomorphic to $X$.
Therefore $W$ is a first-order theory of equivalence relations with finitely many equivalence classes.
However, the theory of an equivalence relation with finitely many equivalence classes is not first-order definable, this is a contradiction, so we're done.
Best Answer
First, a quick correction: when you write
this isn't what you mean. By definition, the theory of anything is first-order axiomatizable: the theory is the relevant set of first-order sentences (unless another logic is specified)! What you mean is that a particular class of structures is not first-order axiomatizable, namely the class $\mathbb{F}$ of $\{E\}$-structures such that $E$ is an equivalence relation with finitely many classes. In fact, in my opinion it's a good idea to drop the word "axiomatizable" entirely here in favor of "elementary" (or "$\mathcal{L}$-elementary" for a different logic $\mathcal{L}$), which I'll do going forward.
As to your question itself, the answer is yes.
Let $\mathbb{F}$ be the class of $\{E\}$-structures in which $E$ is an equivalence relation with finitely many classes. The non-first-order-elementarity of $\mathbb{F}$ is a direct consequence of the compactness theorem, which means that $\mathbb{F}$ is also non-elementary in any compact logic. And there are indeed compact logics strictly stronger than $\mathsf{FOL}$ - see e.g. Mekler/Shelah in $\mathsf{ZFC}$, or Shelah assuming a weakly compact cardinal - although they are admittedly somewhat rare in practice; unlike say the downward Lowenheim-Skolem property there doesn't seem to be a nice-and-nontrivial way to extract a compact fragment from a given logic.
In fact, all that's really needed is "every finitely satisfiable countable theory is satisfiable;" if memory serves, this is called $(\omega,\omega)$-compactness.