Alphabeta Math
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.

✓ 15 results · all verified · 10 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Ordinals, Cardinals, and Transfinite Recursion

1 · Prerequisites

2 · Summary

Well-orders extend ordinary induction by giving every nonempty subset a least element. The development uses partial orders, chains, natural-number induction and well-ordering, the pigeonhole principle, and the set-theoretic axioms of Separation, Union, and Replacement. Zorn's lemma, choice functions, and the Axiom of Choice enter only in the results comparing choice with the existence of well-orders on arbitrary sets.

Well-orders, order isomorphisms, and initial segments support transfinite induction and recursion, followed by rigidity and comparability. Von Neumann ordinals are then developed through their basic closure and trichotomy laws, Burali--Forti, Mostowski collapse, limit ordinals, and the characterization of ω as the least limit ordinal. Hartogs' theorem supplies a choice-free bound, after which the well-ordering theorem and its converse establish the equivalence with the Axiom of Choice. Cardinals and the final choice ledger organize these consequences and their precise foundational assumptions.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-09-26 (gpt-6-sol)Open item page →

Well-order and well-ordered set

Definition

Let W be a set. A well-order on W is a total order ≤ on W (Partial order and partially ordered set) with the property that

every nonempty S⊆W has a least element, i.e. an ℓ∈S with ℓ≤s for all s∈S.

The pair (W,≤) is then a well-ordered set, and W is well-ordered by ≤.

A least element of S is unique when it exists: two of them are below each other, hence equal by antisymmetry (Partial order and partially ordered set). We may therefore write min⁡S for it.

Strict form. Everything on this page is more convenient in terms of the associated strict order x<y:  ⟺  (x≤y and x≠y) (Partial order and partially ordered set). Spelled out strictly, a well-order on W is a relation < that is

  • irreflexive: x<x holds for no x∈W;
  • transitive: x<y and y<z imply x<z;
  • trichotomous: for all x,y∈W exactly one of x<y, x=y, y<x holds;
  • and such that every nonempty S⊆W has an element ℓ with no s∈S satisfying s<ℓ.

The two presentations determine each other by x≤y  ⟺  (x<y or x=y), and we write (W,<) or (W,≤) as convenient.

Remarks

  • Totality is not an extra hypothesis. If ≤ is a partial order on W in which every nonempty subset has a least element, then ≤ is already total: apply the hypothesis to the two element subset {x,y}, whose least element is below the other. Totality is nevertheless stated, because in the strict presentation trichotomy has to be written down explicitly.
  • A well-order is total, so every subset of a well-ordered set is a chain (Chain in a poset), and W itself is one. Chains are therefore not the interesting invariant here; the least element property is.
  • The model case is (N,≤), which is a linear order (≤ is a linear order on N) in which every nonempty subset has a least element (The well-ordering principle). Ordinals, defined later on this page, are the exact generalisation of that picture.
  • (Z,≤) and (R,≤) are total orders but not well-orders: Z has no least element at all, and the bounded set {x∈R:0<x<1} has none either. Being bounded below does not help, which is exactly why well-ordering is a strong condition.
  • The empty set carries exactly one well-order, the empty relation, vacuously. Every one element set carries exactly one.
  • A well-order admits no infinite strictly decreasing sequence x0>x1>x2>⋯, since the set of its terms would have no least element. This direction follows directly from the definition; no converse is used here.
DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-07-26 (claude-opus-5)Open item page →

Order embedding and order isomorphism

Definition

Let (P,≤P) and (Q,≤Q) be posets (Partial order and partially ordered set).

A function f:P→Q is an order embedding when for all x,y∈P

x≤Py  ⟺  f(x)≤Qf(y).

An order embedding is automatically injective: f(x)=f(y) gives f(x)≤Qf(y) and f(y)≤Qf(x), hence x≤Py and y≤Px, hence x=y by antisymmetry (Partial order and partially ordered set).

An order isomorphism is a surjective order embedding, equivalently a bijection f:P→Q with x≤Py  ⟺  f(x)≤Qf(y) for all x,y∈P. The posets P and Q are order isomorphic, written P≅Q, when an order isomorphism P→Q exists.

Remarks

  • The condition is an equivalence, not an implication. A bijection satisfying only x≤Py⇒f(x)≤Qf(y) need not be an order isomorphism: let P={a,b} carry the discrete order, in which a and b are incomparable, and let Q={0,1} carry 0<1. The bijection a↦0, b↦1 preserves every relation of P, because P has none beyond reflexivity, yet its inverse does not preserve 0<1.
  • For total orders the implication form does suffice. If P and Q are totally ordered and f:P→Q is a bijection with x<Py⇒f(x)<Qf(y), then f is an order isomorphism: given f(x)<Qf(y), the alternative y≤Px would give f(y)≤Qf(x), which is impossible. Since a well-order is total (Well-order and well-ordered set), a strictly increasing bijection between well-orders is automatically an order isomorphism.
  • Strict form. An order isomorphism satisfies x<Py  ⟺  f(x)<Qf(y), because it is injective and preserves both ≤ and = in both directions.
  • The identity is an order isomorphism, the inverse of an order isomorphism is one, and a composite of two is one. Hence ≅ is reflexive, symmetric and transitive on any set of posets. It is not a relation on "all posets", since there is no set of all posets.
  • Order isomorphisms transport well-ordering. If f:P→Q is an order isomorphism and (P,≤P) is a well-order (Well-order and well-ordered set), so is (Q,≤Q): totality transfers because f is a surjective embedding, and a nonempty S⊆Q has f−1[S] nonempty, whose least element ℓ is carried by f to a least element of S. This transfer is used repeatedly below and is the reason order isomorphism, rather than mere bijection, is the right notion of sameness here.
  • Order isomorphisms respect initial segments. If f:P→Q is an order isomorphism and x∈P, then f carries {y∈P:y<Px} onto {z∈Q:z<Qf(x)}: the strict form gives the inclusion one way, and surjectivity gives it the other, since z<Qf(x) has the form z=f(y) with y<Px. Consequently the restriction of f to that set is again an order isomorphism.
  • Functions, bijections, ordered pairs and Cartesian products are built in this library, at A function is a relation f with (a,b)∈f and (a,c)∈f implying b=c; f:A→B, the value f(a), domain and codomain, Injection, surjection, bijection, The Kuratowski ordered pair (a,b):={{a},{a,b}} and The Cartesian product A×B:={ z∈P(P(A∪B)):∃a∈A ∃b∈B z=(a,b) }; "subset" and "union" are built alongside them. This item fixes only the order-theoretic terminology on top of that vocabulary.
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-07-26 (claude-opus-5)Open item page →

Initial segment of a well-order

Definition

Let (W,<) be a well-order (Well-order and well-ordered set).

A subset I⊆W is an initial segment of W when it is downward closed: if x∈I and y<x then y∈I. It is a proper initial segment when I≠W.

For a∈W write

W<a:={x∈W:x<a},W≤a:={x∈W:x≤a}=W<a∪{a},

and call W<a the initial segment determined by a.

Every initial segment I, carrying the order inherited from W, is itself a well-order: the inherited order is total, and a nonempty subset of I is a nonempty subset of W, so it has a least element, which lies in I.

Remarks

  • ∅ and W are initial segments of W; each W<a is a proper initial segment, since a∉W<a by irreflexivity; and each W≤a is an initial segment.
  • Every proper initial segment is W<a for exactly one a. Let I⊊W be an initial segment and put a=min⁡(W∖I), which exists because W∖I is a nonempty subset of the well-order W (Well-order and well-ordered set). If x<a then x∉W∖I by minimality of a, so x∈I; hence W<a⊆I. Conversely let x∈I. Then x≠a, because a∉I, and a<x is impossible, because downward closure would then put a∈I; so x<a by trichotomy, and I⊆W<a. Therefore I=W<a. For uniqueness, suppose W<a=W<b with a≠b, say a<b; then a∈W<b=W<a, that is a<a, which is impossible.
  • Nesting. If b<a then (W<a)<b=W<b, so an initial segment of an initial segment of W is an initial segment of W. This is used whenever two well-orders are compared.
  • The initial segments of W are therefore exactly the sets W<a for a∈W, together with W itself, and inclusion orders them in the same shape as W with one extra element added on top.
  • The corresponding notion for a general poset would be a downward closed set, or "lower set". Nothing on this page needs it outside the well-ordered case, so the definition is stated only there, where the second clause above makes the family of initial segments completely explicit.
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Transfinite induction

Statement

Let (W,<) be a well-order (Well-order and well-ordered set) and let S⊆W satisfy the following: for every a∈W, if W<a⊆S then a∈S (Initial segment of a well-order). Then S=W.

In property form: if a property P of elements of W satisfies "whenever P(x) holds for every x<a, it holds at a", then P(a) holds for every a∈W.

This is a theorem of ZF. No form of the Axiom of Choice is used. Choice is perfectly available at this point in the library, since Zorn's lemma is proved from it on the previous page; the claim made here is about this proof, which never invokes it.

Facts & Assumptions

Given: A well-order (W,<) and a subset S⊆W with the stated closure property. No base case is assumed separately: the hypothesis applied to the least element of W, where the initial segment below it is empty, supplies it.

[A1]

For every a∈W: if W<a⊆S then a∈S.

[L1]

Every nonempty subset of W has a least element, and the order is total (Well-order and well-ordered set).

[L2]

W<a={x∈W:x<a} (Initial segment of a well-order).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that S≠W.

assume-contra
2.1

Since S⊆W, the set C=W∖S is then nonempty.

step 1.1
3.1

Let a=min⁡C, the least element of C in the order of W, which exists because C is a nonempty subset of W.

step 2.1L1choose
4.1

Every x∈W with x<a satisfies x∉C, by minimality of a, hence x∈S; that is, W<a⊆S.

step 3.1L2
5.1

The hypothesis on S therefore applies at a and gives a∈S.

step 4.1A1
6.1

But a∈C=W∖S gives a∉S, which is impossible; hence W∖S is empty and S=W.

step 5.1step 3.1discharge-contradiction∎

Remarks

Where the well-ordering is used. Only once, to produce the least element of W∖S. Nothing else about W enters the argument, so the same proof establishes the statement for an arbitrary well-founded relation once that notion is available.

No separate base case. Applying the hypothesis at a=min⁡W, when W is nonempty, forces min⁡W∈S, because the initial segment below min⁡W is empty and is therefore contained in S vacuously. This is why transfinite induction is stated with a single clause where ordinary induction has two, and it is also why the statement holds vacuously for W=∅.

