Kleene fixed-point theorem: Difference between revisions

Revision as of 18:27, 8 April 2012

Revision as of 18:28, 8 April 2012

Line 14:

where <math>\textrm{lfp}</math> denotes the least fixed point.

This result 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 axiomatic set theory requires provinga definition of, and existence proof for, the ascending Kleene chain that excludes the ellipsis "..." contained in the above informal definition. Such an existence proof appear to requires use of Tarski's theorem.

:<math> sup \left(\left\{f^n(\bot) \mid n\in\mathbb{N}\right\}\right)</math>,

which requires (in an axiomatic theory) a definition of, and existence proof for, the ascending Kleene chain that excludes the ellipsis "..." contained in the above informal definition. Such an existence proof appear to requires use of Tarski's theorem.