Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

αβ+γ=αβ⋅αγ\alpha^{\beta+\gamma} = \alpha^{\beta}\cdot\alpha^{\gamma} and (αβ)γ=αβ⋅γ(\alpha^{\beta})^{\gamma} = \alpha^{\beta\cdot\gamma}; and for α>1\alpha > 1 exponentiation is strictly increasing with β≤αβ\beta \le \alpha^{\beta}

Statement

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

(a) Base values. α1=α\alpha^{1} = \alpha; 1β=11^{\beta} = 1; 0β=00^{\beta} = 0 for every β>0\beta > 0; αβ>0\alpha^{\beta} > 0 whenever α>0\alpha > 0; and αβ>1\alpha^{\beta} > 1 whenever α>1\alpha > 1 and β>0\beta > 0.

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

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

(d) The fixed-point bound, for α>1\alpha > 1. β≤αβ\beta \le \alpha^{\beta} for every ordinal β\beta.

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

(f) Product law. (αβ)γ=αβ⋅γ(\alpha^{\beta})^{\gamma} = \alpha^{\beta \cdot \gamma} for all ordinals α\alpha, β\beta, γ\gamma.

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

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

Facts & Assumptions

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

[L1]

α0=1\alpha^{0} = 1, αδ+=αδ⋅α\alpha^{\delta^{+}} = \alpha^{\delta} \cdot \alpha, and αλ=sup⁡{αβ:0<β<λ}\alpha^{\lambda} = \sup\{\alpha^{\beta} : 0 < \beta < \lambda\} for limit λ\lambda (Ordinal exponentiation αβ\alpha^{\beta}, with the conventions α0=1\alpha^{0} = 1 and 00=10^{0} = 1).

[L2]

α⋅0=0\alpha \cdot 0 = 0, α⋅δ+=α⋅δ+α\alpha \cdot \delta^{+} = \alpha \cdot \delta + \alpha, and α⋅λ=sup⁡{α⋅ξ:ξ∈λ}\alpha \cdot \lambda = \sup\{\alpha \cdot \xi : \xi \in \lambda\} for limit λ\lambda (Ordinal multiplication α⋅β\alpha \cdot \beta); α+0=α\alpha + 0 = \alpha, α+δ+=(α+δ)+\alpha + \delta^{+} = (\alpha + \delta)^{+}, and α+λ=sup⁡{α+ξ:ξ∈λ}\alpha + \lambda = \sup\{\alpha + \xi : \xi \in \lambda\} (Ordinal addition α+β\alpha + \beta).

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

[L4]

Ordinal multiplication is associative and μ(ν+θ)=μν+μθ\mu(\nu + \theta) = \mu\nu + \mu\theta (Ordinal multiplication is associative, and α⋅(β+γ)=α⋅β+α⋅γ\alpha \cdot (\beta + \gamma) = \alpha\cdot\beta + \alpha\cdot\gamma).

[L5]

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

[L6]

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

[L7]

Transfinite induction over the ordinals: if a property PP of ordinals fails at some β0\beta_0, apply Transfinite induction to the well-order (β0+,∈)(\beta_0^{+}, \in) and to S={ξ∈β0+:P(ξ)}S = \{\xi \in \beta_0^{+} : P(\xi)\}; since every nonempty set of ordinals has an ∈\in-least element (Trichotomy and well-ordering of the ordinals), if PP holds at ξ\xi whenever it holds at every ordinal in ξ\xi, then PP holds at every ordinal.

Proof

technique · direct
1.1

α1=α0+=α0⋅α=1⋅α=α\alpha^{1} = \alpha^{0^{+}} = \alpha^{0} \cdot \alpha = 1 \cdot \alpha = \alpha.

L1L3
1.2

1β=11^{\beta} = 1 for every β\beta, by induction: 10=11^{0} = 1; 1δ+=1δ⋅1=1⋅1=11^{\delta^{+}} = 1^{\delta} \cdot 1 = 1 \cdot 1 = 1; and at a limit λ\lambda the set {1β:0<β<λ}\{1^{\beta} : 0 < \beta < \lambda\} is {1}\{1\}, nonempty because 1∈λ1 \in \lambda, so its supremum is ⋃{1}=1\bigcup\{1\} = 1.

L1L3L6L7
1.3

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

L1L3L6L7
2.1

αβ>0\alpha^{\beta} > 0 for every β\beta, whenever α>0\alpha > 0, by induction: α0=1>0\alpha^{0} = 1 > 0; αδ+=αδ⋅α>0\alpha^{\delta^{+}} = \alpha^{\delta} \cdot \alpha > 0 by [L3] since both factors are positive; and at a limit λ\lambda, α1=α\alpha^{1} = \alpha belongs to the set whose supremum is αλ\alpha^{\lambda}, because 1∈λ1 \in \lambda and 1≠01 \ne 0, so αλ≥α>0\alpha^{\lambda} \ge \alpha > 0.

