The proof of the Completeness Theorem for first order logic uses the axiom choice and is a central result in model theory.
Chang and Keisler claim that model theory has important applications to set theory and these notes (1), for example, explore model theory and set theory, including forcing .
I am just concerned about the circularity of this. For example, is completeness used to deduce relative consistency results involving ZF and AC? Does forcing use any theorems that depend on the AC?
The completeness theorem only depends on the axiom of choice if the vocabulary of the theory is "wild".
For theories with an at most countable (or just well-orderable) vocabulary, no additional choice is necessary for proving the completeness theorem.
This is quite sufficient to prove the instances of completeness that are used when speaking of set theory, where the non-logical vocabulary is not only countable but finite (namely the single binary relation $\in$).
Quite apart from this, use of the axiom of choice is generally harmless when proving relative consistency results. If you don't believe in AC in the actual universe, you can just carry out your argument within $L$ (where AC always holds), and since $L$ has the same ordinals as the ambient universe -- and so in particular the same integers -- what $L$ believes about the consistency of theories agrees with what the ambient universe believes.