The Downward Löwenheim-Skolem Theorem

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.