Alphabeta Math
Session-authored (Fable 5 assisted)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

7 results · all verified · 6 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Filters and Ultrafilters

1 · Prerequisites

2 · Summary

Filters formalize families of subsets that are closed under finite intersection and enlargement. The development uses partial orders, chains, upper bounds, and maximal elements in its application of Zorn's lemma. Natural-number order and induction support the tail-filter construction, while the Axiom of Choice and its known equivalents provide the background for comparing the strength of the ultrafilter lemma.

The definitions of filters, filter bases, the finite intersection property, and ultrafilters lead first to the generated-filter lemmas. The union-of-a-chain lemma then supplies the upper bounds needed for the ultrafilter lemma. Maximality is converted into the complement-decision characterization, from which finite primality follows. The final results distinguish principal from free ultrafilters and record precisely which implications use full choice and which belong to weaker choice principles.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Filter on a set

Definition

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

The set of all filters on XX is written Filt(X)\mathrm{Filt}(X). It is a subset of P(P(X))\mathcal{P}(\mathcal{P}(X)), hence a set, and it is ordered by inclusion: FG\mathcal{F} \subseteq \mathcal{G} is read "G\mathcal{G} is finer than F\mathcal{F}", and F\mathcal{F} is coarser than G\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 \emptyset. The two conventions differ by exactly one object, since (F4) forces any family satisfying (F1), (F3) and (F4) that contains \emptyset to be all of P(X)\mathcal{P}(X): if F\emptyset \in \mathcal{F} then BX\emptyset \subseteq B \subseteq X gives BFB \in \mathcal{F} for every BXB \subseteq X. That single extra object is the improper filter P(X)\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".

Remarks

  • The intuition is "large". Read AFA \in \mathcal{F} as "AA is a large subset of XX", where largeness is relative to F\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.
  • XX \neq \emptyset follows. By (F1) the set XX belongs to F\mathcal{F} and by (F2) the set \emptyset does not, so XX \neq \emptyset. Equivalently, there are no filters on the empty set: P()={}\mathcal{P}(\emptyset) = \{\emptyset\}, and any filter on \emptyset would have to contain \emptyset by (F1) and omit it by (F2). No hypothesis "XX \neq \emptyset" 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 XX has two distinct points xyx \neq y there is no finest filter, since a filter containing every filter would contain the principal filters at xx and at yy, hence both {x}\{x\} and {y}\{y\}, hence their intersection \emptyset, 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.
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Filter base and the filter it generates

Definition

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

  • (B1) nonemptiness: B\mathcal{B} \neq \emptyset;
  • (B2) properness: B\emptyset \notin \mathcal{B};
  • (B3) downward directedness: for all B1,B2BB_1, B_2 \in \mathcal{B} there is B3BB_3 \in \mathcal{B} with B3B1B2B_3 \subseteq B_1 \cap B_2.

The upward closure of B\mathcal{B} in XX is

B:={AX  :  BA for some BB}.\langle \mathcal{B} \rangle := \{\, A \subseteq X \;:\; B \subseteq A \text{ for some } B \in \mathcal{B} \,\}.

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

Remarks

  • (B3) does not ask that B1B2B_1 \cap B_2 itself belong to B\mathcal{B}, only that some member of B\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 {nN:Nn}\{n \in \mathbb{N} : N \leq n\} of N\mathbb{N}, are the special case B3=B1B2B_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 XX, satisfies (B2) by (F2), and satisfies (B3) with B3=B1B2B_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 BF\mathcal{B} \subseteq \mathcal{F} and every member of F\mathcal{F} contains a member of B\mathcal{B}, then B\mathcal{B} is a filter base and B=F\langle \mathcal{B} \rangle = \mathcal{F}: (B1) holds because XFX \in \mathcal{F} contains some member of B\mathcal{B}, (B2) because BF\mathcal{B} \subseteq \mathcal{F}, and (B3) because B1B2FB_1 \cap B_2 \in \mathcal{F} contains some member of B\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 B\langle \mathcal{B} \rangle and never about B\mathcal{B} itself. The criterion is sufficient, and it is not a claim that a filter has many bases: any base of F\mathcal{F} is a subfamily of it, so the filter {X}\{X\} on XX has exactly one base, namely {X}\{X\}.
  • (B2) is exactly the properness of the generated filter, and it is not automatic: dropping it would allow B\emptyset \in \mathcal{B} and then B=P(X)\langle \mathcal{B} \rangle = \mathcal{P}(X), the improper filter excluded by the convention recorded in Filter on a set.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

The upward closure of a filter base is the smallest filter containing it

Statement

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

B={AX  :  BA for some BB}.\langle \mathcal{B} \rangle = \{\, A \subseteq X \;:\; B \subseteq A \text{ for some } B \in \mathcal{B} \,\}.

Then:

  1. B\langle \mathcal{B} \rangle is a filter on XX (Filter on a set);
  2. BB\mathcal{B} \subseteq \langle \mathcal{B} \rangle, and BF\langle \mathcal{B} \rangle \subseteq \mathcal{F} for every filter F\mathcal{F} on XX with BF\mathcal{B} \subseteq \mathcal{F}, so B\langle \mathcal{B} \rangle is the smallest filter on XX containing B\mathcal{B};
  3. every filter F\mathcal{F} on XX is itself a filter base, and it generates itself: F=F\langle \mathcal{F} \rangle = \mathcal{F}.

Facts & Assumptions

Given: A set XX, a filter base BP(X)\mathcal{B} \subseteq \mathcal{P}(X), and B\langle \mathcal{B} \rangle as displayed in the statement.

[A1]

B\mathcal{B} \neq \emptyset, B\emptyset \notin \mathcal{B}, and for all B1,B2BB_1, B_2 \in \mathcal{B} there is B3BB_3 \in \mathcal{B} with B3B1B2B_3 \subseteq B_1 \cap B_2 (Filter base and the filter it generates).