Successors and limits. The scheme that looks stronger, with one clause for the least element, one for successors and one for limits, is the specialisation of this theorem to a well-order in which those three kinds of element are distinguished. Nothing is gained by assuming it separately, and the three-clause form is what gets used once ordinals are available.

Least counterexample. The dual reading is often the useful one: if S≠W then the hypothesis must fail somewhere, so there is a least a with a∉S and every x<a in S. Steps 2.1 to 5.1 are precisely the construction of that least counterexample.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-07-26 (claude-opus-5)Open item page →

Transfinite recursion

Statement

Let (W,<) be a well-order (Well-order and well-ordered set) and let G be a class function: a rule, given by a formula in the language of set theory, that assigns a set G(h) to every function h whose domain is a proper initial segment of W (Initial segment of a well-order). Then there is exactly one function F with domain W such that

F(a)=G(F↾W<a)for every a∈W.

Here F↾W<a is the restriction of F to the initial segment determined by a, so the value of F at a is prescribed in terms of all its earlier values at once.

Because G is a class function rather than a set, this is a theorem schema of ZF: one theorem for each formula defining G. It uses Replacement, and it uses no form of the Axiom of Choice.

Facts & Assumptions

Given: A well-order (W,<), a class function G as in the statement, and the axioms of ZF. Call a function h an attempt when dom(h) is an initial segment of W and h(b)=G(h↾W<b) for every b∈dom(h). The empty function is an attempt, with domain the initial segment ∅.

[A1]

G(h) is a well-determined set for every function h whose domain is a proper initial segment of W.

[A2]

The axioms of ZF are available, in particular Separation, Union and Replacement. No choice principle is assumed.

[L1]

Transfinite induction on (W,<): if W<a⊆S implies a∈S for every a∈W, then S=W (Transfinite induction).

[L2]

W<a={x∈W:x<a} and W≤a=W<a∪{a} are initial segments, an intersection of initial segments is an initial segment, and (W<a)<b=W<b for b<a (Initial segment of a well-order).

[L3]

The order of W is total and every nonempty subset of W has a least element (Well-order and well-ordered set).

Proof

technique · direct
1.1

Let h and k be attempts and put D=dom(h)∩dom(k); then D is an initial segment of W, being an intersection of two downward closed sets.

L2construct
2.1

Put S={a∈W:a∉D or h(a)=k(a)} and suppose W<a⊆S for some a∈D; since D is downward closed, W<a⊆D, so h and k agree at every x<a, that is h↾W<a=k↾W<a, and therefore h(a)=G(h↾W<a)=G(k↾W<a)=k(a), giving a∈S.

step 1.1A1L2
3.1

If instead a∉D then a∈S outright, so for every a∈W the implication "W<a⊆S implies a∈S" holds, and transfinite induction gives S=W: any two attempts agree on the intersection of their domains.

step 2.1L1
4.1

In particular, for each a∈W there is at most one attempt with domain W<a, and at most one attempt with domain W, since two of them would have that same set as the intersection of their domains.

step 3.1
5.1

Let T={a∈W:there is an attempt with domain W<a}, which is a set by Separation applied to W, and note that the attempt in question is unique when it exists.

step 4.1A2construct
6.1

Suppose W<a⊆T; for each b<a let hb be the unique attempt with domain W<b and put hb+=hb∪{(b,G(hb))}, a function with domain W≤b which is again an attempt, because it agrees with hb below b and hb+(b)=G(hb)=G(hb+↾W<b).

step 5.1step 4.1A1L2construct
7.1

The assignment b↦hb+ is given by a formula, so Replacement makes {hb+:b<a} a set; let u be the union of that set.

step 6.1A2construct
8.1

u is a function: any two of the hb+ are attempts and therefore agree on the intersection of their domains, so no argument receives two different values.

step 7.1step 3.1
8.2

dom(u) is the union of the sets W≤b for b<a, which equals W<a: each such W≤b is contained in W<a by transitivity of the order, and each x<a lies in W≤x.

step 7.1step 6.1L2L3
9.1

u is an attempt with domain W<a: for c<a we have u↾W<c=hc+↾W<c=hc and u(c)=hc+(c)=G(hc), so u(c)=G(u↾W<c).

step 8.1step 8.2step 6.1
10.1

Hence a∈T whenever W<a⊆T, so T=W by transfinite induction: for every a∈W there is a unique attempt ha with domain W<a.

step 9.1step 5.1step 4.1L1
11.1

Replacement applied to the formula a↦ha+=ha∪{(a,G(ha))} makes {ha+:a∈W} a set; let F be its union, which by the arguments of steps 8.1 and 8.2 is a function whose domain is the union of the sets W≤a for a∈W, namely W itself.

step 10.1step 8.1step 8.2A2construct
12.1

F satisfies the recursion: for a∈W we get F↾W<a=ha and F(a)=ha+(a)=G(ha), so F(a)=G(F↾W<a), and in particular F is an attempt with domain W.

step 11.1step 9.1
13.1

Uniqueness: any function F′ with domain W satisfying F′(a)=G(F′↾W<a) for all a is by definition an attempt with domain W, hence equals F.

step 12.1step 4.1
14.1

There is therefore exactly one function F with domain W and F(a)=G(F↾W<a) for every a∈W.

step 12.1step 13.1∎

Remarks

Which axioms are spent. Separation produces T in step 5.1; Replacement produces the sets of attempts in steps 7.1 and 11.1; Union assembles them. Replacement is genuinely needed and cannot be traded away: the attempts ha are not subsets of any single set given in advance, so Separation alone cannot collect them. This is the standard reason transfinite recursion is unavailable in Zermelo set theory without Replacement.

No choice is used, and the reason is uniqueness. At every stage the object to be used is the unique attempt with a given domain, singled out by step 4.1, never one of many candidates. A construction phrased as "at stage a pick some element not yet used" is a different theorem and does cost a choice principle; the difference is exactly the content of FALSE: transfinite induction and recursion need the Axiom of Choice.

Class function, not a set function. G has to be allowed to take values anywhere in the universe, since F(a) may be an arbitrary set, so G cannot be assumed to be a set of ordered pairs. That is why the result is a schema. When G happens to be an honest set function, defined on the set of all functions from proper initial segments of W into a fixed set A and taking values in A, the statement is an ordinary theorem of ZF and the same proof applies verbatim.

Relation to ordinary recursion. Taking W=N recovers the familiar recursion on the natural numbers, but not literally the published The recursion theorem: that theorem prescribes g(σ(n)) in terms of g(n) alone, whereas G here sees the whole earlier history F↾W<a. Course-of-values recursion on N is the special case of the present theorem, and it is what later pages use whenever a construction at stage n consults all earlier stages.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-07-26 (claude-opus-5)Open item page →

Rigidity of well-orders

Statement

Let (W,<) be a well-order (Well-order and well-ordered set) and let f:W→W be strictly increasing, that is x<y⇒f(x)<f(y). Then:

(a) a≤f(a) for every a∈W;

(b) W is not order isomorphic (Order embedding and order isomorphism) to any proper initial segment W<a of itself (Initial segment of a well-order);

(c) the identity is the only order isomorphism W→W;

(d) for any two well-orders V and W there is at most one order isomorphism V→W.

This is a theorem of ZF; no choice principle is used.

Facts & Assumptions

Given: A well-order (W,<) and a strictly increasing function f:W→W. The well-order (W,<) and the map f are arbitrary, so once claim (a) is proved it may be applied to any well-order and any strictly increasing self-map of it.

[A1]

x<y implies f(x)<f(y), for all x,y∈W.

[L1]

Every nonempty subset of W has a least element, and the order is total, so failure of f(a)<a is exactly a≤f(a) (Well-order and well-ordered set).

[L2]

W<a={x∈W:x<a} is a proper initial segment of W and is itself a well-order (Initial segment of a well-order).

[L3]

An order isomorphism between total orders is a strictly increasing bijection, its inverse is one, composites of order isomorphisms are order isomorphisms, and an order isomorphism carries the initial segment below x onto the initial segment below its image (Order embedding and order isomorphism).

Proof

technique · contradiction
1.1

Let A={a∈W:f(a)<a} and suppose, for contradiction, that A≠∅.

constructassume-contra
2.1

Being a nonempty subset of W, the set A has a least element m, and f(m)<m by the definition of A.

step 1.1L1choose
3.1

Applying [A1] to f(m)<m gives f(f(m))<f(m), so f(m) itself lies in A.

step 2.1A1
4.1

Thus f(m)∈A and f(m)<m, contradicting the minimality of m in A; so A=∅, and by totality a≤f(a) for every a∈W, which is claim (a).

step 3.1step 2.1L1
5.1

Claim (b) follows: if g:W→W<a were an order isomorphism for some a∈W, then g followed by the inclusion of W<a into W would be a strictly increasing map W→W, so claim (a) would give a≤g(a), while g(a)∈W<a says g(a)<a, and trichotomy forbids both.

step 4.1L2L3
5.2

Claim (c) follows: an order isomorphism f:W→W is strictly increasing and so is its inverse, so claim (a) gives a≤f(a) and a≤f−1(a) for every a; applying f to the second inequality gives f(a)≤a, and antisymmetry yields f(a)=a.

step 4.1L3L1
6.1

Claim (d) follows: if g,h:V→W are order isomorphisms then h−1∘g is an order isomorphism of the well-order V onto itself, hence the identity by claim (c), so g=h.

step 5.2L3
7.1

The supposition of step 1.1 is therefore refuted, claim (a) holds, and claims (b), (c) and (d) were derived from it in steps 5.1, 5.2 and 6.1; the lemma holds in full.

step 4.1step 5.1step 5.2step 6.1discharge-contradiction∎

Remarks

Transfinite induction in disguise. Steps 1.1 to 4.1 are exactly the proof of Transfinite induction specialised to the set S={a∈W:a≤f(a)}: if x≤f(x) for all x<a then a≤f(a), because f(a)<a would put f(a) below a with f(f(a))<f(a). The argument can therefore be run by citing that theorem instead of taking a least element by hand, and nothing changes.

Rigidity is what makes order types well defined. Claim (d) says a well-order has no room for a nontrivial symmetry, so "the" isomorphism between two isomorphic well-orders is unique and can be spoken of without choosing anything. That is precisely why no choice principle appears anywhere in the comparison of well-orders (Comparability of well-orders) or in the assignment of order types (Every well-order has a unique order type).