step 1.1L1L3L5L6L7
3.1

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

step 1.1step 2.1L1L3L5L6L7
4.1

Clause (c): let α>1\alpha > 1. Including the term at β=0\beta = 0 does not change the supremum in [L1], since α0=1≤α1\alpha^{0} = 1 \le \alpha^{1} and 1∈λ1 \in \lambda, so αλ=sup⁡{αβ:β∈λ}\alpha^{\lambda} = \sup\{\alpha^{\beta} : \beta \in \lambda\}. If D⊆λD \subseteq \lambda is nonempty with sup⁡D=λ\sup D = \lambda, then {αη:η∈D}\{\alpha^{\eta} : \eta \in D\} is a subset of that set, giving ≤\le; conversely each β∈λ=⋃D\beta \in \lambda = \bigcup D lies in some η∈D\eta \in D, so αβ<αη\alpha^{\beta} < \alpha^{\eta} by step 3.1, giving ≥\ge.

step 3.1step 1.1L1L5L6
4.2

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

step 3.1step 2.1L1L5L6
4.3

Clause (d): let α>1\alpha > 1; by induction on β\beta. At β=0\beta = 0, 0≤1=α00 \le 1 = \alpha^{0}. At β=δ+\beta = \delta^{+}, δ≤αδ<αδ+\delta \le \alpha^{\delta} < \alpha^{\delta^{+}} by step 3.1, so δ<αδ+\delta < \alpha^{\delta^{+}} and hence δ+≤αδ+\delta^{+} \le \alpha^{\delta^{+}} by [L5]. At β=λ\beta = \lambda a limit, every ξ∈λ\xi \in \lambda satisfies ξ≤αξ<αλ\xi \le \alpha^{\xi} < \alpha^{\lambda} by step 3.1, so ξ∈αλ\xi \in \alpha^{\lambda}, giving λ⊆αλ\lambda \subseteq \alpha^{\lambda}.

step 3.1L1L5L6L7
4.4

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

step 3.1L1
5.1