[L1]

A filter on XX is a family FP(X)\mathcal{F} \subseteq \mathcal{P}(X) with XFX \in \mathcal{F}, F\emptyset \notin \mathcal{F}, ABFA \cap B \in \mathcal{F} whenever A,BFA, B \in \mathcal{F}, and BFB \in \mathcal{F} whenever AFA \in \mathcal{F} and ABXA \subseteq B \subseteq X (Filter on a set).

[L2]

A filter base on XX is a nonempty family of subsets of XX that omits \emptyset and is downward directed, the three conditions listed in [A1] (Filter base and the filter it generates).

Proof

technique · direct
1.1

Every member of B\langle \mathcal{B} \rangle is a subset of XX by definition, so BP(X)\langle \mathcal{B} \rangle \subseteq \mathcal{P}(X); and XBX \in \langle \mathcal{B} \rangle, since B\mathcal{B} has a member BB and BXB \subseteq X.

givenA1
1.2

B\emptyset \notin \langle \mathcal{B} \rangle: if BB \subseteq \emptyset for some BBB \in \mathcal{B} then B=B = \emptyset, and B\emptyset \notin \mathcal{B}.

givenA1
1.3

B\langle \mathcal{B} \rangle is closed upward in XX: if ABA \in \langle \mathcal{B} \rangle, say BAB \subseteq A with BBB \in \mathcal{B}, and AAXA \subseteq A' \subseteq X, then BAB \subseteq A', so ABA' \in \langle \mathcal{B} \rangle.

given
1.4

B\langle \mathcal{B} \rangle is closed under pairwise intersection: given A1,A2BA_1, A_2 \in \langle \mathcal{B} \rangle pick B1,B2BB_1, B_2 \in \mathcal{B} with BiAiB_i \subseteq A_i, and then B3BB_3 \in \mathcal{B} with B3B1B2A1A2XB_3 \subseteq B_1 \cap B_2 \subseteq A_1 \cap A_2 \subseteq X, so A1A2BA_1 \cap A_2 \in \langle \mathcal{B} \rangle.

givenA1
1.5

BB\mathcal{B} \subseteq \langle \mathcal{B} \rangle, because BBB \subseteq B and BXB \subseteq X for every BBB \in \mathcal{B}.

given
1.6

If F\mathcal{F} is a filter on XX with BF\mathcal{B} \subseteq \mathcal{F} and ABA \in \langle \mathcal{B} \rangle, say BAXB \subseteq A \subseteq X with BBFB \in \mathcal{B} \subseteq \mathcal{F}, then upward closure of F\mathcal{F} gives AFA \in \mathcal{F}; hence BF\langle \mathcal{B} \rangle \subseteq \mathcal{F}.

givenL1
1.7

Every filter F\mathcal{F} on XX is a filter base: XFX \in \mathcal{F} gives F\mathcal{F} \neq \emptyset, properness gives F\emptyset \notin \mathcal{F}, and for B1,B2FB_1, B_2 \in \mathcal{F} the member B3=B1B2B_3 = B_1 \cap B_2 of F\mathcal{F} satisfies B3B1B2B_3 \subseteq B_1 \cap B_2.

L1L2
2.1

B\langle \mathcal{B} \rangle satisfies all four filter axioms, so it is a filter on XX.

step 1.1step 1.2step 1.3step 1.4L1
2.2

For a filter F\mathcal{F} on XX, applying step 1.5 and step 1.6 to the filter base F\mathcal{F} gives FF\mathcal{F} \subseteq \langle \mathcal{F} \rangle and FF\langle \mathcal{F} \rangle \subseteq \mathcal{F}, that is F=F\langle \mathcal{F} \rangle = \mathcal{F}.

step 1.7step 1.5step 1.6
3.1

So B\langle \mathcal{B} \rangle is a filter containing B\mathcal{B} and contained in every filter that contains B\mathcal{B}, hence the smallest such filter, and every filter is a filter base generating itself.

step 2.1step 2.2step 1.5step 1.6

Remarks

  • The only place directedness (B3) is used is step 1.4, the intersection axiom. Drop it and the upward closure of B\mathcal{B} is still closed upward and still proper, but it need not be closed under intersection: on X={0,1}X = \{0, 1\} the family B={{0},{1}}\mathcal{B} = \{\{0\}, \{1\}\} has upward closure {{0},{1},X}\{\{0\}, \{1\}, X\}, which does not contain {0}{1}=\{0\} \cap \{1\} = \emptyset 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 Filt(X)\mathrm{Filt}(X) and is a genuine least element of the set of filters containing B\mathcal{B}, not merely a minimal one, since part 2 compares B\langle \mathcal{B} \rangle with every such filter. This is the opposite situation to Ultrafilter, where only maximality is available.
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Finite intersection property

Definition

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

ins(i):={xX  :  xs(i) for every in},\textstyle\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=0n = 0, that is n=n = \emptyset, the condition is vacuous and the empty intersection is XX.

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

ins(i)for every nN and every finite list s:nA.\textstyle\bigcap_{i \in n} s(i) \neq \emptyset \quad \text{for every } n \in \mathbb{N} \text{ and every finite list } s : n \to \mathcal{A}.

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

Remarks

  • The empty intersection is XX, and it is included above, so a family with the FIP forces XX \neq \emptyset (take n=0n = 0). Many texts state the condition only for n1n \geq 1 and add "XX \neq \emptyset" or "A\mathcal{A} \neq \emptyset" as a separate standing hypothesis. The two readings agree except when A=\mathcal{A} = \emptyset, where the n1n \geq 1 reading is vacuous and this one still asks that XX be nonempty. Including n=0n = 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 XX 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 N\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 A\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 {{nN:Nn}:NN}\{\,\{n \in \mathbb{N} : N \leq n\} : N \in \mathbb{N}\,\} of tails of N\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 nn lies in the tail starting at σ(n)\sigma(n). That gap between finite and infinite intersections is the whole reason filters are worth having.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

