Let be a Theory in a countable language (i.e. is countable)
If has a Model, then has a countable model.
Proof
By the Soundness Theorem, is consistent.
Then the model constructed in the proof of Model Existence Lemma is countable.
Refinement
Let be a Model, and any set of formulas.
Then there is a countable
such that is a Substructure of
and all formulas in are Absolute between and .
Proof
WLOG is closed under subformulas.
Suppose
Define, using Axiom of Choice:
Then define and
and set
We can show that all formulas are Absolute between and
using Tarski-Vaught Test.
By induction, all are countable:
Then is countable.