Definition. Consistent subset [dt-0013]

A subset $Y \subseteq X$ of a poset $X$ is consistent iff $\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x$ Such an $x$ is called an upper bound of $Y$ .

Context

From chains to directed sets [dt-000Z]

with contributions from Liam O'Connor

While $\omega$ -chains are technically sufficient for denotational semantics, for our purposes it is a little more convenient to think in terms of directed sets rather than chains.

Definition. Directed set [dt-0010]

Liam O'Connor

Formally, a non-empty subset $Y \subseteq X$ of a poset $(X,\sqsubseteq )$ is directed iff: $\forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z$

The

z

above is an upper bound of

x

and

y

. Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.

Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.

Example. Power sets are directed [dt-0011]

The power set of any set $X$ is directed under $\subseteq$ .

Below: $\cal {P}(\{1,2,3\})$ :

Theorem. Chain → Directed [dt-0012]

Liam O'Connor

All non-empty chains are directed.

Proof.

Liam O'Connor

Let $C$ be a chain. Then, given two elements $x,y \in C$ we know from totality that either $x \sqsubseteq y$ or $y \sqsubseteq x$ . If $x \sqsubseteq y$ , then $y$ is the upper bound, otherwise $x$ is the upper bound.

Definition. Consistent subset [dt-0013]

A subset $Y \subseteq X$ of a poset $X$ is consistent iff $\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x$ Such an $x$ is called an upper bound of $Y$ .

Theorem. Alternative characterisation of directedness [dt-0014]

Liam O'Connor

A subset $Y \subseteq X$ of a poset $X$ is directed iff every finite subset of $Y' \subseteq Y$ has an upper bound in $Y$ .

Proof.

Liam O'Connor

⇐: Every pair of elements $x,y \in Y$ has an upper bound simply by taking the upper bound of the set $\{x,y\}.$
⇒: Given a finite set $X = \{x_1,x_2,\dots , x_n\}$ , we can show it has an upper bound by an inductive process, first taking the upper bound of $x_1$ and $x_2$ , and then taking the upper bound of that an $x_3$ and so on until we have an upper bound for the whole set. This induction works because the set $X$ is finite.

Corollary. [dt-0015]

Liam O'Connor

From Theorem [dt-0014] we can see that a finite set $S$ is directed iff it has a top element $\top$ , i.e. $\forall x \in S.\ x \sqsubseteq \top$ .

Backlinks

Remark. [dt-004H]

Liam O'Connor

The second requirement in Definition [dt-004G] can, in light of the first, be expressed equivalently as: $x \sqcup y$ exists for all consistent $x,y \in D$ . This is useful when needing to show that a given cpo is a Scott domain.

Definition. Consistent completeness [dt-004E]

Liam O'Connor

A poset $A$ is consistent complete (or bounded complete) iff $\bigsqcup X$ exists for all consistent $X \subseteq A$ . That is, any set with an upper bound (a consistent set) has a least upper bound.

Related

Definition. Poset [dm-0004]

Liam O'Connor

A partially ordered set, or poset for short, is a pair $(X, \sqsubseteq )$ of a set $X$ equipped with a partial order $(\sqsubseteq ) \subseteq X \times X$ .

Sometimes, when the ordering is arbitrary or clear from context, the set $X$ itself may be referred to as a poset.

Definition. Upper bound [dm-000C]

An upper bound of a set $Y$ is some $x$ such that $\forall y \in Y.\ y \sqsubseteq x$ (where $\sqsubseteq$ is some partial order).