Filters and Ultrafilters

Let $X$ be a set. A family $\mathcal{F}\subseteq \mathcal{P}(X)$ of subsets of $X$ (The power set $\mathcal{P}(x)=\{z:z\subseteq x\}$, Subset $x\subseteq y$, proper subset $x⊊y$, and the separation notation $\{z\in x:\phi (z)\}$) is a filter on $X$ when it satisfies:

• (F1) nontriviality: $X\in \mathcal{F}$;
• (F2) properness: $\mathrm{\varnothing }\mathrm{\notin }\mathcal{F}$;
• (F3) closure under pairwise intersection (The intersection $\bigcap x$ of a nonempty set, the binary intersection $a\cap b:=\bigcap \{a,b\}$, and disjointness): if $A,B\in \mathcal{F}$ then $A\cap B\in \mathcal{F}$;
• (F4) upward closure in $X$: if $A\in \mathcal{F}$ and $A\subseteq B\subseteq X$ then $B\in \mathcal{F}$.

The set of all filters on $X$ is written $\mathrm{F}\mathrm{i}\mathrm{l}\mathrm{t}(X)$. It is a subset of $\mathcal{P}(\mathcal{P}(X))$, hence a set, and it is ordered by inclusion: $\mathcal{F}\subseteq \mathcal{G}$ is read "$\mathcal{G}$ is finer than $\mathcal{F}$", and $\mathcal{F}$ is coarser than $\mathcal{G}$.

Convention: filters are proper. Condition (F2) is part of the definition throughout this library, so "filter" always means "proper filter". The competing convention drops (F2), calls the resulting objects filters, and says proper filter for one that omits $\mathrm{\varnothing }$. The two conventions differ by exactly one object, since (F4) forces any family satisfying (F1), (F3) and (F4) that contains $\mathrm{\varnothing }$ to be all of $\mathcal{P}(X)$: if $\mathrm{\varnothing }\in \mathcal{F}$ then $\mathrm{\varnothing }\subseteq B\subseteq X$ gives $B\in \mathcal{F}$ for every $B\subseteq X$. That single extra object is the improper filter $\mathcal{P}(X)$. This library follows the more widely adopted convention, in which the improper filter is not a filter; a reader arriving from the other convention should read every unqualified "filter" below as "proper filter".

• The intuition is "large". Read $A\in \mathcal{F}$ as "$A$ is a large subset of $X$", where largeness is relative to $\mathcal{F}$. Then (F1) says the whole space is large, (F2) says the empty set is not, (F3) says two large sets overlap largely, and (F4) says a superset of a large set is large. Properness is what stops "large" from being vacuous: without (F2) every subset counts as large and the notion carries no information, which is the mathematical reason the improper filter is excluded rather than a matter of taste.
• $X\mathrm{\ne }\mathrm{\varnothing }$ follows. By (F1) the set $X$ belongs to $\mathcal{F}$ and by (F2) the set $\mathrm{\varnothing }$ does not, so $X\mathrm{\ne }\mathrm{\varnothing }$. Equivalently, there are no filters on the empty set: $\mathcal{P}(\mathrm{\varnothing })=\{\mathrm{\varnothing }\}$, and any filter on $\mathrm{\varnothing }$ would have to contain $\mathrm{\varnothing }$ by (F1) and omit it by (F2). No hypothesis "$X\mathrm{\ne }\mathrm{\varnothing }$" is therefore needed anywhere below; it is delivered by the existence of a filter.
• (F3) extends to any finite list of members and not beyond: an intersection of infinitely many members of a filter is usually not a member, and demanding that it be one is a strictly stronger notion. The families that generate filters by finite intersections are exactly those with the finite intersection property (Finite intersection property, A family lies in a filter exactly when it has the finite intersection property).
• Filters are usually presented by a smaller family that they are generated from, a filter base (Filter base and the filter it generates, The upward closure of a filter base is the smallest filter containing it), because writing out every superset is neither possible nor informative.
• The maximal filters under the inclusion order recorded above are the ultrafilters (Ultrafilter), and every filter is contained in one (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter). Maximal here means maximal, not greatest: as soon as $X$ has two distinct points $x\mathrm{\ne }y$ there is no finest filter, since a filter containing every filter would contain the principal filters at $x$ and at $y$, hence both $\{x\}$ and $\{y\}$, hence their intersection $\mathrm{\varnothing }$, which (F2) forbids. Incomparability of those two principal filters is not the reason: incomparable elements are perfectly compatible with a greatest element above them both, and reading "maximal" as "greatest" is the error recorded in FALSE: every maximal element is a greatest element. The argument is set out in Ultrafilter.

