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 : strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities and
Statement
Let , , be ordinals (Ordinal (von Neumann)) and let be a limit ordinal (Successor and limit ordinals), with and as in Ordinal addition and Ordinal multiplication . Then:
(a) Identities. , , , and .
(b) Strictly increasing on the right, for . implies ; equivalently . Hence left cancellation: implies ; and , with equality exactly when .
(c) Weakly increasing on the left, for . implies , and . Only the weak inequality holds, and that is best possible: while , which is refuted in full among this page's false statements.
(d) Strictly increasing on the right, for . If then implies . Hence for : implies , and whenever . Also if and only if or .
(e) Weakly increasing on the left, for . implies .
(f) Continuity at limits. and , which are the defining clauses restated as supremum properties. More usefully, if is nonempty with , then
(g) Limits go to limits. is a limit ordinal, and is a limit ordinal whenever .
Throughout, for a set 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 , , and a limit ordinal . The order is and .
, , and for limit (Ordinal addition ).
, , and for limit (Ordinal multiplication ).
is an ordinal; is an ordinal and is the least upper bound of any set of ordinals; if and only if or ; and (claims (b), (c), (e), (f) of Basic closure properties of ordinals).
Exactly one of , , holds, and every nonempty set of ordinals has an -least element (Trichotomy and well-ordering of the ordinals).
Every ordinal is exactly one of , a successor, or a limit; and a nonzero ordinal is a limit if and only if implies , in which case (Successor and limit ordinals).
Transfinite induction over the ordinals: if a property of ordinals fails at some , apply Transfinite induction to the well-order , which is a well-order by clause 2 of Ordinal (von Neumann) and claim (c) of Basic closure properties of ordinals, and to , whose initial segment below is ; so if holds at whenever it holds at every ordinal in , then holds at every ordinal.
Proof
For ordinals : if and only if , since gives by transitivity and , while gives ; consequently , and implies , because gives .
For a set of ordinals is its least upper bound, so if every member of is some member of then ; for a limit ordinal one has , (because and ), and , so also .
Directly from the clauses: ; ; ; and .
for every , by induction: at this is ; at , ; and at a limit , .
for every , by induction: at this is [L2]; at , ; and at a limit , .
for every , by induction: at this is [L2]; at , by step 1.3; and at a limit , .
Claim (b), the inequality: by induction on , for every one has . At there is nothing to prove. At , gives by [L3], so , using the claim at when , and . At a limit, gives by step 1.2, and .
Claim (c), the inequality for : by induction on . At it is . At , the claim at gives , hence by step 1.1. At a limit, every with is , so the suprema compare by step 1.2.
, since by step 1.3 and step 2.1; together with step 1.3 and steps 2.1 to 2.3 this proves claim (a).
Left cancellation for : if then or by [L4], so by step 2.4 and [L3]; and with equality exactly when , again by step 2.4. This completes claim (b).
: since , step 2.5 gives , and by step 2.1. This completes claim (c).
Claim (d), the inequality: let ; by induction on , for every one has . At there is nothing to prove. At , gives using the claim at , and by step 2.4 applied to . At a limit, by step 1.2 and .
Claim (e): let ; by induction on . At both sides are . At , the claim at gives , so , the first inequality by step 2.5 and the second by step 2.4. At a limit, the suprema compare by step 1.2.
The rest of claim (d): for , gives by step 3.4 and [L4], which is cancellation; for by step 3.4 and step 3.1; and forces or , since and give , while or each give by step 2.2 and [L2].
Claim (f): the first two identities are [L1] and [L2] with . For the refinement, let be nonempty with ; then gives , and conversely each lies in some , so 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 .
Claim (g): , because by step 1.2 and so by step 2.4 and step 1.3; and is not a successor, since would put , hence for some , whence 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 in place of , shows is a limit ordinal when .
Claims (a) to (g) are established.
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 and , and they are exhibited as false statements later on this page. Cancellation therefore holds on the left only: gives , whereas does not, since .
Continuity is what later "least such ordinal" arguments consume. Clause (f) in its refined form says that to evaluate or it is enough to run over any set unbounded in , not over all of . That is the step used in Ordinal multiplication is associative, and , in and ; and for exponentiation is strictly increasing with and again in Cantor normal form: every nonzero ordinal is with and each 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 every ordinal is with , in exactly one way the least with has to be a successor, and the reason is exactly that 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.