A new and subtle order-theoretic fixed point theorem

Question

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.

Answer 1

Re-formulating an order-theoretic idea for categories can often clarify how it works, by making it proof relevant (as Type Theorists would say), as well as linking to older studies of initial algebras.

Firstly, we simplify the sub-poset $X_0$ given in the question to $$ W \;\equiv\; \{w\in X \vert w\leq s w\;\&\; \forall a\in X.s a\leq a\Rightarrow w\leq a\}. $$ Now replace the inequalities $w\leq s w$ and $s a\leq a$ with coalgebras $\xi:W\to S W$ and algebras $\alpha:S A\to A$ for the functor $S$.

Jim Lambek observed that the initial algebra for a functor has invertible structure map $\alpha$, so it can also be considered as a coalgebra. We call such a thing a fixed point.

Instead of $\forall\Rightarrow$, we select those coalgebras $W$ that, for each algebra $A$, have a unique coalgebra-to-algebra homomorphism $W\to A$. This idea was first used in the categorical treatment of recursion by Christian Mikkelsen and Gerhard Osius.

By Lambek's lemma, the universal property of the initial algebra is equivalent to recursiveness for the same object considered as a coalgebra. Conversely, if a recursive coalgebra is a fixed point then it is the initial algebra.

The functor $S$ preserves recursiveness.

From now on we work in the category $\mathcal W$ of recursive coalgebras and coalgebra homomorphisms.

Using Lambek's lemma with the arrows reversed, the terminal recursive coalgebra is also a fixed point and conversely. Hence there is at most one fixed point in $\mathcal W$ (up to unique isomorphism, of course).

The structure maps $\xi$ of the objects in $\mathcal W$ now define a natural transformation $\sigma:{\mathsf{id}}\to S$ and moreover $S\sigma=\sigma_S$. This is a called a well pointed endofunctor.

Well pointed endofunctors (of any category $\mathcal V$) form a category $\mathcal F$ whose morphisms are natural transformations making commutative triangles. The identity endofunctor (with identity natural transformation) is the initial object.

Pataraia's observation becomes composition of endofunctors, where the diagonal of the naturality square provides the effect on the natural transformations. This preserves the commutativity property for well pointedness. Of course, the identity endofunctor is the identity for this composite.

This composition can be regarded as a non-symmetric monoidal structure that is strictly associative, with a strict unit that is also initial (so it is co-affine). We do not actually need to develop this structure in order to obtain the fixed point property.

Then the category $\mathcal F$ is a directed diagram, so if it has directed colimits it has a terminal object $T$.

Applying the terminal well pointed endofunctor $T$ to any object of the category yields an algebra for any (other) well pointed endofunctor $S$.

However, by Proposition 5.2 of Kelly's paper (whose proof is very similar to Lambek's lemma), any such algebra is a fixed point.

The key question is when a category with a terminal well pointed endofunctor has a terminal object. We know from the simple example of the three-element poset like a $\mathsf V$ that this doesn't happen automatically. More interestingly, Kelly introduced well pointed endofunctors because of their relationship to idempotent monads and reflective subcategories, but of course the latter need not be singletons.

However, when $\mathcal V$ is our category $\mathcal W$ of recursive coalgebras, its well pointed endofunctor $S$ can have at most one fixed point.

Putting this together with the infinitary part, the original category has an initial $S$-algebra iff it has colimits for the directed diagram $\mathcal F$.

That is, we have identified a specific directed diagram over which colimits are needed, instead of all of them or ordinals.

(The usual categorical analogue of directed joins is filtered colimits, but we don't seem to get those without forcing them using coequalisers.)

The special condition says that the reflective subcategory of fixed points is equivalent to the singleton category. Since we need to assume that the original category has an initial object, it is connected, whilst the reflective subcategory is the image of the category under a functor.

Therefore it is enough to say that for any two fixed points that are linked by a morphism, this is a unique isomorphism.

This is an Answer to the Question because originally asked it in order to find out whether I had priority for the special condition. It seems that I did.

Pataraia didn't publish his result in a journal or, it seems, even leave his own clear notes before he died in 2011. However, I have studied reports of what he did from Martin Escardo, Mamuka Jibladze, Peter Johnstone and Alex Simpson. These all say that he just used the subposet generated by $\bot$, $s$ and directed joins, just as Zermelo, Bourbaki and Witt had done for the analogous classical result.

I had had a notion of well founded element of a poset (in the form of $X_0$ in the question) in the 1990s. But I didn't know what to do with it before I heard of Pataraia's result (from Alex Simpson).

In fact my special condition arose (much more recently) out of my work adapting von Neumann's recursion theorem to well founded coalgebras for endofunctors that preserve monos but not necessarily inverse images.

Gregory Max Kelly, A Unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on Bulletin of the Australian Mathematical Society 22 (1980) 1--83.

Joachim Lambek, A Fixpoint Theorem for Complete Categories, Mathematische Zeitschrift 103 (1968) 151--161.

Christian Mikkelsen, Lattice-theoretic and Logical Aspects of Elementary Topoi Reprints in Theory and Applications of Categories 29 (2022) 1--89

Gerhard Osius, Categorical Set Theory: a characterisation of the Category of Sets, Journal of Pure and Applied Algebra 4 (1974) 79--119.

Mamuka Jibladze, Obituary of Dito Pataraia, categories email forum, 23 December 2011.

Paul Taylor, Well founded coalgebras and recursion, with referees.