A family lies in a filter exactly when it has the finite intersection property

Statement

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

A:={ins(i)  :  nN, s:nA}\mathcal{A}^{\cap} := \{\, \textstyle\bigcap_{i \in n} s(i) \;:\; n \in \mathbb{N},\ s : n \to \mathcal{A} \,\}

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

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

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

Facts & Assumptions

Given: A set XX, a family AP(X)\mathcal{A} \subseteq \mathcal{P}(X), and A\mathcal{A}^{\cap} as displayed in the statement. Parts 2 and 3 assume, respectively, that A\mathcal{A} has the finite intersection property and that A\mathcal{A} is contained in a filter on XX.

[A1]

A\mathcal{A} has the finite intersection property when ins(i)\bigcap_{i \in n} s(i) \neq \emptyset for every nNn \in \mathbb{N} and every s:nAs : n \to \mathcal{A}, the case n=0n = 0 reading XX \neq \emptyset (Finite intersection property).

[L1]

A filter on XX contains XX, omits \emptyset, is closed under pairwise intersection, and is closed upward in XX (Filter on a set).

[L2]

A filter base on XX is nonempty, omits \emptyset, and is downward directed; its upward closure is the smallest filter on XX containing it (Filter base and the filter it generates, The upward closure of a filter base is the smallest filter containing it).

[L3]

In the von Neumann encoding σ(n)=n{n}\sigma(n) = n \cup \{n\} and nnn \notin n, so, A\mathcal{A} being nonempty, a function u:nAu : n \to \mathcal{A} extends to a function u:σ(n)Au' : \sigma(n) \to \mathcal{A} by prescribing u(n)u'(n) to be any member of A\mathcal{A} (The natural numbers N\mathbb{N} (von Neumann), Every natural number is a transitive set and is not a member of itself).

[L4]

Induction on N\mathbb{N}: a property holding at 00 and passing from nn to σ(n)\sigma(n) holds for every natural number (The principle of mathematical induction).

Proof

technique · direct
1.1

Every member of A\mathcal{A}^{\cap} is a subset of XX, and XAX \in \mathcal{A}^{\cap} as the intersection of the empty list, so A\mathcal{A}^{\cap} \neq \emptyset.

givenA1
1.2

AA\mathcal{A} \subseteq \mathcal{A}^{\cap}: for AAA \in \mathcal{A} the list s:1As : 1 \to \mathcal{A} with s(0)=As(0) = A has i1s(i)=A\bigcap_{i \in 1} s(i) = A, since 1=σ(0)={0}1 = \sigma(0) = \{0\}.

givenL3
1.3

Adjoining one member keeps the family: if B=kpu(k)AB = \bigcap_{k \in p} u(k) \in \mathcal{A}^{\cap} and AAA \in \mathcal{A}, then extending uu to u:σ(p)Au' : \sigma(p) \to \mathcal{A} with u(p)=Au'(p) = A gives kσ(p)u(k)=BA\bigcap_{k \in \sigma(p)} u'(k) = B \cap A, so BAAB \cap A \in \mathcal{A}^{\cap}.

givenL3
1.4

Splitting off the last entry: for t:σ(n)At : \sigma(n) \to \mathcal{A} one has jσ(n)t(j)=(jnt(j))t(n)\bigcap_{j \in \sigma(n)} t(j) = \left(\bigcap_{j \in n} t(j)\right) \cap t(n), since σ(n)=n{n}\sigma(n) = n \cup \{n\}.

givenL3
1.5

If A\mathcal{A} has the finite intersection property then no member of A\mathcal{A}^{\cap} is empty, that is A\emptyset \notin \mathcal{A}^{\cap}.

A1given
2.1

A\mathcal{A}^{\cap} is closed under pairwise intersection, by induction on the length nn of the second list: for n=0n = 0 the second intersection is XX and BX=BAB \cap X = B \in \mathcal{A}^{\cap}; and if the claim holds for all lists of length nn, then for t:σ(n)At : \sigma(n) \to \mathcal{A} the set Bjσ(n)t(j)=(Bjnt(j))t(n)B \cap \bigcap_{j \in \sigma(n)} t(j) = \left(B \cap \bigcap_{j \in n} t(j)\right) \cap t(n) lies in A\mathcal{A}^{\cap} by the case nn followed by step 1.3.

step 1.3step 1.4L4
2.2

Every filter F\mathcal{F} on XX with AF\mathcal{A} \subseteq \mathcal{F} satisfies AF\mathcal{A}^{\cap} \subseteq \mathcal{F}, by induction on the length nn of the list: the empty intersection is XFX \in \mathcal{F}, and jσ(n)t(j)=(jnt(j))t(n)\bigcap_{j \in \sigma(n)} t(j) = \left(\bigcap_{j \in n} t(j)\right) \cap t(n) is an intersection of two members of F\mathcal{F}.

step 1.4L1L4
3.1

Under the finite intersection property, A\mathcal{A}^{\cap} is a filter base on XX: it is nonempty by step 1.1, omits \emptyset by step 1.5, and is downward directed because B1B2B_1 \cap B_2 itself lies in A\mathcal{A}^{\cap}.

step 1.1step 1.5step 2.1L2
3.2

Conversely, if AF\mathcal{A} \subseteq \mathcal{F} with F\mathcal{F} a filter on XX, then AF\mathcal{A}^{\cap} \subseteq \mathcal{F} and F\emptyset \notin \mathcal{F}, so no intersection of a finite list in A\mathcal{A} is empty: A\mathcal{A} has the finite intersection property.

step 2.2L1A1
4.1

