Logic more expressive than FOL that can't express the theory of equivalence relations with finitely many equivalence classes.

Question

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:

1. $\forall x \mathop. R(x, x)$
2. $\forall x \forall y \mathop. R(x, y) \to R(y, x)$
3. $\forall x \forall y \forall z \mathop. R(x, y) \land R(y, z) \to R(x, z)$
4. all the sentences in $T$
5. If there's only one equivalence class, then $E$ always holds.
6. 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.

Answer 1

First, a quick correction: when you write

"the theory of an equivalence relation with finitely many equivalence classes is not first-order axiomatizable,"

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.

Answer 2

You've really asked two quite distinct questions here. Noah has answered your first question, I'll address your second. In the future, it's really better to keep it to one question per post.

Your argument that the class of connected (directed) graphs is not axiomatizable works, modulo a subtlety.

Your general strategy is this: Suppose we have some class $C$ of $L$-structures that we know is not elementary ($=$ axiomatizable by a first-order $L$-theory). Now we have another class $C'$ of $L'$-structures, and we want to show that $C'$ is not elementary. Assume for contradiction that $C'$ is elementary, say axiomatized by and $L'$-theory $T'$. Using $T'$, produce an $(L\cup L')$-theory $T^*$ such that the class of $L$-reducts of models of $T^*$ is exactly $C$.

At this point, we have not shown that $C$ is elementary, for a contradiction. What we've shown is that $C$ is pseudo-elementary: it is the class of $L$-reducts of models of some theory in a larger language.

Fortunately, the class $C$ you're interested in, namely the class of equivalence relations with finitely many classes, is not even pseudo-elementary. The standard compactness argument goes through to prove this stronger result. And this suffices to make your strategy work.

Incidentally, I think working with equivalence relations makes things more complicated than they need to be. Consider instead the class $C$ of finite sets (in the empty language). $C$ is not pseudo-elementary: by compactness no first-order theory $T^*$ has models of arbitrary finite size but no infinite models.

Now let's use your strategy to prove that the class $C'$ of connected (directed) graphs is not elementary. Suppose for contradiction that $T'$ axiomatizes $C'$. Consider the following theory $T^*$:

1. $T'$
2. $\forall x\, \exists! y\, xEy$ (where $\exists! y$ means "there exists a unique $y$)

Now a model $M$ of $T^*$ is a connected directed graph in which every vertex has out-degree $1$. If $M$ is non-empty, pick some $v\in M$. Then $vEw$ for a unique $w$. Now since $M$ is connected, there is some path from $w$ to $v$, say of length $n$. Then it's easy to see that $M$ is just a cycle of length $n+1$ (I'm including the cases of cycles of length $1$ - a vertex with a self-loop - and $2$ - a pair of vertices with edges to each other). The reducts of $T^*$ to the empty language (i.e. the underlying sets of models of $T^*$) are exactly the finite sets, contradiction.

Incidentally, the same proof shows that the class of connected directed graphs is not even pseudo-elementary.