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 ${\displaystyle {\textrm {lfp}}}$ denotes the least fixed point.

This result is often attributed to Alfred Tarski, but Tarski's fixed point theorem does not consider how fixed points can be computed by iterating f from some seed (also, it pertains to monotone functions on complete lattices).

We first have to show that the ascending Kleene chain of ${\displaystyle f}$ exists in ${\displaystyle L}$. To show that, we prove the following:

...
Wikipedia