Łoś theorem

This theorem characterizes truth in an ultraproduct. Łoś's theorem says that a first-order formula holds in an ultraproduct exactly when it holds in a set of factors belonging to the ultrafilter.

For a family of first-order structures, take free filters on the index set as worlds, ordered by inclusion, and product sequences as parameters. Force an atom when its coordinate truth set belongs to the filter. Conjunction is local, implication and negation quantify over filter extensions, and a disjunction is forced when every extension has a further extension forcing one disjunct. Existence is witnessed by a product sequence and universality holds for all sequences at all extensions. With the axiom of choice, induction on formulas identifies forcing with membership of the classical coordinate truth set. Equivalently, every ultrafilter extension satisfies the formula in its ultraproduct. Thus the semantics validates classical logic. A local disjunction rule would fail this identification: a set and its complement can both be absent from a free filter, while their union is the whole index set.

For a prime number $p$, a nonprincipal ultrafilter on $\mathbb{N}$ givesThe Łoś theorem makes $K$ a field of characteristic $p$. For every natural number $m$, almost all factors have at least $m$ elements, so $K$ is infinite.