# A new and subtle order-theoretic fixed point theorem

Sometimes a very simple argument appears out of the blue and overturns a subject. It is not based on pre-existing theory and heavy involvement in such a theory is actually a handicap in finding such arguments.

Questions

• Have you seen arguments containing either my Special Condition or my Well Founded Elements? The context would probably not identify these ideas clearly, but I do mean them specifically and not any of other historical ones mentioned below.

• Please post some examples of proofs that have been re-formulated to use these ideas instead of the earlier ones. That is, I am encouraging you to re-visit the proofs in the textbooks and your own work that purportedly rely on transfinite recursion, and identify the place where something like my Special Condition is proved, after which you can delete the transfinite recursion.

My webpage includes my papers and slides for two recent seminars. One is about the history of order-theoretic fixed point theorems (largely not what you may think it was) and the other about my application to well founded coalgebras, but both including the Pataraia fixed point theorem.

My version of the fixed point theorem

Let $$s:X\to X$$ be an endofunction of a poset such that

• $$X$$ has a least element $$\bot$$;
• $$X$$ has joins of directed subsets (or chains, classically),
• $$s$$ is monotone: $$\forall x y.x\leq y\Rightarrow s x\leq s y$$;
• $$s$$ is inflationary: $$\forall x.x\leq s x$$;
• $$\forall x y.x=s x\leq y=s y\Rightarrow x=y$$ (the Special Condition).

Then

• $$X$$ has a greatest element $$\top$$;
• $$\top$$ is the unique fixed point of $$s$$;
• if $$\bot$$ satisfies some predicate and it is preserved by $$s$$ and directed joins then it holds for $$\top$$.

Proof 1 Using the lemma for which Max Zorn denied responsibility, $$X$$ has at least one maximal element.

If $$a$$ and $$b$$ are maximal then, since $$a\geq\bot\leq b$$, there is also $$c$$ that is maximal with $$a\geq c\leq b$$. Then $$a=s a$$ and $$b=s b$$ since $$s$$ is inflationary. Since it's also monotone and $$a$$ is maximal, $$c\leq s c\leq s a\leq a$$ and similarly $$s c\leq b$$, so $$c=s c$$ by maximality for its property. By the final condition, $$a=c=b$$.

This also explains why the "obvious" simple counterexamples aren't.

I suggested previously that there might be invocations of Zorn's Lemma in the literature where the thing is actually unique, but this doesn't seem to be a fruitful line. I was thinking of uniqueness up to unique isomorphism, but the algebraic closure is an intriguing question, although I cannot think how to express it as a fixed point of a generally applicable functor on fields. Regarding maximal ideals, to be an example of my question this would need to be some special construction, not just the definition of a general local ring.

Proof 2 If $$X$$ also has binary and therefore all joins, it has $$\top$$ and $$s\top=\top$$. Then by Tarski's elaboration of Knaster's fixed point theorem says that there is a lattice of fixed points, but the Special Condition collapses this to just one.

Proof 3 Using ordinal or transfinite recursion.

We could start from any basepoint, not just $$\bot$$, but by monotonicity and the Special Condition, the least fixed point over another basepoint must still be the same as the one over $$\bot$$.

However, what is commonly recited as transfinite recursion is not a proof unless it cites von Neumann to justify recursion from induction, and also Hartogs to say when to stop.

Even then, further explanation is required to show that the Hartogs ordinal gives the least/unique fixed point. What is needed to do this is essentially to prove that the application satisfies the Special Condition.

Making a full disclosure of all this material gives an extremely heavy-handed proof, whereas Pataraia's proof below is very simple.

I cannot find any proof of the fixed point theorem in the literature where transfinite recursion would have been both valid and the best available method, ie in the period between von Neumann (1928) and Bourbaki (1949) and Witt (1951).

Also, the traditional account of the ordinals depends heavily on Excluded Middle. An intuitionistic treatment was introduced in the 1990s by André Joyal and Ieke Moerdijk in their book Algebraic Set Theory (CUP 1995), which gave rise to much good research, and by me in my paper Intuitionistic Sets and Ordinals (JSL 61, 1996). However, Hartogs' Lemma is irretrievably classical.

Indeed, this incomplete and heavy-handed approach has been noisily forced on mathematicians for over a century, despite Casimir (Kazimierz) Kuratowski's efforts to show how it could be eliminated in favour of closure operators, giving numerous examples from set theory, topology and measure theory (Fundamenta Mathematicae 3, 1922).

Proof 4 Using the Bourbaki-- Witt Theorem, that the subset $$X_0$$ of $$X$$ generated by $$\bot$$, $$s$$ and joins of chains is itself a chain, indeed $$\forall x,y:X_0.\quad y \leq x \;\lor\; s x \leq y,$$ whence $$X_0$$ is a well ordered set.

Comparing this with the previous argument, the Special Condition does a similar job as restricting to the subset generated by $$\bot$$, $$s$$ and joins of chains.

In fact, Ernst Zermelo had already used the argument behind this result in his second proof of the well-ordering principle.

As an example of my previous comment, the Wikipedia page mis-represents the Bourbaki--Witt Theorem by claiming that it was proved using transfinite recursion. It does give the correct citations, but only because Andrej Bauer added them to an existing wrong page.

