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.
is the least limit ordinal
Statement
Let be the natural numbers (The natural numbers (von Neumann)) with their usual order (Order on the natural numbers). Then:
(i) for all , if and only if ;
(ii) every natural number is an ordinal (Ordinal (von Neumann)), and is an ordinal;
(iii) is a limit ordinal (Successor and limit ordinals);
(iv) every ordinal is or a successor ordinal, and consequently is the least limit ordinal: , that is , for every limit ordinal .
So the natural numbers are exactly the ordinals below , and is the first ordinal at which induction acquires a limit clause.
Everything here is a theorem of ZF, and no choice principle is used. The only axiom beyond the basic ones that any of it needs is Infinity, which is what makes a set at all (The natural numbers exist: a smallest inductive set).
Facts & Assumptions
Given: with and (The natural numbers (von Neumann)), and the order , and (Order on the natural numbers).
is inductive, that is and , and is contained in every inductive set (The natural numbers exist: a smallest inductive set).
The induction principle: a subset of containing and closed under equals (The principle of mathematical induction).
is a linear order on with trichotomy, and for every because ( is a linear order on , Trichotomy of the order on , Left identity for addition).
Every nonempty subset of has a least element (The well-ordering principle).
Every natural number is a transitive set and satisfies (Every natural number is a transitive set and is not a member of itself).
Every nonzero natural number is for some natural number (Every nonzero natural number is a successor).
An ordinal is a transitive set strictly well ordered by , no ordinal is a member of itself, and a limit ordinal is a nonzero ordinal that is not of the form (Ordinal (von Neumann), Basic closure properties of ordinals, Successor and limit ordinals).
for every . This is established at step 1.3 of Trichotomy of the order on , where it is derived from and ; the reference is to that item's numbering, not to any step below.
For ordinals : if and only if or , and any two ordinals are comparable under inclusion (claims (f) and (g) of Basic closure properties of ordinals); exactly one of , , holds, and is the order under which sets of ordinals are well ordered, with strict part (Trichotomy and well-ordering of the ordinals).
Proof
For all , if and only if : from and ([L9]) transitivity gives ; conversely if and failed, then by trichotomy, so by [L3], which is impossible.
is a transitive set: the set contains and is closed under , since together with gives ; so by [L2].
Claim (i): the set contains , because is false and is false, since always and would give by antisymmetry and then ; and gives , because ; hence by [L2].
Claim (ii) for natural numbers: fix ; then is a transitive set by [L6], its elements are natural numbers by step 1.2, and on them membership is the strict order by step 2.1, so is irreflexive, transitive and trichotomous on by [L4] and every nonempty subset of has an -least element by [L5]; hence is an ordinal.
Claim (ii) for : is a transitive set by step 1.2 and membership is the strict order on it by step 2.1, so the same four properties hold by [L4] and [L5]; hence is an ordinal.
Claim (iii): because ; and is not a successor ordinal, since would give and hence because is inductive, contradicting the fact that no ordinal is a member of itself; so is a limit ordinal.
Claim (iv), first half: the ordinals with are exactly the natural numbers, each of which is or of the form with a natural number by [L7], hence or a successor ordinal; so no ordinal -below is a limit ordinal.
Claim (iv), second half, which is where "least" is more than -minimality: let be any limit ordinal; is an ordinal by step 3.2, so by comparability of ordinals under inclusion [L10] either or , and in the second case [L10] gives or ; but would make equal to or to a successor ordinal by step 5.1, contradicting the definition of a limit ordinal in [L8], so and again; hence , that is in the ordering of [L10], for every limit ordinal , and since is itself a limit ordinal by step 4.1 it is the least one.
Claims (i) to (iv) are established.
Remarks
Why claim (i) has to be proved. The published development builds the order on from addition (Order on the natural numbers) and never identifies it with membership; the identification is recorded there as a remark, not a theorem. Ordinals need it as a theorem, because the whole definition of an ordinal is phrased in terms of . Once claim (i) is available, the two pictures of , as "the number of predecessors" and as "the set of its predecessors", coincide.
The finite ordinals. Claims (ii) and (iv) say the natural numbers are exactly the ordinals with , and that each is or a successor. This is the precise sense in which is an initial segment of the ordinals, and it is why ordinary induction (The principle of mathematical induction) is the special case of Transfinite induction at .
Limits exist only because does. The Axiom of Infinity is what makes a set (The natural numbers exist: a smallest inductive set), and it is also what gives this lemma its content: ZF without Infinity cannot prove that any limit ordinal exists, assuming that theory consistent. The reason is that every limit ordinal is itself an inductive set, and so would witness Infinity outright: , because the -least element of a nonempty ordinal is ; and gives , hence by claim (f) of Basic closure properties of ordinals unless , which a limit ordinal excludes. Dropping an axiom is not the same as assuming its negation, and nothing here says that without Infinity every ordinal is or a successor: ZF itself extends ZF without Infinity and has limit ordinals. What is lost is any proof that one exists. The successor operation alone never produces a limit; a limit is always reached by taking a union, here .
Ordinal arithmetic is not developed here. Sums and products of ordinals, and the ordinals , and so on, are defined by transfinite recursion and would fit naturally after this item, but nothing on this page needs them, so they are left to a later page rather than introduced unused.
Depends on
Successor and limit ordinals
Ordinal (von Neumann)
The natural numbers (von Neumann)
Order on the natural numbers
The natural numbers exist: a smallest inductive set
Every nonzero natural number is a successor
Every natural number is a transitive set and is not a member of itself
Discreteness: is the immediate successor
Trichotomy of the order on
is a linear order on
The principle of mathematical induction
The well-ordering principle
Left identity for addition
Basic closure properties of ordinals
Trichotomy and well-ordering of the ordinals