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.

✓ 14 results · all verified · 10 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 4 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

1 · Prerequisites

2 · Summary

Natural-number induction and recursive addition provide the background for finite choice: a selection from a family indexed by a natural number is built one value at a time. The page proves implications and equivalences over ZF; it does not use an independence theorem to classify what ZF itself can prove.

The development introduces chains, upper bounds, maximal elements and chain-complete posets over the partial orders it requires, and applies the Axiom of Choice. For a progressive self-map, the least admissible set is closed under the map and chain suprema; its extremal elements are comparable, and minimality makes the set a chain. Its supremum is fixed, yielding Bourbaki-Witt without monotonicity or Choice. Applying that theorem to chains ordered by inclusion proves Zorn's lemma once Choice selects strict upper bounds. Conversely, Zorn applied to partial choice functions yields a maximal function whose domain is the whole family. Hence Zorn's lemma and Choice are equivalent over ZF, while maximal and greatest elements remain distinct.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Chain in a poset

Definition

Let (P,≤) be a poset (Partial order and partially ordered set). A subset C⊆P is a chain if any two of its elements are comparable: for all x,y∈C, either x≤y or y≤x.

Equivalently, C is a chain if the restriction of ≤ to C is a total order on C.

Remarks

  • The empty set is a chain, and so is every singleton, both vacuously. This is not a technicality to be waved past: the empty chain is exactly what forces a chain-complete poset to have a least element (Chain-complete poset), and that least element is the starting point of the Bourbaki–Witt construction (Bourbaki–Witt fixed point theorem). A convention that quietly excludes the empty chain has to reintroduce the same content as a separate hypothesis.
  • A chain need not be finite, need not be countable, and need not have a largest element. In the power set of N ordered by inclusion, the sets {1,…,n} for n≥1 form a chain with no largest element.
  • "Chain" is a property of a subset, not of the ambient poset. The whole poset P is a chain exactly when ≤ is a total order.
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Upper bound, least upper bound, and strict upper bound

Definition

Let (P,≤) be a poset (Partial order and partially ordered set) and S⊆P.

An element u∈P is an upper bound of S if s≤u for every s∈S.

An element u∈P is a least upper bound (or supremum) of S if u is an upper bound of S and u≤v for every upper bound v of S. When it exists we write u=sup⁡S.

An element u∈P is a strict upper bound of S if s<u for every s∈S.

Remarks

  • A least upper bound is unique when it exists. If u and u′ are both least upper bounds of S then each is an upper bound and each is below the other, so u≤u′ and u′≤u, whence u=u′ by antisymmetry (Partial order and partially ordered set). This is what makes the notation sup⁡S legitimate. Antisymmetry is not peculiar to this argument: the same two-inequality step gives uniqueness of a greatest element (Maximal element and greatest element), and it is used essentially in Bourbaki–Witt fixed point theorem, whose fixed point is obtained by passing from f(c)≤c and c≤f(c) to f(c)=c. Drop antisymmetry and it is the conclusion, not merely the notation, that goes: on two distinct elements each below the other, every subset still has a least upper bound, yet the map exchanging the two satisfies x≤f(x) and has no fixed point.
  • Every element of P is an upper bound of the empty set, vacuously. Consequently sup⁡∅, when it exists, is the least element of P.
  • An upper bound of S need not belong to S, and S may have many upper bounds and no least one. In Q with its usual order, the set {q∈Q:q2<2} has upper bounds but no least upper bound.
  • In a poset, a strict upper bound is exactly an upper bound outside S. If u is strict then u∉S, since u<u is impossible. Conversely, if u is an upper bound and u∉S, then every s∈S satisfies s≤u and s≠u, hence s<u. This distinction from an arbitrary upper bound matters in Zorn's lemma, where the argument must produce one outside the chain.
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Maximal element and greatest element

Definition

Let (P,≤) be a poset (Partial order and partially ordered set) and m∈P.

m is a maximal element of P if no element of P is strictly above it: there is no x∈P with m<x. Equivalently, for every x∈P, if m≤x then x=m.

m is a greatest element (or maximum) of P if x≤m for every x∈P.

Minimal and least elements are defined dually, reversing every inequality.

Remarks

  • Maximal is not greatest, and the difference is the single most common confusion about ordered sets. A maximal element has nothing strictly above it; a greatest element is above everything. In a total order the two coincide, which is why the distinction is invisible to intuition trained on R, but a partial order may have many maximal elements and no greatest one. The refutation is FALSE: every maximal element is a greatest element, witnessed by Two maximal elements and no greatest element ↗.
  • A greatest element is always maximal, and it is unique when it exists: if m and m′ are both greatest then m≤m′ and m′≤m, so m=m′ by antisymmetry. Maximal elements need not be unique.
  • Zorn's lemma concludes that a maximal element exists, never that a greatest one does (Zorn's lemma). In a particular poset the maximal element it produces may happen to be greatest, since a greatest element is maximal; what Zorn never supplies is a guarantee of greatestness. Every application of Zorn therefore has to be phrased so that maximality is enough, typically by arranging the poset so that a maximal object cannot be extended, which is a statement about nothing being strictly above it.
  • Maximality says nothing about comparability: a maximal element may be incomparable to other elements, including to other maximal ones. In Two maximal elements and no greatest element ↗ the two maximal elements are incomparable to each other, and in an antichain every element is maximal and is incomparable to all the rest.
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Chain-complete poset

Definition

A poset (P,≤) is chain-complete if every chain C⊆P (Chain in a poset) has a least upper bound sup⁡C in P (Upper bound, least upper bound, and strict upper bound).

The empty set is a chain, so a chain-complete poset has an element ⊥:=sup⁡∅, and ⊥ is the least element of P: every x∈P is an upper bound of ∅, so ⊥≤x by leastness. In particular a chain-complete poset is nonempty.

