Content deleted Content added
No edit summary |
Added proof, please check for possible mistakes. |
||
Line 16:
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 a definition of, and existence proof for, the ascending Kleene chain, and since axiomatic set theory includes no syntactic element whose semantics are comparable to those of the ellipsis "..." contained in the above informal definition, axiomatic set theory will require a different sort of definition of the ascending Kleene chain. An existence proof for that chain, defined as it must be in a rigorous axiomatic set theory, appears to require use of Tarski's theorem (or an equivalent).
== Proof ==
We first have to show that the ascending Kleene chain of ''f'' exists in L. To show that, we prove the following lemma:
:Lemma 1:''If L is CPO, and f : L → L is a Scott-continuous, then <math>f^n(\bot) \le f^{n+1}(\bot), n \in \mathbb{N}_0</math>
Proof by induction:
* Assume n = 0. Then <math>f^0(\bot) = \bot \leq f^1(\bot)</math>, since ⊥ is the least element.
* Assume n > 0. Then we have to show that <math>f^n(\bot) \leq f^{n+1}(\bot)</math>. By rearranging we get <math>f(f^{n-1}(\bot)) \leq f(f^n(\bot))</math>. By inductive assumption, we know that <math>f^{n-1}(\bot) \leq f^n(\bot)</math> holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.
Immediate corollary of Lemma 1 is the existence of the chain.
Let M be the set of all elements of the chain: <math>\mathbb{M} = \{ \bot, f(\bot), f(f(\bot)), \ldots\}</math>. This set is clearly directed. From definition of CPO follows that this set has a supremum, we will call it ''m''. What remains now is to show that ''m'' is the fixpoint. that is, we have to show that ''f(m) = m''. Because f is continuous, ''f(sup(M)) = sup(f(M))'', that is ''f(m) = sup(f(M))''. But ''sup(f(M)) = sup(M)'' (from the property of the chain) and from that ''f(m) = m'', making ''m'' a fixpoint.
The proof that ''m'' is the least fixpoint can be done by contradiction. Assume ''k'' is a fixpoint and k < m. Than there has to be ''i'' such that <math>k = f^i(\bot) = f(f^i(\bot))</math>. But than for all ''j > i'' the result would never be greater than ''k'' and so ''m'' cannot be a supremum of M, which is a contradiction.
== See also ==
| |||