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.

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

Statement

Let α\alpha, β\beta, γ\gamma be ordinals (Ordinal (von Neumann)) and let λ\lambda be a limit ordinal (Successor and limit ordinals), with ++ and ⋅\cdot as in Ordinal addition α+β\alpha + \beta and Ordinal multiplication α⋅β\alpha \cdot \beta. Then:

(a) Identities. β+0=0+β=β\beta + 0 = 0 + \beta = \beta, β+1=β+\beta + 1 = \beta^{+}, β⋅0=0⋅β=0\beta \cdot 0 = 0 \cdot \beta = 0, and β⋅1=1⋅β=β\beta \cdot 1 = 1 \cdot \beta = \beta.

(b) Strictly increasing on the right, for ++. β∈γ\beta \in \gamma implies α+β∈α+γ\alpha + \beta \in \alpha + \gamma; equivalently β<γ⇒α+β<α+γ\beta < \gamma \Rightarrow \alpha + \beta < \alpha + \gamma. Hence left cancellation: α+β=α+γ\alpha + \beta = \alpha + \gamma implies β=γ\beta = \gamma; and α≤α+β\alpha \le \alpha + \beta, with equality exactly when β=0\beta = 0.

(c) Weakly increasing on the left, for ++. α≤β\alpha \le \beta implies α+γ≤β+γ\alpha + \gamma \le \beta + \gamma, and β≤α+β\beta \le \alpha + \beta. Only the weak inequality holds, and that is best possible: 0<10 < 1 while 0+ω=1+ω0 + \omega = 1 + \omega, which is refuted in full among this page's false statements.

(d) Strictly increasing on the right, for ⋅\cdot. If α>0\alpha > 0 then β<γ\beta < \gamma implies α⋅β<α⋅γ\alpha \cdot \beta < \alpha \cdot \gamma. Hence for α>0\alpha > 0: α⋅β=α⋅γ\alpha \cdot \beta = \alpha \cdot \gamma implies β=γ\beta = \gamma, and α≤α⋅β\alpha \le \alpha \cdot \beta whenever β≥1\beta \ge 1. Also α⋅β=0\alpha \cdot \beta = 0 if and only if α=0\alpha = 0 or β=0\beta = 0.

(e) Weakly increasing on the left, for ⋅\cdot. α≤β\alpha \le \beta implies α⋅γ≤β⋅γ\alpha \cdot \gamma \le \beta \cdot \gamma.

(f) Continuity at limits. α+λ=sup⁡{α+ξ:ξ∈λ}\alpha + \lambda = \sup\{\alpha + \xi : \xi \in \lambda\} and α⋅λ=sup⁡{α⋅ξ:ξ∈λ}\alpha \cdot \lambda = \sup\{\alpha \cdot \xi : \xi \in \lambda\}, which are the defining clauses restated as supremum properties. More usefully, if D⊆λD \subseteq \lambda is nonempty with sup⁡D=λ\sup D = \lambda, then

α+λ=sup⁡{ α+η:η∈D },and, if α>0,α⋅λ=sup⁡{ α⋅η:η∈D }.\alpha + \lambda = \sup\{\, \alpha + \eta : \eta \in D \,\}, \qquad \text{and, if } \alpha > 0, \quad \alpha \cdot \lambda = \sup\{\, \alpha \cdot \eta : \eta \in D \,\}.

(g) Limits go to limits. α+λ\alpha + \lambda is a limit ordinal, and α⋅λ\alpha \cdot \lambda is a limit ordinal whenever α>0\alpha > 0.

Throughout, sup⁡A=⋃A\sup A = \bigcup A for a set AA of ordinals (Basic closure properties of ordinals, claim (e)). Everything here is a theorem of ZF and uses no choice principle.

Facts & Assumptions

