Axiom of Choice in the proof of "Łoś' theorem implies compactness theorem"

Question

The Wikipedia page on the compactness theorem says:

One of those proofs relies on ultraproducts hinging on the axiom of choice as follows:

Proof: Fix a first-order language $L$, and let $\Sigma$ be a collection of $L$-sentences such that every finite subcollection of $L$-sentences, $i\subseteq\Sigma$ of it has a model ${\displaystyle {\mathcal {M}}_{i}}$.

Is the axiom of choice already used here? As an hypothesis, we assume that for each $i$, there is a model $A\models i$. Do we need the axiom of choice here to fix for each $i$ one such specific model $\mathcal M_i$?

Answer 1

Yes, as stated this already appeals to the axiom of choice. We need to choose for each $i$ a model $\cal M_i$.

There is something additional to say about the connection between Los' theorem and compactness, though.

It is a theorem of $\sf ZF$ that Los+Compactness imply choice. And it is consistent that Los' theorem holds, while compactness fails. So when we prove compactness from Los' theorem, we invariably use choice in "preparing the setting in which Los' theorem works".

You can find the surprisingly readable proof of this fact in the following paper:

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.