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

✓ 12 results · all verified · 12 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 12 also cleared it.

Ordinals and Transfinite Recursion: Examples and Counterexamples

1 · Prerequisites

2 · Summary

Objective. This companion page works the machinery of ordinals-and-transfinite-recursion on concrete orders, ordinals and boundary cases. Every item here is a dependency leaf: the theory it consumes is supplied by the parent page and its established prerequisite closure, and nothing outside this page depends on anything homed here. Each item states its hypotheses and checks its argument locally, and the page makes no claim beyond the statements of its items; no ordinal arithmetic, cumulative hierarchy or cardinal arithmetic is used anywhere, and no item spends a choice principle.

Examples and counterexamples

The items are listed in the order in which they appear in the page inventory; same-page dependencies always point backwards.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The finite von Neumann ordinals, and ω as the least limit ordinal

Example

With 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)) and the ordinals of Ordinal (von Neumann):

(i) 0,1,2,3 are ordinals, 1={0}, 2={0,1}, 3={0,1,2}=2∪{2}=2+, and for each k≤3 the set k is exactly the set of ordinals below k, so k={ξ:ξ<k};

(ii) ω=N is an ordinal, ω is a limit ordinal, the union of the members of ω is ω itself, and every element of ω is either 0 or a successor, so no element of ω is a limit ordinal (Successor and limit ordinals, ω is the least limit ordinal);

(iii) ω is the least limit ordinal: ω≤γ for every limit ordinal γ.

No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals N=ω with 0=∅ and σ(n)=n∪{n}, and the ordinal notation of Ordinal (von Neumann): a set α is an ordinal when it is transitive and ∈ strictly well-orders it, with α<β meaning α∈β and α+=α∪{α}.

[F1]

An ordinal is a transitive set on which ∈ is a strict well-order, 0:=∅ is an ordinal, α+=α∪{α}, and for ordinals α<β means α∈β while α≤β means α∈β or α=β (Ordinal (von Neumann)).

[F2]

For every ordinal α: every element of α is an ordinal, and α+ is an ordinal (Basic closure properties of ordinals).

[F3]

N=ω is the smallest inductive set, with 0=∅, σ(n)=n∪{n}, 1={0}, 2={0,1}, 3={0,1,2} and in general n={0,1,…,n−1}; ω is inductive, so 0∈ω and n∈ω implies σ(n)∈ω (The natural numbers N (von Neumann)).

[F4]

Every natural number is an ordinal, and ω is an ordinal; ω is a limit ordinal; every ordinal α∈ω is 0 or a successor ordinal; and ω⊆γ for every limit ordinal γ (ω is the least limit ordinal).

[F5]

An ordinal α is a successor ordinal when α=β+ for some ordinal β, and a limit ordinal when α≠0 and α is not a successor (Successor and limit ordinals).

[F6]

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

Verification

technique · direct
1.1F1F2F3F4

Claim (i): 0=∅ is an ordinal by [F1]; 1=0+={0}, 2=1+={0,1} and 3=2+={0,1,2} by [F3], and each is an ordinal by the successor clause of [F2], so 3=2∪{2}=2+ as displayed. For k≤3: every element ξ of k is a natural number, hence an ordinal by [F4], and conversely every ordinal ξ with ξ<k satisfies ξ∈k by [F1]; the two sides of k={ξ:ξ<k} therefore have the same members, since the elements of k are among the ordinals below k and every ordinal below k is an element of k.

1.2F1F3F4F5F6

Claim (ii): ω is an ordinal by [F4] and is a limit ordinal by [F4], and since ω≠0 by [F3] we may compute the union of its members. First ⋃ω⊆ω: a member of ⋃ω is a member of some n∈ω, and n⊆ω because ω is transitive as an ordinal while n∈ω, so that member lies in ω as well. Conversely ω⊆⋃ω: for n∈ω the successor σ(n)=n∪{n} again lies in ω by inductivity, and n∈σ(n), so every member of ω lies in a member of ω. Hence ⋃ω=ω by extensionality. Finally every element of ω is 0 or a successor by [F4], and a limit ordinal is nonzero and not a successor by [F5], so no element of ω is a limit ordinal.

1.3F1F4

Claim (iii): [F4] states that ω⊆γ, that is ω≤γ in the ordinal order of [F1], for every limit ordinal γ; with ω itself a limit ordinal by [F4], this says ω is the least limit ordinal.

2.1step 1.1step 1.2step 1.3∎

Claims (i) to (iii) are established: the finite levels 0,1,2,3 are ordinals with k={ξ:ξ<k} by step 1.1, the ordinal ω is a limit ordinal, equals the union of its members, and has no limit ordinal among its elements by step 1.2, and it is least among limit ordinals by step 1.3. Every ingredient is a theorem of ZF applied to the given sets, and nothing is selected from a family of sets, so no choice principle is used.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

A set of ordinals that is not an ordinal: {0,1,ω}

Statement refuted

Refuted claim: every set of ordinals is itself an ordinal, since membership well-orders any such set.

The witness is A={0,1,ω}. Its members are ordinals (Ordinal (von Neumann)), and membership restricted to A is a strict well-order: it is irreflexive, transitive as a relation, trichotomous, and every nonempty subset of A has an ∈-least element (Trichotomy and well-ordering of the ordinals). Yet A is not transitive, and therefore not an ordinal: 2∈ω∈A, but 2∉A, because 2 differs from each of 0, 1 and ω. So the well-ordering clause of the definition of an ordinal does not imply the transitivity clause, and the two clauses are genuinely independent: conversely B={0,1,{1}} is transitive but membership does not compare its distinct members 0 and {1}. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals N=ω with 0=∅, σ(n)=n∪{n}, 1={0}, 2={0,1}, and the ordinals of Ordinal (von Neumann); the set A={0,1,ω}.

[F1]

A set α is an ordinal when it is transitive and ∈ restricted to α is a strict well-order; 0=∅ is an ordinal, α+=α∪{α}, and for ordinals α<β means α∈β (Ordinal (von Neumann)).

[F2]

For ordinals α,β: every element of an ordinal is an ordinal, and α∉α (Basic closure properties of ordinals).

[F3]

Any two ordinals satisfy exactly one of α∈β, α=β, β∈α; every nonempty set of ordinals has an ∈-least element; and a set of ordinals ordered by inclusion is well ordered with strict part ∈ (Trichotomy and well-ordering of the ordinals).

[F4]

Every natural number is an ordinal; ω is an ordinal and a limit ordinal; and every ordinal in ω is 0 or a successor ordinal (ω is the least limit ordinal).

[F5]

N=ω is inductive: 0=∅∈ω and n∈ω implies σ(n)=n∪{n}∈ω; hence 1={0} and 2={0,1} are members of ω (The natural numbers N (von Neumann)).

[F6]

An ordinal is a successor ordinal when it equals β+ for some ordinal β, and a limit ordinal when it is nonzero and not a successor (Successor and limit ordinals).

[F7]

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

Counterexample

technique · direct
1.1F1F4F5F6

The members of A={0,1,ω} are ordinals, and the membership relations among them are as follows: 0 and 1 and 2 are natural numbers, hence ordinals by [F4]; ω is an ordinal by [F4]; 1={0} and 2={0,1} by [F5], and 0∈1, 1∈ω, 2∈ω, 0∈ω because 0,1,2 are members of the inductive set ω; moreover 2≠ω, since 2=σ(1)=1+ is a successor ordinal while ω is a limit ordinal by [F4] and [F6].

1.2F1F5

Conversely B={0,1,{1}} is transitive: its members 0=∅, 1={0} and {1} are all subsets of B. But 0≠{1}, since {1} is nonempty, and neither 0∈{1} (because 0≠1) nor {1}∈0 holds. Thus membership on B is not trichotomous and is not a strict well-order. Thus transitivity alone does not imply the well-ordering clause of the ordinal definition.

2.1step 1.1F2

Membership restricted to A is irreflexive: each of 0, 1, ω is an ordinal by step 1.1, and no ordinal is a member of itself by [F2].

2.2step 1.1

Membership restricted to A is transitive as a relation: the only pairs of members of A linked by membership are 0∈1, 1∈ω and 0∈ω by step 1.1, so the only two-step chain is 0∈1∈ω, and it is completed by 0∈ω.

2.3step 1.1F3

Membership restricted to A is trichotomous: any two distinct members of A are ordinals by step 1.1, so exactly one of ξ∈η, ξ=η, η∈ξ holds by [F3].

2.4step 1.1F3

Every nonempty subset of A has an ∈-least element: subsets of A are sets of ordinals by step 1.1, so the least-element clause of [F3] applies.

2.5step 1.1F2F5

The set A is not transitive: 2∈ω and ω∈A by step 1.1, but 2∉A, because 2≠0 (2={0,1} has members while 0=∅ has none), 2≠1 (1={0} but 1∈2, so 1≠2 since no ordinal is a member of itself by [F2]), and 2≠ω by step 1.1.

3.1step 2.1step 2.2step 2.3step 2.4step 2.5step 1.2F1F7∎

