TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Cantor normal form: every nonzero ordinal is $ω^{β_{0}} \cdot c_{0} + \dots + ω^{β_{k - 1}} \cdot c_{k - 1}$ with $β_{0} > \dots > β_{k - 1}$ and each $c_{i}$ a nonzero natural number, in exactly one way

Statement

Let $α$ be an ordinal (Ordinal (von Neumann)) with $α > 0$ . Then there is a natural number $k \geq 1$ , a strictly decreasing list of ordinals $β_{0} > β_{1} > \dots > β_{k - 1}$ and a list of natural numbers $c_{0}, \dots, c_{k - 1}$ with $0 < c_{i} < ω$ , such that

$α = ω^{β_{0}} \cdot c_{0} + ω^{β_{1}} \cdot c_{1} + \dots + ω^{β_{k - 1}} \cdot c_{k - 1},$

and $k$ , the exponents $β_{i}$ and the coefficients $c_{i}$ are uniquely determined by $α$ . This expression is the Cantor normal form of $α$ ; the uniqueness is what licenses the definite article.

Indices run over the von Neumann natural $k = {0, 1, \dots, k - 1}$ , so the leading term is the one with index $0$ . Sums are unbracketed because ordinal addition is associative (Ordinal addition is associative), and powers bind tighter than products, which bind tighter than sums (Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ ).

No choice principle is used.

Facts & Assumptions

Given: An ordinal $α > 0$ . A normal-form datum of length $k$ , for a natural number $k \geq 1$ , is a pair of functions $i \mapsto β_{i}$ and $i \mapsto c_{i}$ with domain the von Neumann natural $k$ (The natural numbers $N$ (von Neumann)), the $β_{i}$ ordinals with $β_{i} \in β_{j}$ whenever $j \in i$ , and the $c_{i}$ ordinals with $0 < c_{i} < ω$ . Its value is $S_{k}$ , where $S_{0} = 0$ and $S_{j^{+}} = S_{j} + ω^{β_{j}} \cdot c_{j}$ for $j \in k$ ; this recursion is legitimate by Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal, and by associativity of $+$ its value is the unbracketed sum displayed in the Statement.

[L1]

Exponent laws for a base $> 1$ , in particular for $ω$ : $β < γ$ implies $ω^{β} < ω^{γ}$ ; $β \leq ω^{β}$ ; $ω^{λ} = \sup {ω^{ξ} : ξ \in λ}$ is a limit ordinal for limit $λ$ ; $ω^{0} = 1$ , $ω^{1} = ω$ , $ω^{β} > 0$ , and $ω^{β + γ} = ω^{β} \cdot ω^{γ}$ ( $α^{β + γ} = α^{β} \cdot α^{γ}$ and $(α^{β})^{γ} = α^{β \cdot γ}$ ; and for $α > 1$ exponentiation is strictly increasing with $β \leq α^{β}$ , Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ ).

[L2]

For $μ > 0$ and any $ν$ there are unique $ξ, ρ$ with $ν = μ \cdot ξ + ρ$ and $ρ < μ$ (For $α > 0$ every ordinal $β$ is $α \cdot ξ + ρ$ with $ρ < α$ , in exactly one way).

[L3]

From Monotonicity of ordinal $+$ and $\cdot$ : strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities $0 + β = β$ and $1 \cdot β = β$ : $0 + μ = μ + 0 = μ$ , $1 \cdot μ = μ \cdot 1 = μ$ , $μ \cdot 0 = 0$ (claim (a)); $ν < θ$ implies $μ + ν < μ + θ$ , and $μ \leq μ + ν$ (claim (b)); $ν \leq μ + ν$ (claim (c)); for $μ > 0$ , $ν < θ$ implies $μ ν < μ θ$ (claim (d)); $μ \leq ν$ implies $μ θ \leq ν θ$ (claim (e)); if $θ$ is a limit and $D \subseteq θ$ is nonempty with $\sup D = θ$ then $μ + θ = \sup {μ + η : η \in D}$ (claim (f)); and $μ \cdot λ$ is a limit ordinal for $μ > 0$ and $λ$ a limit (claim (g)).

[L4]