Under the finite intersection property, A\langle \mathcal{A}^{\cap} \rangle is the smallest filter on XX containing A\mathcal{A}: it is a filter containing AA\mathcal{A}^{\cap} \supseteq \mathcal{A}, and any filter containing A\mathcal{A} contains A\mathcal{A}^{\cap} and hence its upward closure.

step 3.1step 2.2step 1.2L2
5.1

So A\mathcal{A}^{\cap} contains A{X}\mathcal{A} \cup \{X\} and is closed under pairwise intersection, and A\mathcal{A} is contained in some filter on XX if and only if it has the finite intersection property, in which case the smallest such filter is A\langle \mathcal{A}^{\cap} \rangle.

step 1.1step 1.2step 2.1step 4.1step 3.2

Remarks

  • Where the hypothesis bites. Part 1 is unconditional: finite lists can always be extended one entry at a time. Only properness, A\emptyset \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 N\mathbb{N} (von Neumann)).
  • The empty list matters twice: it puts XX into A\mathcal{A}^{\cap}, which is what makes A\mathcal{A}^{\cap} nonempty even when A\mathcal{A} is empty, and it is the base case of both inductions. With the n1n \geq 1 reading of the finite intersection property one would have to add A\mathcal{A} \neq \emptyset as a hypothesis to part 2.
  • The generated filter A\langle \mathcal{A}^{\cap} \rangle is the filter usually written A\langle \mathcal{A} \rangle and called the filter generated by A\mathcal{A}. It is only defined when A\mathcal{A} has the finite intersection property, which is why this library names the base explicitly.
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Ultrafilter

Definition

Let XX be a set and let Filt(X)\mathrm{Filt}(X) be the set of all filters on XX (Filter on a set). Since every filter is a subset of P(X)\mathcal{P}(X), the family Filt(X)\mathrm{Filt}(X) is a subset of P(P(X))\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 XX is a filter on XX that is a maximal element of (Filt(X),)(\mathrm{Filt}(X), \subseteq) (Maximal element and greatest element): a filter U\mathcal{U} on XX such that no filter on XX strictly contains U\mathcal{U}, equivalently such that every filter G\mathcal{G} on XX with UG\mathcal{U} \subseteq \mathcal{G} satisfies G=U\mathcal{G} = \mathcal{U}.

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

Remarks

  • Maximal is not greatest, and here the distinction is not academic. A greatest element of (Filt(X),)(\mathrm{Filt}(X), \subseteq) would be a filter containing every filter, and as soon as XX has two distinct points xyx \neq y no such filter exists: it would contain the principal filters at xx and at yy, hence both {x}\{x\} and {y}\{y\}, hence their intersection \emptyset, which properness forbids (Filter on a set). So on such an XX 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 UV\mathcal{U} \subseteq \mathcal{V} with U\mathcal{U} maximal forces V=U\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 U\mathcal{U} decides every subset by containing either AA 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 N\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 N\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 N\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 N\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: {AX:xA}\{A \subseteq X : x \in A\} is a filter, and if a filter G\mathcal{G} contains it then any BGB \in \mathcal{G} must meet {x}\{x\}, since otherwise B{x}=B \cap \{x\} = \emptyset lies in G\mathcal{G}, so xBx \in B and G\mathcal{G} is contained in the principal filter at xx. This is the one family of examples available without any choice principle.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

The union of a nonempty chain of filters is a filter

Statement

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

The hypothesis D\mathcal{D} \neq \emptyset cannot be dropped: =\bigcup \emptyset = \emptyset contains no set at all, in particular not XX, so it is not a filter.

Facts & Assumptions

Given: A set XX and a nonempty family D\mathcal{D} of filters on XX, any two members of which are comparable under inclusion.

[A1]

D\mathcal{D} \neq \emptyset; every FD\mathcal{F} \in \mathcal{D} is a filter on XX; and for all F1,F2D\mathcal{F}_1, \mathcal{F}_2 \in \mathcal{D} either F1F2\mathcal{F}_1 \subseteq \mathcal{F}_2 or F2F1\mathcal{F}_2 \subseteq \mathcal{F}_1 (Chain in a poset).

[L1]

A filter on XX is a family of subsets of XX containing XX, omitting \emptyset, closed under pairwise intersection, and closed upward in XX (Filter on a set).

[L2]

Inclusion is a partial order on any set of sets (Partial order and partially ordered set), and uu is an upper bound of SS when sus \subseteq u for every sSs \in S (Upper bound, least upper bound, and strict upper bound).

Proof

technique · direct
1.1

Fix a member FD\mathcal{F}_{\ast} \in \mathcal{D}, which exists because D\mathcal{D} is nonempty.

A1choose
1.2

DP(X)\bigcup \mathcal{D} \subseteq \mathcal{P}(X): a member of the union belongs to some filter on XX, hence is a subset of XX.

A1L1
1.3

D\emptyset \notin \bigcup \mathcal{D}: a member of the union belongs to some FD\mathcal{F} \in \mathcal{D}, and F\emptyset \notin \mathcal{F}.

A1L1
1.4

D\bigcup \mathcal{D} is closed upward in XX: if AFDA \in \mathcal{F} \in \mathcal{D} and ABXA \subseteq B \subseteq X then BFDB \in \mathcal{F} \subseteq \bigcup \mathcal{D}.

A1L1
1.5

D\bigcup \mathcal{D} is closed under pairwise intersection: let AF1A \in \mathcal{F}_1 and BF2B \in \mathcal{F}_2 with F1,F2D\mathcal{F}_1, \mathcal{F}_2 \in \mathcal{D}; comparability puts one of the two inside the other, so AA and BB both belong to the larger one, which contains ABA \cap B, and ABDA \cap B \in \bigcup \mathcal{D}.

A1L1
1.6