Steps 2.1 to 2.4 exhibit membership restricted to A as a strict well-order in the sense of [F1] and [F7]: irreflexive, transitive as a relation, trichotomous, with a least element in every nonempty subset. Step 2.5 shows that the set A is not transitive. By [F1] an ordinal must satisfy both clauses, so A is not an ordinal even though it is a set of ordinals; the refuted claim is false, and the well-ordering clause alone does not suffice; step 1.2 proves the converse independence as well. No choice principle is used.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Lexicographic orders: {0,1}×N and N×N

Example

Order pairs of natural numbers lexicographically: (m,n)≺(m′,n′) if and only if m<m′, or m=m′ and n<n′, where < is the order of N (Order on the natural numbers) on the product built in The Cartesian product A×B:={ z∈P(P(A∪B)):∃a∈A ∃b∈B z=(a,b) } with the pairs of The Kuratowski ordered pair (a,b):={{a},{a,b}}. Then:

(i) W={0,1}×N is well ordered by ≺, its initial segment below (1,0) is exactly {0}×N, and n↦(0,n) is an order isomorphism (N,<)→(W<(1,0),≺) (Initial segment of a well-order, Order embedding and order isomorphism); consequently N is order isomorphic to a proper initial segment of W and not to W, by the mutual exclusivity in Comparability of well-orders, with unique witness (1,0);

(ii) N×N is well ordered by ≺;

(iii) if F is the collapsing isomorphism of Every well-order has a unique order type for W, then F(0,n)=n for every n∈N and F(1,0)=ω, so the order type of W is an ordinal to which ω belongs (The natural numbers N (von Neumann)).

No choice principle is used.

Facts & Assumptions

Given: The natural numbers N=ω with the order of Order on the natural numbers, the product N×N and its subset W={0,1}×N, and the lexicographic relation ≺ defined in the Example.

[F1]

z∈A×B holds if and only if z=(a,b) for some a∈A and b∈B, and (a,b)={{a},{a,b}}; in particular {0,1}×N consists of the pairs (0,n) and (1,n) with n∈N (The Cartesian product A×B:={ z∈P(P(A∪B)):∃a∈A ∃b∈B z=(a,b) }, The Kuratowski ordered pair (a,b):={{a},{a,b}}).

[F2]

(a,b)=(c,d) if and only if a=c and b=d ((a,b)=(c,d) if and only if a=c and b=d).

[F3]

The order on N is a linear order: for all naturals m,m′ exactly one of m<m′, m=m′, m′<m holds, and < is transitive (Order on the natural numbers, ≤ is a linear order on N).

[F4]

A natural number is the set of its predecessors: n={j∈N:j<n}, with 0=∅ and N=ω (The natural numbers N (von Neumann)).

[F5]

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

[F6]

For all naturals m,n: m<n if and only if m∈n, and 0∈n whenever n≠0; in particular 0<1 since 1≠0 (On N the order is membership: m<n  ⟺  m∈n).

[F7]

A well-order on a set X is a total order in which every nonempty S⊆X has a least element; in the strict presentation it is irreflexive, transitive, trichotomous, and every nonempty subset has an element with nothing strictly below it in the subset (Well-order and well-ordered set).

[F8]

For a well-order (X,<) and a∈X the initial segment is X<a={x∈X:x<a} (Initial segment of a well-order).

[F9]

An order isomorphism between posets is a surjective order embedding, equivalently a bijection f with x≤y  ⟺  f(x)≤f(y) (Order embedding and order isomorphism).

[F10]

For well-orders V and W exactly one of the following holds: V≅W; V≅W<b for a unique b∈W; or V<a≅W for a unique a∈V (Comparability of well-orders).

[F11]

Every well-order (W,<) is order isomorphic to exactly one ordinal, its order type ot(W); the isomorphism is the collapsing map F(a)={F(b):b<a}, it is unique, and its image is ot(W) (Every well-order has a unique order type).

[F12]

A definable subcollection of a set is a set; in particular the set of first coordinates of a nonempty subset of N×N is a subset of N (The Axiom Schema of Separation: for each formula φ, ∀pˉ ∀x ∃y ∀z (z∈y↔(z∈x∧φ(z,pˉ)))).

Verification

technique · direct
1.1F1F3

The relation ≺ is irreflexive on N×N: (m,n)≺(m,n) would require m<m, or m=m and n<n, and both fail by trichotomy of the order of N.

1.2F1F2F3

The relation ≺ is transitive on N×N: if (m,n)≺(m′,n′) and (m′,n′)≺(m′′,n′′), then the definition gives m≤m′ and m′≤m′′. If m<m′ then m<m′′ by transitivity of the order of N when m′<m′′, and m<m′′ directly when m′=m′′, so (m,n)≺(m′′,n′′). If instead m=m′ and n<n′, then either m′<m′′, giving m<m′′ and hence (m,n)≺(m′′,n′′), or m′=m′′ with n′<n′′, giving m=m′′ together with n<n′<n′′ and hence (m,n)≺(m′′,n′′).

1.3F1F2F3F6F8F9

The initial segment of W below (1,0) is exactly {0}×N, and e(n)=(0,n) is an order isomorphism of (N,<) onto that initial segment: for a pair (m,k)∈W the first coordinate satisfies m∈{0,1}, and (m,k)≺(1,0) means m<1, or m=1 and k<0. The case m=0 satisfies the first disjunct by 0<1 from [F6]; the case m=1 satisfies neither disjunct, since 1<1 is false in the total order and k<0 is impossible because 0≤k for every natural k by [F6]. Hence (m,k)≺(1,0) if and only if m=0, which proves W<(1,0)={0}×N by [F8]. The map e is a bijection onto {0}×N by [F1] and [F2], and for naturals n,m one has n≤m if and only if e(n)≤e(m): if n<m then (0,n)≺(0,m); if n=m then e(n)=e(m) by [F2]; conversely e(n)≺e(m) forces n<m, because the first coordinates are equal and the second coordinate decides, and e(n)=e(m) forces n=m by [F2]. Hence e is an order isomorphism by [F9].

1.4F1F3F6F8

For every n∈N the predecessors of (0,n) in W are exactly the pairs (0,j) with j<n: a pair (m,k)∈W satisfies (m,k)≺(0,n) if and only if m=0 and k<n, since m<0 is impossible for m∈{0,1} because 0≤m by [F6] and the order is total, and the cases m=0 and m=1 reduce to k<n and to the false condition 1<0.

1.5F1F5F6

Claim (i), least elements: let S⊆W be nonempty. If S meets {0}×N, the set A={n∈N:(0,n)∈S} is a nonempty subset of N, hence has a least element n0 by [F5], and (0,n0) is ≺-least in S: a member (0,n) of S has n∈A, so n0≤n, while a member (1,n) of S satisfies (0,n0)≺(1,n) because 0<1 by [F6]. If S does not meet {0}×N then S⊆{1}×N by [F1], the set B={n∈N:(1,n)∈S} is nonempty and has a least element k by [F5], and (1,k) is ≺-least in S, every member of S being (1,n) with k≤n.

1.6F3F5F12

Claim (ii), least elements: let S⊆N×N be nonempty. The set of first coordinates A={m∈N:∃n∈N (m,n)∈S} is a definable subcollection of N, hence a set by [F12], and it is nonempty, so it has a least element m0 by [F5]. The set B={n∈N:(m0,n)∈S} is then nonempty and has a least element k by [F5], and (m0,k) is ≺-least in S: a member (m,n) of S has m≥m0, so if m>m0 then (m0,k)≺(m,n), while if m=m0 then n∈B and n≥k, giving (m0,k)=(m,n) or (m0,k)≺(m,n).

2.1step 1.1F2F3

Trichotomy: given distinct pairs (m,n) and (m′,n′), totality of the order of N decides between m<m′, m=m′ and m′<m; the first gives (m,n)≺(m′,n′) and the third gives (m′,n′)≺(m,n). If m=m′, totality decides between n<n′, n=n′ and n′<n: the first gives (m,n)≺(m′,n′), the third gives (m′,n′)≺(m,n), and n=n′ together with m=m′ gives (m,n)=(m′,n′) by [F2], contrary to distinctness. At most one alternative holds: equality together with either inequality substitutes to (m,n)≺(m,n), excluded by step 1.1; and (m,n)≺(m′,n′) together with (m′,n′)≺(m,n) is impossible, because combining the two defining disjunctions leaves the four alternatives m<m′ with m′<m; m<m′ with m′=m and n′<n; m=m′ and n<n′ with m′<m; and m=m′ and n<n′ with m′=m and n′<n, each contradicting trichotomy of the order of N.

2.2step 1.4F4F5F11

Claim (iii), first part: F(0,n)=n for every n∈N. Otherwise the set of naturals n with F(0,n)≠n is nonempty and has a least element n0 by [F5]; then F(0,j)=j for every j<n0, and the defining equation of the collapse [F11] together with step 1.4 gives F(0,n0)={F(y):y≺(0,n0)}={F(0,j):j<n0}={j:j<n0}=n0 by [F4], a contradiction.

2.3step 1.3F10

Claim (i), the comparability consequence: step 1.3 exhibits an order isomorphism N≅W<(1,0), which is alternative (ii) of [F10] for the pair of well-orders (N,<) and (W,≺) with witness (1,0); by the mutual exclusivity in [F10] the alternative N≅W fails, and the witness (1,0) is unique.