Let $X$ be a set. A family $\mathcal{B}\subseteq \mathcal{P}(X)$ is a filter base on $X$ when it satisfies:

• (B1) nonemptiness: $\mathcal{B}\mathrm{\ne }\mathrm{\varnothing }$;
• (B2) properness: $\mathrm{\varnothing }\mathrm{\notin }\mathcal{B}$;
• (B3) downward directedness: for all $B_1,B_2\in \mathcal{B}$ there is $B_3\in \mathcal{B}$ with $B_3\subseteq B_1\cap B_2$.

The upward closure of $\mathcal{B}$ in $X$ is

$⟨\mathcal{B}⟩:=\{A\subseteq X:B\subseteq A\text{ for some }B\in \mathcal{B}\}\mathrm{.}$

This is a filter on $X$ (Filter on a set), indeed the smallest filter on $X$ containing $\mathcal{B}$, by The upward closure of a filter base is the smallest filter containing it ↗; it is called the filter generated by $\mathcal{B}$, and $\mathcal{B}$ is called a base of it. The definite article is licensed by that lemma and by nothing else: the notation $⟨\mathcal{B}⟩$ is used only for a family already known to be a filter base.

• (B3) does not ask that $B_1\cap B_2$ itself belong to $\mathcal{B}$, only that some member of $\mathcal{B}$ sit inside it. That is what makes a base usable: a family described by a shape, for instance the open discs of the plane that contain the origin, is generally not closed under intersection, since the intersection of two such discs is not a disc, yet it always contains a smaller such disc. Families that are closed under pairwise intersection, such as the tails $\{n\in \mathbb{N}:N\le n\}$ of $\mathbb{N}$, are the special case $B_3=B_1\cap B_2$ of (B3).
• Every filter is a filter base, and it generates itself. A filter satisfies (B1) because it contains $X$, satisfies (B2) by (F2), and satisfies (B3) with $B_3=B_1\cap B_2$ by (F3). Both halves are proved in The upward closure of a filter base is the smallest filter containing it ↗, so "base" is a way of presenting a filter, never a different kind of object.
• When a subfamily is a base for the filter it sits in. If $\mathcal{B}\subseteq \mathcal{F}$ and every member of $\mathcal{F}$ contains a member of $\mathcal{B}$, then $\mathcal{B}$ is a filter base and $⟨\mathcal{B}⟩=\mathcal{F}$: (B1) holds because $X\in \mathcal{F}$ contains some member of $\mathcal{B}$, (B2) because $\mathcal{B}\subseteq \mathcal{F}$, and (B3) because $B_1\cap B_2\in \mathcal{F}$ contains some member of $\mathcal{B}$. So a base is a presentation, not an invariant. What is determined is the generated filter, which is why every statement below is about $⟨\mathcal{B}⟩$ and never about $\mathcal{B}$ itself. The criterion is sufficient, and it is not a claim that a filter has many bases: any base of $\mathcal{F}$ is a subfamily of it, so the filter $\{X\}$ on $X$ has exactly one base, namely $\{X\}$.
• (B2) is exactly the properness of the generated filter, and it is not automatic: dropping it would allow $\mathrm{\varnothing }\in \mathcal{B}$ and then $⟨\mathcal{B}⟩=\mathcal{P}(X)$, the improper filter excluded by the convention recorded in Filter on a set.

