[summary:
A **complete lattice** is a poset that is closed under arbitrary joins and meets. A complete lattice, being closed under arbitrary joins and meets, is closed in particular under binary joins and meets. A complete lattice is thus a specific type of lattice, and hence satisfies associativity, commutativity, idempotence, and absorption of joins and meets. Complete lattices can be equivalently formulated as posets which are closed under arbitrary joins; it then follows that complete lattices are closed under arbitrary meets as well.

Because complete lattices are closed under all joins, a complete lattice $~$L$~$ must contain both $~$\bigvee \emptyset$~$ and $~$\bigvee L$~$ as elements. Since $~$\bigvee \emptyset$~$ is a lower bound of $~$L$~$ and $~$\bigvee L$~$ is an upper bound of $~$L$~$, complete lattices are bounded. ]

A **complete lattice** is a poset that is closed under arbitrary joins and meets. A complete lattice, being closed under arbitrary joins and meets, is closed in particular under binary joins and meets; a complete lattice is thus a specific type of lattice, and hence satisfies associativity, commutativity, idempotence, and absorption of joins and meets.

Complete lattices can be equivalently formulated as posets which are closed under arbitrary joins; it then follows that complete lattices are closed under arbitrary meets as well.

%%hidden(Proof): Suppose that $~$P$~$ is a poset which is closed under arbitrary joins. Let $~$A \subseteq P$~$. Let $~$A^L$~$ be the set of lower bounds of $~$A$~$, i.e. the set $~$\{ p \in P \mid \forall a \in A. p \leq a \}$~$. Since $~$P$~$ is closed under joins, we have the existence of $~$\bigvee A^L$~$ in $~$P$~$. We will now show that $~$\bigvee A^L$~$ is the meet of $~$A$~$.

First, we show that $~$\bigvee A^L$~$ is a lower bound of $~$A$~$. Let $~$a \in A$~$. By the definition of $~$A^L$~$, $~$a$~$ is an upper bound of $~$A^L$~$. Because $~$\bigvee A^L$~$ is less than or equal to any upper bound of $~$A^L$~$, we have $~$\bigvee A^L \leq a$~$. $~$\bigvee A^L$~$ is therefore a lower bound of $~$A$~$.

Now we will show that $~$\bigvee A^L$~$ is greater than or equal to any lower bound of $~$A$~$. Let $~$p \in P$~$ be a lower bound of $~$A$~$. Then $~$p \in A^L$~$. Because $~$\bigvee A^L$~$ is an upper bound of $~$A^L$~$, we have $~$p \leq \bigvee A^L$~$. %%

# Complete lattices are bounded

As a consequence of closure under arbitrary joins, a complete attice $~$L$~$ contains both $~$\bigvee \emptyset$~$ and $~$\bigvee L$~$. The former is the least element of $~$L$~$ satisfying a vacuous set of constraints; every element of $~$L$~$ satisfies a vacuous set of constraints, so this is really the minimum element of $~$L$~$. The latter is an upper bound of all elements of $~$L$~$, and so it is a maximum. A lattice with both minimum and maximum elements is called bounded, and as this discussion has shown, all complete lattices are bounded.

# Basic examples

## Finite Lattices

The collection of all subsets of a finite lattice coincides with its collection of finite subsets. A finite lattice, being a finite poset that is closed under finite joins, is then necessarily closed under arbitrary joins. All finite lattices are therefore complete lattices.

## Powersets

For any set $~$X$~$, consider the poset $~$\langle \mathcal P(X), \subseteq \rangle$~$ of $~$X$~$'s powerset ordered by inclusion. This poset is a complete lattice in which for all $~$Y \subset \mathcal P(X)$~$, $~$\bigvee Y = \bigcup Y$~$.

To see that $~$\bigvee Y = \bigcup Y$~$, first note that because union contains all of its constituent sets, for all $~$A \in Y$~$, $~$A \subseteq \bigcup Y$~$. This makes $~$\bigcup Y$~$ an upper bound of $~$Y$~$. Now suppose that $~$B \in \mathcal P(X)$~$ is an upper bound of $~$Y$~$; i.e., for all $~$A \in Y$~$, $~$A \subseteq B$~$. Let $~$x \in \bigcup Y$~$. Then $~$x \in A$~$ for some $~$A \in Y$~$. Since $~$A \subseteq B$~$, $~$x \in B$~$. Hence, $~$\bigcup Y \subseteq B$~$, and so $~$\bigcup Y$~$ is the least upper bound of $~$Y$~$.

# The Knaster-Tarski fixpoint theorem

