indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
The ultraproduct construction is an important tool in model theory that permits us to produce a new structure from an infinite family of structures. The construction has a decidedly ‘algebraic’ flavor and hence occurs naturally in applications of model theory to algebra.
It is closely related via the Łoś ultraproduct theorem to the compactness theorem: suppose one is given a set of formulas in some first-order language and a family of structures such that any finite subset of formulas is modeled by all but a finite number of structures. Then an ultraproduct of those structures may be used to model the entire set .1
In slightly greater detail, given a family of structures of the same signature in the sense of model theory (or more specially, universal algebra), one can (assuming the ultrafilter principle, a weak form of the axiom of choice) use ultrafilters to form a certain congruence on the direct product and construct a quotient object, a new structure of the same signature, called an ultraproduct. As long as the ultrafilter is free (contains the filter of cofinite subsets), the last sentence of the preceding paragraph is validated.
An ultraproduct of some number of copies of the same structure is called an ultrapower.
Another important facet, somewhat reminiscent of Morita equivalence, is the Keisler-Shelah theorem: Two structures are elementary equivalent iff they have isomorphic ultrapowers: for some set and ultrafilter . This deep result says that the partially syntactic concept of elementary equivalence can be characterized in purely semantic form with the help of ultrapowers.
First we present the bare-bones set-theoretic construction; then we discuss structures and models.
Let be a set, and let be an ultrafilter on , which may be regarded as an element of the Stone-Cech compactification with its usual topology. The ultrapower functor over is the functor
where is the direct image functor between categories of sheaves induced from the inclusion of as a discrete subspace, and the inverse image functor is also known as the “taking the stalk” functor at the point .
Let us extract a more concrete description. Let be an -indexed family of sets, which we can view as an object of . We may view this object as a sheaf over as discrete space; as a presheaf, it takes an open set (an arbitrary subset ) to the set of sections over which is . The direct image functor takes this presheaf to the presheaf which sends an arbitrary open set to , and then the stalk functor sends this to the filtered colimit
and since the basic opens with are cofinal in the system of open neighborhoods of (ordered by reverse inclusion), the colimit may be written more simply as
and this is the ultraproduct, often written as .2 When all the fibers are the same set , this is written as and called an ultrapower of .
Now suppose each carries a structure specified by a signature; in other words, for each function symbol and predicate symbol of the signature there are specified operations and subsets
where denotes arity (constants being considered function symbols of arity zero). Then of course the products carry structures canonically induced from those on the . As all of the function symbols and predicate symbols have finite arity, and since the taking of filtered colimits commutes with finite limits in , we get a canonically induced structure on the ultraproduct . More briefly: since preserves finite limits, it takes an -indexed finitary structure in to a finitary structure of the same type in .
Intuitively (and adopting language used by Lawvere), what is going on is that we have a variable structure varying over some domain , and we consider a point of its compactification as some kind of “ideal point at infinity”, and then we “freeze” (or localize) the variation by passing to germs of the variation at that point .
Notice that if we replace the word “ultrafilter” by the word “filter”, the general structural facts mentioned here would remain true. That is to say: if is a filter consisting of subsets of , then the colimit (with such ordered by reverse inclusion) is still directed or filtered, and we would still get a structure of given finitary type by passing to the colimit. Here, instead of ultrapowers and ultraproducts, one speaks of reduced powers and reduced products.
To be written.
The hyperreal numbers (wikipedia) and nonstandard integers in nonstandard analysis are obtained as countable ultrapowers with help of free ultrafilters on . Such ultrafilters contain all cofinite subsets of integers, but not only them. See wikipedia:ultraproduct.
From Michael Barr’s Models of Sketches
Unlike limits and colimits, an ultraproduct is not defined by any universal mapping property. Of course, if the category has limits and (filtered) colimits, then it has ultraproducts constructed as colimits of products … But usually the category of models of a coherent theory (such as the theory of fields) lacks products and hence does not have categorical ultraproducts.
(Appropriately-defined) ultrapowers of Banach spaces allow one to embed an infinite-dimensional space inside a larger Banach space such that for every bounded family and every ultrafilter on , the -limit exists (just take the germ ).
There are various ways to formalize this: Henson’s positive bounded logic?, continuous logic, or ad hoc variants (e.g. “Banach space structures”, “normed space structures”, etc.)
As one might expect, things which are only “approximately true” inside become “exactly true” in . For example, if is an approximate eigenvalue? (e.g. on the boundary of the spectrum) for a bounded operator , then the germ of the sequence of approximate eigenvectors of becomes a bona fide eigenvector with eigenvalue for on .
Standard references in model theory for ultraproducts are
J. L. Bell, A. B. Slomson, Models and Ultraproducts: An Introduction , North-Holland Amsterdam 1969. (Dover reprint)
P. C. Eklof, Ultraproducts for Algebraists , pp.105-137 in Barwise (ed.), Handbook of Mathematical Logic , Elsevier Amsterdam 1977.
For a more recent textbook treatment see
The categorical perspective on ultraproducts goes back to
T. Okhuma, Ultrapowers in categories , Yokohama Math. J. 14 (1966) pp.17-37.
S. Fakir, L. Haddad, Objets cohérents et ultraproduits dans les catégories , Journal of Algebra 21 (1972) pp.410–421.
For the vacuum engineering point of view of ‘freezing variation’ 3 in the context of non-standard analysis see
The following papers are relevant for understanding the ultraproduct construction via codensity monads:
D. P. Ellerman, Sheaves of structures and generalized ultraproducts , Annals of Mathematical Logic 7 (1974) pp.163–195.
J. F. Kennison, Triples and compact sheaf representation , JPAA 20 (1981) pp.13-38.
Tom Leinster, Codensity and the Ultrafilter Monad , TAC 28 no. 13 (2013) pp.332-370. (tac)
For a fine point concerning the definition of ultraproducts:
M. Makkai, On full embeddings , JPAA, 1980
See also
For ultraproducts in functional analysis see e.g.
For a way to study ultraproducts in a homotopical setting see
Due to the outstanding importance of the compactness theorem, it is possible to prove ‘almost all’ results in model theory by the use of ultraproducts. This approach to model theory is pursued in Bell-Slomson (1969). For contrast, compare with the more sober view of Hodges (1993). ↩
The quotient notation is traditional but (ever so slightly) misleading. If all the are inhabited sets, then all the maps () are quotient maps and the ultraproduct is a quotient of the full product ; there the notation is apt. If one of the is empty, then the full product is empty and thus the ultraproduct is not such a quotient. But it is useful to allow for empty models (when they exist)! The correct definition which works for all cases is as we have it: a filtered colimit over restricted products. See p. 186 and this MO Discussion for a discussion of this topic. ↩
This perspective was apparently inspired by joined work with Miles Tierney on the use of forcing in the context of the continuum hypothesis in early topos theory. ↩
Last revised on July 12, 2022 at 03:44:58. See the history of this page for a list of all contributions to it.