Given: Ordinals α\alpha, β\beta, γ\gamma and a limit ordinal λ\lambda. The order is μ<ν:  ⟺  μ∈ν\mu < \nu :\iff \mu \in \nu and μ≤ν:  ⟺  μ⊆ν\mu \le \nu :\iff \mu \subseteq \nu.

[L1]

α+0=α\alpha + 0 = \alpha, α+δ+=(α+δ)+\alpha + \delta^{+} = (\alpha + \delta)^{+}, and α+λ=⋃{α+ξ:ξ∈λ}\alpha + \lambda = \bigcup\{\alpha + \xi : \xi \in \lambda\} for limit λ\lambda (Ordinal addition α+β\alpha + \beta).

[L2]

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

[L3]

μ+\mu^{+} is an ordinal; ⋃A\bigcup A is an ordinal and is the least upper bound of any set AA of ordinals; μ⊆ν\mu \subseteq \nu if and only if μ∈ν\mu \in \nu or μ=ν\mu = \nu; and μ∉μ\mu \notin \mu (claims (b), (c), (e), (f) of Basic closure properties of ordinals).

[L4]

Exactly one of μ∈ν\mu \in \nu, μ=ν\mu = \nu, ν∈μ\nu \in \mu holds, and every nonempty set of ordinals has an ∈\in-least element (Trichotomy and well-ordering of the ordinals).

[L5]

Every ordinal is exactly one of 00, a successor, or a limit; and a nonzero ordinal λ\lambda is a limit if and only if ξ∈λ\xi \in \lambda implies ξ+∈λ\xi^{+} \in \lambda, in which case ⋃λ=λ\bigcup \lambda = \lambda (Successor and limit ordinals).

[L6]

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), which is a well-order by clause 2 of Ordinal (von Neumann) and claim (c) of Basic closure properties of ordinals, and to S={ξ∈β0+:P(ξ)}S = \{\xi \in \beta_0^{+} : P(\xi)\}, whose initial segment below ξ\xi is ξ\xi; so if PP holds at ξ\xi whenever it holds at every ordinal in ξ\xi, then PP holds at every ordinal.

Proof

technique · direct
1.1

For ordinals μ,ν\mu, \nu: μ∈ν\mu \in \nu if and only if μ+⊆ν\mu^{+} \subseteq \nu, since μ∈ν\mu \in \nu gives μ⊆ν\mu \subseteq \nu by transitivity and {μ}⊆ν\{\mu\} \subseteq \nu, while μ+⊆ν\mu^{+} \subseteq \nu gives μ∈ν\mu \in \nu; consequently μ<ν  ⟺  μ+≤ν\mu < \nu \iff \mu^{+} \le \nu, and μ≤ν\mu \le \nu implies μ+≤ν+\mu^{+} \le \nu^{+}, because μ≤ν<ν+\mu \le \nu < \nu^{+} gives μ<ν+\mu < \nu^{+}.

L3L4
1.2

For a set AA of ordinals sup⁡A=⋃A\sup A = \bigcup A is its least upper bound, so if every member of AA is ≤\le some member of BB then sup⁡A≤sup⁡B\sup A \le \sup B; for a limit ordinal λ\lambda one has ⋃λ=λ\bigcup \lambda = \lambda, 0∈λ0 \in \lambda (because ∅⊆λ\varnothing \subseteq \lambda and ∅≠λ\varnothing \ne \lambda), and ξ∈λ⇒ξ+∈λ\xi \in \lambda \Rightarrow \xi^{+} \in \lambda, so also 1=0+∈λ1 = 0^{+} \in \lambda.

L3L5
1.3

Directly from the clauses: β+0=β\beta + 0 = \beta; β+1=β+0+=(β+0)+=β+\beta + 1 = \beta + 0^{+} = (\beta + 0)^{+} = \beta^{+}; β⋅0=0\beta \cdot 0 = 0; and β⋅1=β⋅0+=β⋅0+β=0+β\beta \cdot 1 = \beta \cdot 0^{+} = \beta \cdot 0 + \beta = 0 + \beta.

