Complete lattice
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.
Proof
Suppose that is a poset which is closed under arbitrary joins. Let . Let be the set of lower bounds of , i.e. the set . Since is closed under joins, we have the existence of in . We will now show that is the meet of .
First, we show that is a lower bound of . Let . By the definition of , is an upper bound of . Because is less than or equal to any upper bound of , we have . is therefore a lower bound of .
Now we will show that is greater than or equal to any lower bound of . Let be a lower bound of . Then . Because is an upper bound of , we have .
Complete lattices are bounded
As a consequence of closure under arbitrary joins, a complete lattice contains both and . The former is the least element of satisfying a vacuous set of constraints; every element of satisfies a vacuous set of constraints, so this is really the minimum element of . The latter is an upper bound of all elements of , 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 , consider the poset of ’s powerset ordered by inclusion. This poset is a complete lattice in which for all , .
To see that , first note that because union contains all of its constituent sets, for all , . This makes an upper bound of . Now suppose that is an upper bound of ; i.e., for all , . Let . Then for some . Since , . Hence, , and so is the least upper bound of .
The Knaster-Tarski fixpoint theorem
Suppose that we have a poset and a monotone function . An element is called -consistent if and is called -closed if . A fixpoint of is then an element of which is both -consistent and -closed.
Let be the set of all fixpoints of . We are often interested in the maximum and minimum elements of , if indeed it has such elements. Most often it is the minimum element of , denoted and called the least fixpoint of , that holds our interest. In the deduction system example from monotone function examples, the least fixpoint of the deduction system is equal to the set of all judgments which can be proven without assumptions. Knowing may be first step toward testing a judgment’s membership in , 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 , denoted , 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 and a monotone function such that neither nor exists.
Show solution
Let and let be the identity function . , and so is monotone. The fixpoints of are all elements of . Because does not have a maximum or minimum element, neither nor exist.
If that was too easy, here is a harder exercise: think of a complete lattice and monotone function for which neither nor exist.
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 be a complete lattice and a monotone function on . Then exists and is equal to . Dually, exists and is equal to .
Proof
We know that both and exist due to the closure of complete lattices under meets and joins. We therefore only need to prove that is a fixpoint of that is less or equal to all other fixpoints of . The rest follows from duality.
Let and . We seek to show that . Let be the set of fixpoints of . Clearly, . Because for all , for all . In other words, is less than or equal to all fixpoints of .
For , , and so . Since is a lower bound of , the definition of gives . Hence, . Using the monotonicity of on the inequality gives , and so . By the definition of , we then have . Since we have established and , we can conclude that .