TheoremStatement: AI-adaptedProof: 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.

$α^{β + γ} = α^{β} \cdot α^{γ}$ and $(α^{β})^{γ} = α^{β \cdot γ}$ ; and for $α > 1$ exponentiation is strictly increasing with $β \leq α^{β}$

Statement

Let $α$ , $β$ , $γ$ be ordinals (Ordinal (von Neumann)) and $λ$ a limit ordinal, with $\cdot$ and $α^{β}$ as in Ordinal multiplication $α \cdot β$ and Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ . Then:

(a) Base values. $α^{1} = α$ ; $1^{β} = 1$ ; $0^{β} = 0$ for every $β > 0$ ; $α^{β} > 0$ whenever $α > 0$ ; and $α^{β} > 1$ whenever $α > 1$ and $β > 0$ .

(b) Strictly increasing in the exponent, for $α > 1$ . $β < γ$ implies $α^{β} < α^{γ}$ .

(c) Continuity in the exponent, for $α > 1$ . $α^{λ} = \sup {α^{η} : η \in D}$ for every nonempty $D \subseteq λ$ with $\sup D = λ$ ; in particular $α^{λ} = \sup {α^{β} : β \in λ}$ , and $α^{λ}$ is a limit ordinal.

(d) The fixed-point bound, for $α > 1$ . $β \leq α^{β}$ for every ordinal $β$ .

(e) Sum law. $α^{β + γ} = α^{β} \cdot α^{γ}$ for all ordinals $α$ , $β$ , $γ$ .

(f) Product law. $(α^{β})^{γ} = α^{β \cdot γ}$ for all ordinals $α$ , $β$ , $γ$ .

Clause (d) is what makes "the largest $β$ with $ω^{β} \leq α$ " a legitimate object when the Cantor normal form is extracted later on this page: it bounds the candidates by $α$ itself, and clause (c) is what makes the collection of candidates attain its supremum.

No choice principle is used. Note that the law $(α \cdot β)^{γ} = α^{γ} \cdot β^{γ}$ is not claimed and is not true; the Remarks below compute a witness at $α = ω$ , $β = γ = 2$ .

Facts & Assumptions

Given: Ordinals $α$ , $β$ , $γ$ and a limit ordinal $λ$ . For a set $A$ of ordinals, $\sup A = ⋃ A$ is its least upper bound (Basic closure properties of ordinals, claim (e)).

[L1]

$α^{0} = 1$ , $α^{δ^{+}} = α^{δ} \cdot α$ , and $α^{λ} = \sup {α^{β} : 0 < β < λ}$ for limit $λ$ (Ordinal exponentiation $α^{β}$ , with the conventions $α^{0} = 1$ and $0^{0} = 1$ ).

[L2]

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

[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 β = β$ : $1 \cdot μ = μ \cdot 1 = μ$ , $μ \cdot 0 = 0 \cdot μ = 0$ and $0 + μ = μ + 0 = μ$ (claim (a)); for $μ > 0$ , $ν < θ$ implies $μ ν < μ θ$ , and $μ ν = 0$ exactly when $μ = 0$ or $ν = 0$ (claim (d)); if $θ$ is a limit and $D \subseteq θ$ is nonempty with $\sup D = θ$ , then $μ \cdot θ = \sup {μ η : η \in D}$ for $μ > 0$ (claim (f)); and $μ + λ$ , and $μ \cdot λ$ for $μ > 0$ , are limit ordinals (claim (g)).

[L4]

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

[L5]

$μ^{+}$ is an ordinal, $μ \subseteq ν$ if and only if $μ \in ν$ or $μ = ν$ , and $μ \notin μ$ (claims (b), (c), (f) of Basic closure properties of ordinals); consequently $μ < ν$ if and only if $μ^{+} \leq ν$ ; and exactly one of $μ \in ν$ , $μ = ν$ , $ν \in μ$ holds (Trichotomy and well-ordering of the ordinals).

[L6]

Every ordinal is exactly one of $0$ , a successor, or a limit; a limit $λ$ satisfies $0 \in λ$ , $1 \in λ$ and $ξ \in λ \Rightarrow ξ^{+} \in λ$ (Successor and limit ordinals, Basic closure properties of ordinals).

[L7]

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 (ξ)}$ ; since every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals), if $P$ holds at $ξ$ whenever it holds at every ordinal in $ξ$ , then $P$ holds at every ordinal.

Proof

technique · direct

1.1

$α^{1} = α^{0^{+}} = α^{0} \cdot α = 1 \cdot α = α$ .

L1L3

1.2

$1^{β} = 1$ for every $β$ , by induction: $1^{0} = 1$ ; $1^{δ^{+}} = 1^{δ} \cdot 1 = 1 \cdot 1 = 1$ ; and at a limit $λ$ the set ${1^{β} : 0 < β < λ}$ is ${1}$ , nonempty because $1 \in λ$ , so its supremum is $⋃ {1} = 1$ .

L1L3L6L7

1.3

