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.
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
Filter on a set
Definition
Let be a set. A family of subsets of (The power set , Subset , proper subset , and the separation notation ) is a filter on when it satisfies:
- (F1) nontriviality: ;
- (F2) properness: ;
- (F3) closure under pairwise intersection (The intersection of a nonempty set, the binary intersection , and disjointness): if then ;
- (F4) upward closure in : if and then .
The set of all filters on is written . It is a subset of , hence a set, and it is ordered by inclusion: is read " is finer than ", and is coarser than .
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 . The two conventions differ by exactly one object, since (F4) forces any family satisfying (F1), (F3) and (F4) that contains to be all of : if then gives for every . That single extra object is the improper filter . 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 as " is a large subset of ", where largeness is relative to . 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.
- follows. By (F1) the set belongs to and by (F2) the set does not, so . Equivalently, there are no filters on the empty set: , and any filter on would have to contain by (F1) and omit it by (F2). No hypothesis "" 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 has two distinct points there is no finest filter, since a filter containing every filter would contain the principal filters at and at , hence both and , hence their intersection , 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.
Filter base and the filter it generates
Definition
Let be a set. A family is a filter base on when it satisfies:
- (B1) nonemptiness: ;
- (B2) properness: ;
- (B3) downward directedness: for all there is with .
The upward closure of in is
This is a filter on (Filter on a set), indeed the smallest filter on containing , by The upward closure of a filter base is the smallest filter containing it ↗; it is called the filter generated by , and is called a base of it. The definite article is licensed by that lemma and by nothing else: the notation is used only for a family already known to be a filter base.
Remarks
- (B3) does not ask that itself belong to , only that some member of 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 of , are the special case of (B3).
- Every filter is a filter base, and it generates itself. A filter satisfies (B1) because it contains , satisfies (B2) by (F2), and satisfies (B3) with 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 and every member of contains a member of , then is a filter base and : (B1) holds because contains some member of , (B2) because , and (B3) because contains some member of . So a base is a presentation, not an invariant. What is determined is the generated filter, which is why every statement below is about and never about itself. The criterion is sufficient, and it is not a claim that a filter has many bases: any base of is a subfamily of it, so the filter on has exactly one base, namely .
- (B2) is exactly the properness of the generated filter, and it is not automatic: dropping it would allow and then , the improper filter excluded by the convention recorded in Filter on a set.
The upward closure of a filter base is the smallest filter containing it
Statement
Let be a set and let be a filter base on (Filter base and the filter it generates), with upward closure
Then:
- is a filter on (Filter on a set);
- , and for every filter on with , so is the smallest filter on containing ;
- every filter on is itself a filter base, and it generates itself: .
Facts & Assumptions
Given: A set , a filter base , and as displayed in the statement.
, , and for all there is with (Filter base and the filter it generates).
A filter on is a family with , , whenever , and whenever and (Filter on a set).
A filter base on is a nonempty family of subsets of that omits and is downward directed, the three conditions listed in [A1] (Filter base and the filter it generates).
Proof
Every member of is a subset of by definition, so ; and , since has a member and .
: if for some then , and .
is closed upward in : if , say with , and , then , so .
is closed under pairwise intersection: given pick with , and then with , so .
, because and for every .
If is a filter on with and , say with , then upward closure of gives ; hence .
Every filter on is a filter base: gives , properness gives , and for the member of satisfies .
satisfies all four filter axioms, so it is a filter on .
For a filter on , applying step 1.5 and step 1.6 to the filter base gives and , that is .
So is a filter containing and contained in every filter that contains , hence the smallest such filter, and every filter is a filter base generating itself.
Remarks
- The only place directedness (B3) is used is step 1.4, the intersection axiom. Drop it and the upward closure of is still closed upward and still proper, but it need not be closed under intersection: on the family has upward closure , which does not contain 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 and is a genuine least element of the set of filters containing , not merely a minimal one, since part 2 compares with every such filter. This is the opposite situation to Ultrafilter, where only maximality is available.
Finite intersection property
Definition
Let be a set and a family of subsets of . A finite list in is a function for some , where is its own set of predecessors in the von Neumann encoding (The natural numbers (von Neumann)). Its intersection is the subset of
a definition by Separation alone, with no recursion involved. For , that is , the condition is vacuous and the empty intersection is .
The family has the finite intersection property, abbreviated FIP, when
Equivalently: no finitely many members of have empty intersection.
Remarks
- The empty intersection is , and it is included above, so a family with the FIP forces (take ). Many texts state the condition only for and add "" or "" as a separate standing hypothesis. The two readings agree except when , where the reading is vacuous and this one still asks that be nonempty. Including 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 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 (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 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 of tails of 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 lies in the tail starting at . That gap between finite and infinite intersections is the whole reason filters are worth having.
A family lies in a filter exactly when it has the finite intersection property
Statement
Let be a set and . Write
for the family of intersections of finite lists in (Finite intersection property), which contains as the empty intersection. Then:
- is closed under pairwise intersection and contains ;
- if has the finite intersection property, then is a filter base on (Filter base and the filter it generates) and is the smallest filter on containing (Filter on a set, The upward closure of a filter base is the smallest filter containing it);
- conversely, if for some filter on , then has the finite intersection property.
Consequently a family of subsets of is contained in some filter on if and only if it has the finite intersection property.
Facts & Assumptions
Given: A set , a family , and as displayed in the statement. Parts 2 and 3 assume, respectively, that has the finite intersection property and that is contained in a filter on .
has the finite intersection property when for every and every , the case reading (Finite intersection property).
A filter on contains , omits , is closed under pairwise intersection, and is closed upward in (Filter on a set).
A filter base on is nonempty, omits , and is downward directed; its upward closure is the smallest filter on containing it (Filter base and the filter it generates, The upward closure of a filter base is the smallest filter containing it).
In the von Neumann encoding and , so, being nonempty, a function extends to a function by prescribing to be any member of (The natural numbers (von Neumann), Every natural number is a transitive set and is not a member of itself).
Induction on : a property holding at and passing from to holds for every natural number (The principle of mathematical induction).
Proof
Every member of is a subset of , and as the intersection of the empty list, so .
: for the list with has , since .
Adjoining one member keeps the family: if and , then extending to with gives , so .
Splitting off the last entry: for one has , since .
If has the finite intersection property then no member of is empty, that is .
is closed under pairwise intersection, by induction on the length of the second list: for the second intersection is and ; and if the claim holds for all lists of length , then for the set lies in by the case followed by step 1.3.
Every filter on with satisfies , by induction on the length of the list: the empty intersection is , and is an intersection of two members of .
Under the finite intersection property, is a filter base on : it is nonempty by step 1.1, omits by step 1.5, and is downward directed because itself lies in .
Conversely, if with a filter on , then and , so no intersection of a finite list in is empty: has the finite intersection property.
Under the finite intersection property, is the smallest filter on containing : it is a filter containing , and any filter containing contains and hence its upward closure.
So contains and is closed under pairwise intersection, and is contained in some filter on if and only if it has the finite intersection property, in which case the smallest such filter is .
Remarks
- Where the hypothesis bites. Part 1 is unconditional: finite lists can always be extended one entry at a time. Only properness, , 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 (von Neumann)).
- The empty list matters twice: it puts into , which is what makes nonempty even when is empty, and it is the base case of both inductions. With the reading of the finite intersection property one would have to add as a hypothesis to part 2.
- The generated filter is the filter usually written and called the filter generated by . It is only defined when has the finite intersection property, which is why this library names the base explicitly.
Ultrafilter
Definition
Let be a set and let be the set of all filters on (Filter on a set). Since every filter is a subset of , the family is a subset of and is therefore a set, carved out by Separation. Inclusion is a partial order on it (Partial order and partially ordered set): is reflexive, antisymmetric by extensionality, and transitive.
An ultrafilter on is a filter on that is a maximal element of (Maximal element and greatest element): a filter on such that no filter on strictly contains , equivalently such that every filter on with satisfies .
An ultrafilter is principal if it is of the form for some , and free, or non-principal, otherwise.
Remarks
- Maximal is not greatest, and here the distinction is not academic. A greatest element of would be a filter containing every filter, and as soon as has two distinct points no such filter exists: it would contain the principal filters at and at , hence both and , hence their intersection , which properness forbids (Filter on a set). So on such an 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 with maximal forces . 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 decides every subset by containing either 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 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 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 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 ; 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: is a filter, and if a filter contains it then any must meet , since otherwise lies in , so and is contained in the principal filter at . This is the one family of examples available without any choice principle.
The union of a nonempty chain of filters is a filter
Statement
Let be a set and let be a nonempty chain (Chain in a poset) in the set of filters on ordered by inclusion (Filter on a set, Partial order and partially ordered set): every member of is a filter on , and any two members of are comparable under . Then is a filter on , and it is an upper bound of for inclusion.
The hypothesis cannot be dropped: contains no set at all, in particular not , so it is not a filter.
Facts & Assumptions
Given: A set and a nonempty family of filters on , any two members of which are comparable under inclusion.
; every is a filter on ; and for all either or (Chain in a poset).
A filter on is a family of subsets of containing , omitting , closed under pairwise intersection, and closed upward in (Filter on a set).
Inclusion is a partial order on any set of sets (Partial order and partially ordered set), and is an upper bound of when for every (Upper bound, least upper bound, and strict upper bound).
Proof
Fix a member , which exists because is nonempty.
: a member of the union belongs to some filter on , hence is a subset of .
: a member of the union belongs to some , and .
is closed upward in : if and then .
is closed under pairwise intersection: let and with ; comparability puts one of the two inside the other, so and both belong to the larger one, which contains , and .
Every satisfies , so is an upper bound of for inclusion.
If instead then , which fails the requirement , so nonemptiness of is genuinely used and cannot be removed.
, because and .
So satisfies all four filter axioms and is an upper bound of : it is a filter on above every member of .
Remarks
- Nonemptiness is used exactly once, at step 1.1, and only for the axiom . 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 , 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 the union of the principal filters at and at contains and but not , so it is not closed under intersection. Comparability at step 1.5 is what repairs this.
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 be a set and let be a filter on (Filter on a set). Then there is an ultrafilter on (Ultrafilter) with .
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 , a filter on , and Zorn's lemma.
is a filter on : , , and is closed under pairwise intersection and upward in (Filter on a set).
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).
The union of a nonempty inclusion-chain of filters on is a filter on and an upper bound of the chain (The union of a nonempty chain of filters is a filter).
An ultrafilter on is a filter that is a maximal element of , and is maximal exactly when forces (Ultrafilter, Maximal element and greatest element).
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 of a poset is an upper bound of a subset when for every (Upper bound, least upper bound, and strict upper bound).
Proof
Let be the set of filters on , a subset of , partially ordered by inclusion.
.
Let , partially ordered by inclusion as a subset of .
, since puts in .
The empty chain of has an upper bound in : every element of is vacuously above all of its members, and is nonempty, so is such an upper bound.
A nonempty chain has an upper bound in : is a filter on and an upper bound of ; it contains because some member of does and every member is contained in the union; hence .
Every chain of has an upper bound in , and is a nonempty poset, so Zorn's lemma yields a maximal element of .
is a filter on with , since .
Let be any filter on with ; then , so , and maximality of in forces .
So no filter on strictly contains : is a maximal element of , that is an ultrafilter on , and it contains .
Remarks
- The empty chain is the load-bearing case. Zorn's lemma requires an upper bound for every chain of , and the empty chain has one exactly when is nonempty. Step 3.1 discharges it with 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 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 and not . Applying Zorn to would produce a maximal filter unrelated to . Restricting to the filters above costs nothing, because step 6.1 transfers maximality back: a filter above is automatically above , so maximality in already means maximality among all filters. That transfer is the only step where the shape of 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 ; 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 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 with the finite intersection property is contained in an ultrafilter on . 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.
Characterisation of ultrafilters: every set or its complement
Statement
Let be a set and a filter on (Filter on a set). The following are equivalent:
- is an ultrafilter on (Ultrafilter);
- for every , either or .
Moreover, for any filter the two alternatives are exclusive: never both and . So an ultrafilter decides every subset of , containing exactly one of and .
Facts & Assumptions
Given: A set and a filter on .
is a filter on : , , is closed under pairwise intersection, and whenever and (Filter on a set).
An ultrafilter on is a filter that is maximal for inclusion among the filters on ; maximality of says that forces (Ultrafilter, Maximal element and greatest element).
Proof
Exclusivity, for any filter. If and both lay in then so would , which properness forbids.
Forward. Assume statement 1, let , and suppose ; the goal is .
Forward. Let .
Forward. Every satisfies : from one gets , and upward closure would then put into , which step 1.2 excludes.
Forward. , since for ; and , since and .
Converse. Assume statement 2 and let be any filter on with ; for one cannot have , since then and , against properness of .
Forward. is a filter on : its members are subsets of by definition; by step 2.2; , because would make empty against step 2.1; it is closed upward in by transitivity of ; and if and with then with , so .
Converse. So for every by statement 2, giving and hence ; no filter strictly contains , so is maximal and statement 2 implies statement 1.
Forward. Maximality of applied to the filter gives , hence by step 2.2; so statement 1 implies statement 2.
The two statements are therefore equivalent, and by step 1.1 an ultrafilter contains exactly one of and for each .
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 alone, and it is what one actually checks and uses. It is the route taken by Ultrafilters are prime: a union in has a member in , 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 and the exclusivity of step 1.1: the forward thread builds a specific filter , the converse thread argues about an arbitrary filter above .
- The filter built at step 1.3 is the filter generated by (A family lies in a filter exactly when it has the finite intersection property): its members are the supersets of the sets with . Those sets are not all the intersections of finite lists drawn from , since a list omitting intersects to a member of and not to a set of the form . The two families generate the same filter all the same: finitely many members of intersect to a single , so every such finite intersection either is a or is a , and in the first case it contains ; conversely each 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 has the finite intersection property, and that check is exactly where is used.
- Exclusivity is a property of filters, not of ultrafilters, and it holds for the trivial reason that and are disjoint. What maximality buys is only the "at least one" half. Reading the characterisation as a two-valued decision on makes an ultrafilter a finitely additive -valued measure on , which is the standard way it is used.
- The characterisation makes ultrafilters visibly rigid: is determined by which of each complementary pair it takes, so an ultrafilter is a consistent choice on all of 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).
Ultrafilters are prime: a union in has a member in
Statement
Let be an ultrafilter on a set (Ultrafilter) and let . If then or .
More generally, for every and every finite list (The natural numbers (von Neumann)), writing , which is when : if then for some .
Facts & Assumptions
Given: A set , an ultrafilter on , and subsets with .
is a filter on : , , is closed under pairwise intersection, and closed upward in (Filter on a set, Ultrafilter).
For every , exactly one of and holds (Characterisation of ultrafilters: every set or its complement).
Induction on : a property holding at and passing from to holds for every natural number; and (The principle of mathematical induction, The natural numbers (von Neumann)).
Proof
Suppose ; then .
As sets, .
Both and lie in , hence so does their intersection.
Upward closure applied to gives ; so or .
The finite case follows by induction on : for the union is empty and , so the hypothesis never holds and the claim is vacuous; and if the claim holds for lists of length , then for one has , so the binary case puts either or in , and in the second alternative the claim for supplies an with .
So an ultrafilter is prime: it contains a member of every finite union it contains.
Remarks
- The converse holds too, and is worth stating even though it is not needed below: a filter with the property that implies or is an ultrafilter, because forces one of and into , 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 (What the ultrafilter lemma costs: a choice principle strictly weaker than AC).
- The finite case does not extend to infinite unions. On an ultrafilter containing every tail contains but no singleton (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal), so a union of infinitely many sets can lie in 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.
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.
- UL is not a theorem of ZF. If ZF is consistent, ZF does not prove that a free ultrafilter on exists (Feferman 1965, by forcing: Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡), and UL produces one by extending the filter of tails, so ZF does not prove UL. This is external to this library exactly as the independence of the Axiom of Choice itself is (FALSE: Zorn's lemma is a theorem of ZF).
- UL does not imply the Axiom of Choice. If ZF is consistent, there is a model of ZF in which UL holds and the Axiom of Choice fails (Halpern and Lévy 1971: Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡). Together with the previous point this places UL strictly between the two, again under the consistency of ZF: it is not provable in ZF, and it is not strong enough to recover AC.
- UL is the Boolean prime ideal theorem. Over ZF, UL is equivalent to the statement that every nontrivial Boolean algebra has a prime ideal, equivalently an ultrafilter in the lattice sense. The dictionary is the one visible in Ultrafilters are prime: a union in has a member in : a maximal filter is a prime filter, and complements turn filters into ideals. The Boolean form is the name under which the principle is catalogued in the literature on weak choice principles.
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 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, once the ultrafilter lemma is available: every ultrafilter is principal
Statement
FALSE. For every set , every ultrafilter on (Ultrafilter) is principal: there is an with .
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 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 is principal.
Facts & Assumptions
Given: The natural numbers with , the successor and the order (The natural numbers (von Neumann), Order on the natural numbers), and the Axiom of Choice in the form used by the ultrafilter lemma.
A filter on contains , omits , and is closed under pairwise intersection and upward in ; 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 is , and it contains .
The upward closure of a filter base on is a filter on , and (The upward closure of a filter base is the smallest filter containing it).
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).
on is reflexive, transitive, antisymmetric and total ( is a linear order on ).
, and means with (Discreteness: is the immediate successor, Order on the natural numbers).
Refutation
For put , the tail at , and let .
because , and because by reflexivity.
is downward directed: given , totality gives say , and then transitivity gives , so the member of satisfies .
For every , : an element of the intersection equals and satisfies , which would give and hence .
is a filter base on , so is a filter on and every tail belongs to it.
By the ultrafilter lemma there is an ultrafilter on with ; in particular for every .
No singleton lies in : if then and both lie in , hence so does their intersection , which a filter omits.
The principal filter at contains , so is not the principal filter at any ; thus is an ultrafilter on that is not principal, and the claim is refuted.
Remarks
- What the refutation consumes. The ultrafilter 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 . A subset of 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 , whereas "cofinite" needs a theory of finite sets that this library has not yet developed. Nothing else changes.
- On a finite the claim is true, which is why the intuition survives: a finite is a finite union of its singletons, primeness (Ultrafilters are prime: a union in has a member in ) puts one singleton into , and upward closure then makes the principal filter at . 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 , read as a subset of , is Lebesgue measurable or has the Baire property (Sierpiński 1938: no free ultrafilter on 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
Standard references
Recommended treatments; not extraction sources.
- Filter (set theory) (Wikipedia)
- Filter (mathematics) (Wikipedia)
- N. Bourbaki, General Topology: Chapters 1-4, Ch. I §6
- B. Kaya, Ultrafilters and How to Use Them
- N. Strickland, Notes on Ultrafilters
- Finite intersection property (Wikipedia)
- Ultrafilter (Wikipedia)
- Ultrafilter (set theory) (Wikipedia)
- Zorn's lemma (Wikipedia)
- Ultrafilter lemma (Wikipedia)
- Boolean prime ideal theorem (Wikipedia)
- Axiom of choice (Wikipedia)
- The Axiom of Choice (Stanford Encyclopedia of Philosophy)
- Fréchet filter (Wikipedia)