A note on the Knaster–Tarski Fixpoint Theorem

Abstract

This note shows that several statements about fixpoints in order theory are equivalent to Knaster–Tarski Fixpoint Theorem for complete lattices. All proofs have been done in Zermelo–Fraenkel set theory without the Axiom of Choice.

1 Introduction

In complete lattice theory, the Knaster–Tarski Fixpoint Theorem [1] states that a monotonic function on a complete lattice has a least fixpoint. The Knaster–Tarski Fixpoint Theorem is a fundamental tool for computer scientist to analyse the formal semantics of programming languages, abstract interpretation, logic. Another basic conclusion about fixpoints in order theory is the Bourbaki–Witt Theorem [2] which has a typical application to proving that the Axiom of Choice implies Zorn’s lemma (see [3] and [4]). The Knaster–Tarski Fixpoint Theorem can act as a starting point to prove an important fixpoint theorem which asserts the existence of the least fixpoint of a monotonic self-mapping f on a CPO (formulated by Theorem 2.1(4) in this note), so can the Bourbaki–Witt Theorem. CPOs are basic models of denotational semantics [5]. In this note, we show that the three foregoing statements about fixpoints are equivalent, where the involved proof does not appeal to the Axiom of Choice. Furthermore, an example reveals that a statement in [4] is incorrect.

2 Main results

We start with some basic notions in order theory. Let $(P, \le )$ be a poset (if it does not lead to confusion, the order relation $\le$ is omitted). A subset D of P is called directed if D is non-empty and for arbitrary $a, b\in D$ there exists some $c\in D$ such that $a\le c$ and $b \le c$. P is called a DCPO if every directed subset D has a least upper bound $\bigvee D$. P is called non-empty chain complete if every non-empty chain C in P has a least upper bound $\bigvee C$ . P is called a complete lattice if every subset S of P (including empty subset) has a least upper bound $\bigvee S$. Let ${\uparrow } a= \{x\in P \mid a\le x \}$ for $a\in P$, and ${\downarrow } a$ is dually defined. If P has a least element, we usually denote it by $\bot$. A DCPO is called a CPO if it has the $\bot$. For other undefined notions in this note, reader may find them in [4], and for more about nonempty chain complete posets, reader may refer to [6].

Theorem 2.1

The following statements are equivalent:

• (1) The Knaster–Tarski Fixpoint Theorem [1, 4]: Let L be a complete lattice and $F: L\rightarrow L$ an order-preserving mapping. Then F has a least fixpoint, given by $\bigwedge \{x\in L \mid F(x)\le x\}$. Dually, $\bigvee \{x\in L \mid x\le F(x)\}$ is the greatest fixpoint of F.

• (2) Bourbaki–Witt Theorem [7]: If P is a non-empty chain complete poset, and the function $f:P\rightarrow P$ satisfies $x\le f(x)$ for all $x\in P$, then f has a fixpoint.

• (3) If P is a DCPO, and the function $f:P\rightarrow P$ satisfies $x\le f(x)$ for all $x\in P$, then f has a fixpoint.

• (4) Let P be a CPO and let the function $f: P\rightarrow P$ be order-preserving. Then f has a least fixpoint.

• (5) Let P be a CPO and let the function $f: P\rightarrow P$ be order-preserving. Then f has a fixpoint.

Proof

$(1)\Rightarrow (2)$: Freely chose a point $a\in P$. Then ${\uparrow } a$ is a non-empty chain complete poset and $f_a$, the restriction to ${\uparrow } a$, is also a function from ${\uparrow } a$ to ${\uparrow } a$, which enjoys $x\le f_a(x)$ for all $x\in {\uparrow } a$. It is sufficient to show that $f_a$ has fixpoints. Thus without loss of generality, we assume that P has the least element $\bot$. Define a mapping $F: \mathcal P(P)\rightarrow \mathcal P(P)$ by

$$\begin{aligned} F(X)=\{\bot \}\cup f(X)\cup \{\bigvee C \mid C\subseteq X \text{ and } \text{ C } \text{ is } \text{ a } \text{ non-empty } \text{ chain }\}. \end{aligned}$$