Totality is essential. For a general poset every claim here fails. On the poset {a,b} with a and b incomparable, the swap a↦b, b↦a is a nonidentity order automorphism, and the strictly increasing condition is vacuous. It is the least element property, used once in step 2.1, that removes this freedom.

Only one direction is available. Claim (a) says f never moves a point strictly down, and no bound in the other direction holds: on (N,≤) the map n↦2n is strictly increasing and moves every nonzero point strictly up, as far up as one likes.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Comparability of well-orders

Statement

Let (V,<V) and (W,<W) be well-orders (Well-order and well-ordered set). Then exactly one of the following holds (Order embedding and order isomorphism, Initial segment of a well-order):

(i) V≅W;

(ii) V≅W<b for a unique b∈W;

(iii) V<a≅W for a unique a∈V.

In particular any two well-orders are comparable: one of them is order isomorphic to an initial segment of the other. No choice principle is used, which is what makes this the choice-free substitute for cardinal comparability.

Facts & Assumptions

Given: Two well-orders (V,<V) and (W,<W), and the axioms of ZF. Write ≅ for order isomorphism, and note that the defining condition below is symmetric in V and W, so every argument may be repeated with their roles exchanged.

[A1]

The axioms of ZF are available, in particular Separation applied to the set V×W. No choice principle is assumed.

[L2]

V<v={x∈V:x<Vv} is a proper initial segment and is itself a well-order; (V<v′)<v=V<v whenever v<Vv′; and a proper initial segment is V<v for a unique v (Initial segment of a well-order).

[L3]

Order isomorphisms compose, invert, are strictly increasing, and carry the initial segment below a point onto the initial segment below its image (Order embedding and order isomorphism).

[L4]

No well-order is order isomorphic to a proper initial segment of itself (Rigidity of well-orders).

Proof

technique · direct
1.1

By Separation applied to V×W, the collection f={(v,w)∈V×W:V<v≅W<w} is a set.

A1L2L3construct
2.1

f is a function: if V<v≅W<w and V<v≅W<w′ with w≠w′, say w<Ww′, then W<w=(W<w′)<w is a proper initial segment of the well-order W<w′ and W<w′≅V<v≅W<w, contradicting [L4]; hence w=w′.

step 1.1L2L3L4
2.2

f is injective: the same argument with the roles of V and W exchanged shows that V<v≅W<w≅V<v′ forces v=v′.

step 1.1L2L3L4
3.1

Let v<Vv′ with v′∈dom(f), and let g:V<v′→W<f(v′) be an order isomorphism; then g carries (V<v′)<v=V<v onto (W<f(v′))<g(v)=W<g(v), so V<v≅W<g(v), whence v∈dom(f) with f(v)=g(v), and g(v)∈W<f(v′) gives f(v)<Wf(v′).

step 2.1L2L3
4.1

Consequently dom(f) is an initial segment of V and f is strictly increasing on it.

step 3.1L2
4.2

By the same argument with the roles of V and W exchanged, applied to the transpose of f, which is a function because f is injective, ran(f) is an initial segment of W.

step 3.1step 2.2L2
5.1

f is therefore a strictly increasing bijection from the initial segment dom(f) of V onto the initial segment ran(f) of W, hence an order isomorphism between them.

step 4.1step 4.2step 2.2L3
6.1

dom(f) and ran(f) are not both proper: if dom(f)=V<a and ran(f)=W<b then step 5.1 gives V<a≅W<b, so (a,b)∈f and therefore a∈dom(f)=V<a, that is a<Va, which is impossible.

step 5.1step 1.1L2
7.1

Since every initial segment is either the whole set or of the form V<a respectively W<b, exactly three configurations remain, and they give (i) V≅W, (ii) V≅W<b, and (iii) V<a≅W respectively.

step 5.1step 6.1L2
8.1

The three are mutually exclusive: (i) with (ii) gives W≅W<b; (i) with (iii) gives V≅V<a; and (ii) with (iii) give an isomorphism φ:V→W<b whose restriction carries V<a onto W<φ(a), so W≅V<a≅W<φ(a); each conclusion contradicts [L4].

step 7.1L3L4
8.2

The witnesses are unique: W<b≅V≅W<b′ forces b=b′ by the argument of step 2.1, and V<a≅W≅V<a′ forces a=a′ by the argument of step 2.2.

step 7.1L4L2
9.1

Exactly one of (i), (ii), (iii) holds, with a unique witness in cases (ii) and (iii).

step 7.1step 8.1step 8.2∎

Remarks

Where no choice enters. The relation f is carved out of V×W by Separation, and the isomorphisms witnessing V<v≅W<w are never selected: by rigidity (Rigidity of well-orders) there is at most one of them, so the definition of f quantifies over them rather than picking one. That is the entire reason comparability of well-orders is a ZF theorem while comparability of arbitrary sets is not.

An alternative proof by recursion. One can instead define f by transfinite recursion (Transfinite recursion), sending v to the least element of W not already in the image of V<v, and stopping when W is exhausted. That route needs the recursion theorem and a little care about where the construction halts; the argument above needs only Separation and is recorded here for that reason.

Comparability is not trichotomy of size. The statement compares well-orders, not sets. Two sets need not be comparable in size in ZF at all; that they always are is equivalent to the Axiom of Choice. What survives choice-free is this lemma together with Hartogs: an ordinal that does not inject into a given set, and the ledger of what each costs is The proved choice ledger: hypotheses, equivalences, and upper bounds.

Reading it as a linear order on order types. Once every well-order is assigned an ordinal (Every well-order has a unique order type), case (ii) reads "the order type of V is smaller than that of W" and case (iii) reads the reverse, so this lemma is the statement that the ordinals are linearly ordered, proved before ordinals are available.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Ordinal (von Neumann)

Definition

A set α is an ordinal when both of the following hold.

  1. α is a transitive set: every element of α is also a subset of α, that is x∈α⇒x⊆α.
  2. The membership relation restricted to α, namely {(x,y)∈α×α:x∈y}, is a strict well-order of α (Well-order and well-ordered set): it is irreflexive, transitive as a relation, trichotomous on α, and every nonempty subset of α has an ∈-least element.

Ordinals are written with lowercase Greek letters, and for ordinals we set

α<β:  ⟺  α∈β,α≤β:  ⟺  (α∈β or α=β).

Write 0:=∅, which is an ordinal because both clauses hold vacuously, and write α+:=α∪{α} for the successor of α.

Remarks

  • Two different transitivities. Clause 1 is about the set α: it contains all members of its members. Clause 2 asks in part that the relation ∈ be transitive on α. If every element of α is itself a transitive set then the relation ∈ is transitive on α; the converse holds given clause 1, and fails without it. For α={{{∅}}} the relation {(x,y)∈α×α:x∈y} is empty, hence vacuously transitive, yet the sole element {{∅}} of α is not a transitive set, since {∅}∈{{∅}} while ∅∉{{∅}}. Under clause 1 the two readings do coincide, because then every member of a member of α again lies in α, where the relation has something to say. Neither clause implies the other, and both are needed.
  • Every ordinal is literally the set of all smaller ordinals. By clause 1 and the notation above, α={β:β<α}, so the ordinals carry their own order relation as membership. This is von Neumann's device, and it is what makes it unnecessary to define an order type as an equivalence class of well-orders: apart from the class of the empty well-order, which is the singleton {∅}, such a class is a proper class rather than a set, whereas the representative chosen here is always a set.
  • The natural numbers are ordinals, and so is ω. Each natural number is a transitive set (Every natural number is a transitive set and is not a member of itself), and on N membership coincides with the usual strict order, so each natural number and N=ω itself (The natural numbers N (von Neumann)) satisfy both clauses. Both facts are proved in ω is the least limit ordinal, where they are needed; they are recorded here because they are the intended picture.
  • The Axiom of Foundation is not used here. Some treatments define an ordinal as a transitive set linearly ordered by ∈, which is equivalent to the definition above only in the presence of Foundation (The Axiom of Foundation: ∀S (∃t (t∈S)→∃s (s∈S∧¬∃u (u∈s∧u∈S)))), since Foundation is what supplies the least element. The least element property is written into the definition instead, so nothing on this page depends on Foundation even though the library does state it as an axiom of ZFC.
  • The definition is absolute in a strong sense: whether a set is an ordinal depends only on its members and the membership relation among them, with no reference to any ambient construction. That is why ordinals can be used to index constructions in any model of ZF without further hypotheses.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-07-26 (claude-opus-5)Open item page →

Basic closure properties of ordinals

Statement

Let α and β be ordinals (Ordinal (von Neumann)). Then:

(a) every element of α is an ordinal;

(b) α∉α;

(c) α+=α∪{α} is an ordinal;

(d) if A is a nonempty set of ordinals then ⋂A is an ordinal;

(e) if A is any set of ordinals then ⋃A is an ordinal;

(f) α⊆β if and only if α∈β or α=β;

(g) any two ordinals are comparable under inclusion: α⊆β or β⊆α.

Everything here is a theorem of ZF and uses no choice principle.

Facts & Assumptions

Given: Ordinals α, β and, where stated, a set A all of whose members are ordinals. Claim (g) is not in the usual list of basic facts, but claim (e) needs it, so it is proved here rather than deferred; the trichotomy statement is then read off from it on the next item of this page.

[A1]

An ordinal is a transitive set on which ∈ is a strict well-order: irreflexive, transitive as a relation, trichotomous, and with a least element in every nonempty subset (Ordinal (von Neumann)).

[L1]

The restriction of a strict well-order to a subset is again a strict well-order, since totality and least elements are inherited by subsets (Well-order and well-ordered set).

Proof

technique · direct
1.1

Claim (a): let x∈α; then x⊆α by transitivity of α, so ∈ strictly well-orders x by [L1], and x is transitive, because z∈y∈x gives y∈α and z∈α by transitivity of α, whence z∈x by transitivity of the relation ∈ on α; so x is an ordinal.

A1L1
1.2

Claim (b): if α∈α then α is an element of α satisfying α∈α, contradicting irreflexivity of ∈ on α; hence α∉α.

A1
1.3

Claim (f), the easy direction: α∈β gives α⊆β by transitivity of β, and α=β gives α⊆β trivially.

A1
2.1