$0^{β} = 0$ for every $β > 0$ , by induction: at a successor $δ^{+}$ this needs no hypothesis, since $0^{δ^{+}} = 0^{δ} \cdot 0 = 0$ by [L3]; and at a limit $λ$ every $β$ with $0 < β < λ$ has $0^{β} = 0$ , so $0^{λ} = ⋃ {0} = 0$ , the set being nonempty because $1 \in λ$ .

L1L3L6L7

2.1

$α^{β} > 0$ for every $β$ , whenever $α > 0$ , by induction: $α^{0} = 1 > 0$ ; $α^{δ^{+}} = α^{δ} \cdot α > 0$ by [L3] since both factors are positive; and at a limit $λ$ , $α^{1} = α$ belongs to the set whose supremum is $α^{λ}$ , because $1 \in λ$ and $1 \neq 0$ , so $α^{λ} \geq α > 0$ .

step 1.1L1L3L5L6L7

3.1

Clause (b): let $α > 1$ ; by induction on $γ$ , every $β \in γ$ satisfies $α^{β} \in α^{γ}$ . At $γ = 0$ there is nothing to prove. At $γ = δ^{+}$ , $β \leq δ$ gives $α^{β} \leq α^{δ}$ using the claim at $δ$ , and $α^{δ} = α^{δ} \cdot 1 < α^{δ} \cdot α = α^{δ^{+}}$ by [L3], since $α^{δ} > 0$ by step 2.1 and $1 < α$ . At $γ = λ$ a limit: if $β = 0$ then $α^{0} = 1 < α = α^{1} \leq α^{λ}$ , because $1 \in λ$ puts $α^{1}$ in the set whose supremum is $α^{λ}$ ; and if $β > 0$ then $β^{+} \in λ$ with $β^{+} \neq 0$ , so $α^{β} < α^{β^{+}} \leq α^{λ}$ by the successor computation just made.

step 1.1step 2.1L1L3L5L6L7

4.1

Clause (c): let $α > 1$ . Including the term at $β = 0$ does not change the supremum in [L1], since $α^{0} = 1 \leq α^{1}$ and $1 \in λ$ , so $α^{λ} = \sup {α^{β} : β \in λ}$ . If $D \subseteq λ$ is nonempty with $\sup D = λ$ , then ${α^{η} : η \in D}$ is a subset of that set, giving $\leq$ ; conversely each $β \in λ = ⋃ D$ lies in some $η \in D$ , so $α^{β} < α^{η}$ by step 3.1, giving $\geq$ .

step 3.1step 1.1L1L5L6

4.2

The second half of clause (c): for $α > 1$ and $λ$ a limit, $α^{λ} \neq 0$ by step 2.1, and $α^{λ}$ is not a successor, since $α^{λ} = μ^{+}$ would put $μ$ in $α^{β}$ for some $β$ with $0 < β < λ$ , whence $μ^{+} \leq α^{β} < α^{β^{+}} \leq α^{λ} = μ^{+}$ by step 3.1 and [L6], which [L5] forbids; so $α^{λ}$ is a limit ordinal.

step 3.1step 2.1L1L5L6

4.3

Clause (d): let $α > 1$ ; by induction on $β$ . At $β = 0$ , $0 \leq 1 = α^{0}$ . At $β = δ^{+}$ , $δ \leq α^{δ} < α^{δ^{+}}$ by step 3.1, so $δ < α^{δ^{+}}$ and hence $δ^{+} \leq α^{δ^{+}}$ by [L5]. At $β = λ$ a limit, every $ξ \in λ$ satisfies $ξ \leq α^{ξ} < α^{λ}$ by step 3.1, so $ξ \in α^{λ}$ , giving $λ \subseteq α^{λ}$ .

step 3.1L1L5L6L7

4.4

The last part of clause (a): for $α > 1$ and $β > 0$ , step 3.1 applied to $0 \in β$ gives $1 = α^{0} < α^{β}$ .

step 3.1L1

5.1

Clause (e), by induction on $γ$ . At $γ = 0$ : $α^{β + 0} = α^{β} = α^{β} \cdot 1 = α^{β} \cdot α^{0}$ . At $γ = δ^{+}$ , assuming the claim at $δ$ : $α^{β + δ^{+}} = α^{(β + δ)^{+}} = α^{β + δ} \cdot α = (α^{β} \cdot α^{δ}) \cdot α = α^{β} \cdot (α^{δ} \cdot α) = α^{β} \cdot α^{δ^{+}}$ , the fourth equality by [L4]. At $γ = λ$ a limit there are three cases. If $α = 0$ then $β + λ$ is a limit and so nonzero, giving $0^{β + λ} = 0$ by step 1.3, while $0^{β} \cdot 0^{λ} = 0^{β} \cdot 0 = 0$ by step 1.3 and [L3]. If $α = 1$ both sides are $1$ by step 1.2 and [L3]. If $α > 1$ then $D = {β + ξ : ξ \in λ}$ is a nonempty subset of the limit ordinal $β + λ$ with supremum $β + λ$ by [L2] and [L3], so step 4.1 gives $α^{β + λ} = \sup {α^{β + ξ} : ξ \in λ} = \sup {α^{β} \cdot α^{ξ} : ξ \in λ}$ by the claim at each $ξ$ ; and $E = {α^{ξ} : ξ \in λ}$ is a nonempty subset of the limit ordinal $α^{λ}$ with supremum $α^{λ}$ by steps 2.1, 3.1 and 4.2, so [L3] with $α^{β} > 0$ gives $α^{β} \cdot α^{λ} = \sup {α^{β} \cdot α^{ξ} : ξ \in λ}$ ; the two suprema are of the same set.