L1L2
2.1

0+β=β0 + \beta = \beta for every β\beta, by induction: at 00 this is 0+0=00 + 0 = 0; at δ+\delta^{+}, 0+δ+=(0+δ)+=δ+0 + \delta^{+} = (0 + \delta)^{+} = \delta^{+}; and at a limit λ\lambda, 0+λ=⋃{0+ξ:ξ∈λ}=⋃λ=λ0 + \lambda = \bigcup\{0 + \xi : \xi \in \lambda\} = \bigcup \lambda = \lambda.

step 1.2step 1.3L1L5L6
2.2

0⋅β=00 \cdot \beta = 0 for every β\beta, by induction: at 00 this is [L2]; at δ+\delta^{+}, 0⋅δ+=0⋅δ+0=0+0=00 \cdot \delta^{+} = 0 \cdot \delta + 0 = 0 + 0 = 0; and at a limit λ\lambda, 0⋅λ=⋃{0}=00 \cdot \lambda = \bigcup\{0\} = 0.

step 1.2step 1.3L2L5L6
2.3

1⋅β=β1 \cdot \beta = \beta for every β\beta, by induction: at 00 this is [L2]; at δ+\delta^{+}, 1⋅δ+=1⋅δ+1=δ+1=δ+1 \cdot \delta^{+} = 1 \cdot \delta + 1 = \delta + 1 = \delta^{+} by step 1.3; and at a limit λ\lambda, 1⋅λ=⋃{ξ:ξ∈λ}=⋃λ=λ1 \cdot \lambda = \bigcup\{\xi : \xi \in \lambda\} = \bigcup \lambda = \lambda.

step 1.2step 1.3L2L5L6
2.4

Claim (b), the inequality: by induction on γ\gamma, for every β∈γ\beta \in \gamma one has α+β∈α+γ\alpha + \beta \in \alpha + \gamma. At γ=0\gamma = 0 there is nothing to prove. At γ=δ+\gamma = \delta^{+}, β∈δ+\beta \in \delta^{+} gives β≤δ\beta \le \delta by [L3], so α+β≤α+δ\alpha + \beta \le \alpha + \delta, using the claim at δ\delta when β∈δ\beta \in \delta, and α+δ∈(α+δ)+=α+δ+\alpha + \delta \in (\alpha + \delta)^{+} = \alpha + \delta^{+}. At γ=λ\gamma = \lambda a limit, β∈λ\beta \in \lambda gives β+∈λ\beta^{+} \in \lambda by step 1.2, and α+β∈(α+β)+=α+β+⊆α+λ\alpha + \beta \in (\alpha + \beta)^{+} = \alpha + \beta^{+} \subseteq \alpha + \lambda.

step 1.1step 1.2L1L3L5L6
2.5

Claim (c), the inequality α+γ≤β+γ\alpha + \gamma \le \beta + \gamma for α≤β\alpha \le \beta: by induction on γ\gamma. At γ=0\gamma = 0 it is α≤β\alpha \le \beta. At γ=δ+\gamma = \delta^{+}, the claim at δ\delta gives α+δ≤β+δ\alpha + \delta \le \beta + \delta, hence (α+δ)+≤(β+δ)+(\alpha + \delta)^{+} \le (\beta + \delta)^{+} by step 1.1. At γ=λ\gamma = \lambda a limit, every α+ξ\alpha + \xi with ξ∈λ\xi \in \lambda is ≤β+ξ\le \beta + \xi, so the suprema compare by step 1.2.

step 1.1step 1.2L1L5L6
3.1

α⋅1=α\alpha \cdot 1 = \alpha, since α⋅1=0+α=α\alpha \cdot 1 = 0 + \alpha = \alpha by step 1.3 and step 2.1; together with step 1.3 and steps 2.1 to 2.3 this proves claim (a).

