 Solution

For a countable first-order language, the Henkin construction introduces only countably many constant symbols: each round needs at most one for each logical formula, there are countably many finite strings in a countable alphabet, and countably many rounds suffice. There are therefore at most countably many closed terms. The term model, and also its quotient set by equality, has at most countably many elements.

It follows that every satisfiable theory in a countable first-order language has an at most countable first-order model. If the theory has no finite first-order model, the constructed first-order model is countably infinite. More generally the same counting argument gives a first-order model of cardinality at most $\max (|L|,{\aleph }_0)$ for any satisfiable theory in language $L$.

For the elementary-substructure version of the downward Löwenheim-Skolem theorem, begin with a first-order structure $M$ and a set $S$ of designated elements. Close $S$, the named constant symbols and one initial element under the language's functions and under chosen witnesses in $M$ for existential formulas with parameters already chosen. Iterate countably often. The resulting set has cardinality at most $\max (|L|,|S|,{\aleph }_0)$, and its induced substructure $N$ is elementary: induction on logical formulas proves the truth equivalence, with the existential case supplied by the chosen witnesses. This is the same witness mechanism as the Henkin formal proof, now keeping witnesses inside a given first-order model.