A map f:P→P is progressive (also inflationary, or increasing in Bourbaki's sense) if x≤f(x)for every x∈P.

Remarks

  • Progressive is not monotone. A progressive map is required to move each point weakly upward; it is not required to preserve the order, and Bourbaki–Witt fixed point theorem assumes no monotonicity whatsoever. This is what makes the theorem strong enough to drive Zorn's lemma, where the map is built from an arbitrary choice function and has no reason to be monotone.
  • On the empty-chain convention. Some authors let "chain" mean nonempty chain, and then state Bourbaki–Witt for a nonempty chain-complete poset. The two conventions give the same theorem. Given P≠∅ chain-complete in the nonempty-chain sense and f progressive, pick any p∈P and pass to P≥p={x∈P:p≤x}: it contains p, it is closed under f because f is progressive, the supremum of a nonempty chain in P≥p again lies in P≥p, and sup⁡∅=p there. So P≥p is chain-complete in the sense used here. Including the empty chain simply packages that reduction into the definition, and it is Wikipedia's convention for a pointed chain-complete order.
  • Chain-completeness is strictly weaker than requiring least upper bounds for all subsets (which would make P a complete lattice). The power set of any set is a complete lattice, hence chain-complete (The power set is chain-complete, with union as supremum ↗); the posets Zorn's lemma is applied to usually are not.
  • The hypothesis cannot be dropped from Bourbaki–Witt fixed point theorem: a progressive map on a poset that is not chain-complete may have no fixed point (A progressive map with no fixed point, on a poset that is not chain-complete ↗).
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Every natural-number-indexed list of nonempty sets has a choice function on its family of values

Statement

Let n∈N and let F be a function with domain n all of whose values are nonempty sets. Then the family of its values, F=F[n]={ F(i):i∈n }, has a choice function (Choice function).

This is a theorem of ZF: its proof uses no form of the Axiom of Choice (The Axiom of Choice).

What is proved below is exactly the displayed statement, by induction on n. The natural number n serves as the index set in the von Neumann sense, n={0,1,…,n−1} (The natural numbers N (von Neumann)), so "F has domain n" says precisely that the members of F are listed as F(0),…,F(n−1). The listing need not be injective, and F is the set of values, so repetitions are harmless and are not counted.

The displayed statement and its proof use only a natural-number-indexed function. They do not identify an arbitrary finite family with a particular enumeration.

Facts & Assumptions

Given: A natural number n, used as the index set n={0,…,n−1}, and a function F with domain n such that F(i)≠∅ for every i∈n; write F[n]={F(i):i∈n} for the family of values of F.

[A1]

P(n) denotes the statement: for every function F with domain n all of whose values are nonempty sets, the family F[n] has a choice function.

[L1]

Induction principle: if P(0) holds and P(n) implies P(n+1) for every n∈N, then P(n) holds for every n∈N, where n+1 denotes the successor σ(n) (The principle of mathematical induction, Addition of natural numbers).

[L2]

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

[L3]

0=∅ and σ(n)=n∪{n}, so n⊆σ(n) (The natural numbers N (von Neumann)). Thus a function F with domain σ(n) restricts to a function with domain n; moreover, directly from the definition of image, y∈F[σ(n)] iff y=F(i) for some i∈n or y=F(n), so F[σ(n)]=F[n]∪{F(n)}.

Proof

technique · induction
1.1

Base case: 0=∅, so the only function with domain 0 is the empty function, its family of values is F[0]=∅, and the empty function has domain ∅ and satisfies the defining condition vacuously, so it is a choice function for F[0]; hence P(0) holds.

baseA1L2L3
1.2

Inductive hypothesis: fix n∈N and assume P(n), that every function with domain n whose values are all nonempty has a choice function for its family of values.

ihA1
1.3

Let F be an arbitrary function with domain σ(n)=n∪{n} all of whose values are nonempty sets; write S=F(n) and G=F[n], the family of values of the restriction F↾n, so that F[σ(n)]=G∪{S}.

givenL3
2.1

The restriction F↾n is a function with domain n, and every value of it is a value of F, hence nonempty; so the inductive hypothesis applies to it and supplies a choice function h for G, a function with domain G satisfying h(T)∈T for every T∈G.

step 1.3step 1.2L2L3
2.2

The set S=F(n) is one of the values of F, hence nonempty, so there exists an element of S; fix one and call it a.

step 1.3choose
3.1

Define g=(h↾(G∖{S}))∪{(S,a)}; its two pieces are functions with the disjoint domains G∖{S} and {S}, so g is a function, and its domain is (G∖{S})∪{S}=G∪{S}=F[σ(n)].

step 2.1step 2.2step 1.3construct
4.1

Every T∈F[σ(n)] is either S or a member of G∖{S}; in the first case g(S)=a∈S, and in the second g(T)=h(T)∈T because h is a choice function for G. So g(T)∈T throughout.

step 3.1step 2.1step 2.2
5.1

Hence g is a choice function for F[σ(n)], and since F was an arbitrary function with domain σ(n) with nonempty values, P(n) implies P(n+1).

step 4.1step 3.1step 1.3L2A1
6.1

By the induction principle, P(n) holds for every n∈N: the family of values of any function whose domain is a natural number and whose values are nonempty has a choice function.

step 1.1step 5.1L1discharge-induction∎

Remarks

  • Later finiteness terminology. A finite set is defined later as one equinumerous with a natural number (Finite, countably infinite, countable, uncountable ↗). That terminology is not used in the proof above, which keeps its exact indexed-family scope.
  • Where the Axiom of Choice would be needed, and why it is not needed here. Step 2.2 picks one element out of one nonempty set. That is a single existential instantiation, licensed by first-order logic alone. The induction performs one such instantiation per stage, and the stages are indexed by a natural number, so the process terminates. ZF cannot in general turn an arbitrary infinite family of nonempty sets into a simultaneous choice function; that is the gap The Axiom of Choice fills. An infinite family with a distinguished element in each member may still have an explicit choice function in ZF, as Russell's shoes and socks ↗ shows.
  • Why the family is presented as an indexed one. Stated over "a family of exactly n sets", the successor step would have to assert that deleting one member of a family of n+1 sets leaves exactly n, which is a claim about cardinality and needs a theory of finiteness this page does not have. Indexed by n, the same step is the restriction F↾n of a function, which is immediate from n⊆σ(n) and costs nothing. Nothing else in the argument changes.
  • The listing may repeat, and the argument is arranged so that repetition needs no separate treatment: g is built by overwriting rather than by adjoining, so it is a function whether or not S already occurs among F(0),…,F(n−1). In particular F may have strictly fewer than n members.
  • The lemma is not a special case of the Axiom of Choice that happens to be provable; it is the precise boundary of what is free. Russell's shoes and socks ↗ makes the boundary concrete, and Finite choice written out: a choice function for three sets ↗ works this induction out on a small family.
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Admissible subset (Bourbaki–Witt)

Definition

Let (P,≤) be a chain-complete poset and f:P→P a progressive map (Chain-complete poset). A subset A⊆P is f-admissible (or simply admissible, when f is fixed) if:

  • (C1) closed under f: f(x)∈A for every x∈A;
  • (C2) closed under chain suprema: sup⁡C∈A for every chain C⊆A.

Remarks

  • (C2) already forces ⊥∈A. The empty set is a chain contained in A (Chain in a poset), and sup⁡∅=⊥, so every admissible set contains the least element of P. Presentations that list "⊥∈A" as a third condition are therefore stating a consequence, not an extra hypothesis. This is the first of four places on this page where insisting that the empty set counts as a chain removes a case rather than creating one; the others are The cut at an extremal element is closed under chain suprema, A supremum of extremal elements is extremal and Every element of M is extremal.
  • The suprema in (C2) are taken in P and exist there by chain-completeness; the condition is that they land back inside A.
  • P itself is admissible, so admissible sets exist. The content of A smallest admissible set exists is that there is a smallest one, and its minimality is what carries the two decisive steps of the Bourbaki–Witt argument, Everything in M is comparable to an extremal element and Every element of M is extremal: to prove that all elements of the smallest admissible set M have some property, one shows that the elements of M with that property again form an admissible set. The remaining lemmas use only admissibility of M, progressivity of f, and the order axioms.
  • Nothing here assumes f is monotone, injective, or continuous in any sense. Only (C1), (C2) and progressivity are ever used.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

A smallest admissible set exists

Statement

Let (P,≤) be a chain-complete poset and f:P→P progressive (Chain-complete poset). Then there is a smallest f-admissible subset M⊆P (Admissible subset (Bourbaki–Witt)): M is admissible, and M⊆A for every admissible A⊆P.

Facts & Assumptions

Given: A chain-complete poset (P,≤) and a progressive map f:P→P.

[A1]

A subset A⊆P is admissible when (C1) f(x)∈A for every x∈A, and (C2) sup⁡C∈A for every chain C⊆A (Admissible subset (Bourbaki–Witt)).

[L1]

Every chain of P has a least upper bound in P (Chain-complete poset).

Proof

technique · direct
1.1

P satisfies (C1), because f is a map from P to P, so f(x)∈P for every x∈P.

A1
1.2

P satisfies (C2), because every chain C⊆P has a least upper bound in P.

A1L1
2.1

So P is admissible, and the collection A of all admissible subsets of P is nonempty.

step 1.1step 1.2A1
3.1

Define M=⋂A, the intersection of all admissible subsets of P.

step 2.1construct
4.1

Let x∈M. For every A∈A we have x∈A, hence f(x)∈A by (C1); since this holds for every A∈A, f(x)∈M, so M satisfies (C1).

step 3.1A1
4.2

Let C⊆M be a chain. For every A∈A we have C⊆A, hence sup⁡C∈A by (C2); since this holds for every A∈A, sup⁡C∈M, so M satisfies (C2).

step 3.1A1L1
4.3

If A⊆P is admissible then A∈A, so M⊆A because M is the intersection of a collection containing A.

step 3.1
5.1

M is admissible.

step 4.1step 4.2A1
6.1

M is admissible and contained in every admissible subset, so it is the smallest one.

step 5.1step 4.3∎

Remarks

  • Uniqueness is automatic: two smallest admissible sets each contain the other, so they are equal. This licenses writing M for "the" smallest admissible set throughout Extremal element and its cut (Bourbaki–Witt) and the lemmas that follow.
  • M is never empty. Condition (C2) applied to the empty chain puts ⊥=sup⁡∅ into every admissible set, so ⊥∈M.
  • Minimality is used exactly twice in what follows, in Everything in M is comparable to an extremal element and in Every element of M is extremal, and both times in the same shape: to prove that all of M has some property, one shows that the elements of M with that property again form an admissible set, which minimality then forces to be all of M. That pattern is what replaces transfinite recursion in this proof of Bourbaki–Witt fixed point theorem. The remaining lemmas use only admissibility of M, progressivity of f, and the order axioms.
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Extremal element and its cut (Bourbaki–Witt)

Definition

Let (P,≤) be a chain-complete poset, f:P→P progressive, and let M be the smallest f-admissible subset of P (A smallest admissible set exists).

An element x∈M is extremal if for every y∈M with y<x,f(y)≤x.

For x∈M, the cut at x is the subset Mx:={ y∈M : y≤x  or  f(x)≤y }⊆M.

Remarks

  • Read extremality as: x cannot be jumped over from below. If y sits strictly below x inside M, then applying f to y does not carry it past x. Nothing in the definition says such y exist; ⊥ is extremal vacuously.
  • The cut Mx is the set of elements of M that are comparable to x in the strong sense of lying at or below x, or at or above f(x). It deliberately omits anything strictly between x and f(x). The whole Bourbaki–Witt argument consists of showing that for extremal x the cut is everything (Everything in M is comparable to an extremal element) and that every element is extremal (Every element of M is extremal), and those two facts together say precisely that M is totally ordered (The smallest admissible set is a chain).
  • Both notions are relative to M and to f, not to P. They are scaffolding for one proof and are not used after Bourbaki–Witt fixed point theorem.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The cut at an extremal element is closed under f

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, M the smallest admissible set, and x∈M extremal (Extremal element and its cut (Bourbaki–Witt)). Then the cut Mx satisfies f(y)∈Mx for every y∈Mx.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, an extremal x∈M, and an element y∈Mx.

[A1]

x is extremal: for every z∈M with z<x, f(z)≤x (Extremal element and its cut (Bourbaki–Witt)).

[A2]

Mx={z∈M:z≤x or f(x)≤z} (Extremal element and its cut (Bourbaki–Witt)).

[L1]

M is admissible, so it is closed under f and under suprema of its chains (A smallest admissible set exists, Admissible subset (Bourbaki–Witt)).

[L2]

f is progressive: z≤f(z) for every z∈P (Chain-complete poset).

[L3]

≤ is a partial order: it is reflexive (u≤u) and transitive (u≤v and v≤w imply u≤w), and its strict form u<v means u≤v together with u≠v (Partial order and partially ordered set).

Proof

technique · cases
1.1

Since y∈Mx we have y∈M, and M is closed under f, so f(y)∈M.

A2L1
1.2

Membership of Mx gives y≤x or f(x)≤y, and the relation y≤x holds exactly when y<x or y=x, by the definition of the strict order.

A2L3
1.3

Suppose y<x.

assume-case below
1.4

Suppose y=x.

assume-case equal
1.5

Suppose f(x)≤y.

assume-case above
2.1

In the case y<x, extremality of x gives f(y)≤x, so f(y) lies in M and satisfies f(y)≤x, hence f(y)∈Mx.

step 1.3A1step 1.1A2
2.2

In the case y=x, we get f(y)=f(x), and f(x)≤f(x) by reflexivity, so f(y)∈M satisfies the second alternative, hence f(y)∈Mx.

step 1.4step 1.1A2L3
2.3

In the case f(x)≤y, progressivity gives y≤f(y), so f(x)≤f(y) by transitivity, hence f(y)∈Mx.

step 1.5L2step 1.1A2L3
3.1

The three cases cover every y∈Mx, and each yields f(y)∈Mx.

step 1.2step 2.1step 2.2step 2.3cases-exhaustive∎

Remarks

  • The case y=x is the one that explains the shape of the cut. It is precisely why Mx is defined with f(x)≤z rather than x<z: the image f(x) must itself land inside Mx, and it does so on the upper side.
  • Extremality of x is used only in the first case, and it is exactly what stops f from carrying an element from strictly below x into the forbidden zone strictly between x and f(x). That zone is what the cut omits, and keeping it empty of elements of M is what eventually makes M a chain (The smallest admissible set is a chain).
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The cut at an extremal element is closed under chain suprema

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, M the smallest admissible set, and x∈M extremal (Extremal element and its cut (Bourbaki–Witt)). Then sup⁡C∈Mx for every chain C⊆Mx.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, an extremal x∈M, and a chain C⊆Mx.

[A1]

Mx={z∈M:z≤x or f(x)≤z} (Extremal element and its cut (Bourbaki–Witt)).

[L1]

M is admissible, so it is closed under f and under suprema of its chains (A smallest admissible set exists).

[L2]

Every chain of P has a least upper bound in P (Chain-complete poset).

[L3]

A least upper bound of a set is itself an upper bound of that set and is below every other upper bound (Upper bound, least upper bound, and strict upper bound).

[L4]

≤ is a partial order, in particular transitive: u≤v and v≤w imply u≤w (Partial order and partially ordered set).

Proof

technique · cases
1.1

Write s=sup⁡C, which exists in P because C is a chain.

L2construct
1.2

Since C⊆Mx⊆M and M is closed under suprema of its chains, s∈M.

A1L1
1.3

Suppose every z∈C satisfies z≤x.

assume-case under
1.4

Suppose some z0∈C satisfies z0≰x.

assume-case over
2.1

In the first case x is an upper bound of C, so s≤x because s is the least upper bound, hence s∈Mx.

step 1.3step 1.1L3step 1.2A1
2.2

In the second case z0∈Mx together with z0≰x forces f(x)≤z0, and z0≤s since s is an upper bound of C, so f(x)≤s by transitivity, hence s∈Mx.

step 1.4A1step 1.1step 1.2L3L4
3.1

Either every element of C is below x or some element is not, so the two cases are exhaustive and sup⁡C∈Mx in both.

step 2.1step 2.2cases-exhaustive∎

Remarks

  • The empty chain is covered without a separate argument: it falls into the first case vacuously, and sup⁡∅=⊥≤x.
  • Note which property of the supremum each case uses. The first case uses leastness, that s is below any upper bound; the second uses only that s is an upper bound. Both halves of the definition of least upper bound are needed, which is why chain-completeness cannot be weakened here to the mere existence of some upper bound.
  • Together with The cut at an extremal element is closed under f this makes Mx admissible, which is what Everything in M is comparable to an extremal element feeds to minimality.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

Everything in M is comparable to an extremal element

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, M the smallest admissible set, and x∈M extremal (Extremal element and its cut (Bourbaki–Witt)). Then Mx=M; that is, for every y∈M, either y≤x or f(x)≤y.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, and an extremal x∈M.

[A1]

Mx={z∈M:z≤x or f(x)≤z}, so Mx⊆M by construction (Extremal element and its cut (Bourbaki–Witt)).

[L1]
[L2]

Mx is closed under suprema of its chains (The cut at an extremal element is closed under chain suprema).

[L3]

M is contained in every admissible subset of P (A smallest admissible set exists).

[L4]

A subset is admissible when it is closed under f and under suprema of its chains (Admissible subset (Bourbaki–Witt)).

Proof

technique · direct
1.1

Mx is closed under f.

L1
1.2

Mx is closed under suprema of its chains.

L2
2.1

So Mx is an admissible subset of P.

step 1.1step 1.2L4
3.1

By minimality of M, every admissible subset contains M, so M⊆Mx.

step 2.1L3
4.1

Together with Mx⊆M this gives Mx=M.

step 3.1A1
5.1

Unfolding the definition of Mx, every y∈M satisfies y≤x or f(x)≤y.

step 4.1A1∎

Remarks

  • This is the first payoff of minimality, and the pattern is worth naming: to prove that everything in M has a property, collect the elements that have it, show the collection is admissible, and let minimality do the rest. The same move proves Every element of M is extremal.
  • The conclusion is a comparability statement with a gap. It says nothing about elements strictly between x and f(x), and indeed the content of the lemma is that M has none: an element of M lies at or below x, or at or above f(x), never inside.
  • The hypothesis that x is extremal is doing real work and cannot be dropped. It is what Every element of M is extremal later supplies for every element, which is what turns this one-sided statement into total comparability (The smallest admissible set is a chain).
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

The image of an extremal element is extremal

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, M the smallest admissible set, and x∈M extremal (Extremal element and its cut (Bourbaki–Witt)). Then f(x) is extremal.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, an extremal x∈M, and an element y∈M with y<f(x).

[A1]

x is extremal: for every z∈M with z<x, f(z)≤x (Extremal element and its cut (Bourbaki–Witt)).

[L1]

For every z∈M, either z≤x or f(x)≤z (Everything in M is comparable to an extremal element).

[L2]

M is closed under f (A smallest admissible set exists).

[L3]

f is progressive: z≤f(z) for every z∈P (Chain-complete poset).

[L4]

≤ is a partial order: it is reflexive (u≤u), transitive (u≤v and v≤w imply u≤w) and antisymmetric (u≤v and v≤u imply u=v), and its strict form u<v means u≤v together with u≠v (Partial order and partially ordered set).

Proof

technique · cases
1.1

f(x)∈M because M is closed under f, so it makes sense to ask whether f(x) is extremal.

L2
1.2

It suffices to show f(y)≤f(x) for the given y∈M with y<f(x), since that is exactly the defining condition.

suffices: f(y) le f(x)
1.3

Comparability at the extremal x gives y≤x or f(x)≤y.

L1
1.4

Suppose y<x.

assume-case strict
1.5

Suppose y=x.

assume-case equal
2.1

The alternative f(x)≤y is impossible: y<f(x) gives y≤f(x) with y≠f(x), so f(x)≤y together with y≤f(x) would force f(x)=y by antisymmetry, contradicting y≠f(x). (Transitivity alone would only give f(x)≤f(x), which is no contradiction; antisymmetry is what is doing the work.) Hence y≤x.

step 1.3step 1.2L4
2.2

In the case y<x, extremality of x gives f(y)≤x, and progressivity gives x≤f(x), so f(y)≤f(x) by transitivity.

step 1.4A1L3L4
2.3

In the case y=x, we get f(y)=f(x), hence f(y)≤f(x) by reflexivity.

step 1.5L4
3.1

The relation y≤x holds exactly when y<x or y=x, by the definition of the strict order, so the two cases are exhaustive and f(y)≤f(x) in both; therefore f(x) is extremal.

step 2.1step 2.2step 2.3L4cases-exhaustive∎

Remarks

  • Step 2.1 is where the comparability lemma earns its place. Without it there would be no way to rule out an element of M sitting strictly between x and f(x), and such an element would break extremality of f(x) immediately.
  • Extremality is not a monotonicity condition in disguise. Nothing here assumes f preserves order, and the proof never compares f of two different elements except through x itself.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-25verified 2026-07-26 (claude-opus-5)Open item page →

A supremum of extremal elements is extremal

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, M the smallest admissible set, and C⊆M a chain every element of which is extremal (Extremal element and its cut (Bourbaki–Witt)). Then sup⁡C is extremal.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, a chain C⊆M of extremal elements, and an element y∈M with y<sup⁡C.

[A1]

Every z∈C is extremal: for every w∈M with w<z, f(w)≤z (Extremal element and its cut (Bourbaki–Witt)).

[L1]

For an extremal z and every w∈M, either w≤z or f(z)≤w (Everything in M is comparable to an extremal element).

[L2]

M is an admissible subset of P, so M⊆P, every chain contained in M is a chain of P, and M is closed under suprema of its chains (A smallest admissible set exists, Admissible subset (Bourbaki–Witt)).

[L3]

sup⁡C is an upper bound of C and is below every upper bound of C (Upper bound, least upper bound, and strict upper bound).

[L4]

f is progressive: z≤f(z) for every z∈P (Chain-complete poset).

[L5]

≤ is a partial order: it is reflexive (u≤u), transitive (u≤v and v≤w imply u≤w) and antisymmetric (u≤v and v≤u imply u=v), and its strict form u<v means u≤v together with u≠v (Partial order and partially ordered set).

Proof

technique · direct
1.1

Write s=sup⁡C; it lies in M because C is a chain contained in M and M is closed under suprema of its chains.

L2construct
1.2

It suffices to show f(y)≤s for the given y∈M with y<s.

suffices: f(y) le s
2.1

If y were an upper bound of C then s≤y, since s is below every upper bound; but y<s means y≤s together with y≠s, and s≤y with y≤s would force y=s by antisymmetry, a contradiction. So y is not an upper bound of C.

step 1.2L3L5
3.1

Hence there exists x∈C with x≰y; fix one.

step 2.1choose
4.1

The element x is extremal, so comparability gives y≤x or f(x)≤y.

step 3.1A1L1
5.1

The alternative f(x)≤y is impossible: progressivity gives x≤f(x), so transitivity would yield x≤y, contradicting x≰y. Hence y≤x.

step 4.1step 3.1L4L5
6.1

Moreover y≠x, since y=x would give x≤y by reflexivity, again contradicting x≰y. So y<x.

step 5.1step 3.1L5
7.1

Extremality of x applied to y gives f(y)≤x.

step 6.1step 3.1A1
8.1

Since x∈C and s is an upper bound of C, we have x≤s, so f(y)≤s by transitivity, and s is extremal.

step 7.1step 3.1L3L5∎

Remarks

  • Step 2.1 is the subtle one, and it is where chain-completeness does real work. The move from y<s to "y is not an upper bound of C" is exactly leastness of the supremum, closed off by antisymmetry: leastness gives s≤y, and it is antisymmetry that turns that together with y≤s into y=s, contradicting y≠s. If sup⁡C were merely some upper bound of C, the step would fail and the lemma with it, which is why the Bourbaki-Witt hypothesis asks for least upper bounds rather than upper bounds.
  • The empty chain is covered without comment: sup⁡∅=⊥, and there is no y∈M with y<⊥, so the condition holds vacuously.
  • Nothing here needs C to have a largest element, and in the intended application it does not have one.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Every element of M is extremal

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, and M the smallest admissible set. Then every element of M is extremal (Extremal element and its cut (Bourbaki–Witt)).

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, and the smallest admissible set M.

[L1]

If x∈M is extremal then f(x) is extremal (The image of an extremal element is extremal).

[L2]

If C⊆M is a chain of extremal elements then sup⁡C is extremal (A supremum of extremal elements is extremal).

[L3]

M is itself admissible, so it is closed under f and under suprema of its chains, and M is contained in every admissible subset of P (A smallest admissible set exists).

[L4]

A subset is admissible when it is closed under f and under suprema of its chains (Admissible subset (Bourbaki–Witt)).

Proof

technique · direct
1.1

Let E={x∈M:x is extremal}, so that E⊆M by construction.

construct
2.1

E is closed under f: if x∈E then f(x)∈M because M is closed under f, and f(x) is extremal because x is; so f(x)∈E.

step 1.1L3L1
2.2

E is closed under suprema of its chains: if C⊆E is a chain then C⊆M, so sup⁡C∈M because M is closed under suprema of its chains, and sup⁡C is extremal because every element of C is; so sup⁡C∈E.

step 1.1L3L2
3.1

So E is an admissible subset of P.

step 2.1step 2.2L4
4.1

By minimality of M, M⊆E.

step 3.1L3
5.1

With E⊆M this gives E=M, so every element of M is extremal.

step 4.1step 1.1∎

Remarks

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

The smallest admissible set is a chain

Statement

Let (P,≤) be a chain-complete poset, f:P→P progressive, and M the smallest admissible set. Then M is a chain (Chain in a poset): any two elements of M are comparable.

Facts & Assumptions

Given: A chain-complete poset (P,≤), a progressive f:P→P, the smallest admissible set M, and two elements x,y∈M.

[L1]

Every element of M is extremal (Every element of M is extremal).

[L2]

If x∈M is extremal then every y∈M satisfies y≤x or f(x)≤y (Everything in M is comparable to an extremal element).

[L3]

f is progressive: z≤f(z) for every z∈P (Chain-complete poset).

[L4]

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

[L5]

≤ is a partial order, in particular transitive: u≤v and v≤w imply u≤w (Partial order and partially ordered set).

Proof

technique · direct
1.1

The element x is extremal, because every element of M is.

L1
2.1

Applying comparability at x to the element y, either y≤x or f(x)≤y.

step 1.1L2
3.1

In the second case progressivity gives x≤f(x), so x≤y by transitivity.

step 2.1L3L5
4.1

So in either case x and y are comparable, and since x and y were arbitrary, M is a chain.

step 2.1step 3.1L4∎

Remarks

  • This is where the two halves of the argument meet. Comparability (Everything in M is comparable to an extremal element) was conditional on extremality, and Every element of M is extremal removes the condition; neither alone gives a chain.
  • M being a chain is exactly what makes sup⁡M available in Bourbaki–Witt fixed point theorem. Chain-completeness supplies suprema for chains only, so without this lemma there would be no reason for sup⁡M to exist at all.
  • Note that M is a chain but P need not be. The construction carves a totally ordered piece out of an arbitrary chain-complete poset, and the fixed point is found at the top of that piece.
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)Open item page →