step 1.3step 2.1step 2.2step 2.3
3.2

Left cancellation for ++: if β≠γ\beta \ne \gamma then β∈γ\beta \in \gamma or γ∈β\gamma \in \beta by [L4], so α+β≠α+γ\alpha + \beta \ne \alpha + \gamma by step 2.4 and [L3]; and α=α+0≤α+β\alpha = \alpha + 0 \le \alpha + \beta with equality exactly when β=0\beta = 0, again by step 2.4. This completes claim (b).

step 2.4step 1.3L3L4
3.3

β≤α+β\beta \le \alpha + \beta: since 0≤α0 \le \alpha, step 2.5 gives 0+β≤α+β0 + \beta \le \alpha + \beta, and 0+β=β0 + \beta = \beta by step 2.1. This completes claim (c).

step 2.5step 2.1L3
3.4

Claim (d), the inequality: let α>0\alpha > 0; by induction on γ\gamma, for every β∈γ\beta \in \gamma one has α⋅β∈α⋅γ\alpha \cdot \beta \in \alpha \cdot \gamma. At γ=0\gamma = 0 there is nothing to prove. At γ=δ+\gamma = \delta^{+}, β≤δ\beta \le \delta gives α⋅β≤α⋅δ\alpha \cdot \beta \le \alpha \cdot \delta using the claim at δ\delta, and α⋅δ=α⋅δ+0∈α⋅δ+α=α⋅δ+\alpha \cdot \delta = \alpha \cdot \delta + 0 \in \alpha \cdot \delta + \alpha = \alpha \cdot \delta^{+} by step 2.4 applied to 0∈α0 \in \alpha. At γ=λ\gamma = \lambda a limit, β+∈λ\beta^{+} \in \lambda by step 1.2 and α⋅β∈α⋅β+⊆α⋅λ\alpha \cdot \beta \in \alpha \cdot \beta^{+} \subseteq \alpha \cdot \lambda.

step 2.4step 1.2step 1.3L2L3L5L6
3.5

Claim (e): let α≤β\alpha \le \beta; by induction on γ\gamma. At γ=0\gamma = 0 both sides are 00. At γ=δ+\gamma = \delta^{+}, the claim at δ\delta gives α⋅δ≤β⋅δ\alpha \cdot \delta \le \beta \cdot \delta, so α⋅δ+=α⋅δ+α≤β⋅δ+α≤β⋅δ+β=β⋅δ+\alpha \cdot \delta^{+} = \alpha \cdot \delta + \alpha \le \beta \cdot \delta + \alpha \le \beta \cdot \delta + \beta = \beta \cdot \delta^{+}, the first inequality by step 2.5 and the second by step 2.4. At γ=λ\gamma = \lambda a limit, the suprema compare by step 1.2.

step 2.4step 2.5step 1.2L2L5L6
4.1

The rest of claim (d): for α>0\alpha > 0, β≠γ\beta \ne \gamma gives α⋅β≠α⋅γ\alpha \cdot \beta \ne \alpha \cdot \gamma by step 3.4 and [L4], which is cancellation; α=α⋅1≤α⋅β\alpha = \alpha \cdot 1 \le \alpha \cdot \beta for 1≤β1 \le \beta by step 3.4 and step 3.1; and α⋅β=0\alpha \cdot \beta = 0 forces α=0\alpha = 0 or β=0\beta = 0, since α>0\alpha > 0 and β>0\beta > 0 give α⋅β≥α⋅1=α>0\alpha \cdot \beta \ge \alpha \cdot 1 = \alpha > 0, while α=0\alpha = 0 or β=0\beta = 0 each give 00 by step 2.2 and [L2].

step 3.4step 3.1step 2.2L2L4
4.2