Every FD\mathcal{F} \in \mathcal{D} satisfies FD\mathcal{F} \subseteq \bigcup \mathcal{D}, so D\bigcup \mathcal{D} is an upper bound of D\mathcal{D} for inclusion.

A1L2
1.7

If instead D=\mathcal{D} = \emptyset then D=\bigcup \mathcal{D} = \emptyset, which fails the requirement XDX \in \bigcup \mathcal{D}, so nonemptiness of D\mathcal{D} is genuinely used and cannot be removed.

L1
2.1

XDX \in \bigcup \mathcal{D}, because XFX \in \mathcal{F}_{\ast} and FD\mathcal{F}_{\ast} \subseteq \bigcup \mathcal{D}.

step 1.1A1L1
3.1

So D\bigcup \mathcal{D} satisfies all four filter axioms and is an upper bound of D\mathcal{D}: it is a filter on XX above every member of D\mathcal{D}.

step 2.1step 1.2step 1.3step 1.4step 1.5step 1.6L1

Remarks

  • Nonemptiness is used exactly once, at step 1.1, and only for the axiom XDX \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 F0\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 xyx \neq y the union of the principal filters at xx and at yy contains {x}\{x\} and {y}\{y\} but not ={x}{y}\emptyset = \{x\} \cap \{y\}, so it is not closed under intersection. Comparability at step 1.5 is what repairs this.
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let XX be a set and let F0\mathcal{F}_0 be a filter on XX (Filter on a set). Then there is an ultrafilter U\mathcal{U} on XX (Ultrafilter) with F0U\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.

Facts & Assumptions

Given: A set XX, a filter F0\mathcal{F}_0 on XX, and Zorn's lemma.

[A1]

F0\mathcal{F}_0 is a filter on XX: XF0X \in \mathcal{F}_0, F0\emptyset \notin \mathcal{F}_0, and F0\mathcal{F}_0 is closed under pairwise intersection and upward in XX (Filter on a set).

[L1]

Zorn's lemma, which assumes the Axiom of Choice: a nonempty poset in which every chain has an upper bound has a maximal element; the hypothesis is about all chains, the empty chain included (Zorn's lemma, The Axiom of Choice).

[L2]

The union of a nonempty inclusion-chain of filters on XX is a filter on XX and an upper bound of the chain (The union of a nonempty chain of filters is a filter).

[L3]

An ultrafilter on XX is a filter that is a maximal element of (Filt(X),)(\mathrm{Filt}(X), \subseteq), and mm is maximal exactly when mxm \leq x forces x=mx = m (Ultrafilter, Maximal element and greatest element).

[L4]

Inclusion partially orders any set of sets, and a chain is a subset any two of whose members are comparable, the empty set included (Partial order and partially ordered set, Chain in a poset); an element uu of a poset is an upper bound of a subset SS when sus \leq u for every sSs \in S (Upper bound, least upper bound, and strict upper bound).

Proof

technique · direct
1.1

Let Filt(X)\mathrm{Filt}(X) be the set of filters on XX, a subset of P(P(X))\mathcal{P}(\mathcal{P}(X)), partially ordered by inclusion.

L3L4construct
1.2

F0Filt(X)\mathcal{F}_0 \in \mathrm{Filt}(X).

A1
2.1

Let P={FFilt(X):F0F}P = \{\, \mathcal{F} \in \mathrm{Filt}(X) : \mathcal{F}_0 \subseteq \mathcal{F} \,\}, partially ordered by inclusion as a subset of Filt(X)\mathrm{Filt}(X).

step 1.1construct
2.2

PP \neq \emptyset, since F0F0\mathcal{F}_0 \subseteq \mathcal{F}_0 puts F0\mathcal{F}_0 in PP.

step 1.2L4
3.1

The empty chain of PP has an upper bound in PP: every element of PP is vacuously above all of its members, and PP is nonempty, so F0\mathcal{F}_0 is such an upper bound.

step 2.1step 2.2L4
3.2

A nonempty chain DP\mathcal{D} \subseteq P has an upper bound in PP: D\bigcup \mathcal{D} is a filter on XX and an upper bound of D\mathcal{D}; it contains F0\mathcal{F}_0 because some member of D\mathcal{D} does and every member is contained in the union; hence DP\bigcup \mathcal{D} \in P.

step 2.1L2L4
4.1

Every chain of PP has an upper bound in PP, and PP is a nonempty poset, so Zorn's lemma yields a maximal element U\mathcal{U} of PP.

step 2.2step 3.1step 3.2L1
5.1

U\mathcal{U} is a filter on XX with F0U\mathcal{F}_0 \subseteq \mathcal{U}, since UP\mathcal{U} \in P.

step 4.1step 2.1
6.1

Let G\mathcal{G} be any filter on XX with UG\mathcal{U} \subseteq \mathcal{G}; then F0UG\mathcal{F}_0 \subseteq \mathcal{U} \subseteq \mathcal{G}, so GP\mathcal{G} \in P, and maximality of U\mathcal{U} in PP forces G=U\mathcal{G} = \mathcal{U}.

step 4.1step 5.1step 2.1L3
7.1

So no filter on XX strictly contains U\mathcal{U}: U\mathcal{U} is a maximal element of Filt(X)\mathrm{Filt}(X), that is an ultrafilter on XX, and it contains F0\mathcal{F}_0.

step 5.1step 6.1L3

Remarks

  • The empty chain is the load-bearing case. Zorn's lemma requires an upper bound for every chain of PP, and the empty chain has one exactly when PP is nonempty. Step 3.1 discharges it with F0\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 \emptyset = \emptyset 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 PP and not Filt(X)\mathrm{Filt}(X). Applying Zorn to Filt(X)\mathrm{Filt}(X) would produce a maximal filter unrelated to F0\mathcal{F}_0. Restricting to the filters above F0\mathcal{F}_0 costs nothing, because step 6.1 transfers maximality back: a filter above U\mathcal{U} is automatically above F0\mathcal{F}_0, so maximality in PP already means maximality among all filters. That transfer is the only step where the shape of PP 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 F0\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 N\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 XX with the finite intersection property is contained in an ultrafilter on XX. 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 What the ultrafilter lemma costs: a choice principle strictly weaker than AC.
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Characterisation of ultrafilters: every set or its complement

