First-order logic - Does there exist a sentence that is satisfiable by all infinite models and only by them?

Prove or Disprove:
There is $$\boldsymbol{no}$$ alphabet $$\Sigma$$ and closed formula (no free variables) $$\varphi$$ above $$\Sigma$$, such that for any Model $$M$$ it holds that $$M\models\varphi\iff\,|D^M|=\infty$$.

I'm not sure what is the classic way to approach this. I do think that the statement is correct. I tried the next proof:
Assume by contradiction that there exist $$\Sigma,\,\varphi$$ as mention above. So it also holds that for any model $$M$$:
$$M\models\neg\varphi\iff\,|D^M|<\infty$$
Let $$M$$ be a model for $$\Sigma$$ such that $$D^M=\{1,...,n\}$$ and $$M$$ defines functions and relations in $$\Sigma$$ arbitrary.
$$M$$ domain is of finite size so we have $$M\models \neg\varphi$$
Define $$M'$$ to be an expansion of $$M$$:$$\,\,$$ $$D^{M'}=\mathbb{N}$$, and for every $$k\in\mathbb{N}$$,$$\,\,\,M'$$ treats $$k$$ the same way $$M$$ treats $$k\,\,mod\,\,n$$.
Then I proved by induction on $$\varphi$$'s structure that:
$$M\models\neg\varphi$$ $$\iff$$ $$M'\models\neg\varphi$$
and becuase we know that $$M\models\neg\varphi$$ we have $$M'\models\neg\varphi$$ which is contradiction, becuase $$M'$$ domain is of infinite size.

Is my proof correct? Or should I build additional model $$N$$, of finite domain, isomorphic to $$M'$$, and show with $$N$$ the contradiction?
Is there a better known way to prove this? Sometimes there are claims that there is a classic way to prove / disprove, I wonder if in this case as well.

Would appreciate help! :-)

Probably the easiest way to prove this is using the compactness theorem: assume for contradiction that $$\varphi$$ is such a sentence. For every $$n\in\mathbb N$$, let $$E_n$$ denote the sentence $$\exists x_1,\dots,x_n\bigwedge_{i, which asserts that there are at least $$n$$ elements. Since every finite subset of $$S=\{\neg \varphi\}\cup\{E_n:n \in \mathbb N\}$$ is true in a sufficiently large finite structure, $$S$$ is consistent by the compactness theorem. But a model $$M\models S$$ is an infinite structure that does not satisfy $$\varphi$$, a contradiction.

• Got it. Thanks! :-)
– Ella
Jun 15, 2021 at 16:51
• Assume I want to prove this with first-order logic without "=" sign. And I can't add the "=" relation because I want to stay above the exact $\Sigma$- the one promised by the contradiction assumption, which might not consist of "=". How would you prove in such a case?
– Ella
Jun 15, 2021 at 16:57
• For logic without equality, the proof you outlined in the question actually works. Though I wouldn’t bother with modular arithmetic: simply take a finite (even just $1$-element) $\Sigma$-structure $M$ and an infinite $\Sigma$-structure $M'$, where in both you make all predicates $P\in\Sigma$ satisfied by all elements, so that in either model, all atomic formulas are true under arbitrary assignments. Then prove by induction on complexity that the models agree on the truth of all formulas (and, again, that it does not depend on the variable assignment). Jun 15, 2021 at 17:10
• Shouldn't I make $P\in\Sigma$ predicate satisfied by all additional elements $\iff$ the 1-element satisfied by $P$? There is no situation in which adding elements that satisfied by all $P\in\Sigma$ will make $M'$ not satisfy $\varphi$?
– Ella
Jun 15, 2021 at 17:17
• I don’t quite understand the question. You are free to choose the satisfaction of predicates in both models, hence there is no reason not to make it as simple as possible, and making all atomic formulas true is the simplest choice. Jun 15, 2021 at 17:43