Solution (source code)

= Solution

The downward <Löwenheim-Skolem theorem> says that a structure in a <countable> language has a <countable> <elementary substructure> containing any specified finite or <countable> set of its elements. More generally the size bound is $\max(|\mathcal L|,|C|,\aleph_0)$ for a required parameter set $C$. In particular any satisfiable theory in a <countable> language has a model of size at most <countable>.

To see the last assertion directly from the completeness construction, add only countably many witness constants in the <Henkin construction>. There are then countably many finite <closed terms>, and taking their quotient cannot increase <cardinality>. The resulting term model is therefore <countable>. For the elementary-substructure version, perform the witness construction inside the given structure, choosing actual witnesses and closing under the <function symbols>. The induced substructure is elementary by the <Tarski-Vaught test>. This is the same witness mechanism as the completeness construction, with the ambient structure supplying the chosen witnesses.

The upward companion states that a theory with an infinite model has models in every sufficiently large infinite cardinal, at least $|\mathcal L|+\aleph_0$. Add that many pairwise unequal constants, apply compactness, and then the size-bounded construction. The <countable> consequence is the part needed below.