Ultrafilter

Let $X$ be a set and let $\mathrm{Filt}(X)$ be the set of all filters on $X$ (Filter on a set). Since every filter is a subset of $\mathcal{P}(X)$, the family $\mathrm{Filt}(X)$ is a subset of $\mathcal{P}(\mathcal{P}(X))$ and is therefore a set, carved out by Separation. Inclusion is a partial order on it (Partial order and partially ordered set): $\subseteq$ is reflexive, antisymmetric by extensionality, and transitive.

An ultrafilter on $X$ is a filter on $X$ that is a maximal element of $(\mathrm{Filt}(X), \subseteq)$ (Maximal element and greatest element): a filter $\mathcal{U}$ on $X$ such that no filter on $X$ strictly contains $\mathcal{U}$, equivalently such that every filter $\mathcal{G}$ on $X$ with $\mathcal{U} \subseteq \mathcal{G}$ satisfies $\mathcal{G} = \mathcal{U}$.

An ultrafilter is principal if it is of the form $\{\, A \subseteq X : x \in A \,\}$ for some $x \in X$, and free, or non-principal, otherwise.

• Maximal is not greatest, and here the distinction is not academic. A greatest element of $(\mathrm{Filt}(X), \subseteq)$ would be a filter containing every filter, and as soon as $X$ has two distinct points $x \neq y$ no such filter exists: it would contain the principal filters at $x$ and at $y$, hence both $\{x\}$ and $\{y\}$, hence their intersection $\emptyset$, which properness forbids (Filter on a set). So on such an $X$ there is no greatest filter, and reading "maximal" as "greatest" is the error recorded in FALSE: every maximal element is a greatest element. Note what that argument does and does not deliver. It says nothing whatever about which filters are maximal, nor that any is: the absence of a greatest element is compatible with there being no maximal element at all. What does follow, from maximality itself and not from the argument above, is that two distinct ultrafilters are never comparable, since $\mathcal{U} \subseteq \mathcal{V}$ with $\mathcal{U}$ maximal forces $\mathcal{V} = \mathcal{U}$. How many ultrafilters there are is a separate question again, which the argument above does not touch and which this library does not answer at all: the ultrafilter lemma gives EXISTENCE (every filter extends to an ultrafilter), never a count, and The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter says so in its own remarks. See the existence bullet below.
• Maximality is a negative condition, which is what makes it usable: it says nothing can be added, not that everything is already there. The positive reformulation, that $\mathcal{U}$ decides every subset by containing either $A$ or its complement, is Characterisation of ultrafilters: every set or its complement, and it is the form used in practice.
• Existence is free; extension and freeness are not. Ultrafilters exist on every nonempty set with no choice principle at all: the principal filter at a point is one, as the next bullet verifies outright. Two stronger existence statements are what cost something. That every filter is contained in an ultrafilter is The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, proved here from Zorn's lemma (Zorn's lemma); and that some ultrafilter is free is what the ultrafilter lemma buys, since extending the filter of cofinite subsets of $\mathbb{N}$ produces a non-principal one. Neither is a theorem of ZF alone: if ZF is consistent, ZF does not prove that a free ultrafilter on $\mathbb{N}$ exists (Feferman 1965, Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡), and hence does not prove the ultrafilter lemma either. That external result is recorded, not proved, in this library, and the strength the lemma costs is set out in What the ultrafilter lemma costs: a choice principle strictly weaker than AC. So on $\mathbb{N}$ the principal ultrafilters are the only ones ZF alone can be relied on to produce. The same conclusion for every set at once does not follow from Feferman's model, which concerns $\mathbb{N}$; it is the separate and stronger external result Blass 1977: a model of ZF with no free ultrafilter on any set ‡, likewise recorded and not proved here. Once the ultrafilter lemma is available -- and this library proves it from the Axiom of Choice (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter) -- the principal ultrafilters are nevertheless not all of them (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal); in ZF alone that cannot be concluded.
• Principal ultrafilters really are ultrafilters: $\{A \subseteq X : x \in A\}$ is a filter, and if a filter $\mathcal{G}$ contains it then any $B \in \mathcal{G}$ must meet $\{x\}$, since otherwise $B \cap \{x\} = \emptyset$ lies in $\mathcal{G}$, so $x \in B$ and $\mathcal{G}$ is contained in the principal filter at $x$. This is the one family of examples available without any choice principle.