Definition. Complete Lattice [002c]

November 25, 2025

A complete lattice is a partially ordered set in which all subsets have both a greatest lower bound (also known as infimum or meet) and a least upper bound (also known as supremum or join). This means that for any subset \(S\) of the complete lattice \(L\), there exists an element \(\sqcup \ S\) in \(L\) such that: (1)

\(\sqcup \ S\) is a lower bound of \(S\): For all elements \(s \in S\), \(\sqcup \ S \leq s\).
\(\sqcup \ S\) is the greatest of all lower bounds: For any other lower bound \(b\) of \(S\), \(b \leq \sqcup \ S\).

Similarly, there exists an element \(\sqcap \ S\) in \(L\) such that:

\(\sqcap \ S\) is an upper bound of \(S\): For all elements \(s \in S\), \(s \leq \sqcap \ S\).
\(\sqcap \ S\) is the least of all upper bounds: For any other upper bound \(b\) of \(S\), \(\sqcap \ S \leq b\).

In a complete lattice, every subset, including the empty set and the entire set itself, has both a supremum and an infimum within the lattice.

References

Reference. The Hitchhiker’s Guide to Logical Verification (2024 Desktop Edition) [baanen-bentkamp-blanchette-holzl-limperg-hitchhikers-2024]

March 28, 2024
Baanen, Anne, Bentkamp, Alexander, Blanchette, Jasmin, Holzl, Johannes, Limperg, Jannis
https://raw.githubusercontent.com/lean-forward/logical_verification_2024/main/hitchhikers_guide_2024_desktop.pdf

Backlinks

Example. Complete lattice for subsets ordered by inclusion [002g]

November 26, 2025

One of the most basic examples of a complete lattice is the power set of a given set \(X\), denoted as \(\mathcal {P}(X)\), ordered by the subset relation \(\subseteq \). The power set \(\mathcal {P}(X)\) consists of all possible subsets of \(X\), including the empty set \(\emptyset \) and the set \(X\) itself. If we consider the following three element set:

\[ \{a, b, c\} \]

We can draw the (complete) powerset lattice as follows:

Some intuition

November 26, 2025

There's a few observations we can make just by looking at the lattice:

If we take any two subsets on the same level, such as \(\{\{a\}, \{b\}\}\) then two move up a level we take the union of the sets, so: \[ \{a\} \cup \{b\} \to \{a, b\} \] Conversly if we wish to move down a level we take the intersection of the two sets, so for the same pair \[ \{a\} \cap \{b\} \to \{\} \]
Each level expresses the different powersets of \(X\) with a given cardinality. So the bottom level is the powerset of cardinality 0 (i.e. the empty set), the next level up is the powerset of cardinality 1 (i.e. the singletons), then cardinality 2 and finally cardinality 3 at the top level which is just the set \(X\) itself.
Naturally as we move up the lattice the sets get larger (with respect to inclusion) and as we move down the lattice the sets get smaller.

As a reminder, a complete lattice is a partially ordered set (here on inclusion) in which all subsets exhibit both a meet and join. Let's for example take the following subset:

\[ S = \{\{a\}, \{a, b\}\} \]

Lower bound

November 26, 2025

Here the lower bound is any element \((\sqcup S) \in L\) in the larger lattice in which the following property holds:

\[ \forall s \in S.\ (\sqcup S) \leq s \]

In our case we know that \(\leq \ \equiv \ \subseteq \), furthermore we have that the elements of \(S\) are the two sets \(\{a\}\) and \(\{a, b\}\), hence we can rephrase this condition as

\[ (\sqcup S) \subseteq \{a\} \land (\sqcup S) \subseteq \{a, b\} \]

Clearly the lower bound in this instance is then just:

\[ lb(\sqcup S) = \{\{\emptyset \}, \{a\}\} \]

The greatest lower bound is simply the intersection of all lower bounds hence:

\[ \text {glb}(\sqcup S) = \bigcap \ \{\{\emptyset \}, \{a\}\} = \{a\} \]

Upper bound

November 26, 2025

The upper bound is just the flipped condition of the lower bound, i.e.:

\[ \forall s \in S.\ s \leq (\sqcap S) \equiv (\{a\} \subseteq (\sqcap S)) \land (\{a, b\} \subseteq (\sqcap S)) \]

The sets which satisfy this condition are:

\[ \text (ub)(\sqcup S) = \{\{a, b\}, \{a, b, c\}\} \]

The least upper bound is the smallest of the sets which form the upper bound, i.e.:

\[ \text {lub}(\sqcap S) = \{a, b\} \]

Definition. Tarski's Theorem [002b]

November 25, 2025

We define a set \(X\), let \(\mathcal L(X)\) be the complete lattice of all subsets of \(X\) ordered by inclusion. A function \(f: \mathcal L(X) \to \mathcal L(X)\) is said to be monotone in this instance if it preserves inclusion which is to say that the following holds: (1)

\[ A \subseteq B \subseteq X \implies f(A) \subseteq f(B) \]

Pre-and-post fixed point

November 25, 2025

For a monotone function \(f\) a pre-fixed point of \(f\) is a subset \(A \subseteq X\) such that \(f(A) \subseteq A\). Similarly, a post-fixed point of \(f\) is a subset \(B \subseteq X\) such that \(B \subseteq f(B)\).