step 4.1step 4.2step 3.1step 1.2step 1.3step 2.1L1L2L3L4L6L7

6.1

Clause (f), by induction on $γ$ . At $γ = 0$ : $(α^{β})^{0} = 1 = α^{0} = α^{β \cdot 0}$ by [L1] and [L3]. At $γ = δ^{+}$ , assuming the claim at $δ$ : $(α^{β})^{δ^{+}} = (α^{β})^{δ} \cdot α^{β} = α^{β δ} \cdot α^{β} = α^{β δ + β} = α^{β \cdot δ^{+}}$ , the third equality by step 5.1 and the fourth by [L2]. At $γ = λ$ a limit there are four cases. If $β = 0$ then both sides are $1$ , by step 1.2 and [L1] and [L3]. If $β > 0$ and $α = 0$ then the left side is $0^{λ} = 0$ by step 1.3 applied twice, while $β \cdot λ$ is a limit by [L3] and so nonzero, making the right side $0$ as well. If $β > 0$ and $α = 1$ both sides are $1$ by step 1.2. If $β > 0$ and $α > 1$ then $α^{β} > 1$ by step 4.4, so step 4.1 applied with base $α^{β}$ gives $(α^{β})^{λ} = \sup {(α^{β})^{ξ} : ξ \in λ} = \sup {α^{β ξ} : ξ \in λ}$ by the claim at each $ξ$ ; and $D = {β ξ : ξ \in λ}$ is a nonempty subset of the limit ordinal $β \cdot λ$ with supremum $β \cdot λ$ by [L2] and [L3], so step 4.1 applied with base $α$ gives $α^{β \cdot λ} = \sup {α^{β ξ} : ξ \in λ}$ ; the two suprema are of the same set.

step 5.1step 4.4step 4.1step 1.2step 1.3L1L2L3L6L7

7.1

Clauses (a) to (f) are established.

step 6.1step 5.1step 4.1step 4.2step 4.3step 4.4step 3.1step 1.1step 1.2step 1.3step 2.1∎

Remarks

What clause (d) is for, and why it is not a fixed-point theorem. $β \leq α^{β}$ says only that the exponential never falls below the identity. It does not say that $β = α^{β}$ has a solution; that it does is a separate matter, exhibited by hand at $ε_{0}$ on the companion examples page and proved there from clause (c), not from any general fixed-point theory. The inequality is used in 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 to bound the exponents that can occur, which is what turns "the largest $β$ with $ω^{β} \leq α$ " into a search over a set.

The law that is false, computed. $(α \cdot β)^{γ} = α^{γ} \cdot β^{γ}$ fails at $α = ω$ , $β = γ = 2$ . On one side, clause (f) is not available, so compute directly: $(ω \cdot 2)^{2} = (ω \cdot 2) \cdot (ω \cdot 2) = ((ω \cdot 2) \cdot ω) \cdot 2$ by associativity of $\cdot$ , and $(ω \cdot 2) \cdot ω = \sup {(ω \cdot 2) \cdot n : n \in ω} = \sup {ω \cdot (2 \cdot n) : n \in ω} = ω \cdot ω = ω^{2}$ , the last step because ${2 \cdot n : n \in ω}$ is unbounded in $ω$ and $\cdot$ is continuous on the right (claim (f) of 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 β = β$ ); so $(ω \cdot 2)^{2} = ω^{2} \cdot 2$ . On the other side $ω^{2} \cdot 2^{2} = ω^{2} \cdot 4$ , and $ω^{2} \cdot 2 \neq ω^{2} \cdot 4$ by left cancellation for $\cdot$ . The failure is the exponential shadow of the failure of commutativity, and it is the reason clause (f) is stated with the exponent, not the base, distributing.

The three degenerate bases. $α = 0$ and $α = 1$ have to be separated in every limit case, because clause (c) needs $α > 1$ : at $α = 1$ the function is constant and at $α = 0$ it is eventually constant, so neither is strictly increasing and neither has a limit ordinal as its value at a limit. Skipping those cases is the standard way to produce a proof that is wrong exactly at $α \leq 1$ .

Depends on

Used by

Dependency tree · two levels

21 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)
R. Moosa, Set Theory course notes (standard reference, not scraped)

αβ+γ=αβ⋅αγαβ+γ=αβ⋅αγ and (αβ)γ=αβ⋅γ(αβ)γ=αβ⋅γ; and for α>1α>1 exponentiation is strictly increasing with β≤αββ≤αβ