Statement

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

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

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

Facts & Assumptions

Given: A set XX and a filter U\mathcal{U} on XX.

[A1]

U\mathcal{U} is a filter on XX: XUX \in \mathcal{U}, U\emptyset \notin \mathcal{U}, U\mathcal{U} is closed under pairwise intersection, and BUB \in \mathcal{U} whenever AUA \in \mathcal{U} and ABXA \subseteq B \subseteq X (Filter on a set).

[L1]

An ultrafilter on XX is a filter that is maximal for inclusion among the filters on XX; maximality of mm says that mxm \leq x forces x=mx = m (Ultrafilter, Maximal element and greatest element).

Proof

technique · direct
1.1

Exclusivity, for any filter. If AA and XAX \setminus A both lay in U\mathcal{U} then so would A(XA)=A \cap (X \setminus A) = \emptyset, which properness forbids.

A1
1.2

Forward. Assume statement 1, let AXA \subseteq X, and suppose XAUX \setminus A \notin \mathcal{U}; the goal is AUA \in \mathcal{U}.

assume-hyp
1.3

Forward. Let G={BX:CAB for some CU}\mathcal{G} = \{\, B \subseteq X : C \cap A \subseteq B \text{ for some } C \in \mathcal{U} \,\}.

construct
2.1

Forward. Every CUC \in \mathcal{U} satisfies CAC \cap A \neq \emptyset: from CA=C \cap A = \emptyset one gets CXAC \subseteq X \setminus A, and upward closure would then put XAX \setminus A into U\mathcal{U}, which step 1.2 excludes.

step 1.2A1
2.2

Forward. UG\mathcal{U} \subseteq \mathcal{G}, since CACC \cap A \subseteq C for CUC \in \mathcal{U}; and AGA \in \mathcal{G}, since XUX \in \mathcal{U} and XAAXX \cap A \subseteq A \subseteq X.

step 1.3A1
2.3

Converse. Assume statement 2 and let H\mathcal{H} be any filter on XX with UH\mathcal{U} \subseteq \mathcal{H}; for AHA \in \mathcal{H} one cannot have XAUX \setminus A \in \mathcal{U}, since then XAHX \setminus A \in \mathcal{H} and =A(XA)H\emptyset = A \cap (X \setminus A) \in \mathcal{H}, against properness of H\mathcal{H}.

step 1.1A1assume-hyp
3.1

Forward. G\mathcal{G} is a filter on XX: its members are subsets of XX by definition; XGX \in \mathcal{G} by step 2.2; G\emptyset \notin \mathcal{G}, because CAC \cap A \subseteq \emptyset would make CAC \cap A empty against step 2.1; it is closed upward in XX by transitivity of \subseteq; and if C1AB1C_1 \cap A \subseteq B_1 and C2AB2C_2 \cap A \subseteq B_2 with C1,C2UC_1, C_2 \in \mathcal{U} then (C1C2)AB1B2(C_1 \cap C_2) \cap A \subseteq B_1 \cap B_2 with C1C2UC_1 \cap C_2 \in \mathcal{U}, so B1B2GB_1 \cap B_2 \in \mathcal{G}.

step 1.3step 2.1step 2.2A1
3.2

Converse. So AUA \in \mathcal{U} for every AHA \in \mathcal{H} by statement 2, giving HU\mathcal{H} \subseteq \mathcal{U} and hence H=U\mathcal{H} = \mathcal{U}; no filter strictly contains U\mathcal{U}, so U\mathcal{U} is maximal and statement 2 implies statement 1.

step 2.3L1
4.1

Forward. Maximality of U\mathcal{U} applied to the filter GU\mathcal{G} \supseteq \mathcal{U} gives G=U\mathcal{G} = \mathcal{U}, hence AUA \in \mathcal{U} by step 2.2; so statement 1 implies statement 2.

step 3.1step 2.2step 1.2L1
5.1

The two statements are therefore equivalent, and by step 1.1 an ultrafilter contains exactly one of AA and XAX \setminus A for each AXA \subseteq X.

step 4.1step 3.2step 1.1

Remarks

  • This is the working form of the definition. Maximality is a statement about the whole poset of filters; deciding complements is a statement about U\mathcal{U} alone, and it is what one actually checks and uses. It is the route taken by Ultrafilters are prime: a union in U\mathcal{U} has a member in U\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 U\mathcal{U} and the exclusivity of step 1.1: the forward thread builds a specific filter G\mathcal{G}, the converse thread argues about an arbitrary filter H\mathcal{H} above U\mathcal{U}.
  • The filter G\mathcal{G} built at step 1.3 is the filter generated by U{A}\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 CAC \cap A with CUC \in \mathcal{U}. Those sets are not all the intersections of finite lists drawn from U{A}\mathcal{U} \cup \{A\}, since a list omitting AA intersects to a member CC of U\mathcal{U} and not to a set of the form CAC \cap A. The two families generate the same filter all the same: finitely many members of U\mathcal{U} intersect to a single CUC \in \mathcal{U}, so every such finite intersection either is a CC or is a CAC \cap A, and in the first case it contains CAC \cap A; conversely each CAC \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 U{A}\mathcal{U} \cup \{A\} has the finite intersection property, and that check is exactly where XAUX \setminus A \notin \mathcal{U} is used.
  • Exclusivity is a property of filters, not of ultrafilters, and it holds for the trivial reason that AA and XAX \setminus A are disjoint. What maximality buys is only the "at least one" half. Reading the characterisation as a two-valued decision on P(X)\mathcal{P}(X) makes an ultrafilter a finitely additive {0,1}\{0,1\}-valued measure on XX, which is the standard way it is used.
  • The characterisation makes ultrafilters visibly rigid: U\mathcal{U} is determined by which of each complementary pair it takes, so an ultrafilter is a consistent choice on all of P(X)\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).
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

