In order theory, an ultrafilter is a subset of a partially ordered set that is maximal among all proper filters. This implies that any filter that properly contains an ultrafilter has to be equal to the whole poset.
Every filter on a Boolean algebra (or more generally, any subset with the finite intersection property) is contained in an ultrafilter (see ultrafilter lemma) and that free ultrafilters therefore exist, but the proofs involve the axiom of choice (AC) in the form of Zorn's lemma. On the other hand, the statement that every filter is contained in an ultrafilter does not imply AC. Indeed, it is equivalent to the Boolean prime ideal theorem (BPIT), a well-known intermediate point between the axioms of Zermelo–Fraenkel set theory (ZF) and the ZF theory augmented by the axiom of choice (ZFC). In general, proofs involving the axiom of choice do not produce explicit examples of free ultrafilters, though it is possible to find explicit examples in some models of ZFC; for example, Gödel showed that this can be done in the constructible universe where one can write down an explicit global choice function. In ZF without the axiom of choice, it is possible that every ultrafilter is principal.
A proof of 1. ⇔ 2. is also given in (Burris, Sankappanavar, 2012, Corollary 3.13, p.133).
Ultrafilters on powersets are useful in topology, especially in relation to compact Hausdorff spaces, and in model theory in the construction of ultraproducts and ultrapowers. Every ultrafilter on a compact Hausdorff space converges to exactly one point. Likewise, ultrafilters on Boolean algebras play a central role in Stone's representation theorem.
In geometric group theory, non-principal ultrafilters are used to define the asymptotic cone of a group. This construction yields a rigorous way to consider looking at the group from infinity, that is the large scale geometry of the group. Asymptotic cones are particular examples of ultralimits of metric spaces.
Gödel's ontological proof of God's existence uses as an axiom that the set of all "positive properties" is an ultrafilter.
In social choice theory, non-principal ultrafilters are used to define a rule (called a social welfare function) for aggregating the preferences of infinitely many individuals. Contrary to Arrow's impossibility theorem for finitely many individuals, such a rule satisfies the conditions (properties) that Arrow proposes (for example, Kirman and Sondermann, 1972). Mihara (1997, 1999) shows, however, such rules are practically of limited interest to social scientists, since they are non-algorithmic or non-computable.