I have observed in another question that the Zermelo--Bourbaki--Witt theorem ought to have had a fundamental role in textbooks in Algebra.

Proof 5 Using Pataraia's fixed point theorem, which is much simpler and constructive, ie it doesn't use the Axiom of Choice or Excluded Middle, although it is Impredicative.

My version of Dito Pataraia's 1996 Proof

New fixed point theorems often come out of the blue and are based on simple observations that anyone else ought to have seen.

In this case, the anyone else was domain theorists, such as me. I put my blindness down to the indoctrination that I, like other mathematics students across the globe, had had that all mathematical objects are sets. Computer science students are taught that functions are fundamental.

The key point is that, for any dcpo (directed-complete partial order), the set of monotone inflationary endofunctions has least element $$\mathsf{id}$$ and is directed, because $$x \quad\leq\quad f x,g x \quad \leq\quad f(g x),$$ whilst it is also directed-complete pointwise. Hence it has a join (greatest element) $$t$$. Then $$t$$ is idempotent (a closure operator) and its fixed points are also fixed by any other monotone inflationary endofunction.

Now let $$X$$ satisfy the hypotheses at the top of the page, with least element $$\bot$$. Then $$\forall x:X.\quad \bot\;\leq\;x\;\leq\; s x\;\leq\; t x\;=\; s(t x),$$ whence $$\forall x.\quad t\bot\;=\;s(t\bot)\;\leq\;s(t x)\;=\;t x\;\geq\; x,$$ so $$\top\equiv t\bot$$ by the Special Condition and $$\top$$ has the properties claimed.

The induction principle follows because the subset of elements satisfying the predicate has the same properties as $$X$$ itself, so includes $$\top$$.

Dito Pataraia presented his proof at the 65th PSSL in Aarhus in 1996 but never wrote it up before his death in 2011 at the age of 48, reportedly because he thought it was too trivial to publish on its own. The argument above is the result of simplification by Alex Simpson and then by me.

Whilst I have elided some details here, any competent mathematician could easily fill them in. The argument is complete, constructive and far simpler than transfinite recursion.

The proof is simple, but sometimes the significance of the simplest things is the hardest to understand.

Practical use of Pataraia's Theorem

My Special Condition is the essential one, the part that seems to be original with me. It came from a lot of head-scratching: I knew that I had to use Pataraia's fixed point theorem in my (renewed) work on well founded coalgebras, but it took me a long time to work out how.

It will take further experimentation to find out the best idiom for arguments using it.

The first four conditions describe a very common situation for constructions in Algebra, which I mean completely generally, in the original Arabic sense of manipulating symbols.

If the conclusion holds, the fixed point is unique, so the Special Condition actually says that it is sufficient to test that two fixed points linked by the order are equal.

In the situation as usually presented, such as in the Zermelo--Bourbaki--Witt theorem or the original Pataraia--Simpson proof, the dcpo described by the first four conditions needs to be cut down to the subset generated by $$\bot$$, $$s$$ and directed joins.

Everything outside that subset is irrelevant to the application of the fixed point theorem.

However, generating this subset essentially requires recursion or second order logic, but this is what the fixed point theorem is supposed to be doing for us.

The Special Condition instead does this in a first order way.

In some of my applications, proving the Special Condition is already exactly the natural thing to do in the proof.

In others, there is another first order property that can be used to cut down to a subset that then satisfies the special condition. This is the order-theoretic analogue of my categorical definition of a well founded coalgebra: $$X_0\quad=\quad \{ x\in X \| x \leq s x \ \& \ \forall u\in X. s u\land x\leq u \Rightarrow x\leq u \}.$$ I call members of this subset well founded elements. Both well founded relations and well founded coalgebras are examples of this in appropriate settings.

Since this result produces a top element "like magic", it is natural to look for "obvious counterexamples" or a proof, but those are already discussed above.

As I said at the top of the page, I would instead like to challenge other mathematicians, particularly those in (various kinds of) Algebra, to re-examine their (allegedly transfinite) constructions by recursion to see whether the result described above does the job more neatly.

Then there might be other versions of the Special Condition that might yet be used by further different mathematicians in their own proofs.

This is a re-written version of a previous question.

If you are interested in the historical details, please see my slides and then contact me by email. I will then give you access to the trove of other historical material that I have collected, much of which is in German.

• Perhaps $s$ could be a factorisation function, taking a tuple of integers $(a,b,c,\dotsc)$ to a tuple of length one greater, by factorising one of the integers in the tuple. This proves uniqueness of the result given a particular order in which the factorisation gets done.
• This might sound like gibberish, but there are other existence-and-uniqueness-of factorisation type statements like the Krull-Schmidt theorem. The process of breaking down a factor into 2 smaller factors reminds me of $s$.
• If I'm parsing correctly, the "special condition" says that the fixed points of $s$ form a discrete sub-poset of $X$? Commented Mar 3, 2023 at 14:48
• Ok, I suppose I thought unifying least and greatest elements of $X$ would trigger all kinds of trouble with fixed points of $s$ (e.g. they become noncomputable). But I suppose if there is only one element to choose from, it's difficult to argue the fixed point wouldn't trivially exist. Commented Mar 3, 2023 at 21:51