| One can say
that the bother of all fixed-point theorems is Tarski's fixed-point theorems.
Probably all of you know, but let me just point out that essentially the
proof is very simple. We can characterise the greatest fixed point and the
least fixed point very easily: the least fixed point as the infimum of all
these objects and the greatest fixed point as the supremum of all these
And in this definition lies the reason of why having a denotational approach in terms of fixed point, be them either least fixed points or greatest fixed points is mathematically very rewarding. We have immediately from this very definition we can extract two reasoning principles: induction and definition by recursion from the least fixed point and co-induction and definition by co-recursion from the greatest fixed point.
And when we instantiate Tarski's fixed-point theorem to the case of sets, here I write hyper-sets, well then in this case we define inductive and co-inductive types. When we restrict attention to the class of binary relations intended as graphs then we define functions by recursion and co-recursion. And when we restrict attention to sets P of x for some set x well what we are doing is that we are essentially focusing on induction and co-induction.