Let $X$ be a set and let $\mathcal{B}$ be a filter base on $X$ (Filter base and the filter it generates), with upward closure

$⟨\mathcal{B}⟩=\{A\subseteq X:B\subseteq A\text{ for some }B\in \mathcal{B}\}\mathrm{.}$

Then:

1. $⟨\mathcal{B}⟩$ is a filter on $X$ (Filter on a set);
2. $\mathcal{B}\subseteq ⟨\mathcal{B}⟩$, and $⟨\mathcal{B}⟩\subseteq \mathcal{F}$ for every filter $\mathcal{F}$ on $X$ with $\mathcal{B}\subseteq \mathcal{F}$, so $⟨\mathcal{B}⟩$ is the smallest filter on $X$ containing $\mathcal{B}$;
3. every filter $\mathcal{F}$ on $X$ is itself a filter base, and it generates itself: $⟨\mathcal{F}⟩=\mathcal{F}$.

• The only place directedness (B3) is used is step 1.4, the intersection axiom. Drop it and the upward closure of $\mathcal{B}$ is still closed upward and still proper, but it need not be closed under intersection: on $X=\{0,1\}$ the family $\mathcal{B}=\{\{0\},\{1\}\}$ has upward closure $\{\{0\},\{1\},X\}$, which does not contain $\{0\}\cap \{1\}=\mathrm{\varnothing }$ and is not a filter.
• Part 3 is what licenses the phrase "the filter generated by" being applied to a filter: generation is idempotent, so nothing is gained by generating twice.
• Smallest is meant in the inclusion order on $\mathrm{F}\mathrm{i}\mathrm{l}\mathrm{t}(X)$ and is a genuine least element of the set of filters containing $\mathcal{B}$, not merely a minimal one, since part 2 compares $⟨\mathcal{B}⟩$ with every such filter. This is the opposite situation to Ultrafilter, where only maximality is available.

Let $X$ be a set and $\mathcal{A}\subseteq \mathcal{P}(X)$ a family of subsets of $X$. A finite list in $\mathcal{A}$ is a function $s:n\to \mathcal{A}$ for some $n\in \mathbb{N}$, where $n=\{0,1,\dots ,n-1\}$ is its own set of predecessors in the von Neumann encoding (The natural numbers $\mathbb{N}$ (von Neumann)). Its intersection is the subset of $X$

${\bigcap }_{i\in n}s(i):=\{x\in X:x\in s(i)\text{ for every }i\in n\},$

a definition by Separation alone, with no recursion involved. For $n=0$, that is $n=\mathrm{\varnothing }$, the condition is vacuous and the empty intersection is $X$.

The family $\mathcal{A}$ has the finite intersection property, abbreviated FIP, when

${\bigcap }_{i\in n}s(i)\mathrm{\ne }\mathrm{\varnothing }\text{for every }n\in \mathbb{N}\text{ and every finite list }s:n\to \mathcal{A}\mathrm{.}$

Equivalently: no finitely many members of $\mathcal{A}$ have empty intersection.

