Consider the language $L$ with one unary function symbol $f$. I'm interested in the case where the domain of discourse is permitted to be empty as well as the case where it isn't.
My proof below assumes that the domain of discourse is allowed to be empty (and contains a big mistake. If empty domains are allowed we can't just move all the quantifiers to the left)
I'm interested in satisfiable sentences where all models are infinite.
We have a straightforward sentence $\psi$ that insists that $f$ is injective but not a permutation of the domain:
$$ \psi \;\;\text{is the sentence}\;\; (\forall x \forall y \mathop. f(x) = f(y) \to x = y) \land (\exists x \mathop. \forall y \mathop. f(y) \neq x) $$
This sentence correctly rejects the sole $L$-structure on the empty set and the sole $L$-structure on the singleton set.
However, $\psi$ costs three equals signs to express. I'm wondering if this is the minimum.
For concreteness, I allow the connectives $\land, \lor, \lnot, \to, \leftrightarrow$ . Well-formed formulas of the form $a \leftrightarrow b$ are not abbreviations for $(a \to b) \land (b \to a)$ because that would increase the number of $=$ signs. This is an arbitrary choice, but I think it's a defensible one.
What follows is the work I've done already: a proof that solves part of the problem (I think).
I can prove that we need at least two equals signs to get such a satisfiable sentence with only infinite models, but my method of proof is very ad hoc. I'm curious if there's a slick way to show that there aren't any sentences with two equals signs that accomplish the task.
Lemma 101: Every sentence $\varphi$ with one equals sign and no finite models is unsatisfiable.
Intuitively, we win the lemma 101 game if we get a sentence with one equals sign, no finite models and at least one infinite model. I will show that we can't win.
Since $L$ contains no relation symbols, the fact that $\varphi$ contains only one equals sign means that it contains no propositional connectives besides $\lnot$.
Let us suppose, without loss of generality, that every bound variable introduced by a quantifier inside $\varphi$ is used at least once and that all bound variables are distinct.
Thus $\varphi$ is equivalent to a formula of the form $Q_1 x \mathop. t_1(x) = t_2(x)$ or $Q_1 x \mathop. t_1(x) \neq t_2(x)$ or $Q_1 x Q_2 y \mathop. t_1(x, y) = t_2(x, y)$ or $Q_1 x Q_2 y \mathop. t_1(x, y) \neq t_2(x, y)$ . In order to get $\varphi$ into this form, we may need to eliminate double negations or move them inwards and flip quantifiers.
Suppose $\varphi$ is headed by $\forall$, then it holds in the model over the empty set and thus has a finite model.
Suppose $\varphi$ is headed by $\exists$.
If $\varphi$ has the form $\exists x \mathop. f^k(x) = f^j(x)$, then $\varphi$ holds on the structure with one element.
Suppose $\varphi$ has the form $\exists x \mathop. f^k(x) \neq f^j(x)$. If $j = k$, then the sentence is unsatisfiable and we're done.
Suppose without loss of generality that $k \lt j$, then construct a circle of length $j$, i.e. $f(x) = (x + 1) \% j$ with $\%$ being mod like in C or Python. If you start at $0$, applying $f$ $j$ times will take you back to $0$ and applying $f$ $k$ times will not.
If $\varphi$ has the form $\exists x \mathop. \exists y \mathop. f^k(x) = f^j(y)$, then the sole structure on one element works as a model.
If $\varphi$ has the form $\exists x \mathop. \exists y \mathop. f^j(x) \neq f^k(y)$, then the structure considering of two fixed points side by side $f(1) = 1$ and $f(2) = 2$ works as a model.
If $\varphi$ has the form $\exists x \mathop. \forall y \mathop. f^k(x) = f^j(y)$, then the sole structure on one element works as a model.
Suppose $\varphi$ has the form $\exists x \mathop. \forall y \mathop. f^k(x) \neq f^j(y)$.
Let's consider the Skolemized sentence $\forall y \mathop. f^k(c) = f^j(y)$ .
If $k \ge j$, pick $y = f^{(k-j)}(c)$ as our falsifying assignment. This falsifying assignment witnesses that $\varphi$ is unsatisfiable.
Consider the sentence $\forall y \mathop. c \neq f(y)$. Here the finite model on two elements $f(1) = f(2) = 2$, where $c$ = 1, works.
Consider the sentence $\forall y \mathop. c \neq f(f(y))$. Here the finite model on $\{1, 2, 3\}$ where $f(x) = \min \{3, x+1\}$ and $c=1$ works.
Consider the sentence $\forall y \mathop. f(c) \neq f(f(y))$. Here the finite model $\{1, 2, 3, 4\}$ where $c = 1$ and $f(x) = \min \{ 4, x+1\}$ works because $2 \not\in \{3, 4\}$.
More generally, in cases where $k < j$, the finite model on $\{1, \cdots, j+k+1\}$ where $c=1$ and $f(x) = \min \{ j+k+1, x + 1\}$ works as a finite model witnessing the satisfiability of $\forall y \mathop. f^k(c) = f^j(y)$. Visually, it only costs us a finite number of things in our domain to keep $1$ far enough away that $1+k$ falls outside the image of the $j$-th iterate of $f$.
This concludes the proof of Lemma 101.
This argument was so ad hoc though I'm not sure what to do for the two equals sign case.
Best Answer
This sentence says that there is a surjection from a proper subset of the universe to the whole universe, which is possible only if the universe is infinite: $$\exists x\forall y\exists z[z\ne x\land f(z)=y]$$ If empty universes are disallowed, here is an $\forall\exists$ sentence saying that there is an (at least) two-to-one mapping of the universe onto itself, which is possible only if the universe is infinite (or empty).: $$\forall x\forall y\exists z[z\ne x\land f(z)=y]$$