Is there a formula in FOL that is only satisfiable in an infinite domain Is it possible to construct a formula or set of formulas using only equality that are satisfiable only in an infinite domain? I have seen such formulas but they all use a relation like greater than or less than instead of equality.
 A: The answers are already in the comments of bof, but let me make them precise (in particular the negative answer). To summarise, in just the language of equality we have the following:

*

*there is a set $\Sigma$ of formulas such that $M \models \Sigma$ if and only if $M$ is infinite,

*there is no formula $\phi$ such that $M \models \phi$ if and only if $M$ is infinite.

Note that the second point is equivalent to "there is no finite set of formulas $\Phi = \{ \phi_1, \ldots, \phi_n \}$ such that $M \models \Phi$ if and only if $M$ is infinite", just take $\phi$ to be the conjunction $\phi_1 \wedge \ldots \wedge \phi_n$.
Proof of claim 1. For $n \in \mathbb{N}$, let $\sigma_n$ express "there are at least $n$ elements". So for example, we could take $\sigma_n$ to be
$$
\exists x_1 \ldots x_n (\bigwedge_{i \neq j} x_i \neq x_j).
$$
Then $\Sigma = \{ \sigma_n : n \in \mathbb{N} \}$ is easily seen to have the property described in claim 1.
Proof of claim 2. Suppose, for a contradiction, that there is such a $\phi$. Note that we are working in just the language with equality, so the structures we consider are pure sets. By assumption we have that $M \models \neg \phi$ if and only if $M$ is finite. Now consider $T = \{\phi\} \cup \Sigma$, where $\Sigma$ is as in the previous proof. Every finite subset $T_0 \subseteq T$ has a model. This is because it only contains a finite part of $\Sigma$ and so there is a maximal $n$ such that $\sigma_n \in T_0$. Then the set with $n+1$ elements is a model of $T_0$. By compactness there is then a model $M \models T$. So $M \models \phi$, thus $M$ must be finite, but at the same time $M \models \Sigma$, so $M$ must be infinite. A contradiction, so we conclude that no such $\phi$ can exist.
