Solution (source code)

= Solution

For nonempty <first-order structures> $(M_i)_{i\in I}$ and an <ultrafilter> $\mathcal U$ on $I$, define the <ultraproduct> by quotienting the product domain by
$$
a\sim b\quad\Longleftrightarrow\quad\{i:a_i=b_i\}\in\mathcal U.
$$
Functions are interpreted coordinatewise; a relation holds when its coordinate truth <set> belongs to the <ultrafilter>. Closure under finite intersections makes these interpretations independent of representatives. The <Łoś theorem> asserts, for every formula $\varphi$,
$$
\boxed{\prod_iM_i/\mathcal U\models\varphi([a^1],\ldots,[a^r])
\Longleftrightarrow
\{i:M_i\models\varphi(a_i^1,\ldots,a_i^r)\}\in\mathcal U.}
$$

Prove it by structural induction. A term evaluates coordinatewise, by induction on its construction, so atomic equality and relations are exactly their defining truth <sets>. Conjunction uses intersection; negation uses the <ultrafilter> property that exactly one of a <set> and its complement belongs to $\mathcal U$. These establish all Boolean connectives.

For the existential step put $A=\{i:M_i\models\exists x\,\psi(x,\bar a_i)\}$. If an <ultraproduct> witness $[b]$ exists, induction says $\{i:M_i\models\psi(b_i,\bar a_i)\}\in\mathcal U$, and this <set> is contained in $A$, so $A\in\mathcal U$. Conversely if $A\in\mathcal U$, choose a witness $b_i$ at every $i\in A$ and any domain element at the other coordinates. Induction makes $[b]$ a witness. This coordinatewise selection uses choice in the metatheory; nonemptiness of the factors is essential. Universal quantification follows from negation and existence, completing the proof.

For the requested <compactness theorem>, let $I=[T]^{<\omega}$. For each finite $F\subseteq T$, choose $M_F\models F$. For each sentence $\sigma\in T$, its cone $C_\sigma=\{F:\sigma\in F\}$ is nonempty, and intersections of finitely many cones contain the finite union of their requirements. These cones generate a proper filter. The <ultrafilter lemma> extends it to $\mathcal U$. The coordinate models satisfying $\sigma$ include $C_\sigma$, so the Łoś theorem makes their <ultraproduct> satisfy $\sigma$. Since this holds for each $\sigma\in T$, \b[the <ultraproduct> is a model of $T$]. No completeness theorem is needed in this second compactness proof.