On defining sets, suprema, and infima

On defining sets, suprema and infima

We use

(0)

to denote the set for which the membership relation $\in$ satisfies

(1) $z \in \left\langle {x : r.x : {f}{1}^{2}x}\right\rangle \equiv \left\langle {\exists x : r.x : z = {f}{1}^{2}x}\right\rangle$

Please note that by proper choice of any set S can be represented in the format of (0), for instance:

(2) $S = \langle y : y \in S : y\rangle$

Proof Equality of sets being equivalence of membership relations, we observe

$$ = \begin{array}{l} z \in \langle y: y \in S: y \rangle \ {(1) } \end{array} $$

$$ \begin{array}{r l} & {\langle \exists y: y \in S: z = y \rangle} \ {\equiv} & {{\mathrm {t r a d i n g} }} \end{array} $$

$$ \begin{array}{r l} & {\langle \exists y: z = y: y \in S \rangle} \ {=} & {{\mathrm {1 - p o i n t r u l e} }} \ & {z \in S} \end{array} $$

(End of Proof.)

Denotation (0) is by no means unique. We observe for instance

$$ \begin{array}{l} \langle x: r. x: f. x \rangle \ = {(2) \mathrm {w i t h} S := \langle x: r. x: f. x \rangle } \ \langle y: y \in \langle x: r. x: f. x \rangle : y \rangle \ = {(\mathbf {1}) \mathrm {w i t h} z := y } \ (3) \quad \langle y: \langle \exists x: r. x: y = f ^ {2} x \rangle : y \rangle \ \end{array} $$

Formula (3) has the property that the term "y" (at the end) equals the dummy "y" (at the beginning), like in the traditional format for set notation

$$ {y | \langle \exists x: r. x: y = f. x \rangle } $$

in which they coincide. But here the formula is more complicated than (0), and for that reason we prefer to work with the latter's format, the more so since it subsumes the case that term and dummy are equal: for f one can always choose the identity func- tion!

We now assume that, with respect to a partial order $\varepsilon$ ,the underlying lattice is so complete that each set has a supremum ↑ and an infimum ↓; in view of the above observations we base their definition on the format of (0).

The supremum of $\langle x; r.x; f.x \rangle$ is denoted

by $\left\langle {\uparrow x : r.x.f.}x\right\rangle$ and is defined as the value that satisfies for all $z$

(4) $\left\langle {\uparrow x : r.x : f.x}\right\rangle \subseteq z \equiv \left\langle {\forall x : r.x : f.x \subseteq z}\right\rangle$ ;

its infiimun $\langle \downarrow \times : r.x : f.x\rangle$ is similarly postulated to satisfy for all $z$

(5) $z \leq \left\langle {\downarrow x : r.x : f.x}\right\rangle \equiv \left\langle {\forall x : r.x : z \leq {f}_{x}}\right\rangle$ .

from $\vDash$ being a partial order it follows that (4) and (5) define the extrema uniquely.

Homework In view of (0) = (3),

$$ \langle \uparrow x: r. x: f. x \rangle = \langle \uparrow y: \langle \exists x: r. x: y = f. x \rangle : y \rangle $$

should hold. The reader is invited to verify this. (End of Homework.)

For our future calculations we adopt (1), (4) and (5) as the fundamental definitions.

$$ N u e n e, 3 0 m e i 2 0 0 0 $$

prof. dr Edsger W. Dykstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA