Does there exist a universal formula of first-order logic that is satisfiable only by structures with infinite domains?

Question

Following up this question - Here:

Does there exist a universal sentence $A:=\forall x_1 \dots \forall x_n \varphi(x_1 ,\dots ,x_n )$ (where $\varphi$ does not contain quantifiers) that is satisfiable but not in finite models (i.e. only in infinite models)?

Answer 1

Yes. For example, let $\varphi$ be the sentence $$\forall x\forall y \forall z\, ((f(x) = f(y)\rightarrow x = y)\land \lnot (f(z) = c))$$ where $f$ is a unary function symbol and $c$ is a constant symbol. Any model of $\varphi$ is a set $X$ equipped with a function $f\colon X\to X$ which is injective but not surjective. Thus $X$ is infinite.

A set $\mathcal{S}$ of sentences has the finite model property if every satisfiable sentence $\varphi\in \mathcal{S}$ has a finite model. The above example shows that the set of universal $L$-sentences in an arbitrary language $L$ does not have the finite model property. However, it is clear that in a relational language, the set of universal sentences does have the finite model property: If a universal sentence $\varphi$ has a model $M\models \varphi$, any finite subset $A\subseteq M$ is the domain of a substructure of $M$ (since we are in a relational language), and hence $A\models \varphi$.

A classic paper by C. J. Ash classifies all first-order languages $L$ with the property that the set of universal $L$-sentences has the finite model property. In first-order logic with equality, these are exactly the languages which fall into the following cases:

1. No function symbols (only relation symbols and constant symbols).
2. No function or relation symbols of arity $\geq 2$, no constant symbols, and at most one unary function symbol.

In first-order logic without equality, the classification is a bit simpler:

1. No function symbols (only relation symbols and constant symbols).
2. No function or relation symbols of arity $\geq 2$.

Ash also gives many explicit examples of satisfiable universal sentences with only infinite models to show that the results are the best possible (e.g., in a language with a binary function symbol, a language with two unary function symbols, etc.).