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.

On ω\omega the ordinal ++ and \cdot are the Peano operations: ω\omega is closed under ordinal ++, \cdot and exponentiation, and for naturals m,nm, n the ordinal m+nm + n and mnm \cdot n are the natural-number sum and product

Statement

Write ++, \cdot and αβ\alpha^{\beta} for the ordinal operations (Ordinal addition α+β\alpha + \beta, Ordinal multiplication αβ\alpha \cdot \beta, Ordinal exponentiation αβ\alpha^{\beta}, with the conventions α0=1\alpha^{0} = 1 and 00=10^{0} = 1), and +N+_{\mathbb{N}}, N\cdot_{\mathbb{N}} for the natural-number operations defined by Peano recursion (Addition of natural numbers, Multiplication of natural numbers). Let m,nN=ωm, n \in \mathbb{N} = \omega. Then:

(a) Closure. m+nm + n, mnm \cdot n and mnm^{n} all lie in ω\omega.

(b) Agreement for ++ and \cdot. m+n=m+Nnm + n = m +_{\mathbb{N}} n and mn=mNnm \cdot n = m \cdot_{\mathbb{N}} n.

(c) Agreement of the orders. For m,nωm, n \in \omega, mnm \in n if and only if m<nm < n in the additive order of Order on the natural numbers. This is claim (i) of ω\omega is the least limit ordinal and is cited, not reproved.

No agreement is claimed for exponentiation. The dictionary drawn here is with construction-of-the-natural-numbers, which defines addition and multiplication and no exponentiation, and nothing among this page's declared prerequisites supplies a natural-number power for the ordinal power to be compared with. What clause (a) says about mnm^{n} is only that the ordinal power of two naturals is again a natural.

This item is the dictionary between the two arithmetics on N\mathbb{N}. Without it the library would carry two unrelated operations written with the same symbol on the same set. No choice principle is used.

Facts & Assumptions

Given: Natural numbers m,nN=ωm, n \in \mathbb{N} = \omega (The natural numbers N\mathbb{N} (von Neumann)).

[L1]

N=ω\mathbb{N} = \omega carries 0=0 = \varnothing and σ(n)=n{n}\sigma(n) = n \cup \{n\} (The natural numbers N\mathbb{N} (von Neumann)), and (N,0,σ)(\mathbb{N}, 0, \sigma) is the Peano system over which +N+_{\mathbb{N}} and N\cdot_{\mathbb{N}} are defined (The von Neumann naturals form a Peano system). For an ordinal ν\nu the successor is ν+=ν{ν}\nu^{+} = \nu \cup \{\nu\} (Ordinal (von Neumann)), so σ\sigma and +{\cdot}^{+} are the same operation on ω\omega.

[L2]

m+N0=mm +_{\mathbb{N}} 0 = m and m+Nσ(n)=σ(m+Nn)m +_{\mathbb{N}} \sigma(n) = \sigma(m +_{\mathbb{N}} n) (Addition of natural numbers); mN0=0m \cdot_{\mathbb{N}} 0 = 0 and mNσ(n)=mNn+Nmm \cdot_{\mathbb{N}} \sigma(n) = m \cdot_{\mathbb{N}} n +_{\mathbb{N}} m (Multiplication of natural numbers).

[L3]

α+0=α\alpha + 0 = \alpha and α+δ+=(α+δ)+\alpha + \delta^{+} = (\alpha + \delta)^{+} (Ordinal addition α+β\alpha + \beta); α0=0\alpha \cdot 0 = 0 and αδ+=αδ+α\alpha \cdot \delta^{+} = \alpha \cdot \delta + \alpha (Ordinal multiplication αβ\alpha \cdot \beta); α0=1\alpha^{0} = 1 and αδ+=αδα\alpha^{\delta^{+}} = \alpha^{\delta} \cdot \alpha (Ordinal exponentiation αβ\alpha^{\beta}, with the conventions α0=1\alpha^{0} = 1 and 00=10^{0} = 1).

[L4]

Every natural number is an ordinal, ω\omega is a limit ordinal, and every ordinal in ω\omega is 00 or a successor ordinal; moreover mnm \in n if and only if m<nm < n for m,nωm, n \in \omega (claims (i), (ii), (iii), (iv) of ω\omega is the least limit ordinal, with the order of Order on the natural numbers).

[L5]

A limit ordinal is closed under successor (Successor and limit ordinals), and every ordinal is exactly one of 00, a successor or a limit; 1=0+1 = 0^{+} and μ+\mu^{+} is an ordinal (Basic closure properties of ordinals); trichotomy holds for ordinals (Trichotomy and well-ordering of the ordinals).

[L6]

Induction on N\mathbb{N}: a subset of N\mathbb{N} containing 00 and closed under σ\sigma equals N\mathbb{N} (The principle of mathematical induction).

Proof

technique · direct
1.1

On ω\omega the natural-number successor σ\sigma and the ordinal successor +{\cdot}^{+} are literally the same operation, both being νν{ν}\nu \mapsto \nu \cup \{\nu\}; ω\omega is closed under it by [L5], since ω\omega is a limit ordinal by [L4]; and every ordinal in ω\omega is 00 or a successor by [L4], so in evaluating an ordinal recursion at an argument in ω\omega the limit clause never fires.

L1L4L5
1.2