$μ \cdot (ν + θ) = μ ν + μ θ$ , and $\cdot$ is associative (Ordinal multiplication is associative, and $α \cdot (β + γ) = α \cdot β + α \cdot γ$ ).

[L5]

$μ \cdot 0 = 0$ , $μ \cdot δ^{+} = μ \cdot δ + μ$ , $μ \cdot λ = \sup {μ \cdot ξ : ξ \in λ}$ (Ordinal multiplication $α \cdot β$ ); $μ + 0 = μ$ and $μ + δ^{+} = (μ + δ)^{+}$ (Ordinal addition $α + β$ ).

[L6]

$μ^{+}$ is an ordinal; $⋃ A$ is an ordinal and the least upper bound of a set $A$ of ordinals; $μ \subseteq ν$ iff $μ \in ν$ or $μ = ν$ ; $μ \notin μ$ (Basic closure properties of ordinals); hence $μ < ν$ iff $μ^{+} \leq ν$ . Exactly one of $μ \in ν$ , $μ = ν$ , $ν \in μ$ holds, and every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals).

[L7]

Every ordinal is exactly one of $0$ , a successor or a limit; a limit $λ$ has $0, 1 \in λ$ and is closed under successor (Successor and limit ordinals). $ω$ is a limit ordinal and every ordinal in $ω$ is $0$ or a successor (claims (iii) and (iv) of $ω$ is the least limit ordinal).

[L8]

Transfinite induction over the ordinals: if a property $P$ of ordinals fails at some $β_{0}$ , apply Transfinite induction to the well-order $(β_{0}^{+}, \in)$ and to $S = {ξ \in β_{0}^{+} : P (ξ)}$ ; so if $P$ holds at $ξ$ whenever it holds at every ordinal in $ξ$ , then $P$ holds at every ordinal.

Proof

technique · direct

1.1

Preliminaries on $ω$ and on powers of $ω$ : for $n, m \in ω$ one has $n + m \in ω$ , by induction on $m$ over the ordinals in $ω$ , since $n + 0 = n$ , since $n + m^{+} = (n + m)^{+} \in ω$ as $ω$ is closed under successor, and since no ordinal in $ω$ is a limit by [L7]; and $ω^{δ^{+}} = ω^{δ} \cdot ω = \sup {ω^{δ} \cdot n : n \in ω}$ is a limit ordinal, with $ω^{δ} \cdot n < ω^{δ^{+}}$ for every $n \in ω$ , by [L1], [L5] and claims (d) and (g) of [L3].

L1L3L5L7

2.1

Additive indecomposability: for every ordinal $β$ and every $μ < ω^{β}$ one has $μ + ω^{β} = ω^{β}$ . By induction on $β$ . At $β = 0$ , $ω^{0} = 1$ forces $μ = 0$ and $0 + 1 = 1$ . At $β = δ^{+}$ : $μ < ω^{δ^{+}} = \sup {ω^{δ} n : n \in ω}$ gives $n \in ω$ with $μ < ω^{δ} \cdot n$ , and claim (f) of [L3] applied to the nonempty $D = {ω^{δ} \cdot m : m \in ω} \subseteq ω^{δ^{+}}$ gives $μ + ω^{δ^{+}} = \sup {μ + ω^{δ} m : m \in ω}$ , where each $μ + ω^{δ} m \leq ω^{δ} n + ω^{δ} m = ω^{δ} (n + m) < ω^{δ^{+}}$ by [L4], step 1.1 and claim (d) of [L3]; so $μ + ω^{δ^{+}} \leq ω^{δ^{+}}$ , and the reverse inequality is claim (c) of [L3]. At $β = λ$ a limit: $μ < ω^{λ} = \sup {ω^{ξ} : ξ \in λ}$ gives $ξ_{0} \in λ$ with $μ < ω^{ξ_{0}}$ , and $D = {ω^{ξ} : ξ \in λ and ξ_{0} \leq ξ}$ is nonempty, contained in $ω^{λ}$ and has supremum $ω^{λ}$ , because any $η < ω^{λ}$ satisfies $η < ω^{ξ}$ for some $ξ \in λ$ and $ξ$ may be replaced by the larger of $ξ$ and $ξ_{0}$ ; so claim (f) of [L3] gives $μ + ω^{λ} = \sup {μ + ω^{ξ} : ξ_{0} \leq ξ \in λ} = \sup {ω^{ξ} : ξ_{0} \leq ξ \in λ} = ω^{λ}$ , using the claim at each such $ξ$ , legitimate since $μ < ω^{ξ_{0}} \leq ω^{ξ}$ .

