Or more importantly, is it independent of the axiom of choice. The compactness theorem states the given a set of sentences $T$ in a first order Language $L, T$ has a model iff every finite subset of $T$ has a model. So for any natural number $n, T(n)$ is a finite subset of $n$ sentences. Now if every finite subset has a model than adding a sentence $r$ to $T(n)$ gives us $T(n+1)$ which also has a model so there is some transfinite induction going on here when $T$ is countable. This seems to cry out for the application of Zorn's Lemma which is equivalent to the axiom of choice. So to summarize, is the compactness theorem consistent with ~AC (the negation of the axiom of choice which is independent of ZF set theory)?
What Qiaochu writes is true.
The compactness theorem for first-order logic is equivalent (in $\sf ZF$) to the completeness theorem, as well to the ultrafilter lemma, and several other interesting principles. The proof is due to Henkin , but I could not find the paper online, the proof appears in [2, Theorem 2.2].
It should be remarked that if we assume that both the compactness theorem holds, and Los theorem's hold, then we can prove the axiom of choice holds . Therefore we have to be extra careful when we prove the compactness theorems using ultrafilters.
The ultrafilter lemma was proved to be independent from the axiom of choice (i.e. it cannot prove full choice) in 1965. In fact it is consistent that the axiom of countable choice fails, but the ultrafilter lemma holds (see , [2, Theorem 5.21]. Interestingly, this was about a decade after it was known that the ultrafilter lemma and the compactness theorem are equivalent.
To slightly generalize on Qiaochu's last point, if $\cal L$ is a well-orderable language (i.e. the cardinality of the language is an ordinal) then we can prove the compactness theorem for $\cal L$ without using the axiom of choice at all. The problem begins when the languages are not well-ordered. While it may seem strange, remember that if you use a language which includes a constant for every real number, then you can no longer prove that the language is well-orderabe.
In general, the compactness theorem is equivalent to the ultrafilter lemma, which is known to be strictly weaker than the axiom of choice (so is consistent with its negation) but independent of ZF. The models the compactness theorem asserts exist can be constructed using ultraproducts.
Over a countable alphabet, the compactness theorem is provable in ZF. This is because it can be proven from the completeness theorem, which over a countable alphabet is also provable in ZF.