Suzuki commented that Herbrand’s theorem is easily proven using model theory.

Theorem 1 (Herbrand’s Theorem) Let φ(x, y) be a quantifier free L-formula. Let T be a universal theory formulated in L. Suppose that T proves ∀x∃yφ(x, y). Then there are finitely many terms t_{1}(x), ..., t_{n}(x) such that T proves ∀x ⋁_{i≤n} φ(x, t_{i}(x)).

Proof. Suppose otherwise. Then the following set

Σ(x) = {¬φ(x, t(x)) : t(x) a term}

is consistent with T. So there are a model M of T and an element a ∈ M which satisfies Σ(x). Now let N ⊂ M be the substructure generated by a. (i.e. N = {t(a) : t(x) a term}.) Then M ⊧ ¬φ(a, b) for all b ∈ N. Since φ is quantifier free, we have N ⊧ ¬φ(a, b) for all b ∈ N, namely N ⊧ ∀y¬φ(a, y). Since T consists of universal sentences, N is also a model of T, contradicting our assumption that T ⊢ ∀x∃yφ(x, y).

Remark 2 A stronger version of Herbrand’s theorem is also proven by a similar model-theoretic method.