Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

ω2, ωω, and ε0=sup⁡{ω,ωω,ωωω,… } satisfying ωε0=ε0

Example

The first few powers of ω are

ω1=ω,ω2=ω⋅ω,ωω=sup⁡{ ωn:0<n<ω },

and each is strictly larger than the one before (αβ+γ=αβ⋅αγ and (αβ)γ=αβ⋅γ; and for α>1 exponentiation is strictly increasing with β≤αβ, clause (b)). Iterating the exponential produces the ω-tower

t0=ω,tn+1=ωtn,

so t1=ωω, t2=ωωω, and so on. Its supremum

ε0  :=  sup⁡{ tn:n∈ω }

is a limit ordinal satisfying

ωε0=ε0,

so it is a fixed point of β↦ωβ. This is exhibited here by hand: the tower is written down, its supremum is taken, and the fixed point equation is proved from continuity at limits. No fixed-point theorem is used, and none that this library proves applies here: every fixed-point theorem on disk is stated for a set carrying an order or a metric, whereas β↦ωβ is a class operation on the ordinals, which are not a set.

Facts & Assumptions

[L1]

α0=1, αδ+=αδ⋅α, and αλ=sup⁡{αβ:0<β<λ} for limit λ (Ordinal exponentiation αβ, with the conventions α0=1 and 00=1).

[L2]

For α>1: β<γ implies αβ<αγ; and αλ=sup⁡{αη:η∈D} for every nonempty D⊆λ with sup⁡D=λ (claims (b) and (c) of αβ+γ=αβ⋅αγ and (αβ)γ=αβ⋅γ; and for α>1 exponentiation is strictly increasing with β≤αβ). Also α1=α (claim (a) of the same).

[L3]

Recursion along the ordinals: a class rule defined on functions with ordinal domain determines exactly one class function on the ordinals (Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal).

[L4]

⋃A is an ordinal and the least upper bound of a set A of ordinals; μ⊆ν iff μ∈ν or μ=ν; μ∉μ; and μ<ν iff μ+≤ν (Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals, Ordinal (von Neumann)).

[L5]

ω is a limit ordinal, closed under successor, with 1∈ω, and every ordinal in ω is 0 or a successor (ω is the least limit ordinal, Successor and limit ordinals); every ordinal is exactly one of 0, a successor, or a limit (Successor and limit ordinals).

[L7]

Induction on N: a subset of N containing 0 and closed under σ equals N, and σ(n)=n+ (The principle of mathematical induction, The natural numbers N (von Neumann)).

Verification

technique · direct
1.1

ω1=ω by [L2]; ω2=ω1+=ω1⋅ω=ω⋅ω by [L1]; and ω<ωω, since 1<ω gives ω=ω1<ωω by [L2] with base ω>1.

L1L2L5L6
1.2

Define a class function G on functions h with ordinal domain β by G(h)=ω if β=0, G(h)=ωh(δ) if β=δ+, and G(h)=0 if β is a limit; the three cases are exhaustive and exclusive by [L5], so [L3] gives a unique class function F on the ordinals with F(0)=ω and F(δ+)=ωF(δ). Write tn=F(n) for n∈ω; then t0=ω, tn+=ωtn, and T={tn:n∈ω} is a set by Replacement.

L3L5construct
2.1

tn<tn+ for every n∈ω: let S={n∈ω:tn<tn+}; then 0∈S, because t0=ω<ωω=t0+ by step 1.1 and step 1.2; and n∈S implies σ(n)=n+∈S, because applying [L2] with base ω>1 to tn<tn+ gives ωtn<ωtn+, that is tn+<t(n+)+; so S=ω by [L7].

step 1.1step 1.2L2L7
3.1

ε0:=⋃T is an ordinal by [L4]; each tn satisfies tn<tn+⊆ε0 by step 2.1 and [L4], so T⊆ε0 and T is nonempty with sup⁡T=ε0; ε0≠0 because t0=ω∈ε0; and ε0 is not a successor, since ε0=μ+ would put μ∈tn for some n, whence μ+≤tn<tn+≤ε0=μ+ by [L4], which [L4] forbids; so ε0 is a limit ordinal by [L5].

step 2.1step 1.2L4L5
4.1

ωε0=ε0: by [L2] with base ω>1 applied to the nonempty D=T⊆ε0 with sup⁡T=ε0, one gets ωε0=sup⁡{ωtn:n∈ω}=sup⁡{tn+:n∈ω} by step 1.2; and that supremum is ε0, because each tn+⊆ε0 while conversely tn⊆tn+ for every n by step 2.1 and [L4], so the union over the shifted family contains ⋃T=ε0.

step 3.1step 2.1step 1.2L2L4
5.1

So ω2=ω⋅ω, the tower t0=ω, tn+=ωtn is strictly increasing, and its supremum ε0 is a limit ordinal with ωε0=ε0.

step 4.1step 3.1step 2.1step 1.1∎

Remarks

Why Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal and not the recursion theorem over N. The published The recursion theorem builds g:N→A from a function f:A→A on a set A. Here the step is β↦ωβ, a class operation with no set-sized codomain available at this point, so the recursion theorem does not apply as stated. Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal is exactly the class-valued version, and Replacement then makes the range {tn:n∈ω} a set.

What is proved and what is not. That ε0 is a fixed point of β↦ωβ is proved above. That it is the least such fixed point is true and is not proved here; it would follow from the observation that any fixed point is closed under the tower, and it needs nothing new, but nothing on these pages uses it. No general theory of normal functions or of the Veblen hierarchy is developed, and none is needed for the statement above.

ε0 and the Cantor normal form. By Cantor normal form: every nonzero ordinal is ωβ0⋅c0+⋯+ωβk−1⋅ck−1 with β0>⋯>βk−1 and each ci a nonzero natural number, in exactly one way every nonzero ordinal has a unique base-ω normal form. For ε0 that form is ωε0⋅1, whose exponent is ε0 itself, so the normal form does not reduce ε0 to strictly smaller data. Below ε0 it always does, and that is the sense in which ε0 is where base-ω notation runs out.

Cardinality is a separate question, and this page does not settle it. Nothing above says how large ωω or ε0 is as a set. Showing them at most countable would need the countable ordinals to be closed under ordinal exponentiation, which is not proved anywhere in this library; the natural route runs through Assuming countable choice: every at most countable subset of ω1 is bounded below ω1, so no at most countable subset of ω1 is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable and a transfinite induction that no item here carries out. What the tower demonstrates is growth in order type, which is the invariant this page is about.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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