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

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.

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

Statement

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

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

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

Facts & Assumptions

Given: The natural numbers $N$ with $0$ , the successor $σ$ and the order $\leq$ (The natural numbers $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 $X$ contains $X$ , omits $\emptyset$ , and is closed under pairwise intersection and upward in $X$ ; 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 $x$ is ${A \subseteq X : x \in A}$ , and it contains ${x}$ .

[L1]

The upward closure $⟨ B ⟩$ of a filter base $B$ on $X$ is a filter on $X$ , and $B \subseteq ⟨ B ⟩$ (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$ is reflexive, transitive, antisymmetric and total ( $\leq$ is a linear order on $N$ ).

[L4]

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

Refutation

technique · direct

1.1

For $N \in N$ put $T_{N} = {n \in N : N \leq n}$ , the tail at $N$ , and let $B = {T_{N} : N \in N}$ .

construct

2.1

$B \neq \emptyset$ because $T_{0} \in B$ , and $\emptyset \notin B$ because $N \in T_{N}$ by reflexivity.

step 1.1L3

2.2

$B$ is downward directed: given $M, N$ , totality gives say $M \leq N$ , and then transitivity gives $T_{N} \subseteq T_{M}$ , so the member $T_{N}$ of $B$ satisfies $T_{N} \subseteq T_{M} \cap T_{N}$ .

step 1.1L3

2.3

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

step 1.1L4

3.1

$B$ is a filter base on $N$ , so $F = ⟨ B ⟩$ is a filter on $N$ and every tail $T_{N}$ belongs to it.

step 2.1step 2.2A1L1

4.1

By the ultrafilter lemma there is an ultrafilter $U$ on $N$ with $F \subseteq U$ ; in particular $T_{N} \in U$ for every $N \in N$ .

step 3.1L2

5.1

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

step 4.1step 2.3A1L2

6.1

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

step 5.1A1∎

Remarks

What the refutation consumes. The ultrafilter $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 The proved choice cost of the ultrafilter lemma. 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$ . A subset of $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$ , whereas "cofinite" needs a theory of finite sets that this library has not yet developed. Nothing else changes.
On a finite $X$ the claim is true, which is why the intuition survives: a finite $X$ is a finite union of its singletons, primeness (Ultrafilters are prime: a union in $U$ has a member in $U$ ) puts one singleton ${x}$ into $U$ , and upward closure then makes $U$ the principal filter at $x$ . 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$ , read as a subset of ${0, 1}^{N}$ , is Lebesgue measurable or has the Baire property (Sierpiński 1938: no free ultrafilter on $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).

Depends on

Used by

On finite sets the ultrafilter monad is naturally isomorphic to the identity; assuming the ultrafilter lemma, its unit is not invertible on the natural numbers Example

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ultrafilter (set theory) (Wikipedia) (standard reference, not scraped)
Fréchet filter (Wikipedia) (standard reference, not scraped)
The Axiom of Choice (Stanford Encyclopedia of Philosophy) (standard reference, not scraped)
Ultrafilter (Wikipedia) (standard reference, not scraped)