Content deleted Content added
No edit summary |
No edit summary |
||
Line 4:
:''Let L be a [[complete partial order]], and let f : L → L be a [[Scott continuity|Scott-continuous]] (and therefore [[monotone function|monotone]]) [[function (mathematics)|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 set|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 set|upper closure]] is a [[filter (mathematics)|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
:<math> sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>, which requires proving the existence of a fixed point of a set definable without use of the ellipsis : <math> \dots <math>; this requires The '''ascending Kleene chain''' of ''f'' is the [[chain (order theory)|chain]]
| |||