Suppose that we have a poset $~$X$~$ and a monotone function $~$F : X \to X$~$. An element $~$x \in X$~$ is called $~$F$~$**-consistent** if $~$x \leq F(x)$~$ and is called $~$F$~$**-closed** if $~$F(x) \leq x$~$. A fixpoint of $~$F$~$ is then an element of $~$X$~$ which is both $~$F$~$-consistent and $~$F$~$-closed.

Let $~$A \subseteq X$~$ be the set of all fixpoints of $~$F$~$. We are often interested in the maximum and minimum elements of $~$A$~$, if indeed it has such elements. Most often it is the minimum element of $~$A$~$, denoted $~$\mu F$~$ and called the **least fixpoint** of $~$F$~$, that holds our interest. In the deduction system example from Monotone function: examples, the least fixpoint of the deduction system $~$F$~$ is equal to the set of all judgments which can be proven without assumptions. Knowing $~$\mu F$~$ may be first step toward testing a judgment's membership in $~$\mu F$~$, thus determining whether or not it is provable. In less pedestrian scenarios, we may be interested in the set of all judgments which can be proven without assumption using *possibly infinite proof trees*; in these cases, it is the **greatest fixpoint** of $~$F$~$, denoted $~$\nu F$~$, that we are interested in.

Now that we've established the notions of the least and greatest fixpoints, let's try an exercise. Namely, I'd like you to think of a lattice $~$L$~$ and a monotone function $~$F : L \to L$~$ such that neither $~$\mu F$~$ nor $~$\nu F$~$ exists.

%%hidden(Show solution): Let $~$L = \langle \mathbb R, \leq \rangle$~$ and let $~$F$~$ be the identity function $~$F(x) = x$~$. $~$x \leq y \implies F(x) = x \leq y = F(y)$~$, and so $~$F$~$ is monotone. The fixpoints of $~$F$~$ are all elements of $~$\mathbb R$~$. Because $~$\mathbb R$~$ does not have a maximum or minimum element, neither $~$\mu F$~$ nor $~$\nu F$~$ exist. %%

If that was too easy, here is a harder exercise: think of a complete lattice $~$L$~$ and monotone function $~$F : L \to L$~$ for which neither $~$\mu F$~$ nor $~$\nu F$~$ exist.

%%hidden(Show solution): There are none. :p %%

In fact, every monotone function on a complete lattice has both least and greatest fixpoints. This is a consequence of the **Knaster-Tarski fixpoint theorem**.

**Theorem (The Knaster-Tarski fixpoint theorem)**: Let $~$L$~$ be a complete lattice and $~$F : L \to L$~$ a monotone function on $~$L$~$. Then $~$\mu F$~$ exists and is equal to $~$\bigwedge \{x \in L \mid F(x) \leq x\}$~$. Dually, $~$\nu F$~$ exists and is equal to $~$\bigvee \{x \in L \mid x \leq F(x) \}$~$.

%%hidden(Proof): We know that both $~$\bigwedge \{x \in L \mid F(x) \leq x\}$~$ and $~$\bigvee \{x \in L \mid F(x) \leq x \}$~$ exist due to the closure of complete lattices under meets and joins. We therefore only need to prove that $~$\bigwedge \{x \in L \mid F(x) \leq x\}$~$ is a fixpoint of $~$F$~$ that is less or equal to all other fixpoints of $~$F$~$. The rest follows from duality.

Let $~$U = \{x \in L \mid F(x) \leq x\}$~$ and $~$y = \bigwedge U$~$. We seek to show that $~$F(y) = y$~$. Let $~$V$~$ be the set of fixpoints of $~$F$~$. Clearly, $~$V \subseteq U$~$. Because $~$y \leq u$~$ for all $~$u \in U$~$, $~$y \leq v$~$ for all $~$v \in V$~$. In other words, $~$y$~$ is less than or equal to all fixpoints of $~$F$~$.

For $~$u \in U$~$, $~$y \leq u$~$, and so $~$F(y) \leq F(u) \leq u$~$. Since $~$F(y)$~$ is a lower bound of $~$U$~$, the definition of $~$y$~$ gives $~$F(y) \leq y$~$. Hence, $~$y \in U$~$. Using the monotonicity of $~$F$~$ on the inequality $~$F(y) \leq y$~$ gives $~$F(F(y)) \leq F(y)$~$, and so $~$F(y) \in U$~$. By the definition of $~$y$~$, we then have $~$y \leq F(y)$~$. Since we have established $~$y \leq F(y)$~$ and $~$F(y) \leq y$~$, we can conclude that $~$F(y) = y$~$. %%

TODO: Prove the knaster tarski theorem and explain these images

add !'s in front of the following two lines A Knaster-Tarski-style view of complete latticess More Knaster-Tarski-style view of complete latticess