Ultrafilters are prime: a union in U\mathcal{U} has a member in U\mathcal{U}

Statement

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

More generally, for every nNn \in \mathbb{N} and every finite list s:nP(X)s : n \to \mathcal{P}(X) (The natural numbers N\mathbb{N} (von Neumann)), writing ins(i)={xX:xs(i) for some in}\bigcup_{i \in n} s(i) = \{\, x \in X : x \in s(i) \text{ for some } i \in n \,\}, which is \emptyset when n=0n = 0: if ins(i)U\bigcup_{i \in n} s(i) \in \mathcal{U} then s(i)Us(i) \in \mathcal{U} for some ini \in n.

Facts & Assumptions

Given: A set XX, an ultrafilter U\mathcal{U} on XX, and subsets A,BXA, B \subseteq X with ABUA \cup B \in \mathcal{U}.

[A1]

U\mathcal{U} is a filter on XX: XUX \in \mathcal{U}, U\emptyset \notin \mathcal{U}, U\mathcal{U} is closed under pairwise intersection, and closed upward in XX (Filter on a set, Ultrafilter).

[L1]

For every CXC \subseteq X, exactly one of CUC \in \mathcal{U} and XCUX \setminus C \in \mathcal{U} holds (Characterisation of ultrafilters: every set or its complement).

[L2]

Induction on N\mathbb{N}: a property holding at 00 and passing from nn to σ(n)\sigma(n) holds for every natural number; and σ(n)=n{n}\sigma(n) = n \cup \{n\} (The principle of mathematical induction, The natural numbers N\mathbb{N} (von Neumann)).

Proof

technique · direct
1.1

Suppose AUA \notin \mathcal{U}; then XAUX \setminus A \in \mathcal{U}.

L1assume-hyp
1.2

As sets, (AB)(XA)=B(XA)BX(A \cup B) \cap (X \setminus A) = B \cap (X \setminus A) \subseteq B \subseteq X.

given
2.1

Both ABA \cup B and XAX \setminus A lie in U\mathcal{U}, hence so does their intersection.

step 1.1givenA1
3.1

Upward closure applied to (AB)(XA)B(A \cup B) \cap (X \setminus A) \subseteq B gives BUB \in \mathcal{U}; so AUA \in \mathcal{U} or BUB \in \mathcal{U}.

step 2.1step 1.2A1
4.1

The finite case follows by induction on nn: for n=0n = 0 the union is empty and U\emptyset \notin \mathcal{U}, so the hypothesis never holds and the claim is vacuous; and if the claim holds for lists of length nn, then for s:σ(n)P(X)s : \sigma(n) \to \mathcal{P}(X) one has iσ(n)s(i)=(ins(i))s(n)\bigcup_{i \in \sigma(n)} s(i) = \left(\bigcup_{i \in n} s(i)\right) \cup s(n), so the binary case puts either s(n)s(n) or ins(i)\bigcup_{i \in n} s(i) in U\mathcal{U}, and in the second alternative the claim for nn supplies an ini \in n with s(i)Us(i) \in \mathcal{U}.

step 3.1A1L2
5.1

So an ultrafilter is prime: it contains a member of every finite union it contains.

step 3.1step 4.1

Remarks

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5) rests on unproved materialOpen item page →
Rests on 2 statements not proved in this library. Every dependency marked below is recorded with a citation but is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

What the ultrafilter lemma costs: a choice principle strictly weaker than AC

The ultrafilter lemma (UL), that every filter on a set extends to an ultrafilter (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter), is a genuine choice principle. It is neither free nor as expensive as the Axiom of Choice, and this remark records exactly where it sits, separating what this library proves from what it cites.

What is proved here. The Axiom of Choice implies UL. That is The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, which uses Zorn's lemma, and Zorn's lemma is equivalent to the Axiom of Choice over ZF (The Axiom of Choice and Zorn's lemma are equivalent, The Axiom of Choice). Nothing else about the strength of UL is derived in this library, and the three statements below are cited, not proved.

What is cited and not proved.

Why this matters for the rest of the library. A theorem proved from UL is not "a theorem of choice" in the same sense as one proved from the Axiom of Choice. Because the Axiom of Choice and Zorn's lemma are equivalent, a proof through Zorn shows the theorem costs at most the Axiom of Choice, and nothing more than that: it is an upper bound on the price, never a lower one (The Axiom of Choice and Zorn's lemma are equivalent). A result provable from UL alone carries the strictly smaller upper bound UL, and a page that nonetheless routes it through Zorn is overpaying and should say so. UL itself is the standing example, proved here from Zorn and yet, on the cited results above and so under the consistency of ZF, strictly weaker than the Axiom of Choice. That is why The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter is kept as a named statement rather than being inlined into its applications: naming it is what makes the smaller bound visible downstream.

Two honest caveats.

  • This library proves the implication AC \Rightarrow UL and nothing about the converse direction. Calling UL "strictly weaker" is a citation, and it depends on the consistency of ZF, which is not provable inside ZF.
  • The implication proved here goes through Zorn's lemma, so the proof given in The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter uses full choice even though the statement does not require it. A proof of UL from a weaker principle would not change the theorem, only its price. Nothing in this library currently avoids Zorn's lemma at that step.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

FALSE, once the ultrafilter lemma is available: every ultrafilter is principal

Statement

FALSE. For every set XX, every ultrafilter U\mathcal{U} on XX (Ultrafilter) is principal: there is an xXx \in X with U={AX:xA}\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 XX 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 N\mathbb{N} is principal.