3.1step 1.3step 2.2F4F11

Claim (iii), second part: F(1,0)={F(y):y≺(1,0)} by the defining equation of [F11], and the predecessors of (1,0) in W are exactly the pairs (0,n) with n∈N by step 1.3, so F(1,0)={F(0,n):n∈N}={n:n∈N}=N=ω by step 2.2 and [F4]; since the image of F is the order type ot(W), an ordinal, we have ω∈ot(W).

4.1step 1.1step 1.2step 1.5step 1.6step 1.3step 2.1step 2.2step 2.3step 3.1F7∎

The relation ≺ is irreflexive and transitive on N×N by steps 1.1 and 1.2 and trichotomous by step 2.1, so it is the strict presentation of a total order; W inherits it and every nonempty subset of W has a least element by step 1.5, while every nonempty subset of N×N has one by step 1.6, so both are well ordered in the sense of [F7]. Step 1.3 identifies W<(1,0) and the isomorphism n↦(0,n), and step 2.3 records that N is isomorphic to that proper initial segment and to no other initial segment and not to W itself. Steps 2.2 and 3.1 compute the stated collapse values: F(0,n)=n and F(1,0)=ω, so the order type of W is an ordinal containing ω. No object is selected at any stage: the least elements come from the well-ordering of N and the collapse from uniqueness, so no choice principle is used.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The one-point extension of a well-order, and ω with a new top element

Example

Let (V,<) be a well-order (Well-order and well-ordered set) and let ∞∉V; put W=V∪{∞} and define x≺y if and only if x,y∈V and x<y, or x∈V and y=∞. Then:

(i) W is a well-order, W<∞=V (Initial segment of a well-order), and the identity is an order isomorphism of (V,<) onto the proper initial segment W<∞ (Order embedding and order isomorphism), so in Comparability of well-orders applied to (V,<) and (W,≺) it is alternative (ii) that holds, with the unique witness b=∞, and V is not order isomorphic to W;

(ii) for V=N=ω the extension is equinumerous with ω (Equinumerous sets, A≈B and A⪯B) but is not order isomorphic to (ω,<): the extension has a greatest element and ω does not;

(iii) for V=ω the collapsing map of Every well-order has a unique order type carries this extension of ω to an order isomorphism onto the ordinal ω+=ω∪{ω} (Ordinal (von Neumann)), so its order type is ω+.

No choice principle is used.

Facts & Assumptions

Given: A well-order (V,<), a point ∞∉V, the set W=V∪{∞} with the relation ≺ defined in the Example, and V=ω in parts (ii) and (iii), where ω=N with 0=∅ and σ(n)=n∪{n}.

[F1]

A well-order on a set X is a total order in which every nonempty S⊆X has a least element; in the strict presentation it is irreflexive, transitive, trichotomous, and every nonempty subset has an element with nothing strictly below it in the subset (Well-order and well-ordered set).

[F2]

For a well-order and a in it, the initial segment is X<a={x∈X:x<a} (Initial segment of a well-order).

[F3]

An order isomorphism between posets is a surjective order embedding, equivalently a bijection f with x≤y  ⟺  f(x)≤f(y) (Order embedding and order isomorphism).

[F4]

For well-orders V and W exactly one of the following holds: V≅W; V≅W<b for a unique b∈W; or V<a≅W for a unique a∈V (Comparability of well-orders).

[F5]

Every well-order (X,<) is order isomorphic to exactly one ordinal ot(X); the isomorphism is the collapsing map F(a)={F(b):b<a}, it is unique, and its image is ot(X) (Every well-order has a unique order type).

[F6]

Sets A and B are equinumerous when there is a bijection A→B; a function is injective when f(x)=f(y) implies x=y, surjective when every element of the codomain is a value, and bijective when both (Equinumerous sets, A≈B and A⪯B, Injection, surjection, bijection).

[F7]

ω=N with 0=∅, σ(n)=n∪{n}, and n={m∈N:m<n} is the set of its predecessors; N is an inductive set contained in every inductive set (The natural numbers N (von Neumann)).

[F8]

In (N,0,σ): σ(n)≠0 for every n, and σ is injective (The von Neumann naturals form a Peano system).

[F9]

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

[F10]

For naturals: n<σ(n) for every n, and n={m∈N:m<n} (On N the order is membership: m<n  ⟺  m∈n).

[F11]

For every ordinal α the successor is α+=α∪{α} (Ordinal (von Neumann)).

Verification

technique · direct
1.1F1

The relation ≺ is irreflexive: if x≺x with x∈V then x<x, impossible in the total order V; if x=∞ then the definition would need ∞∈V, which is excluded.

1.2F1

Trichotomy: for distinct x,y∈W either both lie in V, and totality of < decides between x<y and y<x, or one of them is ∞, and then x≺∞ when x∈V while y≺∞ when y∈V.

1.3F1

Transitivity: if x≺y and y≺z, then either z=∞, in which case x∈V and x≺z by the second clause, or z∈V; in the second case y∈V and the first clause gives x<y<z, so x<z and x≺z.

1.4F2F3

W<∞=V, and the identity map is an order isomorphism of (V,<) onto (W<∞,≺): a member x of W satisfies x≺∞ exactly when x∈V, by the second clause of the definition; and for x,y∈V one has x<y if and only if x≺y, so the identity is a bijection onto W<∞ preserving and reflecting the order.

1.5F1

Every nonempty S⊆W has a ≺-least element: if S meets V, then S∩V is a nonempty subset of the well-order V with least element ℓ, and ℓ is ≺-least in S, since a member of S∩V is either ℓ itself or lies strictly above ℓ in V, hence in ≺, while ∞ satisfies ℓ≺∞; if S meets V in nothing, then S={∞} and ∞ is least.

1.6F6F7F8F9

For V=ω the extension is equinumerous with ω: the map g with g(∞)=0 and g(n)=σ(n) for n∈ω is a bijection W→ω. It is injective, since σ is injective and σ(n)≠0 for every n, so the values σ(n) are nonzero and distinct and differ from 0=g(∞); and it is surjective, since 0=g(∞) while every m≠0 in ω equals σ(m′)=g(m′) for some m′ by [F9].

1.7F7F10

When V=ω: ∞ is a greatest element of W, because x≺∞ for every x∈V; and ω has no greatest element, because n<σ(n)∈ω for every n∈ω.

1.8F2F7F10

For V=ω and n∈ω the predecessors of n in W are exactly the naturals below n: a member y of W satisfies y≺n if and only if y∈ω and y<n, because y=∞ satisfies neither disjunct of the definition and a natural y satisfies the first exactly when y<n; hence W<n={m∈ω:m<n}=n.

2.1step 1.8F5F10

The collapse computes the finite levels: for V=ω one has F(n)=n for every n∈ω, where F(y)={F(z):z≺y} is the collapsing map of [F5]. Otherwise the set of n with F(n)≠n is nonempty and has a least element n0; then F(m)=m for every m<n0, and by step 1.8 and [F5] we get F(n0)={F(z):z≺n0}={F(m):m<n0}={m:m<n0}=n0 by [F10], a contradiction.

2.2step 1.4F4

Claim (i), the comparability consequence: step 1.4 exhibits an order isomorphism V≅W<∞, which is alternative (ii) of [F4] for the pair of well-orders (V,<) and (W,≺) with witness ∞; by the mutual exclusivity in [F4] the alternative V≅W fails, and the witness is unique.

2.3step 1.7F3F10

Claim (ii), the non-isomorphism: W is not order isomorphic to (ω,<). If f:W→ω were an order isomorphism, then every m∈ω is f(x) for some x∈W, and every x∈W satisfies x=∞ or x≺∞ because ∞ is greatest by step 1.7, so m=f(x)≤f(∞); thus f(∞) would be a greatest element of ω, contradicting step 1.7 since f(∞)<σ(f(∞)) in ω.

3.1step 1.4step 2.1F5F7F11

Claim (iii): for V=ω the predecessors of ∞ are exactly the members of ω by step 1.4, so F(∞)={F(z):z≺∞}={F(n):n∈ω}={n:n∈ω}=ω by step 2.1, the last equality because {n:n∈ω} and ω have the same members; and the image of F is ot(W) by [F5], so ot(W)={F(y):y∈W}={n:n∈ω}∪{ω}=ω∪{ω}=ω+ by [F11]: the collapse is an order isomorphism of W onto the ordinal ω+.

4.1step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 2.1step 2.2step 2.3step 3.1F5∎

Parts (i) to (iii) are established: ≺ is irreflexive, trichotomous and transitive by steps 1.1 to 1.3 and every nonempty subset of W has a least element by step 1.5, so W is a well-order with W<∞=V by step 1.4; the comparability classification and its unique witness are step 2.2. For V=ω the extension is equinumerous with ω by step 1.6 and not order isomorphic to it by step 2.3, and the collapse has image ω+ by steps 2.1 and 3.1, so the order type of the extension is ω+. Nothing is ever selected: the least elements come from the given well-order of V, the bijection in step 1.6 is one explicit formula, and the collapse is unique by [F5], so no choice principle is used.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The lexicographic order on Z×Z is not a well-order

Statement refuted