Clause (e), by induction on γ\gamma. At γ=0\gamma = 0: αβ+0=αβ=αβ⋅1=αβ⋅α0\alpha^{\beta + 0} = \alpha^{\beta} = \alpha^{\beta} \cdot 1 = \alpha^{\beta} \cdot \alpha^{0}. At γ=δ+\gamma = \delta^{+}, assuming the claim at δ\delta: αβ+δ+=α(β+δ)+=αβ+δ⋅α=(αβ⋅αδ)⋅α=αβ⋅(αδ⋅α)=αβ⋅αδ+\alpha^{\beta + \delta^{+}} = \alpha^{(\beta + \delta)^{+}} = \alpha^{\beta + \delta} \cdot \alpha = (\alpha^{\beta} \cdot \alpha^{\delta}) \cdot \alpha = \alpha^{\beta} \cdot (\alpha^{\delta} \cdot \alpha) = \alpha^{\beta} \cdot \alpha^{\delta^{+}}, the fourth equality by [L4]. At γ=λ\gamma = \lambda a limit there are three cases. If α=0\alpha = 0 then β+λ\beta + \lambda is a limit and so nonzero, giving 0β+λ=00^{\beta + \lambda} = 0 by step 1.3, while 0β⋅0λ=0β⋅0=00^{\beta} \cdot 0^{\lambda} = 0^{\beta} \cdot 0 = 0 by step 1.3 and [L3]. If α=1\alpha = 1 both sides are 11 by step 1.2 and [L3]. If α>1\alpha > 1 then D={β+ξ:ξ∈λ}D = \{\beta + \xi : \xi \in \lambda\} is a nonempty subset of the limit ordinal β+λ\beta + \lambda with supremum β+λ\beta + \lambda by [L2] and [L3], so step 4.1 gives αβ+λ=sup⁡{αβ+ξ:ξ∈λ}=sup⁡{αβ⋅αξ:ξ∈λ}\alpha^{\beta + \lambda} = \sup\{\alpha^{\beta + \xi} : \xi \in \lambda\} = \sup\{\alpha^{\beta} \cdot \alpha^{\xi} : \xi \in \lambda\} by the claim at each ξ\xi; and E={αξ:ξ∈λ}E = \{\alpha^{\xi} : \xi \in \lambda\} is a nonempty subset of the limit ordinal αλ\alpha^{\lambda} with supremum αλ\alpha^{\lambda} by steps 2.1, 3.1 and 4.2, so [L3] with αβ>0\alpha^{\beta} > 0 gives αβ⋅αλ=sup⁡{αβ⋅αξ:ξ∈λ}\alpha^{\beta} \cdot \alpha^{\lambda} = \sup\{\alpha^{\beta} \cdot \alpha^{\xi} : \xi \in \lambda\}; 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 γ\gamma. At γ=0\gamma = 0: (αβ)0=1=α0=αβ⋅0(\alpha^{\beta})^{0} = 1 = \alpha^{0} = \alpha^{\beta \cdot 0} by [L1] and [L3]. At γ=δ+\gamma = \delta^{+}, assuming the claim at δ\delta: (αβ)δ+=(αβ)δ⋅αβ=αβδ⋅αβ=αβδ+β=αβ⋅δ+(\alpha^{\beta})^{\delta^{+}} = (\alpha^{\beta})^{\delta} \cdot \alpha^{\beta} = \alpha^{\beta\delta} \cdot \alpha^{\beta} = \alpha^{\beta\delta + \beta} = \alpha^{\beta \cdot \delta^{+}}, the third equality by step 5.1 and the fourth by [L2]. At γ=λ\gamma = \lambda a limit there are four cases. If β=0\beta = 0 then both sides are 11, by step 1.2 and [L1] and [L3]. If β>0\beta > 0 and α=0\alpha = 0 then the left side is 0λ=00^{\lambda} = 0 by step 1.3 applied twice, while β⋅λ\beta \cdot \lambda is a limit by [L3] and so nonzero, making the right side 00 as well. If β>0\beta > 0 and α=1\alpha = 1 both sides are 11 by step 1.2. If β>0\beta > 0 and α>1\alpha > 1 then αβ>1\alpha^{\beta} > 1 by step 4.4, so step 4.1 applied with base αβ\alpha^{\beta} gives (αβ)λ=sup⁡{(αβ)ξ:ξ∈λ}=sup⁡{αβξ:ξ∈λ}(\alpha^{\beta})^{\lambda} = \sup\{(\alpha^{\beta})^{\xi} : \xi \in \lambda\} = \sup\{\alpha^{\beta\xi} : \xi \in \lambda\} by the claim at each ξ\xi; and D={βξ:ξ∈λ}D = \{\beta\xi : \xi \in \lambda\} is a nonempty subset of the limit ordinal β⋅λ\beta \cdot \lambda with supremum β⋅λ\beta \cdot \lambda by [L2] and [L3], so step 4.1 applied with base α\alpha gives αβ⋅λ=sup⁡{αβξ:ξ∈λ}\alpha^{\beta \cdot \lambda} = \sup\{\alpha^{\beta\xi} : \xi \in \lambda\}; 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. β≤αβ\beta \le \alpha^{\beta} says only that the exponential never falls below the identity. It does not say that β=αβ\beta = \alpha^{\beta} has a solution; that it does is a separate matter, exhibited by hand at ε0\varepsilon_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⋅c0+⋯+ωβk−1⋅ck−1\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1} with β0>⋯>βk−1\beta_0 > \cdots > \beta_{k-1} and each cic_i a nonzero natural number, in exactly one way to bound the exponents that can occur, which is what turns "the largest β\beta with ωβ≤α\omega^{\beta} \le \alpha" into a search over a set.

The law that is false, computed. (α⋅β)γ=αγ⋅βγ(\alpha \cdot \beta)^{\gamma} = \alpha^{\gamma} \cdot \beta^{\gamma} fails at α=ω\alpha = \omega, β=γ=2\beta = \gamma = 2. On one side, clause (f) is not available, so compute directly: (ω⋅2)2=(ω⋅2)⋅(ω⋅2)=((ω⋅2)⋅ω)⋅2(\omega \cdot 2)^{2} = (\omega \cdot 2) \cdot (\omega \cdot 2) = ((\omega \cdot 2) \cdot \omega) \cdot 2 by associativity of ⋅\cdot, and (ω⋅2)⋅ω=sup⁡{(ω⋅2)⋅n:n∈ω}=sup⁡{ω⋅(2⋅n):n∈ω}=ω⋅ω=ω2(\omega \cdot 2) \cdot \omega = \sup\{(\omega \cdot 2) \cdot n : n \in \omega\} = \sup\{\omega \cdot (2 \cdot n) : n \in \omega\} = \omega \cdot \omega = \omega^{2}, the last step because {2⋅n:n∈ω}\{2 \cdot n : n \in \omega\} is unbounded in ω\omega 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+β=β0 + \beta = \beta and 1⋅β=β1 \cdot \beta = \beta); so (ω⋅2)2=ω2⋅2(\omega \cdot 2)^{2} = \omega^{2} \cdot 2. On the other side ω2⋅22=ω2⋅4\omega^{2} \cdot 2^{2} = \omega^{2} \cdot 4, and ω2⋅2≠ω2⋅4\omega^{2} \cdot 2 \ne \omega^{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\alpha = 0 and α=1\alpha = 1 have to be separated in every limit case, because clause (c) needs α>1\alpha > 1: at α=1\alpha = 1 the function is constant and at α=0\alpha = 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 α≤1\alpha \le 1.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 40 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources