# 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.

## Soundness

Suppose

a_{0} = glb ( {a: A | F a ≤ a} ). Then, for any

a: A such that

F a ≤ a we know that

a_{0} ≤ a. Thus,

F a_{0} ≤ F a ≤ a. That means

F a_{0} is also a lower bound of

{a: A | F a ≤ a} . So,

F a_{0} ≤ a_{0}
since

a_{0} is its greatest lower bound.

This conclusion is immediately followed by the fact:

F (F a_{0}) ≤ F a_{0}. So,

F a_{0} is an element of

{a: A | F a ≤ a} . Therefore,

a_{0} ≤ F a_{0}.
Thus,

a_{0} = F a_{0}.

## Least Fix Point

Suppose

a_{1} is also a fix point of

F. Then,

a_{1} = F a_{1} and thus

a_{1}
is also an element of

{a: A | F a ≤ a} . But

a_{0} is the greatest lower
bound of this set, therefore

a_{0} ≤ a_{1}.