A devilish remark in „Aluffi: Algebra Chapter 0“[1, Remark VII.2.7] claims that
$^7$ Allegedly, the existence of algebraic closures is a consequence of the compactness theorem for first-odrer logic, which is known to be weaker than the axiom of choice.
I then found out the following things:
- The Compactness theorem is equivalent to the Ultrafilter lemma (equivalently, the boolean prime ideal theorem)
- We can modify Artins iterative approach by extending a certain ideal to a prime ideal (see ) and taking the fraction field, which thus constructs an algebraic closure only using the boolean prime ideal theorem.
However, I have not seen a model-theoretic proof, i.e., a proof using the compactness theorem for first-order logic directly.
Is such a proof known?
 Aluffi, Paolo. Algebra: Chapter 0: Chapter 0. Vol. 104. American Mathematical Soc., 2009.
 Banaschewski, Bernhard. "Algebraic closure without choice." Mathematical Logic Quarterly 38.1 (1992): 383-385.