Conceptually the idea here is that the prefixed points are those sets in \(X\) where the function \(f\) maps to at most all members in \(A\). Conversely, the post-fixed points represent the subset where at least all members of the set are mapped to by other members of the same set. Another way to describe it would be that the pre-fixed points represent a closed or under-approximation of the function \(f\) while the post-fixed points represent a consistent or over-approximation of the function.

A pre-fixed point of \(f\) is also said to be \(f\)-closed and a post-fixed point of \(f\) is said to be \(f\)-consistent.

A least pre-fixed point of a monotone \(f\) is the smallest subset \(A \subseteq X\) such that \(f(A) \subseteq A\), denoted by \(\mu f\). Similarly, a greatest post-fixed point of \(f\) is the largest subset \(B \subseteq X\) such that \(B \subseteq f(B)\), denoted by \(\nu f\).

Every monotone function \(f\) has a unique least pre-fixed point and a unique greatest post-fixed point given by the following equations:

\[ \begin {align*} \mu f & = \bigcap \{ A \subseteq X \mid f(A) \subseteq A \} \\ \nu f & = \bigcup \{ B \subseteq X \mid B \subseteq f(B) \} \end {align*} \]

Of note here is that the least pre-fixed point here corresponds to the closure of the function \(f\). That is to say that it is the smallest set which is closed under the function \(f\). Conversely, the greatest post-fixed point corresponds to the consistency of the function \(f\), being the largest set which is consistent with respect to \(f\).

Lambek's lemma

November 25, 2025

One thing we can observe is that \(\mu f\) is contained in all pre-fixed points of \(f\), by virtue of being the intersection, i.e. closure for all pre-fixed points. Furthermore, we have that \(\mu f\) is itself a pre-fixed point of \(f\)

\[ f(\mu f) \subseteq \mu f \]

and it is thereby the least pre-fixed point. To see this we note that if:

\[ f(A ) \subseteq A \to f(\mu f) \subseteq A \]

Explanation

November 25, 2025

So the idea here is again that since \(A\) is a pre-fixed point of \(f\), by definition we have that \(f(A) \subseteq A\). The implication here is that if we apply \(f\) to our closure, the resulting set must still be within \(A\) since again we definitionally cannot have that \(f\) maps outside \(A\) so even if we constrain ourselves to some smaller set \(\mu f\) it doesn't negate the fact that \(f\) still cannot map outside \(A\).

But by definition of \(\mu f\) we have that

\[ \mu f \subseteq A \]

Explanation

November 25, 2025

This is more or less just restating the definition of \(\mu f\) as the intersection of all pre-fixed points of \(f\), which includes \(A\).

Thus by monotonicity of \(f\) we have the following as required

\[ f(\mu f) \subseteq f(A) \subseteq A \]

Additionally we have

\[ f(f(\mu f)) \subseteq f(\mu f) \]

Which is to reiterate that \(f(\mu f)\) is itself a pre-fixed point of \(f\). Therefore, we have that

\[ \mu f \subseteq f(\mu f) \]

Explanation

November 25, 2025

What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal).

\[ f(\mu f) \subseteq \mu f \]

But why does this actually happen?

A nice perspective to have firstly is seeing the set \(\mu f\) here as a generating set for the function \(f\). In other words if we view the function \(f\) as a set of rules which generate new members in the set from existing members, then the closure \(\mu f\) represents the most precise set of members which can be generated by these rules without introducing any extraneous members.

The effect of this is that because the members in \(\mu f\) are precisely those which can be generated by the rules in \(f\), applying \(f\) to this set will simply regenerate the same members, hence why we have that \(\mu f \subseteq f(\mu f)\) since all the members in \(\mu f\) already correspond to members generated by the members of \(\mu f\) under the rules of \(f\)

Furthermore, since we are working in the context of a complete lattice, as we take the intersection of more and more closed subsets under \(f\) we eventually reach a point where if we take some further intersection (move down more) we end up losing the closed property, but if we move up (i.e. take the union of more closed sets) we end up introducing extraneous members which violate the minimalism property, hence the idea that we stabilize at this set i.e. we are a fixed point on the lattice under the operator.

The implication of this being that the closure \(\mu f\) is a fixed point of \(f\), and, because any fixed point is a pre-fixed point, it is the least pre-fixed point of \(f\). A dual argument shows that the greatest post-fixed point \(\nu f\) is also a fixed point of \(f\). This result is known as Lambek's lemma in Category theory.

Definition. Partial order [002d]

November 25, 2025

Remarks

November 25, 2025


    some piece of code

A partial order is just a preorder with an additional property called antisymmetry. A partial order on a set \(P\) is a binary relation \(\leq \) that satisfies the following three properties for all elements \(a, b, c \in P\):

\(a \leq a\) (Reflexivity): Every element is related to itself.
\(a \leq b \land b \leq c \to a \leq c\) (Transitivity): If an element \(a\) is related to \(b\), and \(b\) is related to \(c\), then \(a\) is also related to \(c\).
\(a \leq b \land b \leq a \to a = b\) (Antisymmetry): If an element \(a\) is related to \(b\), and \(b\) is related to \(a\), then \(a\) and \(b\) must be the same element.

More accurately a partial order is a reflexive, weak, non-strict partial order. Also known as skeletal preorder. [0]