Claim (c) is claim (i) of [L4], quoted as it stands: for m,nωm, n \in \omega, mnm \in n if and only if m<nm < n in the additive order of Order on the natural numbers.

L4
2.1

Claim (b) for ++, together with the additive half of claim (a): let SS be the set of nNn \in \mathbb{N} such that m+n=m+NnNm + n = m +_{\mathbb{N}} n \in \mathbb{N} for every mNm \in \mathbb{N}. Then 0S0 \in S, because m+0=m=m+N0m + 0 = m = m +_{\mathbb{N}} 0 by [L2] and [L3] and mNm \in \mathbb{N}. And nSn \in S implies σ(n)S\sigma(n) \in S, because σ(n)=n+\sigma(n) = n^{+} by step 1.1, so m+σ(n)=m+n+=(m+n)+=σ(m+Nn)=m+Nσ(n)m + \sigma(n) = m + n^{+} = (m + n)^{+} = \sigma(m +_{\mathbb{N}} n) = m +_{\mathbb{N}} \sigma(n), using [L3], the hypothesis at nn, step 1.1 and [L2] in turn, and that value lies in N\mathbb{N} because N\mathbb{N} is closed under σ\sigma. Hence S=NS = \mathbb{N} by [L6].

step 1.1L1L2L3L6
3.1

Claim (b) for \cdot, together with the multiplicative half of claim (a): let TT be the set of nNn \in \mathbb{N} such that mn=mNnNm \cdot n = m \cdot_{\mathbb{N}} n \in \mathbb{N} for every mNm \in \mathbb{N}. Then 0T0 \in T, because m0=0=mN0m \cdot 0 = 0 = m \cdot_{\mathbb{N}} 0 by [L2] and [L3]. And nTn \in T implies σ(n)T\sigma(n) \in T, because mσ(n)=mn+=mn+m=(mNn)+mm \cdot \sigma(n) = m \cdot n^{+} = m \cdot n + m = (m \cdot_{\mathbb{N}} n) + m by [L3], step 1.1 and the hypothesis at nn, while step 2.1 applied to the two naturals mNnm \cdot_{\mathbb{N}} n and mm turns that ordinal sum into (mNn)+Nm(m \cdot_{\mathbb{N}} n) +_{\mathbb{N}} m, which is mNσ(n)m \cdot_{\mathbb{N}} \sigma(n) by [L2] and again lies in N\mathbb{N}. Hence T=NT = \mathbb{N} by [L6].

step 2.1step 1.1L2L3L6
4.1

The exponential half of claim (a): let UU be the set of nNn \in \mathbb{N} such that mnNm^{n} \in \mathbb{N} for every mNm \in \mathbb{N}. Then 0U0 \in U, because m0=1=0+Nm^{0} = 1 = 0^{+} \in \mathbb{N} by [L3] and [L5]. And nUn \in U implies σ(n)U\sigma(n) \in U, because mσ(n)=mn+=mnmm^{\sigma(n)} = m^{n^{+}} = m^{n} \cdot m by [L3] and step 1.1, a product of two naturals, which lies in N\mathbb{N} by step 3.1. Hence U=NU = \mathbb{N} by [L6].

step 3.1step 1.1L3L5L6
5.1

Claims (a), (b) and (c) are established.

step 4.1step 3.1step 2.1step 1.2

Remarks

Why the limit clause never fires below ω\omega. Every ordinal in ω\omega is 00 or a successor (ω\omega is the least limit ordinal, claim (iv)), so the two remaining clauses of each ordinal recursion are exactly the two Peano clauses of Addition of natural numbers and Multiplication of natural numbers. That is the whole reason the two arithmetics agree, and it is also the precise sense in which ordinal arithmetic extends rather than replaces the arithmetic of N\mathbb{N}.

The agreement stops immediately above ω\omega. The natural-number operations are commutative; the ordinal operations are not, and the failure begins at the first infinite ordinal, with 1+ω=ωω+11 + \omega = \omega \ne \omega + 1 (FALSE: ordinal addition is commutative). So this item says the ordinal operations restrict correctly, and says nothing about their behaviour anywhere else.

Exponentiation is closure only. construction-of-the-natural-numbers has no exponentiation, and no prerequisite of this page supplies one, so there is no natural-number power here for the ordinal power to agree with and clause (a) is all that this page claims. Wherever in the library a natural-number exponentiation with the clauses m0=1m^{0} = 1 and mn+=mnmm^{n^{+}} = m^{n} \cdot m is available, the corresponding agreement is a one-line induction of exactly the shape of step 4.1, on top of claim (b) for the product; it is not carried out here only because this page does not declare the page that mints it as a prerequisite.

What would go wrong without this item. The symbol ++ would denote two different functions on N\mathbb{N}, one defined in construction-of-the-natural-numbers and one here, with nothing connecting them. Every later computation mixing finite and infinite ordinals, such as the coefficients of a Cantor normal form (Cantor normal form: every nonzero ordinal is ωβ0c0++ωβk1ck1\omega^{\beta_0}\cdot c_0 + \cdots + \omega^{\beta_{k-1}}\cdot c_{k-1} with β0>>βk1\beta_0 > \cdots > \beta_{k-1} and each cic_i a nonzero natural number, in exactly one way) or the value 2ω=ω2^{\omega} = \omega (FALSE: the ordinal 2ω2^{\omega} is uncountable), silently uses the identification proved here.

Depends on

Used by

Dependency tree · next 3 levels

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