Claim (f), the substantial direction: assume α⊆β and α≠β, let γ be the ∈-least element of the nonempty set β∖α⊆β, and check γ=α; indeed δ∈γ forces δ∈β by transitivity of β and then δ∈α, since otherwise δ∈β∖α with δ∈γ contradicts minimality, so γ⊆α; conversely δ∈α⊆β compared with γ by trichotomy in β cannot satisfy δ=γ or γ∈δ, since each would put γ∈α, using transitivity of α in the second case, so δ∈γ and α⊆γ; hence α=γ∈β.

step 1.3A1
2.2

Claim (c): α+ is transitive, because x∈α+ means x∈α, whence x⊆α⊆α+, or x=α⊆α+; the relation ∈ is irreflexive on α+ by [A1] and step 1.2, transitive there because x∈y∈z with z=α gives x∈y⊆α=z and with z∈α reduces to transitivity in α, and trichotomous there because two elements of α are comparable in α while x∈α satisfies x∈α and neither α∈x nor x=α, both of which would give α∈α; finally a nonempty S⊆α+ has an ∈-least element, namely the ∈-least element of S∩α when that is nonempty and α otherwise.

step 1.2step 1.1A1
2.3

Claim (d): ⋂A is transitive, since x∈⋂A gives x∈δ and hence x⊆δ for every δ∈A, so x⊆⋂A; and ⋂A is a subset of any fixed member of the nonempty set A, so ∈ strictly well-orders it by [L1].

step 1.1A1L1
3.1

Claim (g): γ=α∩β is an ordinal by claim (d) applied to {α,β}, and γ⊆α and γ⊆β, so claim (f) gives γ∈α or γ=α, and likewise for β; both memberships at once would give γ∈α∩β=γ, contradicting claim (b), so γ=α or γ=β, that is α⊆β or β⊆α.

step 2.3step 2.1step 1.3step 1.2
4.1

Claim (e): ⋃A is transitive, since x∈δ∈A gives x⊆δ⊆⋃A; its elements are ordinals by claim (a), so ∈ is irreflexive on it by claim (b) and transitive on it because x∈y∈z with z∈δ∈A puts x,y,z all in the ordinal δ; any two of its elements lie in a common member of A by claim (g) and are therefore comparable, which gives trichotomy by claim (b) and claim (f); and a nonempty S⊆⋃A has an ∈-least element, namely the ∈-least element of S∩δ for any δ∈A meeting S, since an element of S lying ∈-below it would lie in δ by transitivity and contradict minimality.

step 3.1step 1.1step 1.2step 2.1A1
5.1

Claims (a) to (g) are established.

step 1.1step 1.2step 1.3step 2.1step 2.2step 2.3step 3.1step 4.1∎

Remarks

The successor is the immediate successor. Claim (c) makes α+ an ordinal, and it is the least ordinal strictly above α: any γ with α∈γ satisfies α+⊆γ, hence α+≤γ by claim (f). So the ordinals have no gaps immediately above a given point, which is what makes the successor and limit dichotomy of Successor and limit ordinals exhaustive.

Suprema come for free. Claim (e) says a set of ordinals always has a least upper bound, namely ⋃A: it contains every member of A as a subset, hence lies weakly above each by claim (f), and any ordinal weakly above all of them contains ⋃A. Claim (d) gives the dual statement for a nonempty set. Neither needs any completeness assumption, in sharp contrast with the situation for R.

Nonemptiness in claim (d) is essential. The intersection of the empty family is not a set, so the hypothesis cannot be dropped. The union of the empty family, by contrast, is ∅=0, which is why claim (e) needs no such hypothesis.

Claim (g) is a departure from the usual bookkeeping. It is normally derived alongside trichotomy. It is proved here because claim (e) cannot be proved without it, and separating them would either duplicate the argument or create a circular dependency between this lemma and Trichotomy and well-ordering of the ordinals.

The naturals are the model case. Every natural number is a transitive set and satisfies n∉n (Every natural number is a transitive set and is not a member of itself), which is exactly claims (a) and (b) in the situation this definition abstracts, and σ(n)=n∪{n} is the successor operation of claim (c). That every natural number, and ω itself, really is an ordinal is proved in ω is the least limit ordinal.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Trichotomy and well-ordering of the ordinals

Statement

For ordinals α and β (Ordinal (von Neumann)), exactly one of

α∈β,α=β,β∈α

holds. Moreover every nonempty set A of ordinals has an ∈-least element, and consequently A ordered by α≤β:  ⟺  α⊆β is a well-order (Well-order and well-ordered set) whose strict part is membership.

So the ordinals are linearly ordered by ∈, every set of them is well ordered, and Transfinite induction is available on any such set. No choice principle is used.

Facts & Assumptions

Given: Ordinals α, β, and a nonempty set A whose members are all ordinals.

[A1]

An ordinal is a transitive set on which ∈ is a strict well-order (Ordinal (von Neumann)).

[L1]

Every element of an ordinal is an ordinal; α∉α; α⊆β if and only if α∈β or α=β; and any two ordinals are comparable under inclusion (Basic closure properties of ordinals).

[L2]

A partial order is a reflexive, antisymmetric and transitive relation; a total order is a partial order any two of whose elements are comparable; and the strict part of ≤ is x<y:  ⟺  (x≤y and x≠y) (Partial order and partially ordered set).

[L3]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

[L4]

Transfinite induction holds on every well-order (Transfinite induction).

Proof

technique · direct
1.1

At least one alternative holds: by [L1] either α⊆β or β⊆α, and in the first case [L1] gives α∈β or α=β, in the second β∈α or β=α.

L1
2.1

At most one alternative holds: α∈β together with α=β gives α∈α; β∈α together with α=β gives α∈α; and α∈β together with β∈α gives β⊆α by transitivity of α and hence α∈α; each contradicts [L1].

step 1.1A1L1
3.1

Least elements: fix α∈A; if α∩A=∅ then α is ∈-least in A, because β∈A with β∈α would lie in α∩A, so trichotomy leaves α∈β or α=β; otherwise α∩A is a nonempty subset of α and has an ∈-least element γ there, and γ is ∈-least in A, because β∈A with β∈γ would satisfy β∈α by transitivity of α and so lie in α∩A strictly below γ, and trichotomy again leaves γ∈β or γ=β.

step 1.1step 2.1A1L1
4.1

On A the relation α≤β:  ⟺  α⊆β satisfies the three axioms of [L2], since inclusion is reflexive, antisymmetric by extensionality, and transitive, so it is a partial order; it is total by [L1] and step 1.1; its strict part in the sense of [L2] is membership, since α⊆β with α≠β is α∈β by [L1]; and every nonempty subset of A has a least element by step 3.1, so (A,⊆) is a well-order in the sense of [L3] and [L4] applies to it.

step 1.1step 3.1L1L2L3L4
5.1

Exactly one of the three alternatives holds, every nonempty set of ordinals has an ∈-least element, and every set of ordinals is well ordered by inclusion.

step 2.1step 3.1step 4.1∎

Remarks

Why this is not circular. The trichotomy of ∈ on a single ordinal is part of Ordinal (von Neumann); what is proved here is trichotomy between arbitrary ordinals, which is a statement about the whole class and not about any one set. The bridge is inclusion comparability, proved in Basic closure properties of ordinals by intersecting the two ordinals, and the intersection argument is where the two levels meet.

The class of ordinals behaves like a well-order without being a set. Every nonempty set of ordinals has a least element, and in fact so does every nonempty definable collection of them: if φ(α) holds for some α, apply the statement to the set {ξ∈α+:φ(ξ)}, which is nonempty. That the collection of all ordinals is nevertheless not a set is Burali-Forti: there is no set of all ordinals.

A set of ordinals need not be an ordinal. Well-ordering by ∈ is only half of the definition; transitivity is the other half. The set {1,3}, that is {{∅},{∅,{∅},{∅,{∅}}}}, is well ordered by membership but is not transitive, so it is not an ordinal. A transitive set of ordinals is one, which is the form in which this lemma gets used in Every well-order has a unique order type and Hartogs: an ordinal that does not inject into a given set.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

Burali-Forti: there is no set of all ordinals

Statement

There is no set whose members are exactly the ordinals (Ordinal (von Neumann)). More strongly, no set has every ordinal as a member: the ordinals form a proper class.

Facts & Assumptions

Given: The axioms of ZF, in particular the Separation schema. No choice principle is used.

[A1]

Separation: for every set X and every formula φ, the collection {x∈X:φ(x)} is a set.

[L1]

An ordinal is a transitive set on which ∈ is a strict well-order (Ordinal (von Neumann)).

[L2]

Every element of an ordinal is an ordinal, and α∉α for every ordinal α (Basic closure properties of ordinals).

[L3]

Any two ordinals satisfy exactly one of α∈β, α=β, β∈α, and every nonempty set of ordinals has an ∈-least element (Trichotomy and well-ordering of the ordinals).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that some set X has every ordinal as a member.

assume-contra
2.1

By Separation, Ω={x∈X:x is an ordinal} is a set, and by the supposition its members are exactly the ordinals.

step 1.1A1
3.1

Ω is a transitive set: if α∈Ω and x∈α then x is an ordinal, hence x∈Ω; so α⊆Ω.

step 2.1L2
3.2

The relation ∈ is a strict well-order of Ω: it is irreflexive there because α∉α for ordinals, transitive there because x∈y∈z with z an ordinal gives y⊆z and so x∈z, trichotomous there by [L3], and every nonempty subset of Ω is a nonempty set of ordinals and so has an ∈-least element.

step 2.1L1L2L3
4.1

Hence Ω is an ordinal, so Ω∈Ω by step 2.1, contradicting Ω∉Ω; therefore no set has every ordinal as a member, and in particular there is no set of all ordinals.

step 3.1step 3.2step 2.1L1L2discharge-contradiction∎

Remarks

Why this is a theorem and not a paradox. In naive set theory the same computation is a contradiction, because unrestricted comprehension guarantees that the ordinals form a set. In ZF, Separation only carves subsets out of sets already given, so the argument instead refutes the assumption that some set collects them all. The historical statement, Burali-Forti 1897, predates that distinction, which is why it is remembered as a paradox.

Nothing about size is being said. The obstruction is not that there are "too many" ordinals in any measurable sense; it is that the supposed set would be transitive and well ordered by membership, which are exactly the two clauses of Ordinal (von Neumann), so it would have to be one of its own members. The same shape of argument shows there is no set of all sets.