Bourbaki–Witt fixed point theorem

Statement

Let (P,≤) be a chain-complete poset and let f:P→P be progressive, that is x≤f(x) for every x∈P (Chain-complete poset). Then f has a fixed point: there exists c∈P with f(c)=c.

No form of the Axiom of Choice is used, and f is not assumed to be monotone, injective, or continuous in any sense.

Facts & Assumptions

Given: A chain-complete poset (P,≤) and a progressive map f:P→P, with M the smallest f-admissible subset of P.

[L2]

M is admissible: closed under f, and closed under suprema of its chains (A smallest admissible set exists).

[L3]

Every chain of P has a least upper bound in P (Chain-complete poset).

[L4]

f is progressive: x≤f(x) for every x∈P (Chain-complete poset).

[L5]

The order is antisymmetric: u≤v and v≤u imply u=v (Partial order and partially ordered set).

Proof

technique · direct
1.1

M is a chain, so it has a least upper bound in P; write c=sup⁡M.

L1L3construct
1.2

Progressivity gives c≤f(c).

L4
2.1

M is a chain contained in M, and M is closed under suprema of its chains, so c∈M.

step 1.1L1L2
3.1

Since M is closed under f, we have f(c)∈M.

step 2.1L2
4.1

Since c is an upper bound of M and f(c)∈M, we get f(c)≤c.

