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.

✓ 8 results · all verified · 3 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.

Order, Zorn's Lemma, and the Axiom of Choice: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Finite choice written out: a choice function for three sets

Example

Let

F={ {0,1}, {1,2}, {2,3} },

a family of three nonempty sets of natural numbers. A choice function for F (Choice function) can be written down outright, by listing its three values:

g({0,1})=0,g({1,2})=1,g({2,3})=2.

Nothing was assumed to produce it. Each value is one element taken from one set already known to be nonempty, and three such picks are made one after another. The induction of Every natural-number-indexed list of nonempty sets has a choice function on its family of values is exactly this process stated in general. That lemma indexes the family by a natural number rather than counting its members: writing the three sets as the values F(0),F(1),F(2) of a function F with domain 3={0,1,2} (The natural numbers N (von Neumann)), the successor step restricts F to the shorter index set, takes a choice function for those values, and overwrites it with one further pair.

Facts & Assumptions

Given: The family F={{0,1},{1,2},{2,3}}, whose members are sets of natural numbers, together with the function F with domain the von Neumann natural number 3={0,1,2} (The natural numbers N (von Neumann)) given by F(0)={0,1}, F(1)={1,2}, F(2)={2,3}, so that F=F[3].

[L1]

A choice function for a family F is a function g with domain F such that g(S)∈S for every S∈F (Choice function).

[L2]

