An ultraproduct converts coordinatewise finite information into a single first-order structure. Let be nonempty structures in a common first-order language, and let be an ultrafilter on . In , set
The ultraproduct has these equivalence classes as its elements. Functions are interpreted coordinatewise; a relation holds of classes exactly when it holds on a -large set of indices. Intersecting finitely many large agreement sets shows that these interpretations are independent of representatives.
The Łoś theorem, which explains the construction's usefulness, says
Here is the proof. Induction on terms establishes the coordinatewise interpretation of atomic formulas. Finite intersections handle conjunction, and the ultrafilter property handles negation, since precisely one of a set and its complement is large. For an existential quantification, a witness class gives coordinate witnesses on a large set. Conversely, when the coordinate existential truth set is large, select a witness in each of those structures and a default element elsewhere. Its class is a witness in the ultraproduct. This uses choice. Structural induction on formulas now proves the theorem, with universal quantification obtained by negation.
Compactness. If every finite subset of a first-order theory has a model, take to be the finite subsets and choose . The cones for finite have the finite intersection property. Extend their filter to an ultrafilter by the ultrafilter lemma. For each , its cone is large, so the Łoś theorem makes the ultraproduct satisfy . This proves the compactness theorem, including theories of arbitrary set size.
Elementary extensions and nonstandard elements. An ultrapower uses a fixed structure at every coordinate. The diagonal map sending to the class of the constant function is an elementary embedding by the Łoś theorem. For a nonprincipal ultrafilter on , the class of in an ultrapower of the natural numbers exceeds every standard integer, because each corresponding tail is large. In an ultrapower of the real ordered field, the reciprocal of this element is positive and smaller than every positive standard reciprocal integer: an infinitesimal. These examples implement ordinary finite statements in a larger structure without claiming that every external subset or second-order assertion transfers.
Saturation. Such an ultraproduct over is countably saturated. To see the actual diagonal argument, list a finitely satisfiable type with parameters in the ultraproduct and fix representatives for those parameters. For each , the set of coordinates admitting a simultaneous witness to its first formulas belongs to by the Łoś theorem. Arrange that the decrease and put . The decrease, belong to , and have empty intersection. At coordinate , choose a witness to the first formulas, where is the largest with , or choose a default element if there is no such . For each fixed , on the large set . Therefore the resulting class realizes every formula. This proves countable saturation of an ultraproduct over omega; it does not assert saturation at all larger cardinalities.
Algebraic limits. Take finite fields indexed by the primes and a nonprincipal ultrafilter. Their ultraproduct is a field of characteristic zero: for every fixed positive integer , only finitely many primes divide , so on a large set. Every first-order sentence true in all finite fields holds in this infinite field, and more generally so does any sentence true for all but finitely many of the factors. This is a way to create an infinite field retaining uniform first-order information from finite fields. It does not make the field algebraically closed: the first-order sentence that every element is a square already fails in infinitely many of the factors.
Large cardinals. A countably complete ultrafilter gives a well-founded membership ultrapower of the universe. If it had an infinite descending chain represented by , each set
would be large. Countable completeness makes nonempty, giving an actual infinite membership descent at any index in the intersection, contrary to foundation. The Mostowski collapse therefore gives a transitive target and an ultrapower embedding .
For a measure on a measurable cardinal , every function with is constant on a large set: otherwise intersect the fewer than complements of all its fibres. Consequently fixes the ordinals below . The class of the identity function is below and above every constant class below , since all tails are large. Thus and its critical point is . Fine ultrafilters on that are normal ultrafilters on small subsets and kappa-complete yield the stronger embeddings witnessing supercompact cardinals.
These applications share a single principle: an ultraproduct preserves precisely the first-order information seen by its ultrafilter. Principal ultrafilters merely select a factor; nonprincipal ones can produce new sizes, elements and saturation. Existence of the needed ultrafilters and selection of coordinate witnesses are set-theoretic assumptions, and changing the ultrafilter may change the resulting model.
An ultraproduct assembles a family of nonempty first-order structures in one fixed language, using an ultrafilter to specify which coordinate statements hold almost everywhere. Its universe is
Functions are interpreted coordinatewise, and an -ary relation holds on when its coordinate truth set belongs to . Changing representatives changes such a truth set only off a -large set, so these definitions are well defined. A principal ultrafilter simply recovers its distinguished factor; a nonprincipal ultrafilter can produce new elements and structures.
The fundamental result is the Łoś theorem:
Prove it by structural induction on first-order formulas. Atomic formulas are the definition. Intersections handle conjunction, while exactly one of a set and its complement belongs to an ultrafilter, handling negation. For the existential step, if the coordinate existential truth set is in , use choice to select witnesses there and arbitrary values elsewhere; their product function is an ultraproduct witness. Conversely a product witness makes the coordinate existential truth set contain a -large set. Other connectives and universal quantification follow.
In an ultrapower, all factors are one structure . The diagonal map is an elementary embedding by the Łoś theorem. For a nonprincipal on , the class of in an ultrapower of the standard natural numbers is larger than every constant natural number, since each tail belongs to . This gives a nonstandard model of Peano arithmetic. Similarly, an ultraproduct of finite fields with distinct primes tending to infinity has characteristic zero: for every fixed positive integer , the equation fails in all sufficiently late factors. An infinite structure can therefore arise from finite factors.
Ultraproducts prove the compactness theorem. If each finite subset of a theory has a model , index these models by . The cones have the finite intersection property. Extend their filter to an ultrafilter using the ultrafilter lemma. The Łoś theorem makes the resulting ultraproduct satisfy every . This construction also gives elementary extensions realizing prescribed finitely satisfiable types.
A useful stronger property is countable saturation of an ultraproduct over omega. Let a countable type be finitely satisfiable in an ultraproduct over a nonprincipal on . Choose coordinate representatives of its parameters. Let be the coordinates where the first formulas have a simultaneous witness; then , the decrease, and we can replace by . At coordinate , choose a witness to the first formulas, where is the largest with , taking an arbitrary value if there is none. For each fixed , the set where is -large. Its class realizes the entire type. This proof uses countable incompleteness of , not arbitrary completeness or automatic saturation at larger cardinals.
Finally, complete ultrafilters connect ultraproducts to large cardinals. A countably complete ultrafilter prevents an externally infinite descending membership chain in an ultrapower of a well-founded universe: intersect the countably many coordinate truth sets and obtain an impossible descending chain at one coordinate. A kappa-complete nonprincipal ultrafilter on consequently supplies the ultrapower embedding associated with a measurable cardinal. Thus the same construction supports both elementary compactness arguments and large-cardinal embeddings, with the completeness hypothesis deciding which well-foundedness and closure properties survive.