• The empty intersection is $X$, and it is included above, so a family with the FIP forces $X\mathrm{\ne }\mathrm{\varnothing }$ (take $n=0$). Many texts state the condition only for $n\ge 1$ and add "$X\mathrm{\ne }\mathrm{\varnothing }$" or "$\mathcal{A}\mathrm{\ne }\mathrm{\varnothing }$" as a separate standing hypothesis. The two readings agree except when $\mathcal{A}=\mathrm{\varnothing }$, where the $n\ge 1$ reading is vacuous and this one still asks that $X$ be nonempty. Including $n=0$ is what makes A family lies in a filter exactly when it has the finite intersection property hold with no side condition, since the empty intersection is exactly the member $X$ that every filter must contain.
• Lists may repeat, and this is harmless: repeating a member does not change an intersection, so quantifying over lists is the same as quantifying over finite subfamilies. Lists are used rather than "finite subfamilies" because a function out of a natural number is available immediately from The natural numbers $\mathbb{N}$ (von Neumann), whereas a general theory of finite sets is not needed anywhere here.
• The FIP is exactly the condition for a family to sit inside some filter (A family lies in a filter exactly when it has the finite intersection property): the finite intersections of $\mathcal{A}$ form a filter base (Filter base and the filter it generates) precisely when none of them is empty, and conversely every family inside a filter inherits the property from properness (Filter on a set).
• The property is about finite intersections only. The family $\{\{n\in \mathbb{N}:N\le n\}:N\in \mathbb{N}\}$ of tails of $\mathbb{N}$ has the FIP, since the intersection of finitely many tails is the one with the largest starting index and no tail is empty, yet the intersection of all of them is empty, because no $n$ lies in the tail starting at $\sigma (n)$. That gap between finite and infinite intersections is the whole reason filters are worth having.

Let $X$ be a set and $\mathcal{A}\subseteq \mathcal{P}(X)$. Write

${\mathcal{A}}^{\cap }:=\{{\bigcap }_{i\in n}s(i):n\in \mathbb{N},s:n\to \mathcal{A}\}$

for the family of intersections of finite lists in $\mathcal{A}$ (Finite intersection property), which contains $X$ as the empty intersection. Then:

1. ${\mathcal{A}}^{\cap }$ is closed under pairwise intersection and contains $\mathcal{A}\cup \{X\}$;
2. if $\mathcal{A}$ has the finite intersection property, then ${\mathcal{A}}^{\cap }$ is a filter base on $X$ (Filter base and the filter it generates) and $⟨{\mathcal{A}}^{\cap }⟩$ is the smallest filter on $X$ containing $\mathcal{A}$ (Filter on a set, The upward closure of a filter base is the smallest filter containing it);
3. conversely, if $\mathcal{A}\subseteq \mathcal{F}$ for some filter $\mathcal{F}$ on $X$, then $\mathcal{A}$ has the finite intersection property.

Consequently a family of subsets of $X$ is contained in some filter on $X$ if and only if it has the finite intersection property.

• Where the hypothesis bites. Part 1 is unconditional: finite lists can always be extended one entry at a time. Only properness, $\mathrm{\varnothing }\mathrm{\notin }{\mathcal{A}}^{\cap }$, needs the finite intersection property, and it is exactly that property restated. So the content of the lemma is bookkeeping in one direction and a definition unfolded in the other, which is why the finite intersection property is the right hypothesis rather than a convenient one.
• The proof uses induction only to move along the length of a list. No theory of finite sets is needed, because a finite list is a function out of a natural number and a natural number is its own set of predecessors (The natural numbers $\mathbb{N}$ (von Neumann)).
• The empty list matters twice: it puts $X$ into ${\mathcal{A}}^{\cap }$, which is what makes ${\mathcal{A}}^{\cap }$ nonempty even when $\mathcal{A}$ is empty, and it is the base case of both inductions. With the $n\ge 1$ reading of the finite intersection property one would have to add $\mathcal{A}\mathrm{\ne }\mathrm{\varnothing }$ as a hypothesis to part 2.
• The generated filter $⟨{\mathcal{A}}^{\cap }⟩$ is the filter usually written $⟨\mathcal{A}⟩$ and called the filter generated by $\mathcal{A}$. It is only defined when $\mathcal{A}$ has the finite intersection property, which is why this library names the base explicitly.

