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.
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
Finite choice written out: a choice function for three sets
Example
Let
a family of three nonempty sets of natural numbers. A choice function for (Choice function) can be written down outright, by listing its three values:
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 of a function with domain (The natural numbers (von Neumann)), the successor step restricts to the shorter index set, takes a choice function for those values, and overwrites it with one further pair.
Facts & Assumptions
Given: The family , whose members are sets of natural numbers, together with the function with domain the von Neumann natural number (The natural numbers (von Neumann)) given by , , , so that .
A choice function for a family is a function with domain such that for every (Choice function).
For every natural number and every function with domain all of whose values are nonempty, the family of values has a choice function; the proof is an induction on whose successor step restricts to , takes a choice function for , and overwrites it with the single pair for some (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).
Verification
The three members are pairwise distinct: belongs to and to neither of the others, belongs to but not to , and since ; so has exactly three members.
Every member is nonempty: , and .
Let , the set whose three elements are those ordered pairs; it is a relation with domain , and since the three members of are pairwise distinct its three first coordinates are pairwise distinct, so it is single valued: is a function on .
Its values lie where they must: , and , so for every and is a choice function for .
A function of this shape is what the induction of [L2] returns when run on the listing : since has domain and each value is nonempty by step 1.2, [L2] applies with and yields a choice function for , 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 , only on the listing exhibited in the Given.
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 ; since each member has two elements there are choice functions for in all. Nothing in the definition prefers one of them.
-
The particular displayed above is the rule , which happens to work for every nonempty set of natural numbers at once ( is a choice function on ). That is a feature of , not of finiteness. The two ingredients come apart in Russell's shoes and socks, where the family is infinite and carries no such rule.
is a choice function on
Example
Every nonempty subset of has a least element (The well-ordering principle), and that least element is unique, so
is a well defined function, and by construction. It is therefore a choice function on (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 , 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 of nonempty subsets of , with carrying its usual order (Order on the natural numbers).
Every nonempty has a least element: there is with for every (The well-ordering principle).
The order on is antisymmetric: and imply ( is a linear order on ).
A choice function for a family is a function with domain such that for every , and a choice function on is one for (Choice function).
Verification
Let , so and .
has a least element: some satisfies for every .
That least element is unique: if and are both least elements of then and , hence .
So "the least element of " is a definite description, and is a set by Separation, single valued by step 2.2 and total on by step 2.1, hence a function with domain .
Its values lie where they must: is a least element of , and a least element of belongs to , so for every .
Therefore is a choice function for , that is a choice function on , and it was obtained from a rule rather than from any axiom asserting that choices can be made.
Remarks
-
The rule, not the existence, is the point. [L1] gives a least element of each nonempty 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 " a formula in , so the graph of is carved out by Separation from 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 and a function with domain all of whose values are nonempty, and it gives a choice function for the family of the values of . What disqualifies is that it is not for any such : sending each member of to the least index at which takes it as a value injects into , the least index existing by [L1], whereas already contains the pairwise distinct singletons , and no injection exists (The pigeonhole principle on ↗, 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 legitimate notation in a poset (Upper bound, least upper bound, and strict upper bound).
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 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 of two-element sets and a set such that has exactly one element for every .
A choice function for is a function with domain such that for every (Choice function).
The Axiom of Choice asserts that every family of nonempty sets has a choice function (The Axiom of Choice).
Verification
For each , the phrase “the unique element of ” defines one element of from the supplied data.
By Separation, is a set; the uniqueness hypothesis makes it single-valued and total on .
For every , is the unique member of , so . Thus is a choice function constructed in ZF from and .
If the distinguisher 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.
Remarks
- Boundedly many indexed pairs require no choice principle: if the family is listed as , Every natural-number-indexed list of nonempty sets has a choice function on its family of values builds a selection one value at a time. The definition of an arbitrary finite set appears later in Finite, countably infinite, countable, uncountable ↗, so this remark uses only the indexed-family form.
- The argument never uses pairwise disjointness or cardinality two. It uses only the supplied predicate selecting exactly one member of every set.
The power set is chain-complete, with union as supremum
Example
For any set , the power set ordered by inclusion is a poset (Partial order and partially ordered set) in which every -chain (Chain in a poset) has least upper bound
(Upper bound, least upper bound, and strict upper bound). So is chain-complete (Chain-complete poset), and its bottom element is .
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 and its power set , ordered by inclusion.
Axiom of Extensionality: sets with exactly the same elements are equal.
A partial order is a reflexive, antisymmetric and transitive relation (Partial order and partially ordered set).
is an upper bound of when for every , and a least upper bound when in addition for every upper bound of (Upper bound, least upper bound, and strict upper bound).
A subset is a chain when any two of its elements are comparable, and the empty set is a chain (Chain in a poset).
A poset is chain-complete when every chain has a least upper bound, and then is its least element (Chain-complete poset).
Verification
Inclusion partially orders : ; if and then and have the same elements, so by extensionality; and gives .
Let and put , so that exactly when for some ; each such satisfies , hence and .
is an upper bound of : if and then , so .
is least among the upper bounds: let satisfy for every ; any lies in some and hence in , so .
So every subset of has least upper bound , and a chain is in particular a subset, so every chain has one and is chain-complete.
The empty chain is the case , where ; so , which is indeed the least element, since for every .
Remarks
-
The argument proves more than chain-completeness. Neither the construction of nor either of the two bound checks used that is a chain, so every subset of has a supremum and 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 the greatest lower bound is , and the greatest lower bound of the empty family is , the top element. The class is not a set, which is why the empty case is read inside 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 leaves the three-element poset of Two maximal elements and no greatest element, which is still chain-complete, since and are incomparable and so never lie in a common chain, yet it now has two maximal elements and no greatest one.
The chains of a poset, ordered by inclusion, form a chain-complete poset
Example
Let be any poset and let
be the set of its chains (Chain in a poset), ordered by inclusion. Then is chain-complete (Chain-complete poset): an inclusion chain has least upper bound , which is again a chain of because any two of its elements lie in a common member of . Its bottom element is .
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 and the set of chains of , ordered by inclusion; note .
A subset is a chain when any two of its elements are comparable, and the empty set is a chain (Chain in a poset).
Inclusion partially orders . For any , every satisfies , while any containing every also contains every element of ; hence is the least upper bound of (Partial order and partially ordered set, Upper bound, least upper bound, and strict upper bound).
is an upper bound of when for every , and a least upper bound when in addition for every upper bound of (Upper bound, least upper bound, and strict upper bound).
A poset is chain-complete when every chain has a least upper bound, and then is its least element (Chain-complete poset).
A partial order on a set is a relation on that is reflexive, antisymmetric and transitive, each of the three being a condition required of all elements of (Partial order and partially ordered set).
Verification
is a subset of , and inclusion partially orders ; reflexivity, antisymmetry and transitivity are required of all elements of , so they hold in particular for all elements of , and the restriction of inclusion to partially orders .
Let be a chain for inclusion and put .
is a chain of : let , say and with ; as is a chain for inclusion, or , so and both lie in whichever of the two is the larger, and that set is a chain of , hence and are comparable in . So , the case reading with the condition on vacuous.
is an upper bound of for inclusion: for every .
is least among the upper bounds of lying in : such a is in particular an upper bound of in , where is least, so .
So every inclusion chain has least upper bound in , that is is chain-complete, with .
Remarks
-
This is the whole of Zorn's engine. Given a nonempty in which every chain has an upper bound and assuming no maximal element exists, every chain admits a strict upper bound; choosing one for each chain at once turns into a progressive map on , 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.
-
is chain-complete but usually not a complete lattice. An arbitrary union of chains need not be a chain: if are incomparable then and are chains and is not, so the family 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. is nonempty, since , and every chain of 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 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 beyond its being a poset. In particular may be empty, in which case is the one-element poset.
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
ordered by inclusion (Partial order and partially ordered set). Both and are maximal in , neither is greatest, and has no greatest element at all.
Facts & Assumptions
Given: , ordered by inclusion; every member of is a subset of , and .
is maximal in when no satisfies , and greatest when for every (Maximal element and greatest element).
A partial order is reflexive, antisymmetric and transitive, and it need not make every two elements comparable; abbreviates together with (Partial order and partially ordered set).
Counterexample
Inclusion is reflexive, antisymmetric and transitive on any collection of sets, so is a poset, and it has the three elements , , , which are pairwise distinct.
and are incomparable: gives , and gives .
is maximal: if and then , and of the three members of only contains , so ; hence no satisfies .
is maximal, by the same argument with in place of : the only member of containing is .
Neither of them is greatest: , so fails to dominate , and symmetrically fails to dominate .
has no greatest element at all: a greatest would satisfy and , hence ; but , so , which is not a member of .
So 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.
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: has no maximal element either ( 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 with at least two elements by inclusion. The maximal elements are exactly the sets for : any proper sits inside for any , and nothing lies strictly between and . Distinct points give distinct maximal elements, so there is one for each point of , and there is no greatest element. The poset above is the case .
-
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 .
-
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.
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 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: is itself a chain (Chain in a poset) and it has no upper bound in (Upper bound, least upper bound, and strict upper bound).
Facts & Assumptions
Given: with the order (Order on the natural numbers) and addition satisfying and (Addition of natural numbers); abbreviates together with .
is a linear order on : reflexive, antisymmetric, transitive and total ( is a linear order on ).
for every (No natural number equals its own successor).
is maximal in a poset when no satisfies (Maximal element and greatest element).
is an upper bound of when for every (Upper bound, least upper bound, and strict upper bound).
A subset is a chain when any two of its elements are comparable (Chain in a poset).
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
is a poset and it is nonempty, since .
For every one has , so ; and , so .
has no maximal element: for any the element lies strictly above it.
is a chain of the poset , because is total, so any two natural numbers are comparable.
That chain has no upper bound in : an upper bound would satisfy for every , in particular ; combined with , antisymmetry would give , which [L2] forbids. So no is an upper bound of .
So 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 itself; the Axiom of Choice, assumed throughout [L6], is not a property of and is neither used nor contradicted here. The claim is refuted and Zorn's lemma is untouched.
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 that has an upper bound at all has a least one: the set of its upper bounds is a nonempty subset of , so The well-ordering principle hands back its least element. The empty chain has least upper bound : it is vacuously an upper bound, and for every natural because (Left identity for addition, Order on the natural numbers). So the only chains without suprema are the ones with no upper bound whatever, and 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 , since an upper bound of is just some element of ; 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 isolates is the failure of the chain hypothesis alone.
-
Adding a single element above every natural number repairs everything: the chain then has upper bound , every chain has one, and is the maximal element Zorn's lemma promises.
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 on a poset has a fixed point (Bourbaki–Witt fixed point theorem, Chain-complete poset).
The witness is (Order on the natural numbers) with the successor map . It is progressive, and it has no fixed point at all. There is no conflict with Bourbaki–Witt, because is not chain-complete: is a chain (Chain in a poset) with no upper bound in ( 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: with the order (Order on the natural numbers) and addition satisfying and (Addition of natural numbers), together with the map given by .
is a linear order on ( is a linear order on ).
for every (No natural number equals its own successor).
A map is progressive when for every , and a poset is chain-complete when every chain has a least upper bound (Chain-complete poset).
A least upper bound of is in particular an upper bound of (Upper bound, least upper bound, and strict upper bound).
is a chain of and it has no upper bound in ( has no maximal element: Zorn's chain hypothesis fails, Chain in a poset).
Bourbaki–Witt: a progressive map on a chain-complete poset has a fixed point (Bourbaki–Witt fixed point theorem).
Counterexample
is progressive: for every one has , so .
has no fixed point: for every .
is not chain-complete: is one of its chains and has no upper bound in , so it has no least upper bound either, a least upper bound being in particular an upper bound.
So a progressive map on a poset can fail to have a fixed point, and the claim is refuted: progressivity alone buys nothing.
No conflict with [L6] arises, because by step 1.3 the poset is not chain-complete, so Bourbaki–Witt has nothing to say about .
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.
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 with an upper bound in has a least one by The well-ordering principle, a subset of with none has supremum , and the empty chain has supremum . Extending by 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 is order preserving as well as progressive: and by the Given, and adding a fixed natural number preserves in both directions (Order is compatible with addition), so gives . 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 and iterating walks up 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 and under suprema of its chains. When that supremum does not exist there is nothing to reach.
-
This is the same defect as in has no maximal element: Zorn's chain hypothesis fails, read one notch higher up the scale of bounds. There the chain 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
- Choice function (Wikipedia)
- Axiom of choice (Wikipedia)
- I. Khatchatourian, The Axiom of Choice (University of Toronto MAT327 notes)
- Well-ordering principle (Wikipedia)
- B. Russell, Introduction to Mathematical Philosophy (1919), Ch. 12
- Complete partial order (Wikipedia)
- Complete lattice (Wikipedia)
- Bourbaki-Witt Principle (Menemui Matematik 39(1), 2017)
- Bourbaki–Witt theorem (Wikipedia)
- Zorn's lemma (Wikipedia)
- Greatest element and least element (Wikipedia)
- Maximal and minimal elements (Wikipedia)
- Partially ordered set (Wikipedia)
- Encyclopedia of Mathematics, Zorn lemma
- Upper and lower bounds (Wikipedia)