Facts & Assumptions

Given: The natural numbers N\mathbb{N} with 00, the successor σ\sigma and the order \leq (The natural numbers N\mathbb{N} (von Neumann), Order on the natural numbers), and the Axiom of Choice in the form used by the ultrafilter lemma.

[A1]

A filter on XX contains XX, omits \emptyset, and is closed under pairwise intersection and upward in XX; a filter base is a nonempty, downward directed family of nonempty subsets (Filter on a set, Filter base and the filter it generates). The principal filter at xx is {AX:xA}\{A \subseteq X : x \in A\}, and it contains {x}\{x\}.

[L1]

The upward closure B\langle \mathcal{B} \rangle of a filter base B\mathcal{B} on XX is a filter on XX, and BB\mathcal{B} \subseteq \langle \mathcal{B} \rangle (The upward closure of a filter base is the smallest filter containing it).

[L2]

Every filter on a set is contained in an ultrafilter on that set, and an ultrafilter is in particular a filter (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, Ultrafilter).

[L3]

\leq on N\mathbb{N} is reflexive, transitive, antisymmetric and total (\le is a linear order on N\mathbb{N}).

[L4]

m<n    σ(m)nm < n \iff \sigma(m) \leq n, and m<nm < n means mnm \leq n with mnm \neq n (Discreteness: σ(n)\sigma(n) is the immediate successor, Order on the natural numbers).

Refutation

technique · direct
1.1

For NNN \in \mathbb{N} put TN={nN:Nn}T_N = \{\, n \in \mathbb{N} : N \leq n \,\}, the tail at NN, and let B={TN:NN}\mathcal{B} = \{\, T_N : N \in \mathbb{N} \,\}.

construct
2.1

B\mathcal{B} \neq \emptyset because T0BT_0 \in \mathcal{B}, and B\emptyset \notin \mathcal{B} because NTNN \in T_N by reflexivity.

step 1.1L3
2.2

B\mathcal{B} is downward directed: given M,NM, N, totality gives say MNM \leq N, and then transitivity gives TNTMT_N \subseteq T_M, so the member TNT_N of B\mathcal{B} satisfies TNTMTNT_N \subseteq T_M \cap T_N.

step 1.1L3
2.3

For every xNx \in \mathbb{N}, {x}Tσ(x)=\{x\} \cap T_{\sigma(x)} = \emptyset: an element of the intersection equals xx and satisfies σ(x)x\sigma(x) \leq x, which would give x<xx < x and hence xxx \neq x.

step 1.1L4
3.1

B\mathcal{B} is a filter base on N\mathbb{N}, so F=B\mathcal{F} = \langle \mathcal{B} \rangle is a filter on N\mathbb{N} and every tail TNT_N belongs to it.

step 2.1step 2.2A1L1
4.1

By the ultrafilter lemma there is an ultrafilter U\mathcal{U} on N\mathbb{N} with FU\mathcal{F} \subseteq \mathcal{U}; in particular TNUT_N \in \mathcal{U} for every NNN \in \mathbb{N}.

step 3.1L2
5.1

No singleton lies in U\mathcal{U}: if {x}U\{x\} \in \mathcal{U} then {x}\{x\} and Tσ(x)T_{\sigma(x)} both lie in U\mathcal{U}, hence so does their intersection \emptyset, which a filter omits.

step 4.1step 2.3A1L2
6.1

The principal filter at xx contains {x}\{x\}, so U\mathcal{U} is not the principal filter at any xNx \in \mathbb{N}; thus U\mathcal{U} is an ultrafilter on N\mathbb{N} that is not principal, and the claim is refuted.

step 5.1A1

Remarks

  • What the refutation consumes. The ultrafilter U\mathcal{U} is produced by The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, which rests on Zorn's lemma and so on the Axiom of Choice. That is not an artefact of this argument: if ZF is consistent, the existence of a non-principal ultrafilter is not provable in ZF. On that same hypothesis there is a model of ZF in which every ultrafilter, on every set, is principal (Blass 1977: a model of ZF with no free ultrafilter on any set , recorded in this library and not proved here), so the false statement above is consistent with ZF alone and is refuted only once a choice principle is available; how much of one it takes is What the ultrafilter lemma costs: a choice principle strictly weaker than AC. This item is therefore false in ZFC and, if ZF is consistent, not refutable in ZF, an unusual status worth stating plainly rather than hiding.
  • The filter used is the Fréchet filter in disguise. The standard witness is the filter of cofinite subsets of N\mathbb{N}. A subset of N\mathbb{N} is cofinite exactly when it contains a tail, so the filter generated by the tails and the filter of cofinite sets coincide; tails are used here because they need only the order on N\mathbb{N}, whereas "cofinite" needs a theory of finite sets that this library has not yet developed. Nothing else changes.
  • On a finite XX the claim is true, which is why the intuition survives: a finite XX is a finite union of its singletons, primeness (Ultrafilters are prime: a union in U\mathcal{U} has a member in U\mathcal{U}) puts one singleton {x}\{x\} into U\mathcal{U}, and upward closure then makes U\mathcal{U} the principal filter at xx. Stating that argument in full needs the notion of a finite set, so it is recorded here as motivation rather than as a proved item.
  • The ultrafilter comes with no description. Zorn's lemma supplies a maximal element and no construction, and no free ultrafilter on N\mathbb{N}, read as a subset of {0,1}N\{0,1\}^{\mathbb{N}}, is Lebesgue measurable or has the Baire property (Sierpiński 1938: no free ultrafilter on N\mathbb{N} is measurable or has the Baire property , an external result recorded and not proved here), so none can be produced by the usual explicit constructions. The refutation therefore names an object it cannot write down, which is the characteristic mark of the Axiom of Choice (Zorn's lemma).

Sources