= 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 \b[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>.
Back to article page