Consequences used later. Since no set contains all ordinals, for any set A there must be ordinals lying outside every construction indexed by A, which is the crude form of the fact sharpened by Hartogs: an ordinal that does not inject into a given set. The false statement this theorem refutes is recorded as FALSE: the ordinals form a set.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Every well-order has a unique order type

Statement

Every well-order (W,<) (Well-order and well-ordered set) is order isomorphic (Order embedding and order isomorphism) to exactly one ordinal (Ordinal (von Neumann)), called its order type and written ot(W).

The isomorphism is the collapsing map F(a)={F(b):b<a}, and it is unique as well, by rigidity (Rigidity of well-orders).

This uses Replacement, and no form of the Axiom of Choice.

Facts & Assumptions

Given: A well-order (W,<) and the axioms of ZF, in particular Replacement. No choice principle is assumed.

[A1]

The axioms of ZF, in particular Replacement and Union, are available.

[L1]

Transfinite recursion: for a class function G there is a unique F on W with F(a)=G(F↾W<a) for all a (Transfinite recursion).

[L2]

Transfinite induction on (W,<) (Transfinite induction).

[L3]

An ordinal is a transitive set on which ∈ is a strict well-order (Ordinal (von Neumann)), and W<a={x∈W:x<a} (Initial segment of a well-order).

[L4]

Every element of an ordinal is an ordinal, α∉α, and α⊆β if and only if α∈β or α=β (Basic closure properties of ordinals).

[L5]

Any two ordinals satisfy exactly one of α∈β, α=β, β∈α, and every set of ordinals is well ordered by ∈ (Trichotomy and well-ordering of the ordinals).

[L6]

No well-order is order isomorphic to a proper initial segment of itself (Rigidity of well-orders).

Proof

technique · direct
1.1

Apply [L1] with the class function G(h)=ran(h) to obtain the unique function F on W with F(a)={F(b):b<a} for every a∈W.

L1L3construct
2.1

Every value F(a) is an ordinal, by transfinite induction: assume F(b) is an ordinal for every b<a; then F(a) is a set of ordinals by Replacement, it is transitive because F(b)={F(c):c<b}⊆F(a) whenever b<a, and ∈ well-orders it by [L5]; so F(a) is an ordinal.

step 1.1L2L5L3A1
2.2

If b<a then F(b)∈F(a), immediately from the defining equation.

step 1.1
3.1

Conversely F(b)∈F(a) forces b<a: otherwise a=b, giving F(a)∈F(a), or a<b, giving F(a)∈F(b) and hence both F(a)∈F(b) and F(b)∈F(a); each alternative contradicts [L4] or [L5].

step 2.2step 2.1L4L5
3.2

The set α={F(a):a∈W} exists by Replacement and is an ordinal: it is a set of ordinals by step 2.1, it is transitive because x∈F(a) means x=F(b) for some b<a and hence x∈α, and ∈ well-orders it by [L5].

step 2.1step 1.1L5L3A1
4.1

F is therefore a bijection from W onto α with b<a  ⟺  F(b)∈F(a), that is an order isomorphism of (W,<) onto the ordinal α ordered by membership; injectivity holds because b≠a gives b<a or a<b by trichotomy in W, hence F(b)∈F(a) or F(a)∈F(b), and F(a)∉F(a) rules out equality.

step 2.2step 3.1step 3.2L4L5
5.1

Uniqueness: suppose W≅α and W≅β with α≠β ordinals; then α≅β, and by [L5] one is a member of the other, say α∈β, so α⊆β by [L4] and α is the initial segment of β determined by α, making β order isomorphic to a proper initial segment of itself, which [L6] forbids.

step 4.1L4L5L6
6.1

Every well-order is order isomorphic to exactly one ordinal, its order type.

step 4.1step 5.1∎

Remarks

Replacement is the whole cost. The values F(a) are not subsets of any set given in advance, so Separation cannot collect them; steps 2.1 and 3.2 both invoke Replacement, exactly as Transfinite recursion does. In Zermelo set theory, which has Separation but not Replacement, the theorem fails, and the standard witness is explicit: Vω+ω satisfies Zermelo set theory, its ordinals are exactly the ordinals below ω+ω, and it contains relations on ω of order type ω⋅2, which no ordinal of the model is isomorphic to. That model is built inside ZF, so this failure carries no consistency hypothesis; it is quoted from the references below and is not proved here, since Zermelo set theory is nowhere developed in this library.

No choice, and the reason is again uniqueness. Nothing is ever selected: F is produced by recursion from a formula, and the ordinal it lands on is determined. This is what makes order type a choice-free notion, in contrast with cardinality, which needs The well-ordering theorem and hence the Axiom of Choice to be defined for an arbitrary set.

Comparability, restated. With order types available, Comparability of well-orders says exactly that the order types of two well-orders are comparable as ordinals, which is Trichotomy and well-ordering of the ordinals transported back along the collapse. Either lemma can be derived from the other, and both are proved here without choice.

The name. The general Mostowski collapse takes any well-founded extensional relation to a transitive set. The case proved here, a well-order collapsing to an ordinal, is the only one this library needs, and it is stated in that form to avoid introducing well-founded relations before they are used.

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-07-26 (claude-opus-5)Open item page →

Successor and limit ordinals

Definition

Let α be an ordinal (Ordinal (von Neumann)).

  • α is a successor ordinal when α=β+=β∪{β} for some ordinal β, which is then an ordinal by Basic closure properties of ordinals;
  • α is a limit ordinal when α≠0 and α is not a successor ordinal.

Every ordinal is therefore exactly one of: 0, a successor ordinal, or a limit ordinal. The three cases are the three clauses of a definition or a proof by transfinite recursion or induction over the ordinals.

Remarks

  • The predecessor of a successor is unique. If α=β+ then β∈α and every ξ∈α satisfies ξ≤β, so β is the largest element of α and is determined by α. In particular β+=γ+ forces β=γ.
  • Union characterisation. For a nonzero ordinal α: α is a limit ordinal if and only if α=⋃α, and α is a successor if and only if ⋃α∈α, in which case α=(⋃α)+. For the successor case, ⋃(β∪{β})=(⋃β)∪β=β, because ⋃β⊆β by transitivity. For the limit case, ⋃α⊆α always holds by transitivity, and conversely, given ξ∈α, the ordinal ξ+ satisfies ξ+∈α: by Trichotomy and well-ordering of the ordinals the alternatives are ξ+=α, excluded because α is not a successor, and α∈ξ+, which gives α∈ξ or α=ξ and hence α∈α using ξ∈α and transitivity, excluded by Basic closure properties of ordinals; so ξ∈ξ+∈α puts ξ∈⋃α. The hypothesis α≠0 cannot be dropped, since ⋃0=0.
  • Closure under successor. The previous paragraph says exactly that a nonzero ordinal is a limit if and only if it is closed under the successor operation. That is the form in which limit ordinals are recognised in practice.
  • 0 is not a limit ordinal here. Some texts include it, so that "limit ordinal" means "α=⋃α" outright. The convention adopted is the more widely used one, and it is the one that makes "0, successor, limit" a genuine three way split.
  • The least limit ordinal is ω (ω is the least limit ordinal), so the distinction is invisible below ω: every natural number is either 0 or a successor. That is precisely why ordinary induction on N needs only a base case and a successor step, while induction over the ordinals needs a limit clause as well.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

ω is the least limit ordinal

Statement

Let N=ω be the natural numbers (The natural numbers N (von Neumann)) with their usual order (Order on the natural numbers). Then:

(i) for all m,n∈N, m∈n if and only if m<n;

(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 0 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: N=ω with 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)), and the order m≤n  ⟺  ∃k (m+k=n), m<n  ⟺  (m≤n and m≠n) (Order on the natural numbers).

[L1]

ω is inductive, that is 0∈ω and n∈ω⇒σ(n)∈ω, and ω is contained in every inductive set (The natural numbers exist: a smallest inductive set).

[L2]

The induction principle: a subset of N containing 0 and closed under σ equals N (The principle of mathematical induction).

[L3]

m<n  ⟺  σ(m)≤n (Discreteness: σ(n) is the immediate successor).

[L4]

≤ is a linear order on N with trichotomy, and 0≤m for every m because 0+m=m (≤ is a linear order on N, Trichotomy of the order on N, Left identity for addition).

[L5]

Every nonempty subset of N has a least element (The well-ordering principle).

[L6]

Every natural number is a transitive set and satisfies n∉n (Every natural number is a transitive set and is not a member of itself).

[L7]

Every nonzero natural number is σ(m) for some natural number m (Every nonzero natural number is a successor).

[L8]

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).

[L9]

n<σ(n) for every n∈N. This is established at step 1.3 of Trichotomy of the order on N, where it is derived from n+σ(0)=σ(n) and σ(0)≠0; the reference is to that item's numbering, not to any step below.

[L10]

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

technique · direct
1.1

For all m,n∈N, m≤n if and only if m<σ(n): from m≤n and n<σ(n) ([L9]) transitivity gives m<σ(n); conversely if m<σ(n) and m≤n failed, then n<m by trichotomy, so σ(n)≤m<σ(n) by [L3], which is impossible.

L3L4L9
1.2

ω is a transitive set: the set S={n∈ω:n⊆ω} contains 0=∅ and is closed under σ, since n⊆ω together with n∈ω gives σ(n)=n∪{n}⊆ω; so S=ω by [L2].

L2L1
2.1

Claim (i): the set T={n∈ω:m∈n  ⟺  m<n for every m∈ω} contains 0, because m∈∅ is false and m<0 is false, since 0≤m always and m<0 would give m=0 by antisymmetry and then m<m; and n∈T gives σ(n)∈T, because m∈σ(n)  ⟺  (m∈n or m=n)  ⟺  (m<n or m=n)  ⟺  m≤n  ⟺  m<σ(n); hence T=ω by [L2].

step 1.1L2L4
3.1

Claim (ii) for natural numbers: fix n∈ω; then n 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 n by [L4] and every nonempty subset of n has an ∈-least element by [L5]; hence n is an ordinal.

step 1.2step 2.1L4L5L6L8
3.2

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.

step 1.2step 2.1L4L5L8
4.1

Claim (iii): ω≠0 because 0∈ω; 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.

step 3.2L1L8
5.1

Claim (iv), first half: the ordinals α with α∈ω are exactly the natural numbers, each of which is 0 or of the form σ(m)=m+ with m a natural number by [L7], hence 0 or a successor ordinal; so no ordinal ∈-below ω is a limit ordinal.

