Additional reading Taski Fix Point

Tarski Fix Point Theorem

Tarski Fix Point Theorem can be applied on a larger range of functions but on a smaller range of domains. Given a set A and a partial order R on A, we call A, R a complete lattice if for any subset X of A, X has a least upper bound and a greatest lower bound. Tarski fix point theorem says, if F: A -> A is a monotonic function w.r.t. the order R, then the greatest lower bound of set { a: A | F a a } is the least fix point of F.
In comparison with Bourbaki-Witt fix point theorem, Tarski fix point theorem does not require the function F to be continuous but requires every subset of A to have a least upper bound (and a greatest lower bound), not only those chains.


Suppose a0 = glb ( {a: A | F a a} ). Then, for any a: A such that F a a we know that a0 a. Thus, F a0 F a a. That means F a0 is also a lower bound of {a: A | F a a} . So, F a0 a0 since a0 is its greatest lower bound.
This conclusion is immediately followed by the fact: F (F a0) F a0. So, F a0 is an element of {a: A | F a a} . Therefore, a0 F a0. Thus, a0 = F a0.

Least Fix Point

Suppose a1 is also a fix point of F. Then, a1 = F a1 and thus a1 is also an element of {a: A | F a a} . But a0 is the greatest lower bound of this set, therefore a0 a1.
(* 2021-03-22 01:31 *)