step 3.1step 1.1
5.1

From f(c)≤c and c≤f(c), antisymmetry gives f(c)=c, so c is a fixed point of f.

step 4.1step 1.2L5∎

Remarks

  • Why this matters here. The usual route to Zorn's lemma runs through transfinite recursion, which needs ordinals, transfinite induction and replacement. Bourbaki–Witt replaces all of that with the smallest admissible set, so the foundations page that supports Zorn's lemma stays ordinal-free. Ordinals are still worth having, but nothing on the path to Zorn or to the ultrafilter lemma requires them.
  • The theorem itself is choice-free. Choice enters only in Zorn's lemma, at the single step where a strict upper bound is selected for every chain simultaneously. Keeping the two separate is what lets later pages state honestly which of their results need choice.
  • Both hypotheses are load-bearing. Progressivity without chain-completeness fails (A progressive map with no fixed point, on a poset that is not chain-complete ↗), and the fixed point is genuinely produced at the top of a chain, not by iterating f: no iteration argument is available, since f need not be monotone and the chain M need not be countable.
  • The fixed point found is sup⁡M, and M is the smallest admissible set, so the construction is canonical rather than a choice among many fixed points.
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)Open item page →

Zorn's lemma

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let (P,≤) be a nonempty poset in which every chain has an upper bound. Then P has a maximal element (Maximal element and greatest element).