step 3.1step 4.1L7L8
6.1

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 0 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.

step 5.1step 4.1step 3.2L8L10
7.1

Claims (i) to (iv) are established.

step 2.1step 3.1step 3.2step 4.1step 5.1step 6.1∎

Remarks

Why claim (i) has to be proved. The published development builds the order on N 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 n, 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 0 or a successor. This is the precise sense in which N 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 W=ω.

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: 0∈γ, 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 0 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 ω=⋃{n:n∈ω}.

Ordinal arithmetic is not developed here. Sums and products of ordinals, and the ordinals ω+1, ω⋅2 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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Hartogs: an ordinal that does not inject into a given set

Statement

For every set A there is an ordinal (Ordinal (von Neumann)) that does not inject into A, that is, admits no injective function into A. The least such ordinal is the Hartogs number ℵ(A), and it is exactly

ℵ(A)={ot(S,R):S⊆A and R well-orders S},

the set of order types (Every well-order has a unique order type) of the well-ordered subsets of A.

The proof is choice free. That is the whole point of the theorem: in ZF alone, with no assumption that A can be well ordered, one still gets an ordinal too long to be laid inside A.

Facts & Assumptions

Given: A set A and the axioms of ZF, in particular Power Set, Separation, Union and Replacement. No choice principle is assumed. "X injects into A" abbreviates "there is an injective function X→A".

[A1]

Power Set, Separation, Union and Replacement are available.

[L1]

Every well-order is order isomorphic to a unique ordinal, its order type, and the isomorphism is unique (Every well-order has a unique order type).

[L2]

An ordinal is a transitive set on which ∈ is a strict well-order (Ordinal (von Neumann)).

[L3]

Every element of an ordinal is an ordinal, no ordinal is a member of itself, and α⊆β if and only if α∈β or α=β (Basic closure properties of ordinals).

[L4]

Any two ordinals satisfy exactly one of α∈β, α=β, β∈α, and every set of ordinals is well ordered by ∈ (Trichotomy and well-ordering of the ordinals).

[L5]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set); an order isomorphism carries the initial segment below a point onto the initial segment below its image (Order embedding and order isomorphism, Initial segment of a well-order).

Proof

technique · contradiction
1.1

By Power Set and Separation the collection W={(S,R)∈P(A)×P(A×A):R well-orders S} is a set, since every well-order of a subset of A is a subset of A×A.

A1L5construct
2.1

Each (S,R)∈W has a unique order type ot(S,R) by [L1], so the assignment is given by a formula and Replacement makes H={ot(S,R):(S,R)∈W} a set of ordinals; uniqueness is what makes this a definable function, so nothing is selected.

step 1.1L1A1construct
3.1

H is a transitive set: let α=ot(S,R)∈H with order isomorphism g from α onto (S,R), and let β∈α; then β is an ordinal with β⊆α, so β is the initial segment of α below β, and g carries it onto an R-initial segment S′⊆S, which R′=R∩(S′×S′) well-orders with order type β; hence (S′,R′)∈W and β∈H.

step 2.1L1L3L5
3.2

Every α∈H injects into A: writing α=ot(S,R), the order isomorphism from α onto S is in particular an injection of α into S⊆A.

step 2.1L1
4.1

H is an ordinal: it is transitive by step 3.1 and ∈ strictly well-orders it by [L4], since it is a set of ordinals.

step 3.1step 2.1L2L4
5.1

Suppose, for contradiction, that the ordinal H of step 4.1 injects into A, say by an injective j:H→A.

step 4.1assume-contra
6.1

Put S=j[H]⊆A and R={(j(ξ),j(η)):ξ∈η∈H}⊆A×A; then j is a bijection of H onto S carrying membership to R, so R well-orders S and j is an order isomorphism from (H,∈) onto (S,R).

step 5.1step 4.1L5construct
7.1

Hence (S,R)∈W and ot(S,R)=H by the uniqueness in [L1], so H∈H, which no ordinal satisfies; therefore H does not inject into A, and since every member of H does inject into A by step 3.2, trichotomy leaves H≤γ for every ordinal γ that fails to inject, so H=ℵ(A) is the least such ordinal.

step 6.1step 1.1step 2.1step 3.2step 4.1L1L3L4discharge-contradiction∎

Remarks

Where choice would have crept in, and why it does not. A careless proof says "for each well-orderable subset of A choose a well-ordering of it", which is a genuine use of choice. The construction above never chooses: it collects all pairs (S,R), so the well-ordering is part of the datum, and it then maps each pair to its order type, which is unique by Every well-order has a unique order type. The passage from a class of well-orders to a set of ordinals is Replacement, not choice.

What the theorem does and does not say. It does not say A can be well ordered, and it gives no injection of A into an ordinal. It says only that the ordinals run out of room to sit inside A. Under the Axiom of Choice, A is well orderable (The well-ordering theorem) and ℵ(A) is the least ordinal that does not inject into A, that is the least cardinal strictly larger than the cardinality of A -- not merely the least ordinal strictly larger than an ordinal equinumerous with A, since for A=N that would be ω+1, which still injects into N; without choice, ℵ(A) may be incomparable with A in size, and that is still enough for the applications.

The ZF substitute for cardinal comparability. "Any two sets are comparable in size" is equivalent to the Axiom of Choice, so it is unavailable here. What survives is this theorem together with Comparability of well-orders: well-orders are always comparable, and every set has an ordinal it cannot absorb. Hartogs proved in 1915 that cardinal comparability implies the well-ordering theorem, and this construction is the engine of that proof.

A crude bound is not enough. Burali-Forti: there is no set of all ordinals already shows that the ordinals are not a set, so no set can contain them all, but that alone does not produce a single ordinal failing to inject into a given A. The content here is that the failure happens at a definable, and indeed least, place.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The well-ordering theorem

Statement

Assume the Axiom of Choice (The Axiom of Choice). Then every set X can be well ordered: there is a relation on X making it a well-ordered set (Well-order and well-ordered set).

The Axiom of Choice is used only inside Zorn's lemma, and nowhere else in the argument below.

Facts & Assumptions

Given: A set X, the axioms of ZF, and the Axiom of Choice. Write (B,R)⪯(B′,R′) for end extension: B⊆B′, the relation R′ restricted to B is R, and B is an initial segment of (B′,R′).

[A1]

Every family of nonempty sets has a choice function (The Axiom of Choice).

[L1]

Zorn's lemma: a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).

[L2]

A partial order is reflexive, antisymmetric and transitive, and its strict part is x<y meaning x≤y with x≠y (Partial order and partially ordered set).

[L3]

A chain is a subset any two of whose elements are comparable, and the empty set is a chain (Chain in a poset).

[L4]

An upper bound of a subset is an element weakly above every member of it (Upper bound, least upper bound, and strict upper bound).

[L5]

A maximal element has nothing strictly above it (Maximal element and greatest element).

[L6]

A well-order is given in two interchangeable presentations, and the two determine each other (Well-order and well-ordered set): weakly, as a total order ≤ in which every nonempty subset has a least element; strictly, as a relation < that is irreflexive, transitive and trichotomous and in which every nonempty subset S has an element ℓ with no s∈S satisfying s<ℓ. This proof uses the strict presentation throughout, as does Initial segment of a well-order; the end-extension order ⪯ on P below is a separate relation and is weak, since Zorn's lemma is about partial orders.

[L7]

An initial segment is a downward closed subset (Initial segment of a well-order).

Proof

technique · direct
1.1

Let P be the collection of pairs (B,R) with B⊆X and R⊆B×B a strict well-order of B; this is a set by Power Set and Separation applied to P(X)×P(X×X), and it is nonempty because (∅,∅)∈P.

L6construct
2.1

Order P by end extension; this relation is reflexive, transitive, and antisymmetric, since mutual end extension forces the underlying sets and relations to coincide, so (P,⪯) is a poset.

step 1.1L2L7construct
3.1

The empty chain has an upper bound in P, namely (∅,∅), so the hypothesis of Zorn's lemma is not vacuous at the bottom.

step 1.1step 2.1L3L4
3.2

Let C⊆P be a nonempty chain and put B∗=⋃{B:(B,R)∈C} and R∗=⋃{R:(B,R)∈C}.

step 2.1L3construct
4.1

R∗ is a strict total order on B∗: any two elements of B∗ lie in members of C one of which end extends the other, hence lie together in the larger member and are comparable there, and the comparisons made in different members agree, because along the chain each relation is the restriction of every larger one.

step 3.2step 2.1L2L3
5.1

R∗ well-orders B∗: given ∅≠S⊆B∗, choose a member (B,R) of C meeting S and let ℓ be the R-least element of S∩B; if some t∈S satisfied tR∗ℓ then t and ℓ would lie in a common member (B′,R′) of C, and either (B′,R′)⪯(B,R), giving t∈B′⊆B, or (B,R)⪯(B′,R′), in which case B is an initial segment of (B′,R′) and tR′ℓ∈B again gives t∈B; either way t∈S∩B with tRℓ, contradicting minimality of ℓ.

step 4.1step 3.2step 2.1L6L7
6.1

Hence (B∗,R∗)∈P, and it end extends every member of C: the inclusions and restrictions are immediate, and B is an initial segment of (B∗,R∗) by the case analysis of step 5.1; so every nonempty chain has an upper bound.

step 5.1step 4.1step 2.1L4L7
7.1

Zorn's lemma applies to the nonempty poset (P,⪯), in which every chain has an upper bound, and yields a maximal element (M,RM); this is the one and only place the Axiom of Choice is spent, and it is spent inside Zorn's lemma.

step 6.1step 3.1step 1.1L1L5A1
8.1

M=X: otherwise there is x∈X∖M, and putting M′=M∪{x} with R′=RM∪{(m,x):m∈M} gives a well-order of M′, because a nonempty S⊆M′ has as least element the RM-least element of S∩M when that is nonempty and x otherwise, while (M,RM)⪯(M′,R′) with M≠M′ contradicts the maximality of (M,RM).

step 7.1L5L6L7
9.1

Therefore RM is a well-order of M=X, and X can be well ordered.

step 8.1step 7.1∎

Remarks

Where the Axiom of Choice is. Only in step 7.1, and only through Zorn's lemma, whose proof spends it exactly once. Everything else here is plain ZF: forming P is Power Set and Separation, and the chain bound is a union. The word "choose" in step 5.1 names one object whose existence has just been asserted, which is ordinary existential instantiation and not a choice principle; a choice principle is needed only when infinitely many such namings must be made at once. This bookkeeping is the reason Zorn is proved as a separate item rather than inlined.