Using (1), we know F has the least fixpoint $M=\bigcap \{X\subseteq \mathcal P(P) \mid F(X)\subseteq X\}$.

The subsequent proof of the fact that f has a fixpoint in M, which doesn’t appeal to the Axiom of Choice, is given by improving the procedures in [7].

For an element c of M, c is called an extreme point of M if $x<c$ implies $f(x)\le c$. Since $F(M)=M$, we have $\bot \in M$, and hence $\bot$ is an extreme point by the definition. Let E(M) denote the set of extreme points of M, and for every $c\in E(M)$ let

$$\begin{aligned} M(c)=\{x\in M \mid x\le c \text{ or } f(c)\le x\}. \end{aligned}$$

Claim 1: For each $c\in E(M)$, $\bot \in M(c)$.

Trivially since $\bot \le c$, and $\bot \in M$ from $F(M)=M$.

Claim 2: For each $c\in E(M)$, $M(c)=M$.

By the definition of M(c), $M(c)\subseteq M$. To prove $M\subseteq M(c)$, we only need to show $F(M(c))\subseteq M(c)$ because $M=\bigcap \{X\subseteq \mathcal P(P) \mid F(X)\subseteq X\}$:

• (i) $\bot \in M(c)$ by Claim 1.

• (ii) $f(M(c))\subseteq M(c)$: Let $x\in M(c)$. First note $f(x)\in M$ since $x\in M(c)\subseteq M$ and $F(M)=M$. Now we have $x\le c$ or $f(c)\le x$. If $x<c$ then $f(x)\le c$, and hence $f(x)\in M(c)$; if $x=c$ then $f(x)=f(c)$, and again $f(x)\in M(c)$. If $f(c)\le x$, then $f(c)\le x\le f(x)$, so we still have $f(x)\in M(c)$.

• (iii) $\{\bigvee C \mid C\subseteq M(c) \text{ and } \text{ C } \text{ is } \text{ a } \text{ non-empty } \text{ chain }\}\subseteq M(c)$: Note that $C\subseteq M(c)\subseteq M$. So we have $\bigvee C\in M$ since $F(M)=M$. If all elements $x\in C$ are less than c, then $\bigvee C\le c$, and hence $\bigvee C\in M(c)$; if some $x\in C$ is such that $f(c)\le x$, then $f(c)\le x\le \bigvee C$, and again $\bigvee C\in M(c)$.

From (i), (ii), (iii) above, Claim 2 is verified.

Claim 3: Every element of M is an extreme point.

By similar arguments to the proof of Claim 2, we only show $F(E(M))\subseteq E(M)$:

• (i) $\bot \in E(M)$ from above arguments.

• (ii) $f(E(M))\subseteq E(M)$. Let $c\in E(M)$. We need to show $f(c)\in E(M)$, that is, to show that $f(c)\in M$, and if $x\in M$ and $x<f(c)$ then $f(x)\le f(c)$. Noting that $c\in E(M)\subseteq M$, we first have $f(c)\in M$ since $F(M)=M$. Now suppose that $x\in M$ and $x<f(c)$. From Claim 2, we have $M=M(c)$, therefore, there must have $x<c$, $x=c$, or $f(c)\le x$. But $f(c)\le x$ is impossible by the assumption $x<f(c)$. If $x< c$, then $f(x)\le c\le f(c)$ since c is an extreme point; if $x=c$ then $f(x)=f(c)$. Thus $f(c)\in E(M)$, and we have proved $f(E(M))\subseteq E(M)$.

• (iii) $\{\bigvee C \mid C\subseteq E(M) \text{ and } \text{ C } \text{ is } \text{ a } \text{ non-empty } \text{ chain }\}\subseteq E(M)$.

First observe $\bigvee C\in M$, since $C\subseteq E(M)\subseteq M$ and $F(M)=M$.

We show $\bigvee C$ is an extreme point. For this purpose, letting $x\in M$ and $x< \bigvee C$, we need to show $f(x)\le \bigvee C$.

If $f(c)\le x$ for all $c\in C$, then $c\le f(c)\le x$ implies that x is an upper bound of C, in turn $\bigvee C\le x$ which contradicts to the assumption $x< \bigvee C$. Therefore we must have $x\le c$ for some $c\in C$ since $M=M(c)$ by 2.

