Solution (source code)

= Solution

Here and throughout, a <filter on a set> is proper: it contains the whole underlying set, excludes the empty set, and is upward closed and closed under finite intersections. An improper filter cannot be extended to a proper <ultrafilter>.

Order the proper filter extensions of $\mathcal F$ by inclusion. The union of a chain is again a proper <filter on a set>: any two members already occur in one member of the chain, where their intersection belongs; the empty set never appears. By <Zorn lemma>, take a maximal proper extension $\mathcal U$. If $B\notin\mathcal U$, adjoining $B$ must make the generated filter improper, so some $C\in\mathcal U$ has $C\cap B=\varnothing$. Upward closure then gives $B^c\in\mathcal U$. Exactly one of $B,B^c$ belongs to $\mathcal U$, proving the <ultrafilter lemma>.

Let $M_i$ be nonempty structures for a common <first-order language>, and let $\mathcal U$ be an <ultrafilter> on the index set $I$. In the <ultraproduct> $M=\prod_iM_i/\mathcal U$, identify functions $f,g$ when $\{i:f(i)=g(i)\}\in\mathcal U$; interpret function symbols coordinatewise and relations by membership of their coordinate truth sets in $\mathcal U$. The <Łoś theorem> states, for every <first-order formula> $\phi$,
$$
M\models\phi([f_1],\ldots,[f_n])\quad\Longleftrightarrow\quad\{i:M_i\models\phi(f_1(i),\ldots,f_n(i))\}\in\mathcal U.
$$
Changing representatives changes a coordinate truth set only outside a member of $\mathcal U$, so the definitions are well defined.

Prove the theorem by <structural induction> on formulas. An induction on terms gives $t^M([\bar f])=[i\mapsto t^{M_i}(\bar f(i))]$, and therefore the required equivalence for atomic equality and relation formulas. For conjunction the truth set is an intersection, and a finite intersection belongs to a proper <filter on a set> exactly when each constituent does. For negation it is a complement, and the <ultrafilter> decides exactly one of a set and its complement. These prove the Boolean induction steps.

For the existential step, a witness $[g]$ in $M$ gives, by induction, a member of $\mathcal U$ on which $\phi(g(i),\bar f(i))$ holds. It is contained in the coordinate existential truth set, so that set belongs to $\mathcal U$. Conversely, if
$$
J=\{i:M_i\models\exists x\,\phi(x,\bar f(i))\}\in\mathcal U,
$$
choose a coordinate witness $g(i)$ for $i\in J$, and any element of the nonempty factor otherwise. Then the truth set of $\phi(g(i),\bar f(i))$ contains $J$. Induction gives a witness $[g]$ in the <ultraproduct>. Universal quantification follows from negation and existence. This completes the actual proof of the <Łoś theorem>.

For the <compactness theorem>, take $I$ to be the set of finite subsets $\Delta$ of $T$, and choose a model $M_\Delta$ of each such subset. The cones
$$
I_\Gamma=\{\Delta\in I:\Gamma\subseteq\Delta\}\qquad(\Gamma\subseteq T\text{ finite})
$$
are nonempty and satisfy $I_{\Gamma_1}\cap I_{\Gamma_2}=I_{\Gamma_1\cup\Gamma_2}$. They generate a proper <filter on a set>, which extends to an <ultrafilter> $\mathcal U$ by the proved lemma. For every $\sigma\in T$, the coordinate truth set of $\sigma$ contains $I_{\{\sigma\}}\in\mathcal U$. The <Łoś theorem> therefore gives
$$
\boxed{\prod_{\Delta\in I}M_\Delta/\mathcal U\models T.}
$$
This proves the requested <compactness theorem>. In fact the same proof works without the countability restriction on the language.