Kleene fixed-point theorem


In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:
The ascending Kleene chain of f is the chain
obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that
where denotes the least fixed point.
Although Tarski's fixed point theorem
does not consider how fixed points can be computed by iterating f from some seed , this result is often attributed to Alfred Tarski who proves it for additive functions Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.

Proof

We first have to show that the ascending Kleene chain of exists in. To show that, we prove the following:
As a corollary of the Lemma we have the following directed ω-chain:
From the definition of a dcpo it follows that has a supremum, call it What remains now is to show that is the least fixed-point.
First, we show that is a fixed point, i.e. that. Because is Scott-continuous,, that is. Also, since and because has no influence in determining the supremum we have:. It follows that, making a fixed-point of.
The proof that is in fact the least fixed point can be done by showing that any element in is smaller than any fixed-point of . This is done by induction: Assume is some fixed-point of. We now prove by induction over that. The base of the induction obviously holds: since is the least element of. As the induction hypothesis, we may assume that. We now do the induction step: From the induction hypothesis and the monotonicity of , we may conclude the following: Now, by the assumption that is a fixed-point of we know that and from that we get