It is well-known that the compactness theorem for FOL is equivalent to the Boolean Prime Ideal Theorem over ZF, so it is a weak choice principle.
The whole strength of BPIT in the proof of compactness is used in extending a consistent theory to a complete consistent theory. In fact, it is not hard to see that BPIT is equivalent to „every consistent theory can be extended to a complete consistent theory“.
But what if the theory in question is already complete?
Question: does ZF prove that every complete consistent first order theory has a model?
When building a Henkin model, one seemingly has to first Skolemize the theory. In general it is not possible to complete that theory again, even when one has started with a complete theory:
Suppose we live in a model of ZF where there is a collection $\mathcal X$ of nonempty finite sets without a choice function. Consider the language which has a constant $c_x^X$ and unary relation symbol $U_X$ for each $x\in X\in\mathcal X$. Let $T^\prime$ be the theory which says that members of $U_X$ are exactly the $c^X_x$ for $x\in X$. Clearly this has a model so extends to some complete theory $T$. But from any completion of a Skolemization, one can read off a choice function for $\mathcal X$ by asking which one of the $c^X_x$ is the chosen witness of $\exists y U_X(y)$. So such a thing cannot exist.
Note: This is intended to replace my earlier (less complete) answer. But I've left the older answer up since there may be some independent interest in it, and there are also comments there that wouldn't make any sense on this new answer.
The answer below is better in that it fully resolves the status in ZF of the statement "Every complete consistent first-order theory has a model."
Theorem (ZF): The statement "Every complete consistent first-order theory has a model" is equivalent over ZF to the Boolean Prime Ideal Theorem (BPIT).
It's sufficient to show the implication from left to right, since BPIT is known to be equivalent to the statement "Every consistent first-order theory has a model."
So assume that every complete consistent first-order theory has a model. We'll show that BPIT holds by proving the following equivalent statement: Every proper filter over a set $I$ can be extended to an ultrafilter over $I.$ ("Proper" here means that the empty set does not belong to the filter.)
First, however, we'll prove a lemma (in ZF, without using the axiom of choice):
Lemma (ZF): Every proper filter on a countable Boolean algebra can be extended to an ultrafilter.
Proof of Lemma: Let $B$ be a countable Boolean algebra, and let $\scr F$ be a proper filter on $B.$
Let $b_0, b_1, b_2, \dots\;$ be an enumeration of the non-zero members of $B.$
Define $\scr E$ to be $\{x\in B \mid x' \not\in \scr F\}.$ Clearly we have that $\scr F \subseteq \scr E$ and $0 \not\in\scr E.$
Note that the complement of $\scr E$ is closed under join: If $a$ and $b$ are not in $\scr E,$ then $a'$ and $b'$ are in $\scr F,$ so their meet $a'\cdot b'$ is in $\scr F,$ and it follows that $a+b$ is not in $\scr E.$
Define a sequence of members of $B$ by induction, as follows: $$\begin{align} u_0 &= 1; \\ u_{n+1} &= \begin{cases} u_n\cdot b_n, &\text{ if }u_n\cdot b_n \in \scr E,\\ u_n\cdot b_n\hspace{1px}', &\text{ otherwise}. \end{cases} \end{align}$$
You can see by induction that each $u_n$ belongs to $\scr E.$ (Clearly $u_0\in\scr E.$ For the induction step, assume $u_n\in\scr E.$ Then we have $u_n\cdot b_n + u_n\cdot b_n\hspace{1px}' = u_n,$ which is in $\scr E.$ So, by the closure under join of the complement of $\scr E,$ at least one of $u_n\cdot b_n$ and $u_n\cdot b_n\hspace{1px}'$ must be in $\scr E.$ It follows that $u_{n+1}\in\scr E.)$
So $u_0 \geq u_1 \geq u_2 \geq \dots,$ and no $u_n$ is equal to $0.$
You can check that $\{x\in B \mid (\exists n)(x \geq u_n)\}$ is an ultrafilter on the Boolean algebra $B.$ $\tag*{$\blacksquare$}$
Now that the lemma is proven, assume that every complete consistent first-order theory has a model, and let $D$ be a proper filter over a set $I.$ We'll show that $D$ can be extended to an ultrafilter.
For convenience, we'll assume the existence of a transitive set $M$ which contains $2^I$ and $D$ as members and which is a model of ZF. But an examination of the proof will show that $M$ only needs to satisfy finitely much of ZF, so a transitive model $M$ of enough of ZF to make the proof go through provably exists.
Consider the partial ordering $\scr P$ of all finite sequences of pairwise distinct members of $2^I,$ ordered by inclusion. This partial ordering belongs to $M,$ and forcing over it would add a counting of $2^I.$ We'll consider this notion of forcing over $M,$ but we won't actually pass to a generic extension $M[G].$
In V, define the language $\mathscr L$ to consist of:
• a two-place relation symbol $\in;$
and
• a constant symbol $\hat c$ for each $c\in M.$
(Every sentence in $\scr L$ is, of course, a sentence in the language of forcing over $M\text{.}$ $\scr L$ just doesn't include a symbol for the generic filter.)
Let $T$ be the theory of all sentences in the language $\scr L$ that, according to $M,$ are forced to be true by the empty condition in $\scr P$ (or, equivalently, by all conditions in $\scr P).$
Clearly $T$ is consistent.
We claim that $T$ is complete. If not, there is some sentence $\varphi$ in $\scr L$ and there are conditions $p, q\in\scr P$ such that, in $M,$ $p\Vdash\varphi$ and $q\Vdash\neg\varphi.$ (Recall that $\varphi$ is a sentence about a hypothetical generic extension $M[G],$ but $\varphi$ doesn't reference $G$ at all, just members of $M.)$ Without loss of generality we can assume that $p$ and $q$ are of the same length (if not, simply extend the shorter one). We can find an automorphism in $M$ of $\scr P$ mapping $p$ to $q$ (the axiom of choice isn't needed for this because it only involves rearranging finitely many members of $2^I).$ Since $\varphi$ doesn't mention the generic filter, it follows that $p\Vdash\varphi$ iff $q\Vdash\varphi,$ contradicting our assumption.
So $T$ is complete and consistent. It follows from our assumption that $T$ has a model $\langle M'; E\rangle$ (possibly not well-founded).
Let $S$ be $2^I;$ $\hat S$ is the constant symbol in the language of forcing for the power set of $I$ in the ground model. The sentence "There exists a one-to-one function mapping $\omega$ onto $\hat S\,$" is forced by the empty condition. It follows that the empty condition forces the sentence "$\hat S$ is a countable subset of the power set of $I,$ and $\hat S$ is a Boolean algebra under the operations of union, intersection, and complementation."
The empty condition also forces that $\hat D$ is a filter on the Boolean algebra $\hat S.$ It follows that the empty condition forces the sentence "There exists an ultrafilter on the Boolean algebra $\hat S$ that extends $\hat D."$
All these sentences that are forced by the empty condition are satisfied by the model $M'.$ So there is some $U\in M'$ such that $M'\models\;"U$ is an ultrafilter on the Boolean algebra $\hat S$ that extends $\hat D."$
Finally, we can see that, in V, the set $\{X\subseteq I \mid M'\;\models\hat X\in U\}$ is an ultrafilter on $I$ extending $D.$