Note the hypothesis asks only for an upper bound, not a least upper bound, and the conclusion asserts only that a maximal element exists, never that a greatest one does.

Facts & Assumptions

Given: A nonempty poset (P,≤) in which every chain has an upper bound, and the Axiom of Choice.

[A1]

P≠∅, and every chain C⊆P has an upper bound in P.

[A2]

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

[L1]

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

[L2]

m is maximal when there is no x with m<x (Maximal element and greatest element).

[L3]

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

[L4]

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

[L5]

≤ is a partial order, in particular transitive (u≤v and v≤w imply u≤w) and antisymmetric (u≤v and v≤u imply u=v); the strict order u<v means u≤v and u≠v, so < is irreflexive (Partial order and partially ordered set).

[L6]

Inclusion is a partial order on any collection of sets: A⊆A; A⊆B and B⊆A give A=B by extensionality; and A⊆B⊆C gives A⊆C (Partial order and partially ordered set).

Proof

technique · contradiction
1.1

Suppose P has no maximal element.

assume-contra
1.2

Let C be the set of all chains of P, a subset of the power set of P, partially ordered by inclusion.

L4L6construct
2.1

(C,⊆) is a chain-complete poset: if D⊆C is a chain under inclusion then ⋃D is a chain of P, since any two of its elements lie in a common member of D, and it is the least upper bound of D under inclusion; the empty chain has least upper bound ⋃∅=∅, which is a chain.

