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:

Let L be a complete partial order, and let f : L → L be a Scott-continuous (and therefore monotone) function. Then f has a least fixed point, which is the supremum of the ascending Kleene chain of f.

It is often attributed to Alfred Tarski, but the original statement of Tarski's fixed point theorem is about monotone functions on complete lattices. Since all complete lattices are complete partial orders but not vice-versa, and since all monotone functions on complete lattices are Scott-continuous, Tarski's fixed point theorem is entailed by the present result. (It is not guaranteed that all non-empty subsets of a complete partial order are directed; a complete lattice C is a complete partial order with the additional properties that (i) all C's non-empty subsets are directed and (ii) for every non-empty subset of C the subset's upper closure is a filter.) Yet from a set-theoretic point of view Tarski's result seems the more fundamental of the two, in the following sense: proving Kleene's result in formal set theory requires proving the existence of

$sup\left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)$,

which requires proving the existence of a fixed point of a set definable without use of the ellipsis

$\dots <math>;thisrequiresThe'''ascendingKleenechain'''of''f''isthe[[chain(ordertheory)|chain]]:<math>\bot \;\leq \;f(\bot )\;\leq \;f\left(f(\bot )\right)\;\leq \;\dots \;\leq \;f^{n}(\bot )\;\leq \;\dots$

obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that

${\textrm {lfp}}(f)=\sup \left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)$

where ${\textrm {lfp}}$ denotes the least fixed point.

See also

• Knaster–Tarski theorem
• Other fixed-point theorems