If $x<c$ then $f(x)\le c \le \bigvee C$.

If $x=c$, then $c=x< \bigvee C$. Again from $M(c)=M(x)=M$ by Claim 2, $\bigvee C\in M(x)$ implies $f(x)\le \bigvee C$.

Claim 4: fhas a fixpoint $\bigvee M$.

Let $x,y\in M$. Then x is an extreme point by 3, and $y\in M(x)$ by Claim 2. So $y\le x$ or $x\le f(x)\le y$. Thus M is a chain. $f(\bigvee M)\in M$ by $F(M)=M$, therefore, $\bigvee M\le f(\bigvee M)\le \bigvee M$.

$(2)\Rightarrow (3)$: Obviously.

$(3)\Rightarrow (4)$: Let $Q=\{x\in P \mid x\le f(x)\}$. Then $Q\ne \emptyset$ since $\bot \in Q$. The monotonicity of f implies that Q is CPO and the $f_a$ which is the restriction of f to Q is a self-mapping on Q. By (3), $f_a$ has some fixpoints, which are fixpoints of f. Now let

$$\begin{aligned} P_1=Q\cap \{x\in P \mid \forall y\in \text{ fix } (f), x\le y\}, \end{aligned}$$

where $\text{ fix } (f)=\{x\in P \mid x=f(x)\}$.

$P_1\ne \emptyset$ since $\bot \in P_1$.

Let $x\in P_1$. $f(x)\in Q$ from the monotonicity of f, and furthermore for all $y\in \text{ fix } (f)$, $f(x)\le f(y)=y$. Therefore $f(x)\in P_1$, that is, when f is restricted to $P_1$ we obtain a function $f_{P_1}: P_1\rightarrow P_1$.

Let D is a directed subset of $P_1$. $\bigvee D\le f(\bigvee D)$. For all $y\in \text{ fix } (f)$, we have $\bigvee D\le y$ since for all $x\in D$ we have $x\le y$. Therefore $\bigvee D\in P_1$, in other words, $P_1$ is a CPO.

Now we applied (3) to $f_{P_1}: P_1\rightarrow P_1$, and obtain that $f_{P_1}$ has a fixpoint $x_0\in P_1$. By the definition of $P_1$, $x_0$ is the least fixpoint of f.

$(4)\Rightarrow (5)$: Trivially.

$(5)\Rightarrow (1)$: We only need to prove the case of the least fixpoint. Let $L_0=\{x\in L \mid F(x)\le x\}$ and $\mu =\bigwedge \{x\in L \mid F(x)\le x\}$. $L_0\ne \emptyset$ because L has a greatest element. Then $F(\mu )\le \mu$ since F is monotonic. Let ${\downarrow } \mu =\{x\in L \mid x\le \mu \}$. Thus for all $y\in {\downarrow }\mu$, $F(y)\le F(\mu )\le \mu$, that is, the restriction of F to ${\downarrow } \mu$ is a self-mapping on ${\downarrow } \mu$. By using (5), the restriction of F to ${\downarrow } \mu$ has a fixpoint $x_0\in {\downarrow } \mu$ since ${\downarrow } \mu$ is still a complete lattice which is also a CPO. But by the definition of $L_0$, all fixpoints of F are contained in $L_0$. Therefore $x_0\le \mu \le x_0$ and $\mu$ is the least fixpoint of F. $\square$

Example 2.2

Consider the poset $(P, \le )$ where $P=\{0\}\cup \{\frac{1}{k}\,\mid \,k=1,2,3,\cdots \}$ and $\le$ is the usual order relation on real numbers. Define the function $f: P\rightarrow P$ as follows:

$$\begin{aligned} f(x)={\left\{ \begin{array}{ll} 1 &{} \text{ if } x=0, \\ x &{} \text{ otherwise }.\\ \end{array}\right. } \end{aligned}$$

Then for all $x\in P$, $x\le f(x)$. P and f meet the assumption of both Theorem 2.1(2) and Theorem 2.1(3), but f does not have a least fixpoint. This example illustrates that the claim of 8.23 (CPO Fixpoint Theorem III) in page 188 of [4], the proof of which authors do not present, is incorrect.