Bourbaki–Witt theorem

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In mathematics, the Bourbaki–Witt theorem in order theory, named after Nicolas Bourbaki and Ernst Witt, is a basic fixed point theorem for partially ordered sets. It states that if X is a non-empty chain complete poset, and

such that

for all

then f has a fixed point. Such a function f is called inflationary or progressive.

Special case of a finite poset[edit]

If the poset X is finite then the statement of the theorem has a clear interpretation that leads to the proof. The sequence of successive iterates,

where x0 is any element of X, is monotone increasing. By the finiteness of X, it stabilizes:

for n sufficiently large.

It follows that x is a fixed point of f.

Proof of the theorem[edit]

Pick some . Define a function K recursively on the ordinals as follows:

If is a limit ordinal, then by construction

is a chain in X. Define

This is now an increasing function from the ordinals into X. It cannot be strictly increasing, as if it were we would have an injective function from the ordinals into a set, violating Hartogs' lemma. Therefore the function must be eventually constant, so for some

that is,

So letting

we have our desired fixed point. Q.E.D.

Applications[edit]

The Bourbaki–Witt theorem has various important applications. One of the most common is in the proof that the axiom of choice implies Zorn's lemma. We first prove it for the case where X is chain complete and has no maximal element. Let g be a choice function on

Define a function

by

This is allowed as, by assumption, the set is non-empty. Then f(x) > x, so f is an inflationary function with no fixed point, contradicting the theorem.

This special case of Zorn's lemma is then used to prove the Hausdorff maximality principle, that every poset has a maximal chain, which is easily seen to be equivalent to Zorn's Lemma.

Bourbaki–Witt has other applications. In particular in computer science, it is used in the theory of computable functions. It is also used to define recursive data types, e.g. linked lists, in domain theory.

References[edit]