PLS Lab

Consistently complete cpo

A cpo (D, \sqsubseteq) is consistently complete (or bounded complete) just if every subset P \subseteq D that has an upper bound (in D) has a least upper bound.

Intuition

Let P = \{ x, y \} with x, y \in D. An upper bound for P is an element z \in D (not necessarily in P!) such that x \sqsubseteq z and y \sqsubseteq z. This intuitively means that x and y are "consistent": they represent pieces of information that do not contradict each other. In these circumstances, the least upper bound x \sqcup y exists.

Thus, the intuitive idea is that consistent information can be stuck together.

Finite or infinite?

We can alternatively define a consistently complete cpo through the existence if binary consistent suprema: we can ask that the supremum x \sqcup y exists whenever x and y have an upper bound. This implies that suprema of finite consistent sets exist.

However, this is equivalent to the above; this is by the usual trick of turning a colimit into a directed one. The general case obviously implies the finite case. But if we have a consistent set P \subseteq D, define X_P = \{ \bigsqcup Q \mid Q \subseteq P, Q \text{ finite} \}. Each finite Q \subseteq P is consistent, because P is, so the supremum \bigsqcup Q exists. But then X_P is directed, so \bigsqcup X_P exists, and it's equal to \bigsqcup P.

Alternative characterisation

Recall that a complete lattice can be given either by having all suprema, or having all infima: if you have one, then you can give the other.

Similarly, it is possible to characterise consistently complete cpos as cpos having all non-empty infima. The argument is simple: the supremum of a consistent set is just the infimimum of all its upper bounds. Thus, having such infima proves consistent completeness. Conversely, to find infima in a consistently complete set, take the set of all lower bounds; this set is consistent, so it has a supremum.