step 1.2L4L6
2.2

For C∈C let SC be the set of strict upper bounds of C in P.

step 1.2L3construct
3.1

Each SC is nonempty: C has an upper bound u in P by hypothesis, taking any element of the nonempty P when C=∅; by assumption u is not maximal, so there is v with u<v; then for every c∈C transitivity gives c≤v from c≤u≤v, and c≠v, since c=v would give v≤u and u≤v, hence u=v by antisymmetry, contradicting u<v; so c<v for every c∈C and v∈SC.

step 2.2step 1.1A1L2L3L5
4.1

Apply the Axiom of Choice to the family S={SC:C∈C}, every member of which is nonempty, obtaining a choice function g with g(S)∈S for each S∈S; composing with the map C↦SC, which is a function on C, yields a selection C↦g(SC)∈SC defined for every chain C, and no injectivity of C↦SC is needed, since two chains with the same set of strict upper bounds simply receive the same chosen element.

step 3.1A2
5.1

Define f(C)=C∪{g(SC)} for C∈C; this is again a chain, because g(SC) is a strict upper bound of C and so is comparable to every element of C.

step 4.1step 2.2L3L4L5construct
6.1

f is progressive for inclusion, since C⊆f(C) by construction.

step 5.1
7.1

By Bourbaki–Witt applied to the chain-complete C and the progressive f, there is C0∈C with f(C0)=C0, that is g(SC0)∈C0.