Let $X$ be a set and let $\mathrm{F}\mathrm{i}\mathrm{l}\mathrm{t}(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{F}\mathrm{i}\mathrm{l}\mathrm{t}(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{F}\mathrm{i}\mathrm{l}\mathrm{t}(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{F}\mathrm{i}\mathrm{l}\mathrm{t}(X),\subseteq )$ would be a filter containing every filter, and as soon as $X$ has two distinct points $x\mathrm{\ne }y$ no such filter exists: it would contain the principal filters at $x$ and at $y$, hence both $\{x\}$ and $\{y\}$, hence their intersection $\mathrm{\varnothing }$, 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 The proved choice cost of the ultrafilter lemma. 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\}=\mathrm{\varnothing }$ 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.

Let $X$ be a set and let $\mathcal{D}$ be a nonempty chain (Chain in a poset) in the set of filters on $X$ ordered by inclusion (Filter on a set, Partial order and partially ordered set): every member of $\mathcal{D}$ is a filter on $X$, and any two members of $\mathcal{D}$ are comparable under $\subseteq$. Then $\bigcup \mathcal{D}$ is a filter on $X$, and it is an upper bound of $\mathcal{D}$ for inclusion.

The hypothesis $\mathcal{D}\mathrm{\ne }\mathrm{\varnothing }$ cannot be dropped: $\bigcup \mathrm{\varnothing }=\mathrm{\varnothing }$ contains no set at all, in particular not $X$, so it is not a filter.

• Nonemptiness is used exactly once, at step 1.1, and only for the axiom $X\in \bigcup \mathcal{D}$. The other three axioms hold vacuously for the empty chain, which is precisely why the failure is easy to overlook: three of the four checks go through and the one that does not is the one nobody writes out.
• This is the chain-bound half of the hypothesis of Zorn's lemma (Zorn's lemma), and the empty chain is the other half. In The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter the empty chain is bounded not by this lemma but by the given filter ${\mathcal{F}}_0$, which is why that proof must treat the two cases separately.
• Unions of chains are used rather than unions of arbitrary families because an arbitrary union of filters is almost never a filter: for $x\mathrm{\ne }y$ the union of the principal filters at $x$ and at $y$ contains $\{x\}$ and $\{y\}$ but not $\mathrm{\varnothing }=\{x\}\cap \{y\}$, so it is not closed under intersection. Comparability at step 1.5 is what repairs this.

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a set and let ${\mathcal{F}}_0$ be a filter on $X$ (Filter on a set). Then there is an ultrafilter $\mathcal{U}$ on $X$ (Ultrafilter) with ${\mathcal{F}}_0\subseteq \mathcal{U}$.

The hypothesis is spent exactly once, through Zorn's lemma at step 4.1; the rest of the argument is a theorem of ZF.

In particular, every set that carries a filter carries an ultrafilter. The proof uses Zorn's lemma (Zorn's lemma) and therefore the Axiom of Choice. That some choice principle is unavoidable here, if ZF is consistent, is an external independence result, not proved in this library; see the remarks below.

• The empty chain is the load-bearing case. Zorn's lemma requires an upper bound for every chain of $P$, and the empty chain has one exactly when $P$ is nonempty. Step 3.1 discharges it with ${\mathcal{F}}_0$ itself, and step 2.2 is what makes that possible. This is not a formality: the conclusion of The union of a nonempty chain of filters is a filter fails for the empty chain, since $\bigcup \mathrm{\varnothing }=\mathrm{\varnothing }$ is not a filter, which is exactly why that lemma assumes its chain nonempty; so a proof that says "the union of a chain is a filter" without the case split has a genuine gap at the one chain the hypothesis of Zorn's lemma is easiest to forget.
• Why the poset is $P$ and not $\mathrm{F}\mathrm{i}\mathrm{l}\mathrm{t}(X)$. Applying Zorn to $\mathrm{F}\mathrm{i}\mathrm{l}\mathrm{t}(X)$ would produce a maximal filter unrelated to ${\mathcal{F}}_0$. Restricting to the filters above ${\mathcal{F}}_0$ costs nothing, because step 6.1 transfers maximality back: a filter above $\mathcal{U}$ is automatically above ${\mathcal{F}}_0$, so maximality in $P$ already means maximality among all filters. That transfer is the only step where the shape of $P$ is used.
• The conclusion is an ultrafilter, not the ultrafilter. Zorn's lemma delivers a maximal element and no construction, so nothing in the proof distinguishes the ultrafilter it produces from any other filter above ${\mathcal{F}}_0$; the statement asserts existence and no uniqueness whatever. FALSE, once the ultrafilter lemma is available: every ultrafilter is principal runs the argument on the filter of tails of $\mathbb{N}$ and obtains a single free ultrafilter, which it can describe no further. How many ultrafilters extend a given filter is a separate counting question, and this library neither states nor uses an answer to it.
• Combined with A family lies in a filter exactly when it has the finite intersection property, the lemma takes its most usable form: every family of subsets of $X$ with the finite intersection property is contained in an ultrafilter on $X$. That is the version applied in topology and in model theory.
• What this costs. The proof buys the conclusion with the full Axiom of Choice, through Zorn's lemma and The Axiom of Choice and Zorn's lemma are equivalent, but the statement is, if ZF is consistent, strictly weaker than the Axiom of Choice: it is then neither provable in ZF nor strong enough to recover choice. Both of those are external metamathematical results, conditional on the consistency of ZF, and are recorded, with references and without a claim to prove them, in The proved choice cost of the ultrafilter lemma.