step 1.1L1L3L4L5L6L7L8

2.2

The leading exponent exists: for $α > 0$ the set $B = {β \in α^{+} : ω^{β} \leq α}$ contains $0$ , because $ω^{0} = 1 \leq α$ , and it contains every $β$ with $ω^{β} \leq α$ , because $β \leq ω^{β} \leq α$ by [L1]; it has a greatest element $β_{0} = ⋃ B$ , since $⋃ B = 0$ forces $B = {0}$ and $0 \in B$ , since $⋃ B = δ^{+}$ gives $δ \in β$ for some $β \in B$ and hence $δ^{+} \leq β \leq ⋃ B = δ^{+}$ with $β \in B$ , and since $⋃ B = λ$ a limit gives $ω^{ξ} < ω^{β} \leq α$ for every $ξ \in λ$ , whence $ω^{λ} = \sup {ω^{ξ} : ξ \in λ} \leq α$ and $λ \in B$ ; and then $ω^{β_{0}} \leq α < ω^{β_{0}^{+}}$ , the second inequality because $β_{0}^{+} \notin B$ .

step 1.1L1L6L7

3.1

Closure below a power of $ω$ : if $μ < ω^{β}$ and $ν < ω^{β}$ then $μ + ν < μ + ω^{β} = ω^{β}$ , by claim (b) of [L3] and step 2.1.

step 2.1L3

3.2

Existence, by induction on $α > 0$ : take $β_{0}$ from step 2.2, so $ω^{β_{0}} \leq α < ω^{β_{0}^{+}} = ω^{β_{0}} \cdot ω$ ; divide by $ω^{β_{0}} > 0$ using [L2] to get $α = ω^{β_{0}} \cdot c_{0} + ρ$ with $ρ < ω^{β_{0}}$ ; here $c_{0} \neq 0$ , since $c_{0} = 0$ would give $α = ρ < ω^{β_{0}} \leq α$ , and $c_{0} < ω$ , since $ω \leq c_{0}$ would give $ω^{β_{0}} \cdot ω \leq ω^{β_{0}} c_{0} \leq α$ by claims (d) and (b) of [L3], contradicting $α < ω^{β_{0}} \cdot ω$ . If $ρ = 0$ then $α = ω^{β_{0}} c_{0}$ is a normal form of length $1$ . Otherwise $0 < ρ < ω^{β_{0}} \leq α$ , so the claim at $ρ$ gives a normal-form datum for $ρ$ with leading exponent $γ_{0}$ and leading coefficient $d_{0} \geq 1$ , and $ω^{γ_{0}} \leq ω^{γ_{0}} d_{0} \leq ρ < ω^{β_{0}}$ by [L3], so $γ_{0} < β_{0}$ by [L1] and [L6]; prefixing $(β_{0}, c_{0})$ to that datum therefore yields a normal-form datum whose value is $α$ .

step 2.2L1L2L3L6L8

4.1

Tail bound: if $(β_{i}, c_{i})_{i \in k}$ is a normal-form datum then the value $τ$ of its tail $(β_{i}, c_{i})_{1 \leq i < k}$ satisfies $τ < ω^{β_{0}}$ ; indeed $τ = 0 < ω^{β_{0}}$ when $k = 1$ , and for $i \geq 1$ each term satisfies $ω^{β_{i}} c_{i} < ω^{β_{i}} \cdot ω = ω^{β_{i}^{+}} \leq ω^{β_{0}}$ by claim (d) of [L3], [L1] and $β_{i}^{+} \leq β_{0}$ , so induction on the number of terms using step 3.1 gives $τ < ω^{β_{0}}$ .

step 3.1step 1.1L1L3L6L7L8

5.1

