7
$\begingroup$

Pataraia proved in

"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

that in a directed-complete partial order (dcpo) with a minimum element each monotone map has a fixpoint. (For the purpose of this particular theorem, a directed set is a poset in which each finite subset is bounded from above, and a dcpo is a poset in which each directed subset has a supremum.) Dito Pataraia is mostly acknowledged for the new proof method rather than the theorem itself.

Who was the first to actually state and prove this theorem is any way? One can argue that the proof of Markowski's Theorem 9(i) in "Chain-complete posets and directed sets with applications" can be adapted to our situation. Still, the clear-cut statement of the aforementioned theorem is not present in Markowski's paper.

| cite | improve this question | |
$\endgroup$
3
$\begingroup$

The non-constructive version of Pataraia's theorem is called the Bourbaki-Witt fixed point theorem. I learned it from Davey and Priestley's Introduction to Lattices and Order, and Wikipedia gives the following references:

However, as usual, some classically equivalent formulations of this theorem become distinguishable constructively. Andrej Bauer and Peter Lumsdaine have a very nice paper about this, On the Bourbaki-Witt Principle in Toposes, where they examine these issues in detail.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ @user49915: I guess I don't understand your question, then. My understanding was that (a) the Bourbaki-Witt theorem is that every inflationary function on a chain-complete poset has a least fixed point, (b) Pataraia's theorem is that monotone functions on pointed domains have least fixed points, and (c) Markowsky's Theorem is that chain-complete posets and dcpos are the same thing. So (c) implies (a) and (b) are equivalent. (Also, I must admit I never read any of these papers (except the Bauer-Lumsdaine one): I learned the theorems second-hand...) $\endgroup$ – Neel Krishnaswami Jun 27 '18 at 9:39
  • $\begingroup$ Yes, that's right. However, note that if you have a DCPO D and a monotone function f, you can define the set of post-fixed-points $\{ x \in D $\endgroup$ – Neel Krishnaswami Jun 27 '18 at 13:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy