Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-09-26 (gpt-6-sol)
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.

Ultrafilter

Definition

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

An ultrafilter is principal if it is of the form { A⊆X:x∈A } for some x∈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),⊆) would be a filter containing every filter, and as soon as X has two distinct points x≠y no such filter exists: it would contain the principal filters at x and at y, hence both {x} and {y}, hence their intersection ∅, which properness forbids (Filter on a set). So on such an X there is no greatest filter, and reading "maximal" as "greatest" is the error recorded in FALSE: every maximal element is a greatest element. Note what that argument does and does not deliver. It says nothing whatever about which filters are maximal, nor that any is: the absence of a greatest element is compatible with there being no maximal element at all. What does follow, from maximality itself and not from the argument above, is that two distinct ultrafilters are never comparable, since U⊆V with U maximal forces V=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 decides every subset by containing either A or its complement, is Characterisation of ultrafilters: every set or its complement, and it is the form used in practice.
  • Existence is free; the published extension theorem uses choice. On every nonempty set, the principal filter at any point is an ultrafilter, as the next bullet verifies directly. The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter proves from Zorn's lemma that every filter extends to an ultrafilter. Applied to the filter of tails on N, it produces a free ultrafilter under its stated hypotheses, as FALSE, once the ultrafilter lemma is available: every ultrafilter is principal verifies.
  • Principal ultrafilters really are ultrafilters: {A⊆X:x∈A} is a filter, and if a filter G contains it then any B∈G must meet {x}, since otherwise B∩{x}=∅ lies in G, so x∈B and G is contained in the principal filter at x. This is the one family of examples available without any choice principle.

Depends on

Dependency tree · 2 levels

Sources