Uniqueness, by induction on $α > 0$ : let $(β_{i}, c_{i})_{i \in k}$ be a normal-form datum of value $α$ , with tail value $τ$ , so that $α = ω^{β_{0}} c_{0} + τ$ with $τ < ω^{β_{0}}$ by step 4.1; then $ω^{β_{0}} = ω^{β_{0}} \cdot 1 \leq ω^{β_{0}} c_{0} \leq α$ by [L3], and $α < ω^{β_{0}} c_{0} + ω^{β_{0}} = ω^{β_{0}} (c_{0} + 1) \leq ω^{β_{0}} \cdot ω = ω^{β_{0}^{+}}$ by [L3], [L4] and $c_{0} + 1 \leq ω$ ; so $ω^{β_{0}} \leq α < ω^{β_{0}^{+}}$ , which pins $β_{0}$ down, since a second datum with leading exponent $γ_{0} \neq β_{0}$ would satisfy the same two inequalities and, say, $β_{0} < γ_{0}$ would give $α < ω^{β_{0}^{+}} \leq ω^{γ_{0}} \leq α$ by [L1] and [L6]; with $β_{0}$ fixed, the two representations $α = ω^{β_{0}} c_{0} + τ = ω^{β_{0}} d_{0} + σ$ with $τ, σ < ω^{β_{0}}$ agree by the uniqueness in [L2], so $c_{0} = d_{0}$ and $τ = σ$ ; and $τ < ω^{β_{0}} \leq α$ , so the claim at $τ$ makes the two tails identical when $τ > 0$ , while $τ = 0$ forces both data to have length $1$ , since a tail of length at least $1$ has value at least $ω^{β_{1}} c_{1} > 0$ .

step 4.1step 2.2L1L2L3L4L6L8

6.1

Existence is step 3.2 and uniqueness is step 5.1, so every ordinal $α > 0$ has exactly one Cantor normal form.

step 5.1step 3.2∎

Remarks

Where each hypothesis of $α^{β + γ} = α^{β} \cdot α^{γ}$ and $(α^{β})^{γ} = α^{β \cdot γ}$ ; and for $α > 1$ exponentiation is strictly increasing with $β \leq α^{β}$ is spent. The bound $β \leq ω^{β}$ is what makes $B$ in step 2.2 a set: without it, "the largest $β$ with $ω^{β} \leq α$ " ranges over the ordinals, which is not a set, and Separation has nothing to cut. Continuity of $β \mapsto ω^{β}$ at limits is what makes $B$ attain its supremum; without it the maximum could fail to exist and the leading exponent would not be defined.

Additive indecomposability is the whole content of uniqueness. Step 2.1 says that adding anything strictly smaller than $ω^{β}$ on the left of $ω^{β}$ changes nothing. Its consequence, step 3.1, is that the ordinals below $ω^{β}$ are closed under addition, and that is exactly why a tail with strictly smaller exponents cannot reach up to the leading term and disturb it.

Beyond base $ω$ . More general base- $γ$ expansions exist for ordinals $γ > 1$ , with digits below $γ$ , but their proof requires a general digit-and-carry argument. The theorem and proof here concern only base $ω$ .

What is not claimed. Nothing here says the normal form is computable, and nothing here uses or proves anything about $ε_{0}$ . The ordinals $α$ with $α = ω^{α}$ have normal form $ω^{α} \cdot 1$ , whose exponent is $α$ itself, so the normal form does not always reduce a problem to strictly smaller data; one such ordinal, $ε_{0}$ , is exhibited on the companion examples page, where it is shown to satisfy $ω^{ε_{0}} = ε_{0}$ and where it is recorded that its leastness among such fixed points is not proved.

Depends on

Used by

Dependency tree · two levels

43 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

Ordinal arithmetic (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
A. Marks, Set Theory (standard reference, not scraped)

Cantor normal form: every nonzero ordinal is ωβ0⋅c0+⋯+ωβk−1⋅ck−1ωβ0​⋅c0​+⋯+ωβk−1​⋅ck−1​ with β0>⋯>βk−1β0​>⋯>βk−1​ and each cici​ a nonzero natural number, in exactly one way