We saw: if formula has a model of some size, it has many models of same size, from Isomorphism of Interpretations.

Are there first-order formulas that have only finite models?

Are there first-order formulas that have only infinite models?

What is the cardinality of the models we need to consider? There are many useful models whose domain is not a countable set.

Difficulty in checking : there are infinitely many models, of arbitrarily large cardinalities.

Goal: show that if a set of formulas has a model, then it has a particular kind, and this model is countable.