*This post presents a simple lemma related to the Knaster-Tarski fixed-point theorem. I used to think it's obvious, but today I set out to write down the full proof and I was somewhat surprised that I got stuck for awhile. As often is the case, I got unstuck with some help from Rasmus, and his slides in this case.*

**Definitions.** Feel free to skip and refer back only if necessary.

A *partial order* $\le$ is a binary relation that is reflexive, transitive, and antisymmetric.
$$
\begin{align}
&(1) &&x \le x\\
&(2) &&x \le y \land y \le z \to x \le z\\
&(3) &&x \le y \land y \le x \to x = y
\end{align}
$$
A *greatest lower bound* $\inf Y$ of a set $Y$ is a lower bound (smaller than all elements of $Y$) and as big as possible:
$$
\begin{align}
&(4) &&y:Y\to \inf Y \le y\\
&(5) &&(\forall y\; y:Y\to x\le y) \to x\le\inf Y
\end{align}
$$
Lowest upper bounds are defined symmetrically. A set equipped with a preorder is a *complete lattice* when all its subsets $Y$ have a greatest lower bound $\inf Y$ and a lowest upper bound $\sup Y$. A function $f$ is *monotone* when it preserves the order:
$$
\begin{align}
&(6) && x \le y \to f(x) \le f(y)
\end{align}
$$
A *pre-fixed-point* of $f$ is an element $x$ that may only decrease by going thru $f$:
$$
\begin{align}
&(7) && f(x) \le x
\end{align}
$$
Post-fixed-points are defined symmetrically. A *fixed-point* is an element that is both pre- and post-fixed-point. A least fixed point ${\rm lfp}\,f$ of $f$ is the minimum of fixed points:
$$
\begin{align}
&(8) &&f({\rm lfp}\,f)={\rm lfp}\,f\\
&(9) &&f(x)=x \to {\rm lfp}\,f \le x
\end{align}
$$
Note that there is no a-priori reason to believe that least fixed-points (or even fixed-points) exist.
Let ${\rm pre}\,f=\{x:f(x)\le x\}$ denote the set of $f$'s pre-fixed points.

**Lemmas.** Suppose from now on that $f$ is a fixed but arbitrary monotone function, on some complete lattice. Here's the first lemma:
$$
\begin{align}
&(10) &&f(y)\le y \to f(\inf{\rm pre}\,f) \le y
\end{align}
$$
*Proof.*
$$
\begin{align}
& &&f(y) \le y\\
&\Rightarrow &&\{\text{$(4)$ with $Y:={\rm pre}\,f$}\}\\
& &&\inf{\rm pre}\,f \le y\\
&\Rightarrow &&\{(6)\}\\
& &&f(\inf{\rm pre}\,f)\le f(y)\\
&\Rightarrow &&\text{assumption $f(y)\le y$}\\
& &&f(\inf{\rm pre}\,f)\le y
\end{align}
$$

Here's the second lemma:
$$
\begin{align}
&(11) &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f
\end{align}
$$
*Proof.* Instantiate (5) with $x:=f(\inf{\rm pre}\,f)$, and use (10) to discharge the assumption.

Here's the third lemma:
$$
\begin{align}
&(12) &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f)
\end{align}
$$
*Proof.* Be careful here. It's a tricky argument that avoids talking about descending chains and such.
$$
\begin{align}
& &&\{(11)\} \\
& &&f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f \\
&\Rightarrow &&\{(6)\}\\
& &&f(f(\inf{\rm pre}\,f)) \le f(\inf{\rm pre}\,f) \\
&\Rightarrow &&\{\text{$(4)$ with $y:=f(\inf{\rm pre}\,f)$ and $Y:={\rm pre}\,f$}\} \\
& &&\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f)
\end{align}
$$

Here's the fourth lemma:
$$
\begin{align}
&(13) &&{\rm lfp}\,f \le \inf{\rm pre}\,f
\end{align}
$$
*Proof.*
$$
\begin{align}
& &&\{\text{$(3)$ with $x:=\inf{\rm pre}\,f$ and $y:=f(\inf{\rm pre}\,f)$}\}\\
& &&(\inf{\rm pre}\,f \le f(\inf{\rm pre}\,f))\land(f(\inf{\rm pre}\,f) \le \inf{\rm pre}\,f) \to \inf{\rm pre}\,f=f(\inf{\rm pre}\,f)\\
&\Rightarrow &&\{\text{$(11)$ and $(12)$}\}\\
& &&\inf{\rm pre}\,f=f(\inf{\rm pre}\,f) \\
&\Rightarrow &&\{\text{$(9)$ with $x:=\inf{\rm pre}\,f$}\} \\
& &&{\rm lfp}\,f \le \inf{\rm pre}\,f
\end{align}
$$

You guessed: Here's the fifth lemma:
$$
\begin{align}
&(14) &&f(y)\le y \to {\rm lfp}\,f \le y
\end{align}
$$
*Proof.*
$$
\begin{align}
& &&f(y) \le y \\
&\Rightarrow &&\{(10)\} \\
& &&f(\inf{\rm pre}\,f) \le y \\
&\Rightarrow &&\{\text{$(13)$ and $(2)$}\} \\
& &&{\rm lfp}\,f \le y
\end{align}
$$

**Proposition.** Least-fixed points of monotone functions are monotone. Given that both $f$ and $g$ are monotone functions on some complete lattice, we have that
$$
\begin{align}
\bigl(\forall x\; f(x) \le g(x)\bigr) \to {\rm lfp}\,f \le {\rm lfp}\, g
\end{align}
$$
*Proof.*
$$
\begin{align}
& &&f(x) \le g(x) \\
&\Rightarrow &&\{\text{instantiate with $x:={\rm lfp}\,g$}\} \\
& &&f({\rm lfp}\,g) \le g({\rm lfp}\,g) \\
&= &&\{\text{$(8)$ with $f:=g$}\} \\
& &&f({\rm lfp}\,g) \le {\rm lfp}\,g \\
&\Rightarrow &&\{\text{$(14)$ with $y:={\rm lfp}\,g$}\} \\
& &&{\rm lfp}\,f \le {\rm lfp}\, g
\end{align}
$$

## No comments:

## Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.