Refuted claim: the lexicographic order ≺ on Z×Z, defined by (a,b)≺(c,d) if and only if a<c, or a=c and b<d (Order on the integers), is a well-order (Well-order and well-ordered set).

The order ≺ is a total order: it is the lexicographic order of two total orders, and it is proved below from the totality of the order of Z. The nonempty subset {0}×Z nevertheless has no ≺-least element. For every integer n the element (0,n+(−1)) already lies in the subset, and n+(−1)<n in Z, so (0,n+(−1))≺(0,n): every member of the column is strictly above another member. Hence a total order here fails the least-element clause of Well-order and well-ordered set, and it is not a well-order. No choice principle is used anywhere in the argument.

Facts & Assumptions

Given: The integers Z with their order and ring operations, the lexicographic relation ≺ on the set Z×Z defined in the statement, and the axioms of ZF.

[F1]

Integers x=[(a,b)] and y=[(c,d)] satisfy x≤y if and only if a+d≤b+c in N; x<y means x≤y and x≠y; and on representatives 0<[(a,b)] holds exactly when b<a (Order on the integers).

[F2]

The relation of Order on the integers is well defined and a total order on Z, compatible with addition: x≤y implies x+z≤y+z for all integers x,y,z, and its strict part is irreflexive and transitive (The integers form a totally ordered ring).

[F3]