Claim (f): the first two identities are [L1] and [L2] with sup⁡=⋃\sup = \bigcup. For the refinement, let D⊆λD \subseteq \lambda be nonempty with sup⁡D=λ\sup D = \lambda; then {α+η:η∈D}⊆{α+ξ:ξ∈λ}\{\alpha + \eta : \eta \in D\} \subseteq \{\alpha + \xi : \xi \in \lambda\} gives ≤\le, and conversely each ξ∈λ=⋃D\xi \in \lambda = \bigcup D lies in some η∈D\eta \in D, so α+ξ<α+η\alpha + \xi < \alpha + \eta by step 2.4 and the suprema compare by step 1.2; the same argument with step 3.4 in place of step 2.4 gives the multiplicative half when α>0\alpha > 0.

step 3.4step 2.4step 1.2L1L2L3
4.3

Claim (g): α+λ≠0\alpha + \lambda \ne 0, because 1∈λ1 \in \lambda by step 1.2 and so α+=α+1≤α+λ\alpha^{+} = \alpha + 1 \le \alpha + \lambda by step 2.4 and step 1.3; and α+λ\alpha + \lambda is not a successor, since α+λ=μ+\alpha + \lambda = \mu^{+} would put μ∈⋃{α+ξ:ξ∈λ}\mu \in \bigcup\{\alpha + \xi : \xi \in \lambda\}, hence μ∈α+ξ\mu \in \alpha + \xi for some ξ∈λ\xi \in \lambda, whence μ+≤α+ξ<α+ξ+≤α+λ=μ+\mu^{+} \le \alpha + \xi < \alpha + \xi^{+} \le \alpha + \lambda = \mu^{+} by step 1.1 and step 2.4, which [L3] forbids; the same argument with step 3.4 in place of step 2.4, and α⋅1=α>0\alpha \cdot 1 = \alpha > 0 in place of α+1\alpha + 1, shows α⋅λ\alpha \cdot \lambda is a limit ordinal when α>0\alpha > 0.

step 3.4step 2.4step 1.1step 1.2step 1.3L1L2L3L5
5.1

Claims (a) to (g) are established.

step 4.1step 4.2step 4.3step 3.1step 3.2step 3.3step 3.5∎

Remarks

Which asymmetries are real. Strictness holds on the right and fails on the left, for both operations. The failures are not pathologies to be worked around; they are the content of 1+ω=ω1 + \omega = \omega and 2⋅ω=ω2 \cdot \omega = \omega, and they are exhibited as false statements later on this page. Cancellation therefore holds on the left only: α+β=α+γ\alpha + \beta = \alpha + \gamma gives β=γ\beta = \gamma, whereas β+α=γ+α\beta + \alpha = \gamma + \alpha does not, since 0+ω=1+ω0 + \omega = 1 + \omega.

Continuity is what later "least such ordinal" arguments consume. Clause (f) in its refined form says that to evaluate α+λ\alpha + \lambda or α⋅λ\alpha \cdot \lambda it is enough to run over any set unbounded in λ\lambda, not over all of λ\lambda. That is the step used in Ordinal multiplication is associative, and α⋅(β+γ)=α⋅β+α⋅γ\alpha \cdot (\beta + \gamma) = \alpha\cdot\beta + \alpha\cdot\gamma, in αβ+γ=αβ⋅αγ\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} and again 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, each time to move a supremum past an operation.

Clause (g) is what makes the division algorithm work. In For α>0\alpha > 0 every ordinal β\beta is α⋅ξ+ρ\alpha \cdot \xi + \rho with ρ<α\rho < \alpha, in exactly one way the least η\eta with β<α⋅η\beta < \alpha \cdot \eta has to be a successor, and the reason is exactly that α⋅λ\alpha \cdot \lambda is a limit, so the strict inequality cannot first appear at a limit stage.

No completeness is assumed. Every supremum here is a union of a set of ordinals, an ordinal by claim (e) of Basic closure properties of ordinals. The ordinals are closed under suprema of sets for free, which is what makes the limit clauses legitimate in the first place.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 32 results over 17 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