Is the compactness theorem (from mathematical logic) equivalent to the Axiom of Choice?
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 [1], 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 Łoś theorem's hold, then we can prove the axiom of choice holds [4]. 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 [3], [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.
Bibliography.
- Henkin, Leon. "Metamathematical theorems equivalent to the prime ideal theorems for Boolean algebras." Bull. Amer. Math. Soc 60 (1954): 387-388.
- Jech, Thomas J. The Axiom of Choice. Courier Dover Publications, 2008.
- Halpern, James D., and Azriel Lévy. "The Boolean prime ideal theorem does not imply the axiom of choice." Proc. of Symposium Pure Math. of the AMS. Vol. 13. (1971): 83-134.
- Howard, Paul E. "Łoś’ theorem and the Boolean prime ideal theorem imply the axiom of choice." Proceedings of American Math. Society 49 (1975): 426-428.
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.
To supplement the other answers with some references at a more introductory level:
[1, p.109]: “In ZF, the Compactness Theorem (CTh) is a weakening of AC. ZF does not prove CTh, since there are models of ZF in which $\mathcal{P}(\mathbb{R})$ cannot be totally ordered. Also, ZF+CTh does not prove AC, or even that $\mathbb{R}$ can be well-ordered. Working in ZF, one can prove that CTh is equivalent to the Propositional Compactness Theorem, and to the Completeness Theorem. Also, in ZF, one can prove the Compactness and Completeness Theorems in the case that $\mathcal{L}$ is well-ordered;”
[2, Thm. I.15.13 on p.90] is the completeness theorem proved from AC+ (Def. I.3.3, p.19: “every set can be well-ordered”). Below Thm, I.15.13, a comment reads “It is known that the Completeness Theorem is not provable in ZF [...]. However, the Completeness Theorem is provable in ZF$^-$-P in the case that $\mathcal{L}$ can be well-ordered (in particular, when $\mathcal{L}$ is countable).”
Note that, in ZF, AC+ is equivalent to the axiom of choice [2, Thm. I.12.1 on p.68].
[3, p.144]: “We may then state the Gödel Completeness Theorem as $$ \forall\, X\; (CON(X) \leftrightarrow \exists\, \mathfrak{M}\; (\mathfrak{M} \models X)) $$ and prove it within ZF (AC can be avoided here since the language is countable).”
[4, p.24]: In the course of proving results leading to the compactness theorem: “Note: If the vocabulary of $\mathcal{L}$ is finite or denumerable, then Zorn's lemma (and the axiom of choice) can be avoided in the usual way by enumerating the formulae in $F_{\mathcal{L} }$.”
[1] Kenneth Kunen, The foundations of mathematics, College Publications, 2009 (revised ed. 2012)
[2] Kenneth Kunen, Set theory, College Publications, 2011 (revised ed.2013)
[3] Kenneth Kunen, Set theory: An introduction to independence proofs, North Holland, 1980
[4] Albert C. Leisenring, Mathematical logic and Hilbert's $\varepsilon$-symbol, MacDonald Technical & Scientific, 1969