(Z,+,⋅,0,1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, in which every element x has the additive inverse −x, so x+(−x)=0, x+0=x, and addition is associative and commutative (The integers form a commutative ring, Arithmetic on the integers).

[F4]

The canonical embedding of N in Z, written n↦[(n,0)], is injective and preserves addition, multiplication and order; its image is exactly the set of nonnegative integers, so the image of every natural is nonnegative and every integer x≥0 is the image of a unique natural (The naturals embed in the integers).

[F5]

In N one has 1=σ(0), and σ(0)≠0; thus 1≠0 in N (The natural numbers N (von Neumann), The von Neumann naturals form a Peano system).

[F6]

A well-order on a set W is a total order in which every nonempty S⊆W has a least element; equivalently, in the strict presentation, a relation that is irreflexive, transitive, trichotomous, and such that every nonempty S⊆W has an element ℓ with no s∈S satisfying s<ℓ (Well-order and well-ordered set).

[F7]

z∈A×B holds if and only if z=(a,b) for some a∈A and some b∈B, and the ordered pair is (a,b)={{a},{a,b}}, so a pair with equal coordinates a=c, b=d equals (c,d) (The Cartesian product A×B:={ z∈P(P(A∪B)):∃a∈A ∃b∈B z=(a,b) }, The Kuratowski ordered pair (a,b):={{a},{a,b}}).

Counterexample

technique · direct
1.1F1F2

The relation ≺ is irreflexive: (a,b)≺(a,b) would require a<a, or a=a and b<b, and both alternatives fail because the strict order of Z is irreflexive.

1.2F1F2F7

At least one of ≺, =, ≻ links two pairs (a,b) and (c,d): by totality of the order of Z either a<c, or a=c, or c<a; in the first case (a,b)≺(c,d), in the last (c,d)≺(a,b), and in the middle case totality of the order of Z decides between b<d, b=d and d<b, giving (a,b)≺(c,d), (a,b)=(c,d), and (c,d)≺(a,b) respectively.

1.3F1F2

The relation ≺ is transitive: if (a,b)≺(c,d) and (c,d)≺(e,f), then by the definition of ≺ either a<c, or a=c and b<d, and either c<e, or c=e and d<f. If a<c then c≤e in both second alternatives, so a<e by transitivity of the order of Z; if a=c and b<d, then c<e gives a<e, while c=e gives a=e together with b<d<f, hence b<f. In every case (a,b)≺(e,f).

1.4F7

The set {0}×Z is a nonempty subset of Z×Z, and its elements are exactly the pairs (0,n) with n∈Z; for instance (0,0) belongs to it.

1.5F1F2F3F4F5

0<1 in Z: the integer 1 is [(1,0)] and 0 is [(0,0)] by the operations of [F3]; since 1=σ(0)≠0 in N, the representatives [(1,0)] and [(0,0)] are distinct, because the canonical embedding n↦[(n,0)] is injective by [F4]; and [(1,0)] lies in the image of that embedding, which is the set of nonnegative integers, so 0≤1 in Z; therefore 0<1 by [F1].

2.1step 1.1F1F2

At most one of the three alternatives holds: (a,b)≺(c,d) together with (a,b)=(c,d) would substitute to (a,b)≺(a,b), excluded by step 1.1; the same applies to (c,d)≺(a,b) together with equality; and (a,b)≺(c,d) together with (c,d)≺(a,b) is impossible, since the definition of ≺ leaves four combinations: a<c with c<a; a<c with c=a and d<b; a=c and b<d with c<a; and a=c and b<d with c=a and d<b; the first three contradict trichotomy of the order of Z, and the fourth gives both b<d and d<b.

2.2step 1.5F1F2F3

−1<0 in Z: adding the integer −1 to both sides of 0≤1 from step 1.5 gives 0+(−1)≤1+(−1), that is −1≤0; and −1≠0, because −1=0 would give 1=1+0=1+(−1)=0, contradicting 1≠0; hence −1<0.

3.1step 2.2F1F2F3

For every integer n one has n+(−1)<n: adding n to −1≤0 gives n+(−1)≤n+0=n; and n+(−1)≠n, because equality would give −1=(n+(−1))+(−n)=n+(−n)=0; so n+(−1)<n.

4.1step 1.4step 3.1F1F3F7

No member of {0}×Z is ≺-least: given (0,n) in the set, the integer n+(−1) exists in Z and (0,n+(−1)) again lies in {0}×Z by step 1.4, with 0=0 and n+(−1)<n by step 3.1, so (0,n+(−1))≺(0,n): every member of the subset has a strictly smaller member of the subset below it.

5.1step 1.1step 1.2step 1.3step 2.1step 4.1F6∎

The relation ≺ is irreflexive and transitive by steps 1.1 and 1.3, and trichotomous by steps 1.2 and 2.1, so it is the strict presentation of a total order on Z×Z; the set {0}×Z is nonempty by step 1.4 and has no element ℓ with no s≺ℓ, by step 4.1; hence the least-element clause of a well-order fails and ≺ is not a well-order on Z×Z. The refuted claim is therefore false.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

An explicit well-ordering of the integers: 0≺1≺−1≺2≺−2≺⋯

Example

On the integers Z (The integers as equivalence classes of pairs of naturals) define

a≺b  ⟺  (∣a∣<∣b∣) or (∣a∣=∣b∣, a≠b, 0<a),

where ∣⋅∣ is the integer absolute value (The absolute value ∣a∣ of an integer) and < is the order of Order on the integers; explicitly 0≺1≺−1≺2≺−2≺⋯. Then ≺ is a well-order (Well-order and well-ordered set) of Z: every nonempty S⊆Z has a ≺-least element, namely the element of S of least absolute value, the positive one being preferred when both ±n occur; the initial segment (Initial segment of a well-order) below 0 is empty, and for a≠0 the initial segment below a consists of 0 and of every ±n with 1≤n<∣a∣, together with −a when a<0. The usual order of Z is not a well-order of Z, so this is a different well-order of the same set. The relation is given by one explicit formula and no choice principle is used.

Facts & Assumptions

Given: The integers Z with their order, ring operations and absolute value, and the relation ≺ defined in the Example. No choice principle is assumed; every object below is produced by a formula.

[F1]

Integer absolute value: ∣a∣=a when a≥0 and ∣a∣=−a when a≤0, where ≤ is the order of Order on the integers and −a is the additive inverse supplied by The integers form a commutative ring (The absolute value ∣a∣ of an integer).

[F3]

On representatives, x≤y means a+d≤b+c in N, x<y means x≤y and x≠y, and 0<x holds exactly when x≠0 together with 0≤x; integers are ordered by Order on the integers (Order on the integers).

[F4]

The relation of Order on the integers is a total order on Z, compatible with addition: x≤y implies x+z≤y+z; its strict part is irreflexive, transitive and trichotomous (The integers form a totally ordered ring).

[F5]

(Z,+,⋅,0,1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, where 0=[(0,0)], 1=[(1,0)] and every element has the additive inverse −[(a,b)]=[(b,a)]; thus x+(−x)=0, x+0=x, −(−x)=x, and addition is associative and commutative (The integers form a commutative ring, Arithmetic on the integers).

[F6]

The canonical embedding of N in Z, n↦[(n,0)], is injective and preserves addition, multiplication and order; its image is exactly the set of nonnegative integers. We write n also for the integer [(n,0)], so N is identified with the nonnegative integers, every integer x≥0 is a unique natural number under this identification, and the order of N agrees with the integer order on these elements (The naturals embed in the integers).

[F7]

Natural order: m≤n if and only if m+k=n for some k∈N, and this relation is a linear order, so for all naturals m,n exactly one of m<n, m=n, n<m holds (Order on the natural numbers, ≤ is a linear order on N).

[F8]

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

[F9]

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

[F10]

A well-order on a set W is a total order in which every nonempty S⊆W has a least element; in the strict presentation, a relation that is irreflexive, transitive, trichotomous, and such that every nonempty S⊆W has an element ℓ with no s∈S satisfying s<ℓ (Well-order and well-ordered set).

[F12]

Verification

technique · direct
1.1F1F4

The relation ≺ is irreflexive: a≺a would require ∣a∣<∣a∣, impossible because the strict order of Z is irreflexive, or ∣a∣=∣a∣ together with a≠a, which is false outright.

1.2F1F2F4

Trichotomy: let a≠b. Totality of the order of Z decides between ∣a∣<∣b∣, ∣a∣=∣b∣ and ∣b∣<∣a∣; the first gives a≺b and the third gives b≺a. In the middle case ∣a∣=∣b∣=x we have x≥0 by [F2]; if x=0 then a=b=0 by [F2], contradicting a≠b, so x>0, and exactly one of 0<a, 0<b holds: if both held then a=∣a∣=x=∣b∣=b by [F1], contradicting a≠b, while if neither held then a≤0 and b≤0, so ∣a∣=−a and ∣b∣=−b by [F1] and a=−x=b, again contradicting a≠b. Hence in the middle case exactly one of a≺b, b≺a holds, and a≠b throughout.

1.3F1F2F4

Transitivity: suppose a≺b and b≺c, so ∣a∣≤∣b∣≤∣c∣ and, when the first strict alternative fails at a stage, the corresponding tie clause holds there. If ∣a∣<∣b∣ then ∣a∣<∣c∣ by transitivity of the order of Z, so a≺c. If ∣a∣=∣b∣ with a≠b and 0<a, then a=∣a∣>0 by [F1], so ∣b∣>0 and b≠0; were 0<b then b=∣b∣=∣a∣=a, contradicting a≠b, so b≤0 by totality and therefore b<0; the tie clause of b≺c fails because it requires 0<b, so b≺c must hold through ∣b∣<∣c∣, whence ∣a∣<∣c∣ and a≺c.

1.4F1F2F3F4F5F6

Absolute values are nonnegative integers, and they determine the sign: for every integer a, ∣a∣≥0 by [F2], so ∣a∣=k for a unique natural k under the identification of [F6], and ∣a∣=0 exactly when k=0; if ∣a∣=m with m≠0, then either a≥0 and a=∣a∣=m by [F1], or a<0 and −a=∣a∣=m, so a=−m by [F5]. Moreover for m≠0: 0<m, because m≥0 by [F2] while m≠0, so 0<m by [F3]; and adding −m gives −m<0 by [F4] and [F5].

1.5F3F4F5F6F10F11

The usual order of Z is not a well-order: 0<1, because the integer 1=[(1,0)] is the image of the natural 1 under the identification of [F6] and therefore nonnegative, so 0≤1; and 1≠0 since the embedding is injective and 1≠0 in N by [F11]; hence 0<1 by [F3]. Adding −1 to both sides gives −1<0 by [F4] and [F5]; adding an arbitrary integer n gives n+(−1)<n. So the nonempty set Z has no ≤-least element: for every n∈Z the integer n+(−1) lies strictly below n. Hence (Z,≤) is not a well-order in the sense of [F10].

2.1step 1.4F6F8F12

Let S⊆Z be nonempty. The collection K={k∈N:∣s∣=k for some s∈S}, read through the identification of [F6], is a definable subcollection of N, hence a set by [F12], and it is nonempty because every ∣s∣ is a nonnegative integer and so equals a unique natural number by step 1.4. By [F8] the set K has a least element m, so m=∣s0∣ for some s0∈S, and m≤∣s∣ for every s∈S: writing ∣s∣=k with k∈K we have m≤k in N, which is the integer comparison m≤k by [F6].

2.2step 1.4F1F2F4F5F6F7F9

The initial segments are as claimed. For a=0: no b satisfies b≺0, since the first clause would need ∣b∣<0, excluded by ∣b∣≥0, and the second would need ∣b∣=0, which gives b=0 and contradicts b≠0; hence W<0=∅ by [F9]. For a≠0 write ∣a∣=p with p≠0 and a=p or a=−p by step 1.4. For any b, the first clause ∣b∣<∣a∣ is equivalent to k<p, where ∣b∣=k under the identification of [F6]: if k<p then k<p as integers again by [F6], while if k≥p then p≤k in N by [F7], which is the integer comparison p≤k, contradicting ∣b∣<∣a∣=p. The integers of absolute value k are exactly k and −k by step 1.4, so the first clause contributes {0}∪{±n:1≤n<p}; the tie clause ∣b∣=∣a∣, b≠a, 0<b forces b=∣b∣=p by [F1], which differs from a exactly when a=−p, contributing {−a} when a<0 and nothing when a>0. Hence W<a={0}∪{±n:1≤n<p}∪{−a} for a<0 and W<a={0}∪{±n:1≤n<p} for a>0.

3.1step 2.1step 1.4F1F2F6

Case m=0 of step 2.1: some s0∈S has ∣s0∣=0, so s0=0 by [F2], and 0 is ≺-least in S: for s∈S we have ∣s∣≥0=∣0∣, so either ∣s∣>∣0∣, giving 0≺s by the first clause, or ∣s∣=0, giving s=0 by [F2].

3.2step 1.2step 1.4step 2.1F1F2F3F4F5F6

Case m≠0 of step 2.1: then 0<m and −m<0 by step 1.4, and by step 2.1 there is s0∈S with ∣s0∣=m, so s0=m or s0=−m by step 1.4. If m∈S put ℓ=m; if m∉S put ℓ=−m, which lies in S because s0∈S and the alternative s0=m is excluded. In both cases ℓ∈S and ∣ℓ∣=m, and for every s∈S step 2.1 gives m≤∣s∣ in the integer order: if ∣s∣>∣ℓ∣ then ℓ≺s by the first clause, while if ∣s∣=∣ℓ∣ then s=m or s=−m by step 1.4, and either s=ℓ, or s=−m with ℓ=m, in which case ℓ≠s and 0<ℓ, so ℓ≺s by the tie clause. Since ≺ is trichotomous by step 1.2, no s∈S satisfies s≺ℓ: ℓ is ≺-least in S.

4.1step 1.1step 1.2step 1.3step 1.5step 2.1step 2.2step 3.1step 3.2F10∎

Every nonempty S⊆Z has a ≺-least element: step 2.1 produces the natural m of least absolute value, and steps 3.1 and 3.2 cover the cases m=0 and m≠0. Together with irreflexivity, transitivity and trichotomy from steps 1.1 to 1.3 this exhibits ≺ as the strict presentation of a well-order of Z; the initial segments are those computed in step 2.2; and the usual order of Z is not a well-order by step 1.5, so the usual order and the explicit well-order of the same set are different. The relation is given by one explicit formula and no object is selected at any stage, so no choice principle is used.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The shift x↦x+1 is a nonidentity order automorphism of (Z,<)

Statement refuted

Refuted claim: claims (a) and (c) of Rigidity of well-orders hold for every total order, that is, totality in place of well-ordering suffices for both: (a) every strictly increasing f:W→W satisfies a≤f(a) for all a∈W, and (c) the identity is the only order isomorphism W→W.

The witness is Z with its usual order (Order on the integers), a total order that is not a well-order. The shift σ(x)=x+1 is an order isomorphism Z→Z (Order embedding and order isomorphism) with σ(x)≠x for every x, so the identity is not the only order automorphism and claim (c) fails. The shift τ(x)=x−1 in the other direction is strictly increasing and satisfies τ(x)<x for every x, so claim (a) fails as well. In the proof of claim (a) the least-element property is applied once, to the set of points moved down; here that set is all of Z, which has no least element, and this is exactly where the well-ordering hypothesis is spent. No choice principle is used.

Facts & Assumptions

Given: The integers Z with their order and ring operations, and the maps σ(x)=x+1, τ(x)=x−1 on Z.

[F1]

Rigidity of well-orders, claims (a) and (c): if (W,<) is a well-order and f:W→W is strictly increasing then a≤f(a) for every a∈W; and the identity is the only order isomorphism W→W (Rigidity of well-orders).

[F2]

Let (P,≤P) and (Q,≤Q) be posets; f:P→Q is an order embedding when x≤Py  ⟺  f(x)≤Qf(y), an order embedding is injective, and an order isomorphism is a surjective order embedding, equivalently a bijection with x≤Py  ⟺  f(x)≤Qf(y) (Order embedding and order isomorphism).

[F3]

A well-order is a total order in which every nonempty subset has a least element, and its strict part is irreflexive, transitive and trichotomous (Well-order and well-ordered set).

[F4]

On representatives, x≤y means a+d≤b+c in N, x<y means x≤y and x≠y, and 0<[(a,b)] holds exactly when b<a (Order on the integers).

[F5]

The relation of Order on the integers is a total order on Z, compatible with addition: x≤y implies x+z≤y+z for all integers x,y,z; its strict part is irreflexive and transitive (The integers form a totally ordered ring).

[F6]

(Z,+,⋅,0,1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, where 0=[(0,0)], 1=[(1,0)], and every element has the additive inverse −[(a,b)]=[(b,a)]; thus x+0=x, x+(−x)=0, and addition is associative and commutative (The integers form a commutative ring, Arithmetic on the integers).

[F7]

The canonical embedding n↦[(n,0)] of N in Z is injective and preserves order; its image is exactly the set of nonnegative integers, so the image of 1 is nonnegative and differs from the image of 0, which is 0 (The naturals embed in the integers).

[F8]

1=σ(0)≠0 in N (The von Neumann naturals form a Peano system).

[F9]

f:A→B is injective when f(x)=f(y) implies x=y, surjective when every b∈B is f(x) for some x∈A, and bijective when both (Injection, surjection, bijection).

Counterexample

technique · direct
1.1F5F6

The shift σ preserves and reflects the strict order: for integers x,y one has x<y if and only if x+1<y+1. Adding −1 to x+1<y+1 gives x<y, and adding 1 to x<y gives x+1<y+1.

1.2F5F6F9

The shift σ is bijective: it is injective, since x+1=y+1 gives x=(x+1)+(−1)=(y+1)+(−1)=y; and it is surjective, since an arbitrary integer y is σ(y+(−1))=y+(−1)+1=y.

1.3F4F5F6F7F8

1≠0 and −1<0 in Z: the integer 1 is [(1,0)] and lies in the image of the canonical embedding n↦[(n,0)], which consists of the nonnegative integers, so 0≤1; and 1≠0 because that embedding is injective while 1≠0 in N; hence 0<1, and adding −1 to both sides gives −1<0.

1.4F5F6

The backward shift τ(x)=x−1 is strictly increasing: for integers x,y one has x<y if and only if x+(−1)<y+(−1), that is τ(x)<τ(y), by adding 1 or −1 to an inequality.

2.1step 1.1step 1.2step 1.3F2F4F6

The shift σ is an order isomorphism of Z onto itself: it is a bijection by step 1.2 and satisfies x<y  ⟺  σ(x)<σ(y) by step 1.1, so also x≤y  ⟺  σ(x)≤σ(y), since x≤y means x<y or x=y and σ is injective. Moreover σ(x)=x+1≠x for every x: equality would give 1=0 by adding −x to both sides, contradicting step 1.3.

2.2step 1.3step 1.4F5F6

The backward shift τ is strictly increasing by step 1.4 and moves every point down: τ(x)=x+(−1)<x+0=x for every integer x, by adding x to −1<0 from step 1.3.

3.1step 1.3step 2.1step 2.2F1F3F4F5∎

Both claims fail at the total order (Z,<). Claim (c) of [F1] asserts that the identity is the only order isomorphism Z→Z, but σ is a nonidentity order isomorphism by step 2.1. Claim (a) asserts that every strictly increasing f:Z→Z satisfies x≤f(x) for all x, but τ is strictly increasing by step 2.2 with τ(x)<x, so x≤τ(x) fails for every x. In the proof of claim (a) the least element of {x:τ(x)<x} is used once; here {x:τ(x)<x}=Z, a total order with no least element, which is precisely why the well-ordering hypothesis cannot be dropped. The refuted claim that totality suffices for claims (a) and (c) is therefore false.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The Mostowski collapse of a finite chain computes its order type

Example

Let W={a,b,c,d} carry the well-order d≺a≺b≺c (Well-order and well-ordered set). The collapsing map F(x)={F(y):y≺x} of Every well-order has a unique order type then has

F(d)=∅=0,F(a)={0}=1,F(b)={0,1}=2,F(c)={0,1,2}=3,

so F is the order isomorphism of W onto the ordinal 4={0,1,2,3} (Ordinal (von Neumann), The natural numbers N (von Neumann)) and the order type of W is 4. Any function F′ on W with F′(x)={F′(y):y≺x} for all x∈W equals F, by the uniqueness in Every well-order has a unique order type. No choice principle is used: the values are computed and nothing is selected.

Facts & Assumptions

Given: The set W={a,b,c,d} with the total order d≺a≺b≺c, so that d,a,b,c are pairwise distinct and W<d=∅, W<a={d}, W<b={d,a}, W<c={d,a,b}.

[F1]

A well-order on a set X is a total order in which every nonempty S⊆X has a least element; in the strict presentation it is irreflexive, transitive and trichotomous (Well-order and well-ordered set).

[F2]

For a well-order (X,<) and x∈X the initial segment is X<x={y∈X:y<x} (Initial segment of a well-order).

[F3]

Every well-order (X,<) is order isomorphic to exactly one ordinal ot(X); the isomorphism is the collapsing map F(x)={F(y):y<x}, and it is unique (Every well-order has a unique order type).

[F4]

0:=∅ is an ordinal, and for every ordinal α the successor α+=α∪{α} is an ordinal (Ordinal (von Neumann), Basic closure properties of ordinals).

[F5]

The natural numbers are 0=∅, 1={0}, 2={0,1}, 3={0,1,2}, and in general n={0,1,…,n−1}, so in particular 4={0,1,2,3} (The natural numbers N (von Neumann)).

Verification

technique · direct
1.1F4F5

The five numerals are as stated and each of 0,1,2,3,4 is an ordinal: 0=∅ is an ordinal, and 1=0+, 2=1+, 3=2+, 4=3+ are ordinals by the successor clause, while 4={0,1,2,3} by the von Neumann convention.

1.2F1F2

The order d≺a≺b≺c makes W a well-order: it is total and trichotomous by the given chain, and a nonempty subset of W has a least element, namely the first of its elements in the listing d,a,b,c. The initial segments are W<d=∅, W<a={d}, W<b={d,a} and W<c={d,a,b}, read off from the chain.

2.1step 1.2F3F5

The collapse takes the values F(d)=∅=0, F(a)={0}=1, F(b)={0,1}=2, F(c)={0,1,2}=3: by [F3] the map F satisfies F(x)={F(y):y≺x} for every x∈W, and step 1.2 lists the predecessors, so F(d)={}=∅, F(a)={F(d)}={0}, F(b)={F(d),F(a)}={0,1}, F(c)={F(d),F(a),F(b)}={0,1,2}; the identifications with 0,1,2,3 are [F5].

3.1step 2.1F5

The image of F is {0,1,2,3}: the four values are distinct, since 0=∅ has no members, 1={0} has exactly the member 0, 2={0,1} has exactly the members 0,1, and 3={0,1,2} has the additional member 2 by [F5]. Moreover x≺y if and only if F(x)∈F(y) for all x,y∈W: the six strict comparisons of the chain read 0∈1, 0∈2, 0∈3, 1∈2, 1∈3, 2∈3, each true by [F5], while the six reversed non-comparisons read 1∉0, 2∉0, 3∉0, 2∉1, 3∉1, 3∉2, each true because 0=∅ has no members and 1={0}, 2={0,1}.

4.1step 1.1step 3.1F3

Hence F is an order isomorphism of W onto the ordinal 4={0,1,2,3}: it is a bijection onto 4 by step 3.1, and it preserves and reflects the order by step 3.1; since 4 is an ordinal by step 1.1, the uniqueness clause of [F3] identifies it with the order type of W, so ot(W)=4.

5.1step 1.2step 2.1step 4.1F3∎

Uniqueness: if F′ is any function on W with F′(x)={F′(y):y≺x} for all x∈W, then reading the chain in order and using the predecessor lists of step 1.2 gives F′(d)=∅=F(d), F′(a)={F′(d)}={0}=F(a), F′(b)={F′(d),F′(a)}=F(b) and F′(c)={F′(d),F′(a),F′(b)}=F(c); so F′=F. This is the uniqueness of [F3] verified directly on the finite chain. The order type of W is 4 and no object is selected anywhere; in particular no choice principle is used.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The collapsing recursion has no solution on (Z,<)

Statement refuted

Refuted claim: the recursive equation F(a)={F(b):b<a} has a solution for every total order, so the theorem schema Transfinite recursion and its corollary Every well-order has a unique order type need only a linear order in place of a well-order (Well-order and well-ordered set).

The witness is (Z,<) with its usual order (Order on the integers). There is no function F with F(a)={F(b):b<a} for every a∈Z: if there were, then F(a)∈F(b) whenever a<b, and the values along the descending sequence −1>−2>−3>⋯ would form a set S (by Replacement) in which each element xn+1=F(−(n+2)) is a member of the previous one xn=F(−(n+1)), so xn+1∈xn∩S for every n; Foundation applied to the nonempty set S forbids exactly this. So the least-element hypothesis cannot be weakened to totality, and the failure is precisely the infinite descending sequence −1>−2>−3>⋯ that no well-order admits. The argument uses only Foundation, Replacement and the order of Z; no choice principle is used.

Facts & Assumptions

Given: The integers Z with their order and ring operations, ZF with Foundation, and the supposition that a function F satisfies F(a)={F(b):b<a} for every a∈Z. Write xn:=F(−(n+1)) for n∈ω=N, where n+1=σ(n) in N and −(n+1) is the additive inverse of the image of n+1 in Z.

[F1]

Integers are ordered by the relation of Order on the integers: x<y means x≤y and x≠y (Order on the integers).

[F2]

That relation is a total order on Z compatible with addition: x≤y implies x+z≤y+z, and consequently x<y implies −y<−x (The integers form a totally ordered ring).

[F3]

(Z,+,⋅,0,1) is a commutative ring in which every element has an additive inverse, with the operations of Arithmetic on the integers (The integers form a commutative ring, Arithmetic on the integers).

[F4]

The canonical embedding of N in Z, written n↦[(n,0)], is injective and preserves addition and order, and its image is the set of nonnegative integers (The naturals embed in the integers).

[F5]

ω=N with 0=∅ and σ(n)=n∪{n} (The natural numbers N (von Neumann)).

[F6]

For every natural n one has n<σ(n)=n+1, hence n+1<n+2 (On N the order is membership: m<n  ⟺  m∈n).

[F7]

If a formula determines one set w for each z in a set A, then the collection of those w is a set: this is the Axiom Schema of Replacement (The Axiom Schema of Replacement: for each formula φ, if φ defines a class function on A then its image on A is a set).

[F8]

Axiom of Foundation: every set S with at least one member has a member s with s∩S=∅ (The Axiom of Foundation: ∀S (∃t (t∈S)→∃s (s∈S∧¬∃u (u∈s∧u∈S)))).

[F9]

Transfinite recursion: for a well-order (W,<) and a class function G there is exactly one F on W with F(a)=G(F↾W<a) (Transfinite recursion).

[F10]

Every well-order is order isomorphic to exactly one ordinal, its order type, via the collapsing map F(a)={F(b):b<a} (Every well-order has a unique order type).

[F11]

A function is a relation that never assigns two values to one argument; F above is assumed to be such a relation with domain Z (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).

Counterexample

technique · contradiction
1.1assume-contraF11

Suppose, for contradiction, that there is a function F with F(a)={F(b):b<a} for every a∈Z.

1.2F2F3F4F5F6

For every n∈ω the integers satisfy −(n+2)<−(n+1): the naturals satisfy n+1<n+2 by [F6], so the corresponding integers [(n+1,0)] and [(n+2,0)] satisfy [(n+1,0)]≤[(n+2,0)] by order preservation of the embedding n↦[(n,0)], with the values distinct because that embedding is injective while n+1≠n+2, hence [(n+1,0)]<[(n+2,0)]; applying negation reversal then gives −[(n+2,0)]<−[(n+1,0)], which is the displayed inequality.

2.1step 1.1

For all integers a<b one has F(a)∈F(b): by the supposition F(b)={F(c):c<b}, and F(a) is one of the members of that set because a<b.

2.2step 1.1F7F11

The set S={xn:n∈ω} exists: n↦xn is given by the formula w=F(−(n+1)), which determines one w for each n∈ω because F is a function, so Replacement makes the image a set.

3.1step 2.1step 1.2

For every n∈ω one has xn+1∈xn: step 1.2 puts −(n+2)<−(n+1), so step 2.1 applied to the pair a=−(n+2)<b=−(n+1) gives F(−(n+2))∈F(−(n+1)), that is xn+1∈xn.

3.2step 2.2F8

The set S is nonempty, since x0=F(−1) is one of its members; so Foundation applies to S and supplies x∈S with x∩S=∅.

4.1step 3.1step 3.2

Since x∈S, there is m∈ω with x=xm, and then step 3.1 gives xm+1∈xm∩S, because xm+1∈xm and xm+1∈S; this contradicts xm∩S=∅ from step 3.2.

5.1step 1.1step 3.1step 4.1F1F2F8F9F10discharge-contradiction∎

The supposition of step 1.1 is therefore refuted: there is no function F with F(a)={F(b):b<a} for every a∈Z. So a solution of the collapsing recursion is not available on the total order (Z,<), and the least-element hypothesis of [F9] and [F10] cannot be weakened to totality; the failure is the infinite descending sequence −1>−2>−3>⋯, whose values would form the set S that Foundation forbids. The argument used only Foundation, Replacement and the order of Z; no choice principle was used.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The Hartogs number of an n-element set is n+

Example

Let A≈n for some natural number n (Equinumerous sets, A≈B and A⪯B, The natural numbers N (von Neumann)). Then the Hartogs number ℵ(A) of Hartogs: an ordinal that does not inject into a given set equals n+=n∪{n}={0,1,…,n}: the set of order types of well-orders of subsets of A is exactly the set of ordinals α with α≤n, and n+ is the least ordinal that does not inject into A. In particular the cardinality of A determines its Hartogs number, and no choice principle is used.

Facts & Assumptions

Given: A set A with a bijection A≈n onto a natural number n, the ordinals of Ordinal (von Neumann), and the Hartogs number ℵ(A) of Hartogs: an ordinal that does not inject into a given set, namely the least ordinal that admits no injection into A, equal to {ot(S,R):S⊆A, R well-orders S}.

[F1]

ℵ(A) is the least ordinal that does not inject into A, and it equals the set of order types of the well-orders of subsets of A; this is proved without choice (Hartogs: an ordinal that does not inject into a given set).

[F2]

An ordinal is a transitive set on which ∈ is a strict well-order, α+=α∪{α}, every element of an ordinal is an ordinal, α∉α, and for ordinals α,β one has α⊆β if and only if α∈β or α=β (Ordinal (von Neumann), Basic closure properties of ordinals).

[F3]

For ordinals exactly one of α∈β, α=β, β∈α holds; every nonempty set of ordinals has an ∈-least element; and α≤β means α∈β or α=β (Trichotomy and well-ordering of the ordinals, Ordinal (von Neumann)).

[F4]

If A⪯B and B⪯A then A≈B; the bijection is explicit and no choice is used (The Schröder-Bernstein theorem).

[F5]

≈ means the existence of a bijection and ⪯ the existence of an injection (Equinumerous sets, A≈B and A⪯B, Injection, surjection, bijection).

[F6]

Every natural number is an ordinal, ω=N is an ordinal, and every element of ω is a natural number; N is transitive (The natural numbers N (von Neumann), ω is the least limit ordinal).

[F7]

If n≈m with n,m∈N then n=m; and N≉n for every n∈N (claims 3 and 4 of The pigeonhole principle on N).

[F8]

Every well-order is order isomorphic to exactly one ordinal, its order type; an order isomorphism exists exactly when the two well-orders have the same order type (Every well-order has a unique order type).

[F9]

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 between posets is a surjective order embedding, equivalently a bijection f with x≤y  ⟺  f(x)≤f(y) (Order embedding and order isomorphism).

Verification

technique · direct
1.1F2F5F8F9

Transport of well-orders along an injection: let α be an ordinal, let j:α→A be injective, put S=j[α] and R={(j(ξ),j(η)):ξ,η∈α, ξ∈η}. Then R is a well-order of S, the map j is an order isomorphism of (α,∈) onto (S,R), and ot(S,R)=α. Indeed j is a bijection onto S; R is irreflexive because no ordinal satisfies ξ∈ξ; R is transitive as a relation and trichotomous because membership on α is; and a nonempty T⊆S has j−1[T] nonempty in α, whose ∈-least element ξ gives an R-least element j(ξ) of T, since any j(η)∈T with j(η)Rj(ξ) would have η∈ξ and contradict minimality. By construction j(ξ)Rj(η) if and only if ξ∈η, using injectivity of j, so j is an order isomorphism and [F8] gives ot(S,R)=α.

1.2F2F3F4F5F6F7

For every ordinal α: α⪯A if and only if α≤n. First, A≈n, so an injection α→A composed with a bijection A→n gives an injection α→n, and conversely an injection α→n composed with a bijection n→A gives an injection α→A; hence α⪯A if and only if α⪯n. Next α⪯n if and only if α≤n: if α∈n or α=n then α⊆n by [F2], so the inclusion is an injection; conversely assume α⪯n and suppose α≰n, so that n∈α by the trichotomy of [F3]. Then n⊆α because α is transitive, so n⪯α by inclusion, and [F4] with α⪯n gives n≈α. If ω≤α then ω⊆α by [F2], so ω⪯α⪯n, while n⪯ω because n∈ω and ω is transitive; [F4] then gives ω≈n, contradicting [F7]. If instead α∈ω, then α is a natural number by [F6], and [F7] applied to n≈α gives α=n, so α≤n, contrary to n∈α and [F2]; hence the supposition fails and α≤n.

1.3F2F3F6

The set {α:α≤n} equals n+: α≤n means α∈n or α=n by [F3], that is α∈n∪{n}=n+ by [F2], and n+=n∪{n}={0,1,…,n} by the von Neumann convention of [F6].

2.1step 1.1F1F5F8

ℵ(A)={α:α is an ordinal and α⪯A}. One inclusion: if α=ot(S,R) for S⊆A well ordered by R, then the order isomorphism α→(S,R) of [F8] is injective with image S⊆A, so α⪯A. The other: if an ordinal α satisfies α⪯A, witnessed by an injection j, then step 1.1 produces S=j[α]⊆A and a well-order R of S with ot(S,R)=α, so α belongs to the set displayed in [F1].

3.1step 2.1step 1.2step 1.3F1

Therefore ℵ(A)=n+: step 2.1 writes ℵ(A)={α:α is an ordinal and α⪯A} and step 1.2 turns this into {α:α≤n}, which is n+ by step 1.3. Since ℵ(A) is the least ordinal not injecting into A by [F1], the ordinal n+ is that least ordinal, and ot of the subsets of A are exactly the ordinals up to n.

4.1step 3.1F1F8F9∎

If B≈A then ℵ(B)=ℵ(A): the hypothesis gives B≈n as well, so the same computation yields ℵ(B)=n+. Thus the cardinality of a finite set determines its Hartogs number, which is the successor ordinal n+ of its finite size n; nothing was selected at any stage, since the bijections and order types are given or unique by [F8], so no choice principle is used.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The Hartogs number of ω is a limit ordinal above ω

Example

Let H=ℵ(ω) be the least ordinal that admits no injection into ω (Hartogs: an ordinal that does not inject into a given set). Then H is a limit ordinal (Successor and limit ordinals) with ω∈H, so ω<H, and H is uncountable (Finite, countably infinite, countable, uncountable); explicitly H={α:α is an ordinal and is at most countable} is the set of countable ordinals, and H is not the successor of any ordinal. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals N=ω, the Hartogs number H=ℵ(ω), namely the least ordinal that admits no injection into ω, and {ot(S,R):S⊆ω, R well-orders S} for it (Hartogs: an ordinal that does not inject into a given set).

[F1]

ℵ(A) is the least ordinal that does not inject into A, and it equals the set of order types of well-orders of subsets of A; no choice is used (Hartogs: an ordinal that does not inject into a given set).

[F2]

A set is finite when it is equinumerous with some natural number, countably infinite when equinumerous with N=ω, at most countable when finite or countably infinite, and uncountable when not at most countable; ≈ is equinumerosity and ⪯ domination by an injection (Finite, countably infinite, countable, uncountable, Equinumerous sets, A≈B and A⪯B).

[F3]

Subsets of at most countable sets are at most countable (Every subset of an at most countable set is at most countable).

[F4]

Every ordinal is exactly one of 0, a successor ordinal β+=β∪{β}, or a limit ordinal, meaning a nonzero ordinal that is not a successor (Successor and limit ordinals, Ordinal (von Neumann)).

[F5]

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

[F7]

ω=N is an ordinal, every element of ω is a natural number, and every natural number is an ordinal (ω is the least limit ordinal, The natural numbers N (von Neumann)).

[F8]

In (N,0,σ): σ(n)≠0 for every n, and σ is injective (The von Neumann naturals form a Peano system).

[F9]

A function is injective when it never takes equal values at distinct arguments, and bijective when it is injective and onto; an injection is a bijection onto its image (Injection, surjection, bijection).

[F10]

Every well-order is order isomorphic to exactly one ordinal, its order type (Every well-order has a unique order type); an order isomorphism is a bijection preserving and reflecting the order (Order embedding and order isomorphism), and a well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

Verification

technique · direct
1.1F5F9F10

Transport of well-orders along an injection: if α is an ordinal and j:α→ω is injective, then S=j[α]⊆ω and R={(j(ξ),j(η)):ξ,η∈α, ξ∈η} well-order S, the map j is an order isomorphism of (α,∈) onto (S,R), and ot(S,R)=α. Indeed j is a bijection onto S; R is irreflexive since ξ∉ξ; R is transitive and trichotomous because membership on the ordinal α is; and a nonempty T⊆S has j−1[T] nonempty with an ∈-least element ξ, whose image j(ξ) is R-least in T. Since j(ξ)Rj(η) holds exactly when ξ∈η by injectivity, j preserves and reflects the order and [F10] identifies ot(S,R) with α.

1.2F2F3F7F9

For every ordinal α: α⪯ω if and only if α is at most countable. If j:α→ω is injective, then j is a bijection of α onto the subset j[α]⊆ω, which is at most countable by [F3], so α is at most countable because the three size classes of [F2] are defined by equinumerosity; conversely, if α is finite then α≈m for some natural number m, and m⊆ω gives an injection α→ω by composition, while if α is countably infinite then α≈N=ω gives one directly.

2.1step 1.1F1F9F10

H={α:α is an ordinal and α⪯ω}: if α=ot(S,R) for a subset S⊆ω well ordered by R, the order isomorphism α→S is injective into ω; conversely an injection j:α→ω produces S=j[α] and R with ot(S,R)=α by step 1.1, so α is one of the order types displayed in [F1].

3.1step 2.1step 1.2F1

H is the set of at most countable ordinals and admits no injection into ω: by step 2.1 and step 1.2 an ordinal α lies in H exactly when it is at most countable, and by [F1] the ordinal H itself does not inject into ω.

3.2step 2.1F4

ω∈H and H≠0: the identity is an injection ω→ω, so ω⪯ω and hence ω∈H by step 2.1; therefore H has a member and is not the ordinal 0, which has none.

4.1step 3.1F4F5F7F8F9

H is not a successor ordinal: suppose H=α+=α∪{α} for an ordinal α. Then α∈H, so α⪯ω by step 2.1, say through an injection j:α→ω. Define g on the domain α+ by g(β)=σ(j(β)) for β∈α and g(α)=0; this is well defined because α∉α, its values lie in ω because ω is inductive, and it is injective: the value 0 is taken only at α since σ(n)≠0 for every n, and on α the map is σ composed with the injective j, hence injective. So H=α+ would inject into ω, contradicting that H admits no injection into ω by step 3.1.

5.1step 1.2step 3.1step 3.2step 4.1F1F2F4F5

H is a limit ordinal with ω∈H, and it is the set of countable ordinals: H is an ordinal by [F1], it is nonzero by step 3.2 and not a successor by step 4.1, so it is a limit ordinal by [F4]; ω∈H by step 3.2, so ω<H in the ordinal order of [F5]; the identification H={α:α is an ordinal and is at most countable} is step 3.1, and H itself is uncountable because it is the least ordinal that does not inject into ω and an at most countable ordinal would inject into ω by step 1.2.

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

Everything claimed is established: H=ℵ(ω) is a limit ordinal with ω∈H, explicitly the set of at most countable ordinals, hence uncountable and not a successor; the argument used only the transport of well-orders along injections, Schröder-free counting, and the Peano properties of σ, all choice free, so no choice principle is used.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Transfinite induction fails if the least element is exempted from the hypothesis

Statement refuted

Refuted claim: the hypothesis of Transfinite induction may be checked only at elements other than the least element of the well-order: for a well-order W with least element m, if W<a⊆S implies a∈S for every a≠m, then S=W.

The witness is W=ω with its usual order and S=ω∖{0} (The natural numbers N (von Neumann), Initial segment of a well-order). The implication holds at every a≠0 vacuously, because then 0<a while 0∉S, so W<a is never contained in S; yet at a=0 the initial segment W<0=∅ is contained in S while 0∉S. So the hypothesis of the theorem holds at every element except the least and fails at the least, and the conclusion S=W is false. Hence the restriction to a≠m is not a valid form of the theorem: the least element needs no separate base case because the hypothesis applied there is the base case. No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals N=ω with 0=∅, the additive order of Order on the natural numbers, the subset S=ω∖{0}, and a well-order (W,<) with least element m as in the refuted claim, specialised below to W=ω with its usual order.

[F1]

Transfinite induction: if (W,<) is a well-order and W<a⊆S implies a∈S for every a∈W, then S=W (Transfinite induction).

[F2]

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

[F3]

For all naturals m,n: m<n if and only if m∈n; n={m∈N:m<n}; 0≤n for every n and 0∈n whenever n≠0 (On N the order is membership: m<n  ⟺  m∈n).

[F4]

0=∅ and σ(n)=n∪{n} in ω=N, and 0≠1 (The natural numbers N (von Neumann)).

[F5]

The order of N is defined by m≤n if and only if m+k=n for some natural k, with m<n meaning m≤n and m≠n, and it is a linear order (Order on the natural numbers, ≤ is a linear order on N).

[F6]

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

[F7]

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

Counterexample

technique · direct
1.1F3F5F6F7

The set W=ω with its usual order is a well-order, and 0 is its least element: the order of [F5] is linear, and every nonempty subset of N has a least element by [F6], so (ω,<) is a well-order in the sense of [F7]; and 0≤n for every n by [F3], so 0 is the least element.

1.2F2F3F4

Under the identification of membership with the order, W<a=a for every a∈ω: W<a={m∈ω:m<a} by [F2], and {m∈N:m<a}=a by [F3]. In particular W<0=∅, since 0=∅ by [F4].

1.3F4

S=ω∖{0} is a subset of W with 0∉S and S≠W, because 0∈W by [F4].

2.1step 1.3F3

For every a∈ω with a≠0 the implication W<a⊆S⇒a∈S holds vacuously: 0<a by [F3], so 0∈W<a while 0∉S by step 1.3, and therefore W<a is not contained in S.

2.2step 1.2step 1.3

At the least element a=0 the hypothesis fails: W<0=∅⊆S by step 1.2, while 0∉S by step 1.3, so W<0⊆S holds and 0∈S does not.

3.1step 1.1step 1.3step 2.1step 2.2F1∎

The refuted claim is therefore false: the well-order W=ω has least element 0 by step 1.1, the implication W<a⊆S⇒a∈S holds for every a≠0 by step 2.1, yet S≠W by step 1.3, so the conclusion S=W fails. The hypothesis of [F1] is exactly the statement at every a∈W, including a=0, and step 2.2 shows that the instance at the least element is what supplies the base case; exempting it removes precisely the step that forces 0∈S. No choice principle is used.

Sources