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$ .

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$ .

Related

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.

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.