Let $X$ be a set and $\mathcal{U}$ a filter on $X$ (Filter on a set). The following are equivalent:

1. $\mathcal{U}$ is an ultrafilter on $X$ (Ultrafilter);
2. for every $A\subseteq X$, either $A\in \mathcal{U}$ or $X\setminus A\in \mathcal{U}$.

Moreover, for any filter the two alternatives are exclusive: never both $A\in \mathcal{U}$ and $X\setminus A\in \mathcal{U}$. So an ultrafilter decides every subset of $X$, containing exactly one of $A$ and $X\setminus A$.

• This is the working form of the definition. Maximality is a statement about the whole poset of filters; deciding complements is a statement about $\mathcal{U}$ alone, and it is what one actually checks and uses. It is the route taken by Ultrafilters are prime: a union in $\mathcal{U}$ has a member in $\mathcal{U}$, for instance. It is not the only route: FALSE, once the ultrafilter lemma is available: every ultrafilter is principal is refuted from properness and the ultrafilter lemma directly, without this characterisation, and does not list it among its dependencies.
• The two directions run as separate threads, and the mechanical stratification interleaves them, so each step is labelled Forward or Converse. They share nothing except the filter $\mathcal{U}$ and the exclusivity of step 1.1: the forward thread builds a specific filter $\mathcal{G}$, the converse thread argues about an arbitrary filter $\mathcal{H}$ above $\mathcal{U}$.
• The filter $\mathcal{G}$ built at step 1.3 is the filter generated by $\mathcal{U}\cup \{A\}$ (A family lies in a filter exactly when it has the finite intersection property): its members are the supersets of the sets $C\cap A$ with $C\in \mathcal{U}$. Those sets are not all the intersections of finite lists drawn from $\mathcal{U}\cup \{A\}$, since a list omitting $A$ intersects to a member $C$ of $\mathcal{U}$ and not to a set of the form $C\cap A$. The two families generate the same filter all the same: finitely many members of $\mathcal{U}$ intersect to a single $C\in \mathcal{U}$, so every such finite intersection either is a $C$ or is a $C\cap A$, and in the first case it contains $C\cap A$; conversely each $C\cap A$ is itself one of the finite intersections. The upward closures therefore coincide, which is all that "generated by" asks. Step 2.1 is the check that $\mathcal{U}\cup \{A\}$ has the finite intersection property, and that check is exactly where $X\setminus A\mathrm{\notin }\mathcal{U}$ is used.
• Exclusivity is a property of filters, not of ultrafilters, and it holds for the trivial reason that $A$ and $X\setminus A$ are disjoint. What maximality buys is only the "at least one" half. Reading the characterisation as a two-valued decision on $\mathcal{P}(X)$ makes an ultrafilter a finitely additive $\{0,1\}$-valued measure on $X$, which is the standard way it is used.
• The characterisation makes ultrafilters visibly rigid: $\mathcal{U}$ is determined by which of each complementary pair it takes, so an ultrafilter is a consistent choice on all of $\mathcal{P}(X)$ at once. This is why producing one in general is done here from a choice principle rather than by a construction (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).

