In model theory, an ultrapower of a structure with respect to an ultrafilter is a common method for creating new structures, with applications to nonstandard arithmetic and nonstandard analysis. It is a standard construction for constructing models which embody infinite and infinitesimal quantities, as in Abraham Robinson’s nonstandard analysis.
An ultrapower is a special case of ultraproduct; see the description under the sheaf-theoretic interpretation below.
Let be a set, and let be an ultrafilter on ; that is, a collection of subsets such that
If and , then ,
If , then ,
For every set , either belongs to or its complement belongs to .
(The first three axioms are the defining axioms for a filter, and the last is satisfied for maximal filters, aka ultrafilters.)
Let be a model of a (finitary, single-sorted) first-order theory (given by a signature together with a set of axioms in the language generated by ). Then the ultrapower
is the set of -equivalence classes on the set of functions , where if and only if
The ultrapower is a structure of under the evident pointwise definitions: for each -ary function symbol , define
and observe that implies that , so that the interpretation of descends to equivalence classes. Similarly, for each -ary relation symbol , say if
for any chosen representatives . Note that the well-definedness of the interpretations of functions and relations depends only on the filter axioms.
That the ultrapower is a model of the theory is a consequence of Los's theorem. (Here one needs all of the ultrafilter conditions, in particular one needs condition 4 in order to accommodate satisfaction of formulas involving instances of negation.)
An ultrafilter on a set may be regarded as a point in the Stone-Cech compactification of the discrete space , and ultrapowers may be interpreted as a special case of taking stalks.
Namely, let be the inclusion. This is a continuous function; hence it induces a geometric morphism between the sheaf toposes over these spaces. Then, under the composite
the set is taken to the ultrapower .
An object of is just an -indexed collection of sets, and the more general ultraproduct is the value obtained by applying the composite
to the object .
For any filter on a set , we can form the 2-colimit of the pseudofunctor
Each is the logical morphism of toposes given by the pullback functor . The 2-colimit is itself a topos denoted , in fact a 2-valued topos if is an ultrafilter, and the functor defined by
defines a logical morphism.
If is a principal ultrafilter, then the ultrapower of is isomorphic to again. Thus the interest in ultrapowers relies on the existence of non-principal ultrafilters, which requires some sort of choice principle.
An important application is to as a model of the theory of ordered fields. If is a non-principal ultrafilter on the set of natural numbers , then the model provides a model for nonstandard analysis (in the sense promulgated by Abraham Robinson). There are in particular infinitesimal elements in the ultrapower, for example the -equivalence class of the sequence .
At the same time, the ultrapower is elementarily equivalent to , so that the sentences true for in the first-order theory of ordered fields coincide with the sentences that are true for the ultrapower. This principle assures us that any conclusions adduced with the help of infinitesimals in the ultrapower are still valid in the standard model ; in some cases, however, the arguments based on infinitesimals may offer more perspicuous proofs.