Łoś ultraproduct theorem



The Łoś ultraproduct theorem characterizes the first-order theory of an ultraproduct of \mathcal{L}-structures (for \mathcal{L} some signature). It generalizes the transfer principle from nonstandard analysis, by replacing the hyperreals *^*\mathbb{R} with an ultraproduct and formulas from the standard reals \mathbb{R} with formulas which are true on an “ultrafilter-large” subset of factors of the ultraproduct.


The theorem is usually given in this form:


let (A i) iI(A_i)_{i \in I} be a family of nonempty \mathcal{L}-structures, and let 𝒰\mathcal{U} be an ultrafilter on II. Let *A^* A be the ultraproduct of A iA_i with respect to 𝒰\mathcal{U}. Since each A iA_i was nonempty, *A^* A is the quotient of the product iIA i\prod_{i \in I} A_i by the equivalence relation which identifies sequences which coincide on a subset of indices belonging to 𝒰\mathcal{U}. Let (a i) iI(a_i)_{i \in I} be such a sequence, and let [(a i)][(a_i)] denote its equivalence class. Then for each \mathcal{L}-formula φ(x)\varphi(x),

*Aφ([a i]){jI|A jφ(a j)}𝒰.^* A \models \varphi([a_i]) \iff \{j \in I | A_j \models \varphi(a_j)\} \in \mathcal{U}.

The above follows from a more fundamental fact:


Any functor

[𝒰]:Set ISet[\mathcal{U}] : \mathbf{Set}^I \to \mathbf{Set}

which specifies a choice of ultraproduct (and hence comparison maps, since ultraproducts are colimits) is elementary (logical in the terminology of Makkai-Reyes, i.e. a pretopos morphism.)


A functor is a pretopos morphism precisely when it preserves initial and terminal objects, pullbacks, disjoint sums, and quotients by internal equivalence relations.

Initial objects: a product of empty sets is empty, and a colimit of empty sets is empty.

Terminal objects: a product of terminal objects is terminal, and the quotient of a singleton is a singleton.

Pullbacks: a product of pullbacks is a pullback, and finite limits commute with filtered colimits.

Disjoint sums: a product of disjoint sums is a disjoint sum of products, and colimits commute with colimits.

Quotients: a product of quotients X i/E iX_i / E_i is a quotient of products IX i/ IE i\prod_I X_i / \prod_I E_i, and colimits commute with colimits.

Now we can show the theorem:

Proof of theorem

Since the ultraproduct functor is elementary, then the process of taking points M(X)M(X) of a definable set XX inside models MM commutes with taking ultraproducts. In symbols,

( iIM i/𝒰)(X)( iIM i(X)/𝒰).\left(\prod_{i \in I} M_i / \mathcal{U}\right) (X) \simeq \left(\prod_{i \in I} M_i(X) / \mathcal{U}\right).

Since this is a filtered colimit, a sequence x¯\overline{x} satisfies that its germ [x¯][\overline{x}] is in iIM i/𝒰(X)\prod_{i \in I} M_i / \mathcal{U}(X) if and only if there is some J𝒰J \in \mathcal{U} such that the restriction of x¯\overline{x} to JJ is in jJM j(X)\prod_{j \in J} M_j(X). i.e. if x jM j(X)x_j \in M_j(X) for each jJj \in J.


An immediate consequence of the Łoś theorem is the transfer principle for the hyperreals.

The compactness theorem also follows quickly from the Łoś theorem, so anything that you build using compactness can be realized a bit more concretely as an ultraproduct.


The proposition should be interpreted as saying that Set simultaneously carries a pretopos structure and an ultracategory structure, and that these two structures commute. Indeed, one can view Set as a dualizing object for a generalized Stone duality between pretoposes and ultracategories; this is the starting point of Makkai duality.

There is an analogous statement for ultraproducts of structures in continuous logic.