Let $\mathcal{U}$ be an ultrafilter on a set $X$ (Ultrafilter) and let $A,B\subseteq X$. If $A\cup B\in \mathcal{U}$ then $A\in \mathcal{U}$ or $B\in \mathcal{U}$.

More generally, for every $n\in \mathbb{N}$ and every finite list $s:n\to \mathcal{P}(X)$ (The natural numbers $\mathbb{N}$ (von Neumann)), writing ${\bigcup }_{i\in n}s(i)=\{x\in X:x\in s(i)\text{ for some }i\in n\}$, which is $\mathrm{\varnothing }$ when $n=0$: if ${\bigcup }_{i\in n}s(i)\in \mathcal{U}$ then $s(i)\in \mathcal{U}$ for some $i\in n$.

• The converse holds too, and is worth stating even though it is not needed below: a filter $\mathcal{U}$ with the property that $A\cup B\in \mathcal{U}$ implies $A\in \mathcal{U}$ or $B\in \mathcal{U}$ is an ultrafilter, because $A\cup (X\setminus A)=X\in \mathcal{U}$ forces one of $A$ and $X\setminus A$ into $\mathcal{U}$, which is Characterisation of ultrafilters: every set or its complement. Primeness and maximality are therefore the same condition, which is why the ultrafilter lemma is a form of the Boolean prime ideal theorem (The proved choice cost of the ultrafilter lemma).
• The finite case does not extend to infinite unions. On $\mathbb{N}$ an ultrafilter containing every tail contains $\mathbb{N}={\bigcup }_{x\in \mathbb{N}}\{x\}$ but no singleton (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal), so a union of infinitely many sets can lie in $\mathcal{U}$ with no single member of the union doing so.
• Read through the two-valued measure of Characterisation of ultrafilters: every set or its complement, primeness says that a union of finitely many null sets is null, the complementary form of closure under finite intersection.

This item records only the choice cost established by proofs already present in the library.

The Axiom of Choice implies Zorn's lemma, and the converse implication is also proved here (The Axiom of Choice and Zorn's lemma are equivalent). The proof of the ultrafilter lemma applies Zorn's lemma to the partially ordered set of filters extending a given filter (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter). Consequently the present development proves

$\mathrm{A}\mathrm{C}⟹\text{every filter extends to an ultrafilter}\mathrm{.}$

That is an upper bound on this proof, not a lower bound on the statement. Nothing in the argument proves that the ultrafilter lemma implies AC, that it is provable in ZF, or that it is not provable in ZF. Those questions require the later Boolean-algebra and symmetric-model machinery. Until those proofs are built, no Foundations item may use the recorded model results as a substitute.

The distinction matters downstream. A theorem that assumes an ultrafilter may cite that assumption directly. A theorem that constructs one using The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter inherits the AC-based proof supplied here. Neither case licenses an unproved assertion about the least possible choice principle.

FALSE. For every set $X$, every ultrafilter $\mathcal{U}$ on $X$ (Ultrafilter) is principal: there is an $x\in X$ with $\mathcal{U}=\{A\subseteq X:x\in A\}$.

The claim is plausible because the principal ultrafilters are the only ones anybody can write down. Each is given by a formula in one parameter, they are easy to check, and on a finite $X$ there are no others. What the claim misses is that The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter manufactures ultrafilters from filters that no point generates, and it does so without ever naming the result.

What refutes the claim, and what that costs. The refutation below assumes the ultrafilter lemma, which this library proves from the Axiom of Choice (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter). The claim is not refuted in ZF alone: as the remarks record, it is consistent with ZF that every ultrafilter on $\mathbb{N}$ is principal.