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 the ordinal and are the Peano operations: is closed under ordinal , and exponentiation, and for naturals the ordinal and are the natural-number sum and product
Statement
Write , and for the ordinal operations (Ordinal addition , Ordinal multiplication , Ordinal exponentiation , with the conventions and ), and , for the natural-number operations defined by Peano recursion (Addition of natural numbers, Multiplication of natural numbers). Let . Then:
(a) Closure. , and all lie in .
(b) Agreement for and . and .
(c) Agreement of the orders. For , if and only if in the additive order of Order on the natural numbers. This is claim (i) of 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 is only that the ordinal power
of two naturals is again a natural.
This item is the dictionary between the two arithmetics on . 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 (The natural numbers (von Neumann)).
carries and (The natural numbers (von Neumann)), and is the Peano system over which and are defined (The von Neumann naturals form a Peano system). For an ordinal the successor is (Ordinal (von Neumann)), so and are the same operation on .
and (Addition of natural numbers); and (Multiplication of natural numbers).
and (Ordinal addition ); and (Ordinal multiplication ); and (Ordinal exponentiation , with the conventions and ).
Every natural number is an ordinal, is a limit ordinal, and every ordinal in is or a successor ordinal; moreover if and only if for (claims (i), (ii), (iii), (iv) of is the least limit ordinal, with the order of Order on the natural numbers).
A limit ordinal is closed under successor (Successor and limit ordinals), and every ordinal is exactly one of , a successor or a limit; and is an ordinal (Basic closure properties of ordinals); trichotomy holds for ordinals (Trichotomy and well-ordering of the ordinals).
Induction on : a subset of containing and closed under equals (The principle of mathematical induction).
Proof
On the natural-number successor and the ordinal successor are literally the same operation, both being ; is closed under it by [L5], since is a limit ordinal by [L4]; and every ordinal in is or a successor by [L4], so in evaluating an ordinal recursion at an argument in the limit clause never fires.
Claim (c) is claim (i) of [L4], quoted as it stands: for , if and only if in the additive order of Order on the natural numbers.
Claim (b) for , together with the additive half of claim (a): let be the set of such that for every . Then , because by [L2] and [L3] and . And implies , because by step 1.1, so , using [L3], the hypothesis at , step 1.1 and [L2] in turn, and that value lies in because is closed under . Hence by [L6].
Claim (b) for , together with the multiplicative half of claim (a): let be the set of such that for every . Then , because by [L2] and [L3]. And implies , because by [L3], step 1.1 and the hypothesis at , while step 2.1 applied to the two naturals and turns that ordinal sum into , which is by [L2] and again lies in . Hence by [L6].
The exponential half of claim (a): let be the set of such that for every . Then , because by [L3] and [L5]. And implies , because by [L3] and step 1.1, a product of two naturals, which lies in by step 3.1. Hence by [L6].
Claims (a), (b) and (c) are established.
Remarks
Why the limit clause never fires below . Every ordinal in is or a successor ( 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 .
The agreement stops immediately above . The natural-number operations are commutative; the ordinal operations are not, and the failure begins at the first infinite ordinal, with (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 and 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 , 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 with and each a nonzero natural number, in exactly one way) or the value (FALSE: the ordinal is uncountable), silently uses the identification proved here.
Depends on
- Ordinal addition $\alpha + \beta$
- Ordinal multiplication $\alpha \cdot \beta$
- Ordinal exponentiation $\alpha^{\beta}$, with the conventions $\alpha^{0} = 1$ and $0^{0} = 1$
- Addition of natural numbers
- Multiplication of natural numbers
- The von Neumann naturals form a Peano system
- The principle of mathematical induction
- The natural numbers $\mathbb{N}$ (von Neumann)
- $\omega$ is the least limit ordinal
- Successor and limit ordinals
- Basic closure properties of ordinals
- Trichotomy and well-ordering of the ordinals
- Order on the natural numbers
- Ordinal (von Neumann)
Used by
- 1 + ω = ω and ω + 1 > ω, computed both from the recursion and as order types Example
- 2 · ω = ω while ω · 2 = ω + ω, pictured as order types Example
- The Cantor normal form of (ω² + ω· 3 + 5) · ω², computed by the division algorithm Example
- FALSE: (β + γ)·α = β·α + γ·α for all ordinals False statement
- FALSE: ordinal addition is commutative False statement
- FALSE: ordinal multiplication is commutative False statement
- FALSE: the ordinal 2^ω is uncountable False statement
- FALSE: β < γ implies β + α < γ + α False statement
- Every natural number and ω are cardinals, every infinite cardinal is a limit ordinal, and on the natural numbers the cardinal operations are the published finite counting operations, with | A | in the finite sense equal to | A | in the cardinal sense Theorem
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
- Ordinal arithmetic (Wikipedia) (standard reference, not scraped)
- Peano axioms (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)