step 2.1step 6.1L1
8.1

But g(SC0) is a strict upper bound of C0, so every element of C0 is strictly below it, giving g(SC0)<g(SC0), which is impossible because < is irreflexive.

step 7.1step 4.1L3L5discharge-contradiction∎

Remarks

  • The Axiom of Choice is used exactly once, at step 4.1, and nowhere else. Everything before it, including Bourbaki–Witt, is a theorem of ZF. That is why the fixed point theorem is kept as a separate item: it marks the boundary between what is free and what is bought.
  • The hypothesis is about all chains, including the empty one, whose upper bounds are exactly the elements of P. So on this library's convention, where ∅ is a chain (Chain in a poset), requiring every chain to have an upper bound already forces P≠∅, and the nonemptiness hypothesis is stated separately for emphasis rather than as an independent assumption. In particular the empty poset does not satisfy the hypothesis: there the empty chain has no upper bound, because there is nothing at all to be one. Under the competing convention, on which chains are required to be nonempty, nonemptiness of P is genuinely independent and cannot be dropped. See (N,≤) has no maximal element: Zorn's chain hypothesis fails ↗ for the failure when unbounded chains exist.
  • The conclusion is maximal, not greatest, and conflating the two is the most common error in applying the lemma (FALSE: every maximal element is a greatest element).
  • The converse holds: Zorn's lemma implies the Axiom of Choice (Zorn's lemma implies the Axiom of Choice), so the two are equivalent over ZF (The Axiom of Choice and Zorn's lemma are equivalent).
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Zorn's lemma implies the Axiom of Choice

Statement

Assume Zorn's lemma: every nonempty poset in which every chain has an upper bound has a maximal element. Then every family of nonempty sets has a choice function (Choice function); that is, the Axiom of Choice holds.

Facts & Assumptions

Given: A family F all of whose members are nonempty, and Zorn's lemma.

[A1]

Every member of F is nonempty.

[A2]

By the assumed Zorn principle, a nonempty poset in which every chain has an upper bound has a maximal element.

[L2]

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

[L3]

m is maximal when there is no element strictly above it (Maximal element and greatest element).

[L4]

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

[L5]

A chain is a subset of a poset in which any two members are comparable (Chain in a poset).

Proof

technique · contradiction
1.1

Suppose F has no choice function.

assume-contra
1.2

Let P be the set of partial choice functions: pairs (G,h) with G⊆F and h a choice function for G, ordered by (G,h)≤(G′,h′) when G⊆G′ and h′ restricted to G equals h.

L2construct
2.1

P is nonempty, since the empty function is a choice function for the empty subfamily, so (∅,∅)∈P.

step 1.2L2
2.2

Every chain in P has an upper bound: given a chain, take the union of the domains and the union of the functions. Any two partial choice functions in the chain are comparable by [L5], so the smaller is a restriction of the larger; their values therefore agree on overlapping domains. Thus the union is a function and is a choice function for the union of the domains.

step 1.2L2L5
2.3

The relation just defined is a partial order on P: it is reflexive, since G⊆G and h restricted to G is h; antisymmetric, since (G,h)≤(G′,h′) and (G′,h′)≤(G,h) give G⊆G′ and G′⊆G, hence G=G′, and then h=h′ restricted to G=G′, which is h′ itself; and transitive, since G⊆G′⊆G′′ gives G⊆G′′, while restricting h′′ to G is the same as first restricting it to G′, which gives h′, and then restricting h′ to G, which gives h. So (P,≤) is a poset.

step 1.2L4
3.1

By the assumed Zorn principle P has a maximal element (G,h).

step 2.1step 2.2step 2.3A2
4.1

If G=F then h is a choice function for F, contrary to the assumption; so there exists S∈F with S∉G.

step 3.1step 1.1L2choose
5.1

The set S is nonempty, so there exists an element of S; fix one and call it a.

step 4.1A1choose
6.1

Then (G∪{S},h∪{(S,a)}) lies in P and is strictly above (G,h), since S∉G.

step 4.1step 5.1step 1.2L2
7.1

This contradicts maximality of (G,h), so the assumption fails and F has a choice function.

step 6.1step 3.1L3discharge-contradiction∎

Remarks

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

The Axiom of Choice and Zorn's lemma are equivalent

Statement

Over ZF, the Axiom of Choice (The Axiom of Choice) and Zorn's lemma (Zorn's lemma) are equivalent: each implies the other.

