Do the relative consistency results involving the axiom of choice use completeness of FOL? 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?
 A: 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.
A: As a whole forcing has nothing to do with the axiom of choice.
First of all, forcing is usually done internally to the universe. What does it mean? After all, there are no generics in the universe (well, for nontrivial forcings), it means that we can talk about Boolean valued models and those give us the complete picture as far as forcing is concerned.
The entire formalization of forcing can be carried out in Peano arithmetic, so as far as forcing arguments go, the assumption of choice in the meta-theory is entirely irrelevant.
It's not only that, if you do feel that forcing begins with a model of set theory (or enough set theory), then forcing does not use completeness as much as it uses soundness: if $M\models T+\varphi$, then $T\cup\{\varphi\}$ is consistent. You start with a countable model, and you construct a new one. And this construction is entirely "by hand", so the axiom of choice is not involved there at all.
But forcing does depend on the axiom of choice holding internally to the model. Not in the general theorems, those don't use choice at all. The axiom of choice is used in three main points:

*

*The mixing lemma (sometimes known as the maximality principle), which stats that if $p\Vdash\exists x\varphi(x)$, then there is some name $\dot x$ such that $p\Vdash\varphi(\dot x)$. This is in fact equivalent to the axiom of choice.


*Closure implies not adding sets of certain size. For example, you might want to argue that a forcing which is closed under countable sequences will not add a new real number (or any new $\omega$-sequence, for that matter). This turns out to be equivalent to Dependent Choice (and actually the failure of Dependent Choice is equivalent to the existence of a $\sigma$-closed forcing which collapses $\omega_1$).
In general, $\Bbb P$ is $\kappa$-closed $\iff$ no new $\kappa$-sequences are added, is equivalent to $\sf DC_\kappa$.


*Chain conditions are used thoroughly in forcing (as a complement to closure), and without the axiom of choice it is possible that a forcing does not have any maximal antichains to begin with, or that using those maximal antichains requires some form of choice to do anything meaningful.
So for example the fact that a forcing has only countable antichains does not mean that it won't do all sort of weird things to the universe of sets. It just might be that all the antichains are finite, and so the argument is useless.
All in all, forcing has little to do with the axiom of choice, but the way we use forcing depends a lot on the axiom of choice. But internally, not in the meta-theory.
