Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (claude-sonnet-5 + deepseek-v4-pro)verified 2026-08-05 (claude-sonnet-5)
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.

Cofinality cf⁡(α), and regular and singular cardinals

Definition

Let α be an ordinal (Ordinal (von Neumann)). The cofinality of α is

cf⁡(α)  :=  the least ordinal β for which some f:β→α has cofinal range,

cofinal range meaning that f[β] is a cofinal subset of α (Cofinal subset of an ordinal): every ζ∈α satisfies ζ≤f(ξ) for some ξ∈β. That such a least ordinal exists, and that a witnessing map of that length may be taken strictly increasing, is For every ordinal α there is a least ordinal β admitting a map β→α with cofinal range, and that map may always be taken strictly increasing, and both are theorems of ZF. So cf⁡ is defined at every ordinal, without any choice principle.

Regular and singular. An infinite cardinal κ — a cardinal (Cardinal (initial ordinal) and cardinality) with ω⊆κ (Cardinal sum κ⊕λ, product κ⊗λ and exponentiation κλ, and why they are written apart from the ordinal operations), for instance any ℵα (The successor cardinal κ+, the alephs ℵα, the beths ℶα, successor and limit cardinals, and the identifications ℵ0=ω and ℵ1=ω1) — is

  • regular when cf⁡(κ)=κ;
  • singular when cf⁡(κ)≠κ.

The two cases are exhaustive by definition, and by cf⁡(α)≤α; cf⁡(0)=0 and cf⁡(α+1)=1; for a limit ordinal λ the value cf⁡(λ) is an infinite cardinal with cf⁡(cf⁡(λ))=cf⁡(λ), so it is regular; and every cofinal subset of λ has cardinality at least cf⁡(λ), a value that is attained ↗ singular means exactly cf⁡(κ)<κ, since cf⁡(α)≤α always holds.

Remarks

Why regularity is defined for cardinals and not for ordinals. The definition of cf⁡ applies to every ordinal, and it must, because the construction quantifies over maps into α of every length. But cf⁡(α)=α is an uninteresting condition on a general ordinal: it fails at ω+1 and at ω⋅2 for reasons that have nothing to do with size, and it holds only at 0, at 1, and at infinite cardinals, where it is exactly the regularity defined above and so fails at every singular one. Calling an ordinal regular would therefore say nothing new, which is why the words are attached to cardinals here.

What a singular cardinal is, in one sentence. A cardinal that is reachable from below by fewer than κ steps: there is a strictly increasing family of ordinals below κ, indexed by an ordinal strictly shorter than κ, whose supremum is κ. That is exactly the failure of regularity, and ℵ0 is regular in ZF; assuming the Axiom of Choice every successor aleph ℵα+1 is regular; cf⁡(ℵω)=ℵ0, so ℵω is singular, and under choice it is the least singular infinite cardinal exhibits a cardinal for which it happens.

Why cf⁡(κ) being a regular cardinal is a theorem and not part of the definition. Regularity is defined through cf⁡, so building "cf⁡(κ) is regular" into the definition would make the definition refer to itself. The statement is true, and it is cf⁡(α)≤α; cf⁡(0)=0 and cf⁡(α+1)=1; for a limit ordinal λ the value cf⁡(λ) is an infinite cardinal with cf⁡(cf⁡(λ))=cf⁡(λ), so it is regular; and every cofinal subset of λ has cardinality at least cf⁡(λ), a value that is attained ↗; it is recorded here as the item that discharges the naming obligation of this definition, and nothing above depends on it.

Only one notion of "cofinal" exists in this library. Cofinal subset of an ordinal introduces cofinal subsets, because the boundedness theorem for ω1 needs them, and deliberately introduces neither the cofinality function nor the regular/singular vocabulary. Both are introduced here, and the definition above is written in exactly that item's terms, so no second notion is created.

Depends on

Used by

Dependency tree · two levels

34 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