Facts & Assumptions

Given: The axioms of ZF.

[L1]

The Axiom of Choice implies Zorn's lemma (Zorn's lemma).

[L2]

Zorn's lemma implies the Axiom of Choice (Zorn's lemma implies the Axiom of Choice).

Proof

technique · direct
1.1

Assuming the Axiom of Choice, every nonempty poset in which each chain has an upper bound has a maximal element, which is Zorn's lemma.

L1
1.2

Assuming Zorn's lemma, every family of nonempty sets has a choice function, which is the Axiom of Choice.

L2
2.1

Each statement implies the other over ZF, so they are equivalent.

step 1.1step 1.2∎

Remarks

5 · Examples, counterexamples and false statements

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

FALSE: every maximal element is a greatest element

Statement

FALSE. In every poset, a maximal element is a greatest element: if m has nothing strictly above it, then every element is below m (Maximal element and greatest element).

The statement is plausible because it is true in every totally ordered set, which is where most intuition about order is formed. What defeats it is a maximal element that is not above everything, which only a partial order permits; and since Zorn's lemma delivers maximal elements and nothing more, believing this is the standard way to misapply it.

Facts & Assumptions

Given: The definitions of maximal and greatest element in a poset.

[A1]

m is maximal when there is no x with m<x; m is greatest when x≤m for every x (Maximal element and greatest element).

[L1]

A partial order is a reflexive, antisymmetric, transitive relation, and it need not make every two elements comparable (Partial order and partially ordered set).

Refutation

technique · direct
1.1

Let P={a,b} with a≠b, and let ≤ relate each element only to itself, so that the relation is {(a,a),(b,b)}.

construct
2.1

This relation is reflexive by construction, antisymmetric because u≤v and v≤u only occur when u=v, and transitive because u≤v and v≤w only occur when u=v=w; so (P,≤) is a poset.

step 1.1L1
2.2

But b≤a fails, so a is not greatest; and a≤b fails, so b is not greatest.

step 1.1A1
3.1

There is no x∈P with a<x: the only x with a≤x is a itself, and a<a is false. So a is maximal, and by the same argument so is b.

step 1.1step 2.1A1
4.1

So (P,≤) has maximal elements and no greatest element, refuting the claim.

step 3.1step 2.2∎

Remarks

  • The counterexample is as small as it can be. The empty poset has no maximal element and satisfies the claim vacuously; a one-element poset satisfies it outright, since its single element is maximal and is greatest by reflexivity. So two elements is the minimum, and the antichain above achieves it.
  • Incomparability alone is not what refutes the claim. A poset can contain incomparable elements and still have a greatest one: take P={a,b,c} with a<c and b<c and nothing else, where a and b are incomparable while c is above everything. What a refutation needs is a maximal element that is not greatest, which is a strictly stronger demand than the presence of an incomparable pair.
  • The same phenomenon at scale: ordering the proper subsets of a set by inclusion, every subset missing exactly one point is maximal, and when the set has at least two points there are several such subsets and no greatest one.
  • Why this matters for Zorn. Zorn's lemma concludes that a maximal element exists. Applications must therefore be arranged so that maximality alone is decisive, typically by making "nothing is strictly above it" mean "it cannot be extended". Reading the conclusion as "there is a greatest element" is not a harmless slip: it is a strictly stronger claim that the lemma does not support.
  • A greatest element, when one exists, is maximal and is unique. Only the converse fails.

Sources