The order-theoretic fixed point theoremPaul Taylor |
This page is part of my research on Induction, recursion, replacement and the ordinals using category theory. Those who want to follow my categorical work should follow that link, although this page is essential preliminary material for it. It has also become apparent that I need to get this more basic message across.
MathOverflow has censored my most important posting on that site, but fortuitously it was archived just beforehand.
Here is the simple proof that they don’t want you to know about.
This is not as you may well believe it to be, so I have translated various relevant papers and given a seminar about it.
A poset or partially ordered set is a set X together with a reflexive, transitive antisymmetric relation ≤:
| ∀ x. x≤ x ∀ x y z. x≤ y≤ z⇒ x≤ z ∀ x y. x≤ y≤ x⇒ x=y |
The classical notion of a chain in a poset was replaced with directed subsets around 1970 in lattice-theoretic topology, homotopy theory, constructive topology and denotational semantics of programming languages.
A subset I⊂ X of a poset is directed if
| ∃ x. x∈ I ∀ x,y∈ I. ∃ z∈ I. x≤ z≥ y. |
One important advantage is that the product of two directed subsets is again directed, which is not the case for chains.
Then a dcpo is a directed-complete partial order. That is, it has joins of all directed subsets.
Any dcpo carries the Scott topology and a function is Scott continuous iff it preserves directed joins. This is used in theoretical computer science to provide mathematical semantics of the λ-calculus and programming languages. However, this page is about functions that need not be Scott-continuous.
A function s:X→ X from a poset to itself is
Notice that, given any two inflationary monotone endofunctions r and s,
| ∀ x:X. x ≤ r x, s x ≤ r(s x), s(r x). |
We may form directed joins of inflationary monotone endofunctions pointwise. Since the whole set of them is directed, any dcpo has a greatest such. This is a closure operator, as explained below.
However, to obtain the least fixed point of a particular function requires some argument to cut down the dcpo before applying this idea.
Dito Pataraia (1997) used this idea to give the first constructive proof of the fixed point theorem, with no mention of ordinals. However, he never published it himself before he died in 2011. The versions of his work that have circulated privately are much more complicated than the proof on this page.
For any inflationary monotone endofunction s:X→ X and element a∈ X, we write
| s⊥ a for s a=a |
and extend this relation to sets S of functions and A⊂ X of points by
| S⊥ ≡ Fix S ≡ {a∈ X ∣ ∀ s∈ S.s⊥ a} |
and
| ⊥A ≡ {s:X→ X ∣ ∀ a∈ A.s⊥ a}. |
Hence these two operators define a contravariant adjunction or Galois connection, just as they do for subgroups and subfields,
| A⊂S⊥≡Fix S ⇐⇒ ∀ s∈ S.∀ a∈ A. s⊥ a ⇐⇒ S⊂⊥A. |
Using a Galois connection to cut down the dcpo was my idea (2025).
Then id∈⊥A trivially, whilst if r∈⊥A and s∈⊥A then r· s∈⊥A, since (r· s)a≡ r(s a)=s a=a, and these satisfy id≤ r,s≤ r· s, s· r.
Hence ⊥A is a directed set of inflationary monotone endofunctions of a dcpo. It therefore has a pointwise join m, which is the greatest element of ⊥A.
By the observation about composing inflationary monotone endofunctions, m· m∈⊥A, so m· m≤ m since m is the greatest element. But id≤ m since we’re only dealing with inflationary functions and then m≤ m· m. So they’re equal and m is a closure operator,
| ∀ x:X. x ≤ m x = m(m x). |
Since {m}⊂⊥A we have A ⊂{m}⊥≡Fix {m}, whilst any s∈⊥A satisfies s≤ m and so Fix {m}⊂Fix S. Putting A ≡Fix S in this,
| Fix S ⊂ Fix m ⊂ ⋂{Fix s ∣ s∈ S} ≡ Fix S. |
Theorem In any dcpo X, the common fixed points of any set S of inflationary monotone endofunctions of X form exactly the fixed point set of a unique closure operator m:X→ X.
The fixed point theorem as usually stated can be deduced from this:
Any monotone endofunction s:X→ X of a dcpo with least element ⊥ has a least fixed point, given by m⊥.
More generally, any set of monotone endofunctions has a least common fixed point, given in the same way.
This result, omitting the word “inflationary”, is obtained by restricting X to the subset
| {x:X ∣ ∀ s∈ S. x≤ s x}. |
Sometimes what is required is to show that a dcpo has a greatest element.
This is another consequence of the main theorem, with ⊤=m⊥, so long as s satisfies the special condition that
| ∀ x y. x = s x ≤ y ⇒ x=y |
or, for a set of functions,
| ∀ x y. (∀ s∈ S. x = s x ≤ y) ⇒ x=y |
It was the need to find greatest elements of dcpos in my research on well founded coalgebras that led me to the careful study of the order-theoretic fixed point theorem.
Suppose that the dcpo X has a least element ⊥ and we have any predicate φ(x) on X that satisfies
Then φ(z), where z is the least fixed point.
This is valid because the subset {x:X ∣ φ(x)} may be used in place of X itself in the arguments above and the function has a least fixed point within the subset.
This may readily be generalised to common fixed points of a set of functions.
This induction principle is present in the work of Ernst Zermelo, Kazimierz Kuratowski and other early set theorists.
It was first used as a consequence of Pataraia’s constructive fixed point theorem by Martín Escardó (2003).
If anything is to be said in favour of using ordinal recursion for these things it is that it tells us how to get to the fixed point.
In terms of functions, the ordinals give their iterates, but the double dual ⊥(S⊥) in the Galois connection provides an intrinsic characterisation of what functions arise as such iterates.
Applying ⊥(S⊥) to the least element ⊥ likewise gives the directed set of points whose join is the fixed point.
We say that x∈ X is a well founded element with respect to s:X→ X if
| x≤ s x and ∀ a. a=sa ⇒ x≤ a, |
although there are variations on this idea with s a≤ a or s a∧ x≤ a instead of s a=a. Notice the similarity with the “special condition” above.
Applying this abstract notion to the dcpos of initial segments of a relation or subcoalgebras for a functor recovers the (intuitionistic) proof rule for induction and my notion of well founded coalgebra.
I suggest that, in other applications of this theorem, it may be instructive to characterise the well founded elements with respect to the relevant “successor” function.
A functor S:X→X is called well pointed if it is given together with a natural transformation σ:id→ S that satisfies Sσ=σ S.
An object A∈X carries an algebra structure for this well pointed endofunctor iff σ A is invertible, and then the structure is unique.
We may define a Galois connection essentially as above. Instead of a greatest element, ⊥A has a terminal object and this is an idempotent monad.
The methods of argument above are similar to those that have been used in Algebra since Emmy Noether. Composition of functions and Galois connections (as a form of universal properties) are like the hammer and screwdriver of mathematics. Students should be taught to use these tools rather than to recite proofs of complex theorems, because that is how they will use pure mathematics, whether in academic research or outside universities.
The reason why I asked various Questions on MathOverflow was to get pointers to places in the curriculum and research where results purportedly require transfinite recursion but the arguments actually use ideas like those above. In particular, I thought that my “special condition” might lie hidden in invocations of various traditional fixed point or maximality principles, which I listed in the Question that has now been censored.
I view Mathematics as a huge machine. It is like, for example, a laptop connected to the Internet, which involve many parts, such as the kernel and the routing protocols. These continually undergo development by brilliant people with PhDs, whilst the end-user is often oblivious to them. Mathematicians should have the humility to recognise their colleagues in other disciplines like fellow engineers working on this machine.
This has become particularly important with the rise of machine-validated proofs in languages like Lean, Agda and Coq. One should be able to search their libraries of proofs for “dependencies” on foundational material such as the order-theoretic fixed point theorems. Then the proofs that rely on antiquated methods such as transfinite recursion could be replaced with more subtle methods.
Regarding the purpose of Mathematics as to get Fields Medals or win points on MathOverflow is like saying that the purpose of Mechanical Engineering is to win Formula One races. But every racing driver knows perfectly well that their success and their life depends crucially on the skill of the engineer who works on the nuts and bolts of their car. An engineer’s innovation might also win the race.
This document was translated from LATEX by HEVEA.