The Bourbaki-Witt theorem (Theorem 2.3.1) is a very natural result: take a chain-complete poset X, an inflationary map f (namely, f(x) is always above x), and a point x₀ in X, then f has a fixed point above x₀.  This is obtained by the following process: start from x=x₀, and repetitively replace the current value of x by f(x).  If you ever build infinitely many values of x without reaching a fixed point, then take the supremum of all values obtained so far.  Repeat these two operations (replacing f(x) by x, taking sups) for as long as needed.

This is the intuitive idea, but making it a formal proof is more challenging.  Notably, the proof I’m giving of Theorem 2.3.1 seems to progress rather laboriously, going through a series of auxiliary results that should be mostly obvious, but nonetheless require some ingenuity.

Another proof would go through so-called ordinal iteration.  In set theory, one can show that there are objects called ordinals, which generalize the natural numbers by including infinite ordinals.  The sleight-of-hand definition is: the class of ordinals is the smallest class containing 0, such that a+1 is an ordinal for every ordinal a, and the sup of every chain of ordinals is an ordinal.  Actually defining it, which means in particular defining the ordering between ordinals, requires some set-theoretic cunning.  (See the wikipedia page on ordinals.)  One can then obtain the fixed point that the Bourbaki-Witt theorem claims exists by ordinal induction.  That is, we define a collection x_a of points of X by: x₀ is already defined, x_a+1=f(x_a), and if a is the sup of a chain of ordinals b, then x_a is the sup in X of the chain of elements f(x_b).  The class of all ordinals is not a set, i.e., it is not small.  But X is small, so the elements x_a cannot be all distinct.  One then shows that if x_a is equal to x_b, then it is a fixed point of f.  If you include all the needed set theory, this is far from elementary.

Dito Pataraia once found an elegant, and rather elementary of something very close to the Bourbaki-Witt theorem [1].  Apparently, he would only very rarely publish his results, so his proof first appeared in a paper by Martín Escardó [2].  My attention was drawn to this result by an anonymous referee, whom I am thanking here.

What Dito Pataraia proved was a version of the Bourbaki-Witt theorem that requires a bit more assumptions, and produces a vastly stronger result.

The main change in assumptions is that we now require our inflationary maps to be monotonic as well.  This is the case in many applications.  One exception is the Caristi-Waszkiewicz theorem (Exercise 7.4.42).  The other change is that he requires X not to be an inductive poset, rather to be a dcpo; that does not make much of a change, since Markowsky’s Theorem (p.61) tells us that inductive posets and dcpos are one and the same thing, but Markowsky’s Theorem is itself non-trivial.

The big change is in the result: we can find a fixed point x above x₀, not of one inflationary map, but of an arbitrary family (f_i)_{i in I} of inflationary (monotonic) maps simultaneously: we shall have f_i(x)=x with the same x for every i in I.

Here is how Pataraia does it.  In a bold move, he goes to a higher-order concept right away.  Given a dcpo X, he considers the set Infl(X) of all inflationary monotonic maps from X to X.  With the pointwise ordering, Infl(X) is a dcpo, and sups are computed pointwise, as usual.  More: Infl(X) is itself directed.  The key is that for any two inflationary monotonic maps f, g, their composition f o g is inflationary, monotonic, and above both f (since g is inflationary and f monotonic) and g (since f is inflationary).  It follows that Infl(X) has a supremum ⊤.  This is an inflationary, monotonic map.  For every f in Infl(X), f o ⊤ is below ⊤ because ⊤ is the top element, and f o ⊤ is above ⊤ because f is inflationary: so f o ⊤ = ⊤.  It follows that, for every x in X, f(⊤(x)) = ⊤(x).  In other words, ⊤(x) is a fixed point of f, and one that is above x as well since ⊤ is inflationary.  Hence:

Theorem ([2], improving on [1]): On a dcpo X, every family (f_i)_i in I of inflationary (monotonic) maps has a common fixed point x above any given point x₀.  We can take x=⊤(x₀), where ⊤ is an inflationary monotonic map that is independent of x₀ and of the family (f_i)_i in I.

We can also require the common fixed point x to be least.  In this case, we must accept that x will depend on the family (f_i)_i in I.

Theorem ([2]): On a dcpo X, every family (f_i)_i in I of inflationary (monotonic) maps has a least common fixed point x above any given point x₀.

We then obtain the following fixed point induction principle, akin to Fact 2.3.3:

Trick: To show that a property P holds of the least common fixed point x, it is enough to show that P(x₀) holds, that P(y) implies P(f_i(y)) for every y in X and every i in I, and that for every directed family D of elements y of X such that P(y) holds, P(sup D) holds.

Indeed, the set of points that satisfy P is one that  contains x₀, is closed under applications of every f_i, and is closed under taking sups of directed families, hence contains the set F mentioned in the proof of the previous theorem.

— Jean Goubault-Larrecq(June 13th, 2013)

1. Dito Pataraia. A constructive proof of Tarski’s fixed-point theorem for dcpo’s. Presented in the 65th Peripatetic Seminar on Sheaves and Logic, in Aarhus, Denmark, November 1997.
2. Martín H. Escardó. Joins in the frame of nuclei.  Applied Categorical Structures, April 2003, Volume 11, Issue 2, pp 117-124.