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.