For every natural number n and every function F with domain n all of whose values are nonempty, the family of values F[n] has a choice function; the proof is an induction on n whose successor step restricts F to n⊆σ(n), takes a choice function for F[n], and overwrites it with the single pair (F(n),a) for some a∈F(n) (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Verification

technique · direct
1.1

The three members are pairwise distinct: 0 belongs to {0,1} and to neither of the others, 1 belongs to {1,2} but not to {2,3}, and {0,1}≠{2,3} since 0∉{2,3}; so F has exactly three members.

given
1.2

Every member is nonempty: 0∈{0,1}, 1∈{1,2} and 2∈{2,3}.

given
2.1

Let g={ ({0,1},0), ({1,2},1), ({2,3},2) }, the set whose three elements are those ordered pairs; it is a relation with domain F, and since the three members of F are pairwise distinct its three first coordinates are pairwise distinct, so it is single valued: g is a function on F.

step 1.1construct
3.1

Its values lie where they must: g({0,1})=0∈{0,1}, g({1,2})=1∈{1,2} and g({2,3})=2∈{2,3}, so g(S)∈S for every S∈F and g is a choice function for F.

step 2.1step 1.2L1
4.1

A function of this shape is what the induction of [L2] returns when run on the listing F: since F has domain 3 and each value is nonempty by step 1.2, [L2] applies with n=3 and yields a choice function for F[3]=F, obtained in three stages, one pick at each index, so no choice principle is invoked and none is needed. Nothing here rests on counting the members of F, only on the listing exhibited in the Given.

step 3.1step 1.2givenL2∎

Remarks

  • Where an axiom would have been needed, and why it was not. Each pick is a single existential instantiation from a single nonempty set, licensed by first-order logic alone. Three of them are made, one at a time, and three is a natural number, so the process stops. What ZF does not supply is a choice function for every arbitrary family of nonempty sets. An infinite family can still have a choice function given by a defining rule — such as the minimum rule below — so the gap filled by the Axiom of Choice is arbitrary families, not mere infinitude.

  • Choice functions are not unique. Taking the larger element of each pair gives another one, with values 1,2,3; since each member has two elements there are 2⋅2⋅2=8 choice functions for F in all. Nothing in the definition prefers one of them.

  • The particular g displayed above is the rule S↦min⁡S, which happens to work for every nonempty set of natural numbers at once (min⁡ is a choice function on N). That is a feature of N, not of finiteness. The two ingredients come apart in Russell's shoes and socks, where the family is infinite and carries no such rule.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

min⁡ is a choice function on N

Example

Every nonempty subset of N has a least element (The well-ordering principle), and that least element is unique, so

min⁡:P(N)∖{∅}⟶N,min⁡S=the least element of S,

is a well defined function, and min⁡S∈S by construction. It is therefore a choice function on N (Choice function), given by a single rule and produced with no appeal to the Axiom of Choice.

What makes the choice free here is the structure of the order (Order on the natural numbers), not the size of the family. The order well-orders N, and a well-order names a canonical element of every nonempty subset; how large the family of nonempty subsets is then does not matter.

Facts & Assumptions

Given: The family F=P(N)∖{∅} of nonempty subsets of N, with N carrying its usual order (Order on the natural numbers).

[L1]

Every nonempty S⊆N has a least element: there is ℓ∈S with ℓ≤s for every s∈S (The well-ordering principle).

[L2]

The order on N is antisymmetric: m≤n and n≤m imply m=n (≤ is a linear order on N).

[L3]

A choice function for a family F is a function g with domain F such that g(S)∈S for every S∈F, and a choice function on N is one for P(N)∖{∅} (Choice function).

Verification

technique · direct
1.1

Let S∈F, so S⊆N and S≠∅.

given
2.1

S has a least element: some ℓ∈S satisfies ℓ≤s for every s∈S.

step 1.1L1
2.2

That least element is unique: if ℓ and ℓ′ are both least elements of S then ℓ≤ℓ′ and ℓ′≤ℓ, hence ℓ=ℓ′.

step 1.1L2
3.1

So "the least element of S" is a definite description, and min⁡={(S,ℓ)∈F×N:ℓ∈S and ℓ≤s for all s∈S} is a set by Separation, single valued by step 2.2 and total on F by step 2.1, hence a function with domain F.

step 2.1step 2.2construct
4.1

Its values lie where they must: min⁡S is a least element of S, and a least element of S belongs to S, so min⁡S∈S for every S∈F.

step 3.1step 2.1
5.1

Therefore min⁡ is a choice function for F, that is a choice function on N, and it was obtained from a rule rather than from any axiom asserting that choices can be made.

step 4.1L3∎

Remarks

  • The rule, not the existence, is the point. [L1] gives a least element of each nonempty S separately. Turning a family of separate existence statements into one function is exactly what the Axiom of Choice does in general, and it is exactly what is avoided here: uniqueness of the least element makes "the least element of S" a formula in S, so the graph of min⁡ is carved out by Separation from F×N with no further axiom.

  • Every natural-number-indexed list of nonempty sets has a choice function on its family of values does not apply, and not for the reason usually given. That lemma carries no finiteness hypothesis at all, and it refuses that reading explicitly: it is stated over an indexed family, a natural number n and a function F with domain n all of whose values are nonempty, and it gives a choice function for the family F[n] of the values of F. What disqualifies F=P(N)∖{∅} is that it is not F[n] for any such F: sending each member of F[n] to the least index at which F takes it as a value injects F[n] into n, the least index existing by [L1], whereas F already contains the n+1 pairwise distinct singletons {0},{1},…,{n}, and no injection σ(n)→n exists (The pigeonhole principle on N ↗, which this library proves on a later page). Size is not what is at stake here, structure is, and Russell's shoes and socks is the contrasting case: a family of two element sets, with no listing of this kind and no rule either.

  • The same construction works verbatim on any set carrying a well-order, with "least element" read in that order. Whether every arbitrary set carries a well-order is a different question, and answering it affirmatively is again a form of the Axiom of Choice. The library does prove it, but only from that axiom and only on a later page (The well-ordering theorem ↗); nothing in this example uses it, and no item on this page lists it as a dependency.

  • Antisymmetry does the whole of the uniqueness work, and it is the only order axiom needed for it. This is the same one-line argument that makes sup⁡ legitimate notation in a poset (Upper bound, least upper bound, and strict upper bound).

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

Russell's shoes and socks

Example

Russell's illustration separates an explicit selection rule from a bare request for simultaneous choices. For a family of pairs of shoes, suppose the data includes a set L meeting each pair in exactly one member—the left shoe. Then ZF constructs a choice function. For a family of pairs of indistinguishable socks, no such distinguisher is supplied; asking for a selection from every pair is an instance of choice for pairs. This example proves the first claim and identifies the second statement without asserting any model-theoretic nonimplication.

Facts & Assumptions

Given: A family F of two-element sets and a set L such that S∩L has exactly one element for every S∈F.

[L1]

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

[L2]

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

Verification

technique · direct
1.1

For each S∈F, the phrase “the unique element of S∩L” defines one element of S from the supplied data.

given
2.1

By Separation, g={(S,x)∈F×⋃F:S∩L={x}} is a set; the uniqueness hypothesis makes it single-valued and total on F.

step 1.1construct
3.1

For every S∈F, g(S) is the unique member of S∩L, so g(S)∈S. Thus g is a choice function constructed in ZF from F and L.

step 2.1L1
4.1

If the distinguisher L is omitted, step 2.1 has no defining predicate to use. The assertion that an arbitrary family of pairs nevertheless has a choice function is precisely the corresponding restricted instance of [L2]. This identifies the sock question but neither assumes nor proves an independence result.

step 2.1L1L2∎

Remarks

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The power set is chain-complete, with union as supremum

Example

For any set X, the power set P(X) ordered by inclusion is a poset (Partial order and partially ordered set) in which every ⊆-chain D (Chain in a poset) has least upper bound

sup⁡D=⋃D∈P(X)

(Upper bound, least upper bound, and strict upper bound). So (P(X),⊆) is chain-complete (Chain-complete poset), and its bottom element is ⊥=sup⁡∅=⋃∅=∅.

Both halves of "least upper bound" are checked below. Chain-completeness asks for the least one, not merely for some upper bound, and it is leastness that the Bourbaki–Witt argument consumes.

Facts & Assumptions

Given: A set X and its power set P(X)={A:A⊆X}, ordered by inclusion.

[F1]

Axiom of Extensionality: sets with exactly the same elements are equal.

[L1]

A partial order is a reflexive, antisymmetric and transitive relation (Partial order and partially ordered set).

[L2]

u is an upper bound of S when s≤u for every s∈S, and a least upper bound when in addition u≤v for every upper bound v of S (Upper bound, least upper bound, and strict upper bound).

[L3]

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

[L4]

A poset is chain-complete when every chain has a least upper bound, and then ⊥=sup⁡∅ is its least element (Chain-complete poset).

Verification

technique · direct
1.1

Inclusion partially orders P(X): A⊆A; if A⊆B and B⊆A then A and B have the same elements, so A=B by extensionality; and A⊆B⊆C gives A⊆C.

givenF1L1
1.2

Let D⊆P(X) and put U=⋃D, so that x∈U exactly when x∈D for some D∈D; each such D satisfies D⊆X, hence U⊆X and U∈P(X).

givenconstruct
2.1

U is an upper bound of D: if D∈D and x∈D then x∈U, so D⊆U.

step 1.2L2
2.2

U is least among the upper bounds: let V∈P(X) satisfy D⊆V for every D∈D; any x∈U lies in some D∈D and hence in V, so U⊆V.

step 1.2L2
3.1

So every subset D of P(X) has least upper bound ⋃D, and a chain is in particular a subset, so every chain has one and (P(X),⊆) is chain-complete.

step 1.1step 2.1step 2.2L3L4
4.1

The empty chain is the case D=∅, where U=⋃∅=∅; so ⊥=sup⁡∅=∅, which is indeed the least element, since ∅⊆A for every A∈P(X).

step 3.1step 1.2L4∎

Remarks

  • The argument proves more than chain-completeness. Neither the construction of U nor either of the two bound checks used that D is a chain, so every subset of P(X) has a supremum and (P(X),⊆) is a complete lattice. Chain-completeness is strictly weaker, and the posets to which Zorn's lemma is applied usually have only the weaker property (The chains of a poset, ordered by inclusion, form a chain-complete poset is the standard instance).

  • Infima are present too: for nonempty D the greatest lower bound is ⋂D, and the greatest lower bound of the empty family is X, the top element. The class ⋂∅ is not a set, which is why the empty case is read inside P(X) rather than absolutely.

  • The empty chain is not a technicality. It is what forces a chain-complete poset to have a least element at all, and here it produces ∅. A convention that excludes the empty chain has to reintroduce the same content as a separate nonemptiness hypothesis (Chain-complete poset records the reduction between the two conventions).

  • Chain-completeness is not the same as having a top. Deleting the top element from P({1,2}) leaves the three-element poset of Two maximal elements and no greatest element, which is still chain-complete, since {1} and {2} are incomparable and so never lie in a common chain, yet it now has two maximal elements and no greatest one.

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The chains of a poset, ordered by inclusion, form a chain-complete poset

Example

Let (P,≤) be any poset and let

C={ C⊆P:C is a chain of P }

be the set of its chains (Chain in a poset), ordered by inclusion. Then C is chain-complete (Chain-complete poset): an inclusion chain D⊆C has least upper bound ⋃D, which is again a chain of P because any two of its elements lie in a common member of D. Its bottom element is ⊥=sup⁡∅=∅.

This is the poset that Zorn's lemma builds at its step 1.2 and declares chain-complete at its step 2.1, so what follows is that step worked out in full: the engine of Zorn's lemma, running on its own.

Facts & Assumptions

Given: A poset (P,≤) and the set C of chains of P, ordered by inclusion; note C⊆P(P).

[L1]

A subset C⊆P is a chain when any two of its elements are comparable, and the empty set is a chain (Chain in a poset).

[L2]

Inclusion partially orders P(P). For any D⊆P(P), every C∈D satisfies C⊆⋃D, while any V containing every C∈D also contains every element of ⋃D; hence ⋃D is the least upper bound of D (Partial order and partially ordered set, Upper bound, least upper bound, and strict upper bound).

[L3]

u is an upper bound of S when s≤u for every s∈S, and a least upper bound when in addition u≤v for every upper bound v of S (Upper bound, least upper bound, and strict upper bound).

[L4]

A poset is chain-complete when every chain has a least upper bound, and then ⊥=sup⁡∅ is its least element (Chain-complete poset).

[L5]

A partial order on a set X is a relation on X that is reflexive, antisymmetric and transitive, each of the three being a condition required of all elements of X (Partial order and partially ordered set).

Verification

technique · direct
1.1

C is a subset of P(P), and inclusion partially orders P(P); reflexivity, antisymmetry and transitivity are required of all elements of P(P), so they hold in particular for all elements of C, and the restriction of inclusion to C partially orders C.

givenL2L5
1.2

Let D⊆C be a chain for inclusion and put U=⋃D.

givenconstruct
2.1

U is a chain of P: let x,y∈U, say x∈C1 and y∈C2 with C1,C2∈D; as D is a chain for inclusion, C1⊆C2 or C2⊆C1, so x and y both lie in whichever of the two is the larger, and that set is a chain of P, hence x and y are comparable in P. So U∈C, the case D=∅ reading U=∅∈C with the condition on x,y vacuous.

step 1.2L1
2.2

U is an upper bound of D for inclusion: C⊆⋃D=U for every C∈D.

step 1.2L3
3.1

U is least among the upper bounds of D lying in C: such a V is in particular an upper bound of D in P(P), where ⋃D is least, so U⊆V.

step 2.2L2L3
4.1

So every inclusion chain D⊆C has least upper bound ⋃D in C, that is C is chain-complete, with ⊥=sup⁡∅=∅.

step 2.1step 3.1L4∎

Remarks

  • This is the whole of Zorn's engine. Given a nonempty P in which every chain has an upper bound and assuming no maximal element exists, every chain C admits a strict upper bound; choosing one for each chain at once turns C↦C∪{chosen strict upper bound} into a progressive map on C, and Bourbaki-Witt applied to the chain-completeness proved here returns a chain equal to its own extension, which is absurd. That is Zorn's lemma, and the Axiom of Choice is used at exactly one point of it, the simultaneous choice of strict upper bounds, and nowhere in this example.

  • C is chain-complete but usually not a complete lattice. An arbitrary union of chains need not be a chain: if x,y∈P are incomparable then {x} and {y} are chains and {x,y} is not, so the family {{x},{y}} has no supremum given by union. This is exactly the gap between this example and The power set is chain-complete, with union as supremum, and it is why chain-completeness rather than completeness is the right hypothesis for Bourbaki–Witt fixed point theorem.

  • An immediate consequence, at the price of the Axiom of Choice. C is nonempty, since ∅∈C, and every chain of C has an upper bound by the verification above. Assume in addition the Axiom of Choice (The Axiom of Choice), which Zorn's lemma assumes outright: Zorn's lemma then applies to C and yields a maximal element, so every poset has a maximal chain. This is the Hausdorff maximal principle, and it costs exactly one application of Zorn, hence the Axiom of Choice. The chain-completeness verified above costs nothing.

  • The verification never used any property of P beyond its being a poset. In particular P may be empty, in which case C={∅} is the one-element poset.

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

Two maximal elements and no greatest element

Statement refuted

Refuted claim: in every poset a maximal element is a greatest element, so that having nothing strictly above it forces an element to lie above everything (FALSE: every maximal element is a greatest element, Maximal element and greatest element).

The witness is

P=P({1,2})∖{{1,2}}={ ∅, {1}, {2} },

ordered by inclusion (Partial order and partially ordered set). Both {1} and {2} are maximal in P, neither is greatest, and P has no greatest element at all.

Facts & Assumptions

Given: P=P({1,2})∖{{1,2}}={∅,{1},{2}}, ordered by inclusion; every member of P is a subset of {1,2}, and {1,2}∉P.

[L1]

m is maximal in P when no x∈P satisfies m<x, and greatest when x≤m for every x∈P (Maximal element and greatest element).

[L2]

A partial order is reflexive, antisymmetric and transitive, and it need not make every two elements comparable; x<y abbreviates x≤y together with x≠y (Partial order and partially ordered set).

Counterexample

technique · direct
1.1

Inclusion is reflexive, antisymmetric and transitive on any collection of sets, so (P,⊆) is a poset, and it has the three elements ∅, {1}, {2}, which are pairwise distinct.

givenL2
1.2

{1} and {2} are incomparable: 1∉{2} gives {1}⊈{2}, and 2∉{1} gives {2}⊈{1}.

givenL2
2.1

{1} is maximal: if x∈P and {1}⊆x then 1∈x, and of the three members of P only {1} contains 1, so x={1}; hence no x∈P satisfies {1}⊊x.

step 1.1L1
2.2

{2} is maximal, by the same argument with 2 in place of 1: the only member of P containing 2 is {2}.

step 1.1L1
2.3

Neither of them is greatest: {2}⊈{1}, so {1} fails to dominate {2}, and symmetrically {2} fails to dominate {1}.

step 1.2L1
2.4

P has no greatest element at all: a greatest M∈P would satisfy {1}⊆M and {2}⊆M, hence {1,2}⊆M; but M⊆{1,2}, so M={1,2}, which is not a member of P.

step 1.1givenL1
3.1

So (P,⊆) is a poset with two maximal elements and no greatest element, which refutes the claim: having nothing strictly above it does not force an element to lie above everything.

step 2.1step 2.2step 2.3step 2.4∎

Remarks

  • This witness is not the smallest one. The refutation in FALSE: every maximal element is a greatest element uses a two element antichain, which is minimal, but not for the reason one might expect: the empty poset satisfies the claim vacuously, having no maximal element at all, while a one element poset satisfies it outright, since its single element is maximal and is greatest by reflexivity. Two elements is therefore the least size at which the claim can fail, and it does fail there. Vacuous satisfaction is not confined to the empty poset, incidentally: (N,≤) has no maximal element either ((N,≤) has no maximal element: Zorn's chain hypothesis fails), and satisfies the claim for that reason. The witness here adds a least element ∅ below both maximal elements, which matters because it shows the failure is not caused by the poset splitting into unrelated pieces. Even a poset with a bottom, in which every element is comparable to something, can carry several maximal elements.

  • The general pattern. Order the proper subsets of a set X with at least two elements by inclusion. The maximal elements are exactly the sets X∖{x} for x∈X: any proper A⊊X sits inside X∖{x} for any x∈X∖A, and nothing lies strictly between X∖{x} and X. Distinct points give distinct maximal elements, so there is one for each point of X, and there is no greatest element. The poset above is the case X={1,2}.

  • What would rescue the claim is totality. In a totally ordered set a maximal element is greatest, since every other element is comparable to it and cannot be strictly above it, which is why the confusion survives in intuition trained on R.

  • Maximality says nothing about comparability: here each maximal element is incomparable to the other, and both are above only ∅. Applications of Zorn's lemma must therefore be arranged so that "nothing is strictly above it" already means "it cannot be extended", since nothing stronger is available.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

(N,≤) has no maximal element: Zorn's chain hypothesis fails

Statement refuted

Refuted claim: the chain hypothesis of Zorn's lemma is redundant, that is every nonempty poset has a maximal element (Zorn's lemma, Maximal element and greatest element).

The witness is (N,≤) with its usual order (Order on the natural numbers). It is nonempty and has no maximal element whatsoever, and the hypothesis of Zorn's lemma that it violates is exactly one: N is itself a chain (Chain in a poset) and it has no upper bound in N (Upper bound, least upper bound, and strict upper bound).

Facts & Assumptions

Given: N with the order m≤n  ⟺  ∃k∈N (m+k=n) (Order on the natural numbers) and addition satisfying m+0=m and m+σ(n)=σ(m+n) (Addition of natural numbers); m<n abbreviates m≤n together with m≠n.

[L1]

≤ is a linear order on N: reflexive, antisymmetric, transitive and total (≤ is a linear order on N).

[L2]

n≠σ(n) for every n∈N (No natural number equals its own successor).

[L3]

m is maximal in a poset when no x satisfies m<x (Maximal element and greatest element).

[L4]

u is an upper bound of S when s≤u for every s∈S (Upper bound, least upper bound, and strict upper bound).

[L5]

A subset is a chain when any two of its elements are comparable (Chain in a poset).

[L6]

Zorn's lemma, stated under the Axiom of Choice (The Axiom of Choice), which it assumes outright: a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma). The Axiom of Choice is a standing assumption of the theorem, not a hypothesis on the poset.

Counterexample

technique · direct
1.1

(N,≤) is a poset and it is nonempty, since 0∈N.

givenL1
1.2

For every n∈N one has n+σ(0)=σ(n+0)=σ(n), so n≤σ(n); and n≠σ(n), so n<σ(n).

givenL2
2.1

N has no maximal element: for any n the element σ(n) lies strictly above it.

step 1.2L3
2.2

N is a chain of the poset (N,≤), because ≤ is total, so any two natural numbers are comparable.

step 1.1L1L5
3.1

That chain has no upper bound in N: an upper bound u would satisfy n≤u for every n, in particular σ(u)≤u; combined with u≤σ(u), antisymmetry would give u=σ(u), which [L2] forbids. So no u∈N is an upper bound of N.

step 2.2step 1.2L1L2L4
4.1

So (N,≤) is a nonempty poset with no maximal element, and of the hypotheses [L6] places on the poset the single one that fails is that every chain has an upper bound, the offending chain being N itself; the Axiom of Choice, assumed throughout [L6], is not a property of (N,≤) and is neither used nor contradicted here. The claim is refuted and Zorn's lemma is untouched.

step 1.1step 2.1step 3.1L6∎

Remarks

  • Nothing exotic is at work. The poset is totally ordered, it is the most familiar order there is, and it is even well ordered (The well-ordering principle). What it lacks is a ceiling. So the hypothesis Zorn's lemma really needs is boundedness of chains, and no amount of good behaviour elsewhere substitutes for it.

  • It fails only at the top. Every chain of N that has an upper bound at all has a least one: the set of its upper bounds is a nonempty subset of N, so The well-ordering principle hands back its least element. The empty chain has least upper bound 0: it is vacuously an upper bound, and 0≤u for every natural u because 0+u=u (Left identity for addition, Order on the natural numbers). So the only chains without suprema are the ones with no upper bound whatever, and N is one of them. The same observation, read as a statement about suprema rather than upper bounds, is A progressive map with no fixed point, on a poset that is not chain-complete.

  • Nonemptiness is not what fails here, and how much work it does depends on the convention. Under the convention of Chain in a poset, where ∅ counts as a chain, "every chain has an upper bound" already forces P≠∅, since an upper bound of ∅ is just some element of P; the separate nonemptiness hypothesis of Zorn's lemma is then emphasis rather than extra strength. Under the competing convention, where "chain" means nonempty chain, the empty poset satisfies the chain hypothesis vacuously and has no maximal element, so nonemptiness must be assumed outright. Either way, what (N,≤) isolates is the failure of the chain hypothesis alone.

  • Adding a single element ∞ above every natural number repairs everything: the chain N then has upper bound ∞, every chain has one, and ∞ is the maximal element Zorn's lemma promises.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

A progressive map with no fixed point, on a poset that is not chain-complete

Statement refuted

Refuted claim: the chain-completeness hypothesis of the Bourbaki–Witt fixed point theorem is decoration, that is every progressive map f:P→P on a poset has a fixed point (Bourbaki–Witt fixed point theorem, Chain-complete poset).

The witness is (N,≤) (Order on the natural numbers) with the successor map f(n)=σ(n)=n+1. It is progressive, and it has no fixed point at all. There is no conflict with Bourbaki–Witt, because (N,≤) is not chain-complete: N is a chain (Chain in a poset) with no upper bound in N ((N,≤) has no maximal element: Zorn's chain hypothesis fails), hence with no least upper bound (Upper bound, least upper bound, and strict upper bound).

Facts & Assumptions

Given: N with the order m≤n  ⟺  ∃k∈N (m+k=n) (Order on the natural numbers) and addition satisfying m+0=m and m+σ(n)=σ(m+n) (Addition of natural numbers), together with the map f:N→N given by f(n)=σ(n).

[L1]

≤ is a linear order on N (≤ is a linear order on N).

[L2]

n≠σ(n) for every n∈N (No natural number equals its own successor).

[L3]

A map is progressive when x≤f(x) for every x, and a poset is chain-complete when every chain has a least upper bound (Chain-complete poset).

[L4]

A least upper bound of S is in particular an upper bound of S (Upper bound, least upper bound, and strict upper bound).

[L5]

N is a chain of (N,≤) and it has no upper bound in N ((N,≤) has no maximal element: Zorn's chain hypothesis fails, Chain in a poset).

[L6]

Bourbaki–Witt: a progressive map on a chain-complete poset has a fixed point (Bourbaki–Witt fixed point theorem).

Counterexample

technique · direct
1.1

f is progressive: for every n one has n+σ(0)=σ(n+0)=σ(n), so n≤σ(n)=f(n).

givenL1L3
1.2

f has no fixed point: f(n)=σ(n)≠n for every n∈N.

givenL2
1.3

(N,≤) is not chain-complete: N is one of its chains and has no upper bound in N, so it has no least upper bound either, a least upper bound being in particular an upper bound.

L3L4L5
2.1

So a progressive map on a poset can fail to have a fixed point, and the claim is refuted: progressivity alone buys nothing.

step 1.1step 1.2L3
2.2

No conflict with [L6] arises, because by step 1.3 the poset is not chain-complete, so Bourbaki–Witt has nothing to say about (N,≤).

step 1.3L6
3.1

Chain-completeness is therefore exactly what Bourbaki–Witt is buying: drop it and the same theorem's other hypothesis, progressivity, is left standing beside a map with no fixed point.

step 2.1step 2.2∎

Remarks

  • The failure is sharp, and it is a missing supremum. Adjoin one element ∞ above every natural number. The enlarged poset is chain-complete: a subset containing ∞ has supremum ∞, a subset of N with an upper bound in N has a least one by The well-ordering principle, a subset of N with none has supremum ∞, and the empty chain has supremum 0. Extending f by f(∞)=∞ keeps it progressive, and the fixed point Bourbaki-Witt promises is ∞, precisely the supremum that was missing. Any progressive map on the enlarged poset must fix ∞, since ∞ is greatest.

  • Monotonicity is not the issue. The map f(n)=σ(n) is order preserving as well as progressive: σ(m)=m+σ(0) and σ(n)=n+σ(0) by the Given, and adding a fixed natural number preserves ≤ in both directions (Order is compatible with addition), so m≤n gives σ(m)≤σ(n). So this is not a case of a badly behaved map defeating the theorem; a perfectly well behaved map is defeated by the poset. Conversely Bourbaki–Witt fixed point theorem assumes no monotonicity at all, which is what lets Zorn's lemma apply it to a map built from an arbitrary choice function.

  • No iteration argument could have worked. Starting at 0 and iterating f walks up N forever without converging, and the fixed point in Bourbaki-Witt is not reached by iterating: it is the supremum of the smallest set closed under f and under suprema of its chains. When that supremum does not exist there is nothing to reach.

  • This is the same defect as in (N,≤) has no maximal element: Zorn's chain hypothesis fails, read one notch higher up the scale of bounds. There the chain N had no upper bound, which is what Zorn's lemma asks of every chain; here the same chain has no least upper bound, which is what Bourbaki–Witt fixed point theorem asks of every chain through chain-completeness. A least upper bound is in particular an upper bound, so the first failure implies the second, and adjoining one top element repairs both at once.

Sources