End extension is doing real work. Ordering P merely by "R is the restriction of R′" is not enough. Without the requirement that B be an initial segment of B′, a union of a chain of well-orders can fail to be a well-order, because a set S could keep acquiring smaller elements as one moves up the chain and end with no least element. Step 5.1 is exactly the point where initial segments rule that out.

Maximal, not greatest. Zorn's lemma concludes that a maximal element exists, never that a greatest one does, and maximal does not imply greatest (FALSE: every maximal element is a greatest element). The argument is arranged so that maximality suffices: step 8.1 shows a maximal well-ordered piece cannot omit a point, because a point could always be appended on top.

The converse holds. Every set being well orderable implies the Axiom of Choice (The well-ordering theorem implies the Axiom of Choice), so the two are equivalent over ZF, as is Zorn's lemma (Choice, Zorn and well-ordering are equivalent). This equivalence is all that the present proof uses; independence from ZF is a later theorem requiring additional machinery.

Zermelo 1904. The original proof does not go through Zorn's lemma; it uses a choice function on P(X)∖{∅} directly and builds the well-order by transfinite recursion (Transfinite recursion), taking at each stage the chosen element of the set of points not yet used. That route is available here too, and it makes the use of choice even more visible: one choice function, consulted at every stage.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The well-ordering theorem implies the Axiom of Choice

Statement

Work in ZF and assume that every set can be well ordered (Well-order and well-ordered set). Then the Axiom of Choice holds (The Axiom of Choice): every family of nonempty sets has a choice function (Choice function).

Facts & Assumptions

Given: The axioms of ZF together with the hypothesis that every set carries a well-order. Let F be an arbitrary family of nonempty sets.

[A1]

By the Given, every set carries a well-order.

[L1]

A choice function for F is a function g on F with g(S)∈S for every S∈F (Choice function).

[L2]

The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

[L3]

In a well-order every nonempty subset has a least element, and that least element is unique (Well-order and well-ordered set).

Proof

technique · direct
1.1

Let U=⋃F, which is a set by the Union axiom of ZF, available by the Given, and note that every member of F is a subset of U.

givenconstruct
2.1

By hypothesis there is a well-order < on U; fix one.

step 1.1A1choose
3.1

Every S∈F is a nonempty subset of U, so it has a least element with respect to <, and that element is unique.

step 2.1step 1.1L3
4.1

Hence g={(S,y)∈F×U:y is the <-least element of S} is a function on F with g(S)∈S for every S, since uniqueness in step 3.1 gives exactly one y for each S.

step 3.1L1
5.1

So g is a choice function for F, and since F was an arbitrary family of nonempty sets, the Axiom of Choice holds.

step 4.1L1L2∎

Remarks

One well-order, then no more choosing. The single act of naming a well-order of U in step 2.1 is an existential instantiation, not a choice principle: one object is named, not one per member of F. After that, the rule "take the least element" is canonical, and the resulting g is a set by Separation on F×U. That is the entire content of the implication, and it is why "well order the union" is the standard way to manufacture choice functions.

The same trick, free of charge, on N. Nothing above needs the hypothesis when U already carries a canonical well-order. Every family of nonempty subsets of N has the explicit choice function S↦min⁡S, by The well-ordering principle, with no axiom at all. The Axiom of Choice is exactly the assertion that this convenience is always available.

Direction matters. This item proves one implication only. The converse, that the Axiom of Choice yields a well-order of every set, is The well-ordering theorem and is the harder half; the two together give the equivalence recorded in Choice, Zorn and well-ordering are equivalent.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Choice, Zorn and well-ordering are equivalent

Statement

Over ZF the following three statements are equivalent:

(1) the Axiom of Choice (The Axiom of Choice);

(2) Zorn's lemma;

(3) the well-ordering theorem, that every set can be well ordered.

Facts & Assumptions

Given: The axioms of ZF. Each implication below is itself a theorem of ZF, so what is established here is an equivalence proved in ZF, with no appeal to any further principle. Read it exactly that way: ZF proves each of (1), (2), and (3) to follow from the others. The equivalence alone does not say that ZF proves any one of them outright.

[L1]

The Axiom of Choice implies that every set can be well ordered (The well-ordering theorem).

[L2]

If every set can be well ordered then the Axiom of Choice holds (The well-ordering theorem implies the Axiom of Choice).

[L3]

The Axiom of Choice and Zorn's lemma are equivalent over ZF (The Axiom of Choice and Zorn's lemma are equivalent).

[L4]

The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

Proof

technique · direct
1.1

Assuming (1), every set can be well ordered, which is (3).

L1
1.2

Assuming (3), every family of nonempty sets has a choice function, which is (1).

L2
2.1

Statements (1) and (3) therefore imply each other over ZF and are equivalent.

step 1.1step 1.2L4
3.1

Statements (1) and (2) are equivalent over ZF by [L3].

step 2.1L3
4.1

Equivalence is transitive, so (1), (2) and (3) are equivalent over ZF.

step 2.1step 3.1∎

Remarks

What this licenses. Any later result may be proved with whichever of the three forms is convenient, at exactly the same cost. Applications that build an object stage by stage naturally use (3) through Transfinite recursion; applications that maximise something naturally use (2); applications about products of nonempty sets use (1).

What is not proved here. No independence conclusion follows from an equivalence proof. Establishing models in which the equivalent principles hold or fail belongs to the later constructibility, forcing, and symmetric-model pages and is not a premise of this item.

Other principles get no information from this. The equivalence says nothing about the ultrafilter lemma, dependent choice, or countable choice. Every theorem using one of those principles must state the actual hypothesis; the locally established implication ledger is The proved choice ledger: hypotheses, equivalences, and upper bounds.

Historical note. Zermelo proved (1) implies (3) in 1904, Kuratowski and Zorn isolated (2) in 1922 and 1935, and the circle of equivalences was standard by the 1940s. The choice-free content of the theory of well-orders, by contrast, was settled earlier: Hartogs proved in 1915 that cardinal comparability implies (3), which is what makes Hartogs: an ordinal that does not inject into a given set a choice-free theorem worth isolating.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Cardinal (initial ordinal) and cardinality

Definition

Write X≈Y, and say X and Y are equinumerous, when there is a bijection X→Y.

An ordinal κ (Ordinal (von Neumann)) is a cardinal, equivalently an initial ordinal, when

no α∈κ satisfies α≈κ,

that is, κ is not equinumerous with any strictly smaller ordinal.

Cardinality, under the Axiom of Choice. Assume the Axiom of Choice (The Axiom of Choice) and let X be a set. Then X carries a well-order (The well-ordering theorem), which has an order type α (Every well-order has a unique order type) and in particular α≈X. Now α+=α∪{α} is an ordinal (Basic closure properties of ordinals, claim (c)) whose elements are ordinals (claim (a)) and which contains α, so C={ξ∈α+:ξ≈X} is a nonempty set of ordinals and has an ∈-least element κ (Trichotomy and well-ordering of the ordinals). This κ is the cardinality of X, written ∣X∣; it is a cardinal, because β∈κ with β≈κ≈X would lie in α+ and contradict the minimality of κ.

Well-definedness: κ does not depend on the well-order or on α. The recipe above instantiates a well-order of X and an order type α for it, and X will in general carry many well-orders with many different order types, so the value κ has to be shown independent of both. It is, because κ is in fact the least ordinal equinumerous with X outright, a description in which neither the well-order nor α appears. Let β be any ordinal with β≈X. By trichotomy for ordinals (Trichotomy and well-ordering of the ordinals) exactly one of β∈α+, β=α+, α+∈β holds. In the first case β∈C, so κ⊆β by minimality of κ. In the other two cases claim (f) of Basic closure properties of ordinals gives α+⊆β, and α∈α+ because α+=α∪{α}, so α∈β and hence α⊆β by claim (f) again; and α∈C, so κ⊆α by minimality, whence κ⊆β. In every case κ⊆β, that is κ≤β. So κ is the least element of the collection of all ordinals equinumerous with X, and any two runs of the recipe, from any two well-orders of X, return the same κ.

Remarks

  • What the well-definedness argument does and does not need. The obligation is that ∣X∣ depend on X alone, and it is discharged in the definition itself, from two lemmas that are genuine prerequisites of this item and therefore sit in deps rather than in justified_by: comparability and trichotomy of ordinals (Trichotomy and well-ordering of the ordinals) and the elementary closure facts (Basic closure properties of ordinals). Neither mentions cardinals, so neither points forward, and no separate discharging lemma is needed. The bound α+ is a device for turning "the least ordinal equinumerous with X" into a Separation instance over a set; the argument above is what shows that the device does not change the answer.

  • The definition is choice-free; the cardinality assignment is not. Being a cardinal is a property of an ordinal and needs no axiom beyond ZF. Attaching a cardinality to an arbitrary set is a different matter: a set that carries no well-order is equinumerous with no ordinal at all, so ∣X∣ simply does not exist for it. Without the Axiom of Choice there is no ordinal-valued notion of size for arbitrary sets, and what survives is Hartogs: an ordinal that does not inject into a given set: every set A has a smallest ordinal ℵ(A) that does not inject into it.

  • Most ordinals are not cardinals. The successor ω+=ω∪{ω} is equinumerous with ω∈ω+, by the explicit bijection sending ω to 0 and each natural number n to σ(n), which is a bijection because σ is injective and its image is exactly the nonzero natural numbers. So ω+ is an ordinal and not a cardinal, and the same shift applies to the successor of any ordinal containing ω. Cardinals are sparse among ordinals, which is precisely why the least one equinumerous with a given set is a useful representative.

  • Which ordinals up to and including ω are cardinals. Every natural number is a cardinal, and so is ω. Both facts are counting facts rather than order facts, and both come from the pigeonhole principle (The pigeonhole principle on N), proved on the countability page. Every natural number is an ordinal, and so is ω (ω is the least limit ordinal, claim (ii)); and if α∈n with n a natural number then α is itself a natural number, since N is a transitive set (On N the order is membership: m<n  ⟺  m∈n), with α<n by claim (i) of ω is the least limit ordinal. So if some α∈n had α≈n, claim 3 of the pigeonhole principle would force α=n and hence n∈n, which claim (b) of Basic closure properties of ordinals forbids; therefore n is a cardinal. And if some α∈ω had α≈ω, then α would be a natural number equinumerous with N=ω, which claim 4 of the pigeonhole principle forbids; therefore ω is a cardinal. Nothing else on this page depends on either fact, and the definition above is stated so that it does not.

  • Notation. The infinite cardinals are traditionally written ℵ0,ℵ1,…, with ℵ0=ω. That last equation can now be stated outright rather than quoted: it says ω is the least ordinal equinumerous with ω, which is precisely the assertion that ω is a cardinal, established in the previous remark from claim 4 of The pigeonhole principle on N. Nothing below rests on it. The notation ℵ(A) for the Hartogs number of A (Hartogs: an ordinal that does not inject into a given set) comes from the same source and is deliberately close: under the Axiom of Choice ℵ(A) is the successor cardinal of ∣A∣.

  • Why initial ordinals rather than equivalence classes. The natural definition of "cardinal" as the class of all sets equinumerous with a given one never yields a set, for the same reason as in Burali-Forti: there is no set of all ordinals. Choosing the least ordinal in the class is von Neumann's fix, and it works exactly when the class contains an ordinal, which is exactly when the set can be well ordered.

RemarkRemark: AI-adaptedProof: Not applicableverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The proved choice ledger: hypotheses, equivalences, and upper bounds

This ledger records only conclusions established by local proofs. It separates an assumption actually used by an argument from a claim about the weakest possible assumption, which usually needs additional model theory.

Equivalent formulations proved over ZF. The Axiom of Choice, Zorn's lemma, and the assertion that every set can be well ordered are equivalent by The Axiom of Choice and Zorn's lemma are equivalent and Choice, Zorn and well-ordering are equivalent. Thus a proof using any one of them may be translated into a proof using either of the others. This is an equivalence statement; it does not itself prove an independence result.

Where the supplied proofs spend full choice. Zorn's lemma uses The Axiom of Choice to select a strict upper bound for every chain that has no maximal member. Its structural fixed-point core, Bourbaki–Witt fixed point theorem, is choice-free. The well-ordering theorem then obtains a well-order through Zorn. The proof that every vector space has a basis similarly extends an independent set by Zorn (Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if L⊆S⊆V with L independent and span⁡(S)=V, there is a basis B of V with L⊆B⊆S, Every vector space has a basis). These routes establish AC as a sufficient hypothesis; they do not establish that every consequence needs AC.

Weaker hypotheses remain distinct in this ledger. Countable choice and dependent choice are separately stated principles (The Axiom of Countable Choice (ACω), The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain). A theorem using one must carry that exact assumption in its statement and proof. This item does not assert any unproved reverse implication or nonimplication among them.

Choice-free substitutes. Hartogs: an ordinal that does not inject into a given set gives, for every set A, an ordinal that does not inject into A, without comparing arbitrary sets. Comparability of well-orders compares already supplied well-orders without choosing well-orders for arbitrary sets. Transfinite induction and recursion likewise operate on a supplied well-order. These results are not weakened by the fact that assigning ∣A∣ to an arbitrary set requires a well-orderability hypothesis.

The later constructibility, forcing, Boolean-algebra, and symmetric-model pages are responsible for proving relative consistency and strictness claims. Until then, recorded external results are targets, never dependencies of this ledger or of any other Foundations item.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

FALSE: the ordinals form a set

Statement

FALSE. The ordinals (Ordinal (von Neumann)) form a set: there is a set Ω whose members are exactly the ordinals.

The claim is plausible because the ordinals look locally set sized. Every ordinal α is itself precisely the set of all ordinals below it, so every downward closed collection of ordinals that stops somewhere is a set, and it is tempting to conclude that the collection of all of them is a set as well. In ZF that inference is unavailable: Separation produces a set only as a subset of a set already in hand, and here there is no such ambient set to start from.

Facts & Assumptions

Given: The axioms of ZF, in particular Separation. No choice principle is used.

[A1]

Separation carves a subset out of a set already given; it never produces a set from a defining property alone.

[L1]

No set has every ordinal as a member (Burali-Forti: there is no set of all ordinals).

[L2]

Every element of an ordinal is an ordinal, and no ordinal is a member of itself (Basic closure properties of ordinals).

[L3]

An ordinal is a transitive set on which ∈ is a strict well-order, and α<β means α∈β (Ordinal (von Neumann)).

Refutation

technique · contradiction
1.1

Suppose the claim: there is a set Ω whose members are exactly the ordinals.

assume-contra
1.2

The source of the intuition is genuine but limited: by [L3] and [L2] each ordinal α equals {β:β<α}, so every collection of ordinals bounded above by some ordinal is a set, being a subset of that bound; by [A1] this says nothing about the unbounded collection of all ordinals.

A1L2L3
2.1

Under the supposition, Ω is a set having every ordinal as a member.

step 1.1
3.1

No such set exists: it would be transitive by [L2], since every element of an ordinal is an ordinal and so a member of it, and ∈ would strictly well-order it, so it would itself be an ordinal by [L3] and hence a member of itself, which [L2] forbids; this is exactly [L1].

step 2.1L1L2L3
4.1

Steps 2.1 and 3.1 are contradictory, so no set has the ordinals as its members: the ordinals form a proper class and the claim is false.

step 2.1step 3.1L1discharge-contradiction∎

Remarks

Bounded is not unbounded. The honest version of the intuition is: for every ordinal α, the ordinals below α form a set, namely α itself. Nothing in ZF upgrades a family of sets indexed by a proper class into one set, and the attempt to do so here is exactly what Burali-Forti: there is no set of all ordinals refutes.

The same trap, one level up. "The sets form a set" fails for a closely related reason, and "the cardinals form a set" fails because the cardinals (Cardinal (initial ordinal) and cardinality) are unbounded among the ordinals. In each case the correct statement replaces "set" by "proper class", which in ZF means a formula rather than an object.

What is still available. Nothing about the theory of ordinals needs them to form a set. Every construction on this page indexes by a set of ordinals, or by a single ordinal, or runs along an arbitrary well-order; Transfinite recursion and Hartogs: an ordinal that does not inject into a given set are both stated so that only sets are ever formed.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

FALSE: transfinite induction and recursion need the Axiom of Choice

Statement

FALSE. Transfinite induction (Transfinite induction) and transfinite recursion (Transfinite recursion) require the Axiom of Choice (The Axiom of Choice): arguments that run along a well-order past the finite stages are not available in ZF alone.

The claim is plausible because the constructions one meets first do cost the Axiom of Choice. Well ordering an arbitrary set, extending a linearly independent family to a basis, building a maximal object stage by stage: each of these is usually presented as a transfinite recursion, and each really does need choice. The confusion is about which half of the argument is expensive. It is never the recursion.

Facts & Assumptions

Given: The axioms of ZF. The two theorems named in the claim are proved earlier on this page, and the point at issue is which axioms those proofs consume.

[A1]

The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

[L1]

Transfinite induction is proved from a single property of the well-order, that every nonempty subset has a least element, with no selection anywhere (Transfinite induction).

[L2]

Transfinite recursion is proved from Separation, Union and Replacement, and at every stage the object used is the unique attempt with the given domain, so nothing is selected (Transfinite recursion).

[L3]

The place where this development genuinely spends the Axiom of Choice is Zorn's lemma (Zorn's lemma), consumed once inside the well-ordering theorem (The well-ordering theorem).

Refutation

technique · direct
1.1

By [L1], transfinite induction is a theorem of ZF: its proof takes the least element of the complement of the given set and derives a contradiction, and no family of sets is ever chosen from.

L1
1.2

By [L2], transfinite recursion is a theorem schema of ZF: Replacement collects the attempts, and uniqueness of the attempt with a given domain means the construction is determined rather than selected.

L2
2.1

Both principles are therefore available in ZF without any choice principle, so the claim is false.

step 1.1step 1.2A1
3.1

The correct diagnosis is that the recursion is never itself the cost: by [L2] it is a theorem schema of ZF for every class function given by a formula. What can cost the Axiom of Choice is obtaining that class function, which happens when its defining formula carries a parameter that ZF does not supply, or when ZF does not prove the formula total and functional. A formula whose only parameters are available in ZF, as with the order type assignment and the Hartogs construction on this page, gives a choice-free construction; the informal rule "at stage a take some element not yet used" becomes such a formula only after a choice function has been supplied as a parameter, and supplying it is exactly how the well-ordering theorem spends the axiom, whether through Zorn's lemma or through Zermelo's direct recursion along a choice function.

step 2.1A1L2L3
4.1

Transfinite induction and transfinite recursion are theorems of ZF, and the claim is refuted.

step 2.1step 3.1∎

Remarks

A useful test. Ask what the value at stage a is. If the answer is a definite description, "the least ordinal such that", "the order type of", "the union of the earlier values", and every object the description mentions is one ZF supplies, then the construction is choice-free. If the answer is "some element with the following property", and there is generally more than one, then a choice function is being used and must be paid for. The parameter clause is not decoration: "the element c picks from the set of points not yet used" is a perfectly definite description, and it is Zermelo's construction, whose whole cost is obtaining c.

Three choice-free constructions on this page. The collapsing map of Every well-order has a unique order type, the family of order types in Hartogs: an ordinal that does not inject into a given set, and the comparison map of Comparability of well-orders are all defined by formulas, which is why each is a ZF theorem. Their proofs say so explicitly, and the reason is always the same: rigidity of well-orders makes the relevant witnesses unique (Rigidity of well-orders).

Dependent choice is the usual hidden cost. A construction along N that picks an object at each step, using the previous one, needs the principle of dependent choice (DC). It is not transfinite recursion that costs this; it is the picking. Where DC sits is a separate question and a strictly metamathematical one: if ZF is consistent, then DC is not a theorem of ZF and DC does not imply the Axiom of Choice, so DC is then strictly between the two. Both separations are external results, established by forcing and permutation models, quoted from the references and proved nowhere in this library; the consistency hypothesis cannot be dropped and cannot be proved inside ZF. The refutation above needs none of this, because transfinite induction and transfinite recursion are outright theorems of ZF and the claim is refuted by exhibiting their proofs. The ledger of principles is The proved choice ledger: hypotheses, equivalences, and upper bounds.

Ordinary induction is the same story. Nobody suspects induction on N (The principle of mathematical induction) of using choice, and transfinite induction is the same theorem with N replaced by an arbitrary well-order. The proofs are the same length and use the same single ingredient.

Sources