A little bit of lattice theory

A little bit of lattice theory

The primary purpose of this chapter is to provide an example of a little theory and of its development. Thus it gives us the opportunity to discuss later the phenomenon of theories - i.e. how they can be useful and why they might be worth the trouble -, the notational conventions we have adopted and the discipline we have adhered to in the presentations of our proofs. A secondary purpose is to make our reader familiar with a little bit of lattice theory, a beautiful and general piece of theory that is not half as well known as it deserves. Notations and terminology will be explained as we go along; the explanations will be brief, and we hope that they will be clarified, if necessary, by their usage.

Lattice theory deals with a relation between elements of some "type." A very familiar type is that of the natural numbers, but there are in principle as many types as we care to define: for

instance, another type would be that of all the circles in a plane (in the real Eu- clidean plane" for those that like more precision). We shall use the later letters of the lower-case alphabet , mostly, viz. $u,w,x,y,z$ ,to denote variables of the type in question.

The relation in question is between any two elements of the type, it is denoted by the symbol $\equiv$ (pronounced "is) under"), which we write between the two elements to which it is applied, e.g. $x \leq y$ . Depending on the definition of " $\equiv$ " and the values of $x$ and $y$ , $x \leq y$ is true or not

Examples If the type is that of the natural numbers and $\leq$ means "is a divisor of", then $3 \leq {15}$ is true, but $6 \leq {15}$ is not true (or "is false", as we are used to say).

If the type is that of the circles in the plane, and means "lies inside", let $x, y$ , and $z$ then be circles:

in that case

$x \leq y$ is true ,whereas the other five possible expressions: $y \leq x,x \leq z,z \leq x,$ $y \leq z$ ,and $z \leq y$ are all false.(End of Examples.)

The above two examples nicely illustrate the generality of the theory we are heading for: not only will it be applicable to types with infinitely many elements, it will also be applicable to all sorts of types of very different nature. I would like to stress that such examples are purely illustrative and have no defining function for the theory in question. Theories may be designed with certain applications in mind, but they are never based on them. On the contrary, theories are based on explicit postulates about their ingredients. In the case of lattice theory, these are primarily postulates about relation "under".

The first postulate about $\varepsilon$ is that it is what is called "reflexive", i.e. that each element of the type in question is under itself, in formula - recalling the convention that $x$ denotes a variable of the type in question-

$$ (0) \quad \langle \forall x:: x \subseteq x \rangle $$

which can be read as "for any $x$ it holds that

Remark For our theory to be applicable in the context of our first example, we have to consider any natural number a divisor of itself. i.e. not only is -contrary to Greek tradition-- twelve a divisor of twelve, but even, in spite of the dogma "you are not allowed to divide by zero," is zero a divisor of zero!

Similarly, in the second example, each circle is considered to lie inside itself. (End of Remark.)

There is another way of expressing the

(1) $\left\langle {\forall x,y : x \leq y \land y \leq x \Leftrightarrow x = y}\right\rangle$

which can be read as "for any $x$ and $y$ it holds that $x$ is under $y$ and $y$ is under $x$ if $x$ equals $y$ .

But are (0) and (1) really equivalent? Is "reflexivity" according to (0) really the

same concept as "reflexivity" according to (1)? The answer is "Yes", and below we shall show how this can be established by calculation, i.e. we shall show how we can start with (1), subject it in succession to a number of value-preserving transformations, and end up with (0). We shall first give the calculation, and then some explanation.

$$ \begin{array}{l} \equiv \begin{array}{l} {\langle \forall x, y: x \leq y \land y \leq x \iff x = y \rangle} \ {{\mathrm {n e s t i n g} }} \end{array} \ \langle \forall x: \langle \forall y: x \leq y \land y \leq x \Leftrightarrow x = y \rangle \rangle \ \equiv {t r a d i n g } \ \langle \forall x: \langle \forall y: x = y: x \leq y \land y \leq x \rangle \rangle \ \equiv \quad {\mathrm {o n e - p o i n t r u l e} } \ \langle \forall x: \quad x \leq x \land \quad x \leq x \rangle \ \equiv {\wedge i d e m p o t e n t } \ \end{array} $$

$$ \langle \forall x: x \leq x \rangle $$

For the uninitiated reader, the above 9-line calculation is of course complete gibberish that is absolutely without any convincing power, but for the initiated one it is very different. He recognizes 5 formulae of familiar syntactical structure, separated by, between braces, references to familiar

value-preserving manipulations from the predicate calculus. In the first formula he recognizes (1), in the last one (0), and he knows that the three formulae in between are the intermediate results.

The symbols " $\left\langle {{}^{\prime \prime }\text{and}"}\right\rangle$ " form a bracket pair delineating the scope of so-called "dummy variables"; in (0) that is only x , in (1) it is the pair x,y , and in both the scope extends over the whole formula.

In the first intermediate result, the scopes are nested: the scope of $x$ still extends over the whole formula - from the first to the last $1 = 1$ while the scope of $y$ extends over the inner bracket pair

first intermediate result could be read as "for any $x$ it holds that for any $y$ it holds that $x$ is under $y$ and $y$ is under $x$ if $x$ equals $y$ ". Note that after the first step called "nesting", everything out- side the scope of $y$ (i.e. the initial " $\langle \forall x::\cdots$ " and the final ") remains un- changed for the rest of the calculation; the subsequent manipulations, which are con- fined to the inner subexpression, are in fact independent of the formal environment in which the subexpression is embedded. The

next intermediate result could be read as "for any $x$ it holds that for any $y$ such that $x$ equals $y$ it holds that $x$ is under $y$ and $y$ is under $x$ ", but as a rule we don't, for it quickly becomes much simpler to let the symbols do the work and to manipulate the formulae directly.

It is time to present our next postulate about $\varepsilon$ . It states that $\varepsilon$ is what is called "antisymmetric", i.e. that distinct elements of the type in question are not under each other or, equivalently, that elements that are under each other are equal, in formula

$$ (2) \quad \langle \forall x, y: x \leq y \land y \leq x \Rightarrow x = y \rangle $$

Notational remark. The introduction of the symbol $\Rightarrow$ is only a minor novelty since "p ⇒ q" is no more than a nota- tional alternative for "q <= p". The first one, "p ⇒ q" is read as "if p then q" or as "p implies q", the other one, "q <= p" is read as "q if p" or "q follows from p". The situation is very similar to the presence of the notational alterna- tives "m ≤ n" (m is at most n) and "n ≥ m" (n is at least m) for what is the

same condition on $m$ and $n$ . (End of Notational remark.)

In connection with our earlier examples we note that, for natural numbers, being- a -divisor-of is an antisymmetric relation: if x divides y and y divides x , we are indeed allowed to conclude that x equals y . (This last statement requires a proof , which is not included here.) Similarly, with x and y denoting circles, we note that if x lies inside y and y lies inside x , we can indeed conclude that the two circles are the same. (This statement, too, requires a proof.)

Predicate calculus allows us to combine reflexivity and antisymmetry of $\leq$ , i.e. formulae (1) and (2), into

(3) $\left\langle {\forall x,y : x \leq y \land y \leq x \equiv x = y}\right\rangle$

It is this formula that in a single line reveals the profound importance of relation 5 : demonstrating that two given elements of the type in question are equal is no more and no less than demonstrating separately that the one is under the other and vice versa. The latter is known as a ping-pong argument, and we

shall discuss its potential merits when we have seen more examples of it.

From the reflexivity of $\equiv$ we derive the following laws, known as the laws of "indirect order":

For any $x$ and $y$ it holds that

$\left\langle {\forall z : z \leq x \Rightarrow z \leq y}\right\rangle \Rightarrow x \leq y$ (5) $\left\langle {\forall z : y \leq z \Rightarrow x \leq z}\right\rangle \Rightarrow x \leq y$

Proof We shall prove (4) only, since the proof of (5) is so similar that it can be omitted from this text. For the proof of (4) we observe for any $x$ and $y$

$$ \begin{array}{l} \langle \forall z: z \leq x \Rightarrow z \leq y. \rangle \ \Rightarrow \quad {i n s t a n t i a t e: z := x } \ \end{array} $$

$$ \begin{array}{l} x \leq x \Rightarrow x \leq y \ \equiv \quad {\leq r e f l e x i v e } \ \end{array} $$

$$ \begin{array}{l} \mathrm {t r u e} \Rightarrow x \leq y \ \equiv {\mathrm {p r e d i c a t e} \mathrm {c a l c u l u s :} (\mathrm {t r u e} \Rightarrow p) \equiv p } \ x \le y \ \end{array} $$

The first step exploits that if something holds for any $z$ ,it also holds when we make for $z$ a special choice ( $x$ in this case). This type of reasoning step is called "instantiation": the general $z$ is

so to speak replaced by the special instance X . Instantiation is the major reasoning step next to "substituting equals for equals". The second step, which uses the reflexivity of 5 , introduces the constant "true", viz. the predicate that holds by definition. (It's major properties are that the three expressions

$$ t r u e \Rightarrow p \qquad t r u e \equiv p \qquad t r u e \land p $$

are all equivalent to $p$ .)

(End of Proof.)

The next laws to be derived use the antisymmetry of $\rho \leq$ as well; they are known as the laws of "indirect equality":

For any $x$ and $y$ it holds that

(6) $\left\langle {\forall z : z \leq x \equiv z \leq y}\right\rangle \Rightarrow x = y$ $\left{ {7}\right} \;\left{ {\forall z : x \leq z \equiv y \leq z}\right} \Rightarrow x = y$

Proof We shall only prove (6), the proof of (7) being very similar. For the proof of (6), we observe for any $x$ and $y$

$\left{ \begin{array}{l} {x}{1} = x \ {x}{2} = - 1 \end{array}\right.$ $\left( {x \leq x \equiv x \leq y}\right) \land \left( {y \leq x \equiv y \leq y}\right)$

$$ \begin{array}{l} \equiv {\leq r e f l e x i v e, t w i c e } \ (\mathrm {t r u e} \equiv x \equiv y) \land (y \equiv x \equiv \mathrm {t r u e}) \ \equiv {\mathrm {p r e d i c a t e} ^ {\prime} \mathrm {c a l c u l u s} } \ x \equiv y \wedge y \equiv x \ \equiv \quad \left{ \begin{array}{l} (3) \end{array} \right} \ x = y \ \end{array} $$

(End of Proof.)

Remark In (6) and (7) the implication signs " $\Rightarrow$ " could have been replaced by equivalences "≡", since the implications in the other direction, viz. " $\Leftarrow$ " follow directly from predicate calculus. (End of Remark.)

We now consider the situation that being above two values, $x$ and $y$ say, can be characterized as being above a single value, $w$ say. In that case $w, x$ and $y$ satisfy

$$ (8) \quad \langle \forall z: w \leq z \equiv x \leq z \land y \leq z \rangle $$

Equation (8) then determines $\omega$ uniquely.

$$ \begin{array}{l} \mathrm {P r o o f} \ \mathrm {a n d} \end{array} \begin{array}{l} \mathrm {L e t , f o r g i v e n} \ \mathrm {w i s a t i s f y} \end{array} x, y, w s a t i s f y (8) $$

(9) $\left\langle {\forall z : {w}^{\prime } \leq z \equiv x \leq z \land y \leq z}\right\rangle$

Establishing the uniqueness means establish ing $w = w^{\prime}$ . To this end we observe for any $z$ :

$$ w \le 2 $$

$$ \equiv {(\delta) } $$

$$ = \begin{array}{r l} & x \leq 2 \wedge y \leq 2 \ & {(9) } \end{array} $$

$$ w ^ {\prime} \leq z $$

thus establishing $\left\langle {\forall z\therefore w \leq z \equiv {w}^{\prime } \leq z}\right\rangle$ , from which follows by indirect

$$ e q u a l i t y (7). $$

(End of Proof.)

Our third postulate now says that for

any $x,y$ there does indeed exist a $\omega$

satisfying (8), in all its formal glory:

$$ \langle \forall x, y: \langle \exists w: \langle \forall z: w \le z \equiv x \le z \land y \le z \rangle \rangle . $$

The combination of uniqueness and

existence of the satisfies (8)

allows us to introduce that $w$ -value

as function of $x$ and $y$ . This function

is known under many names , such as

"the lub ( = lowest upper bound ) of x and

$y''$ or "the join of $x$ and $y$ "; we shall

call it "the supremum of $x$ and $y$ and

denote it by " $\times \uparrow y$ " (read: " $x\;{up}\;y$ ") . According

${x}^{ \uparrow }y \leq z \equiv x \in z \land y \in z$

Let us illustrate this with our earlier examples. With $x, y, z$ being natural numbers and $\leq$ meaning "being a divisor of", (10) reads " $x \uparrow y$ is a divisor of $z$ if and only if $x$ and $y$ are both divisors of $z$ ", which tells us that $x \uparrow y$ is the smallest common multiple of $x$ and $y$ . When $x, y, z$ are circles and $\leq$ means "lies inside", $x \uparrow y$ is the smallest circle encompassing both $x$ and $y$ :

Having introduced the operator $\uparrow$ via (10), we can now prove all sorts of properties of it. The first one is the Theorem 1 is idempotent, symmetric, and associative, i.e. for all $x,y,z$ :

(11) $x \uparrow x = x$ (idempotent)

(12) ${x}^{\prime }y = y^{\prime }x$ (symmetric) (13) $\left( {x \uparrow y}\right) \uparrow z = x \uparrow \left( {y \uparrow z}\right) \;$ (associative)

Proof Operator $\uparrow$ inherits these three properties from the conjunction $\wedge$ , which is also idempotent, symmetric, and associative. How it does so, we show in the case of the associativity. We observe for any $x, y, z, w$

$$ \begin{array}{l} (x \uparrow y) \uparrow z \equiv w \ = {1 0) w i t h x, y, z := x ^ {\prime} y, z, w } \ (x \uparrow y) \equiv w \quad \wedge \quad z \equiv w \ \equiv \left{ \begin{array}{l l} (1 0) & w i t h z := w \end{array} \right} \ (x \le w \land y \le w) \land z \le w \ \equiv {\wedge i s ^ {\mathrm {a s s o c i a t i v e}} } \ x \leq w \land (y \leq w \land z \leq w) \ \equiv {(\cdot 1 0) w i t h ^ {y} x, y, z := y, z, w } \ x \le w \land (y ^ {\uparrow} z \le w) \ = {(\uparrow 0) w i t h y, z := y ^ {\uparrow} z, w } \ x \uparrow (y \uparrow z) \le w, \ \end{array} $$

after which the equivalence of first and last lines establishes (13) via indirect equality, i.e. (7). The proofs of (11) and (12) follow the same pattern. (End of Proof.)

In passing I would like to point out the extent to which the design of the last

proof has been forced. At the left-hand side we have an $\uparrow$ with $(x\uparrow y)$ as one of its arguments, and such an $\uparrow$ does not occur at the right-hand side: in the transformation from left to right, that $\uparrow$ has therefore to be removed. Similarly for the 9 in $(x\uparrow y)$ . So, the first two steps remove each an $\uparrow$ (and, similarly, the last two reintroduce each an 1). They do so by an appeal to (10), which so far is our only handle on $\uparrow$ , being its definition. And the middle step rearranges the terms as associatively expresses.

In what follows we shall often exploit the associativity of $\upharpoonright$ by omitting the semantically irrelevant parentheses.

From a manipulative point of view, (10) is an attractive definition because it has lots of dummies for which we can make a specific choice. In the next theorem, $x \uparrow y$ has been chosen for $z$ . Theorem For any $x,y$ holds (14)

Proof We observe for any $x, y$

$$ \begin{array}{l} = \begin{array}{r l} & x \leq x \uparrow y \quad \wedge y \leq x \uparrow y \ & {(1 0) \quad \mathrm {w i t h} \quad z := x \uparrow y } \end{array} \ \equiv \begin{array}{l} x \uparrow y \ {\mathrm {E l s e r f i x i v e , i . e . (0) w i t h} x := x \uparrow y } \end{array} \ \end{array} $$

$$ t r u e. $$

$$ (E n d o f P r o o f) $$

$$ \mathrm {T h e o r e m} \quad W e h a v e f o r a n y x, y $$

$$ (1 5) \quad x \uparrow y \leq y \equiv x \leq y $$

$$ \mathrm {P r o o f} \quad \mathrm {W e o b s e r v e f o r a n y} x, y $$

$$ \begin{array}{l} = \begin{array}{r l} & x \uparrow y \equiv y \ & {(1 0) \mathrm {w i t h} z := y } \end{array} \ \equiv \begin{array}{l} x \leq y \ {\leq i s r e f l e x i v e } \end{array} \ x \equiv y \wedge \mathrm {t r u e} \ \equiv {\mathrm {p r e d i c a t e c a l c u l u s} } \ x \leq y \ \end{array} $$

(The experienced calculator would have allowed himself the combination of the last two steps into one.) (End of Proof.)

And now we have done the groundwork for the fundamental

$$ \begin{array}{l} \mathrm {T h e o r e m} \quad \mathrm {F o r a n y} x, y \quad \mathrm {h o l d s} \ (1 6) \quad x \uparrow y = y \equiv x \leq y \ \mathrm {P r o o f} \quad \mathrm {W e o b s e r v e f o r a n y} x, y \ \end{array} $$

$$ \begin{array}{l} \begin{array}{r l} & {\equiv x \uparrow y = y} \ & {\quad {\mathrm {5 i s r e f l e x i v e a n d a n t i s y m m e t r i c ,}} \ & {\quad \mathrm {i . e . (3) w i t h} \quad x := x \uparrow y }} \end{array} \ \equiv \begin{array}{l} x \uparrow y \leq y \ \left{1 5 \right}; (1 4), 2 n d \end{array} \begin{array}{l} x \uparrow y \ \left{1 5 \right}; (1 4), 2 n d \end{array} \ x \leq y \land \mathrm {t r u e} \ \begin{array}{r l} & {\equiv \quad {\mathrm {p r e d i c a t e c a l c u l u s} }} \ & {\times \leq y} \end{array} \ \end{array} $$

$$ \begin{array}{l} \mathrm {T h e o r e m (1 6) n o w e n a b l e s u s t o p r o v e} \ \mathrm {T h e o r e m .} \quad E \quad i s \quad t r a n s i t i v e, i. e. f o r a n y x, y, z \ (1 7) \quad x \leq y \land y \leq z \Rightarrow x \leq z \ \end{array} $$

$$ \begin{array}{l} \frac {P r o o f}{t o} \mathrm {R e w i t e} \mathrm {t h e d e m o n s t r a n d u m} (1 7) \mathrm {a s} \ x \uparrow y = y \land y \uparrow z = z \Rightarrow x \uparrow z = z \ \end{array} $$

$$ w e o b s e r v e f o r a n y x, y, z $$

$$ x \uparrow z $$

$$ \begin{array}{l} = {y ^ {\uparrow} z = z, f r o m a n t e c e d e n t } \ x \uparrow y \uparrow z \ = {x \uparrow y = y, f r o m a n t e c e d e n t } \ = \begin{array}{l} y ^ {\uparrow z} \ z \end{array} \left{y ^ {\uparrow z} = z, f r o m a n t e c e d e n t \right} \ \end{array} $$

$$ \begin{array}{l} \mathrm {t h u s e s t a b l i s h i n g t h e c o n s e q u e n t o f t h e} \ \mathrm {r e w r i t t e n} \quad \mathrm {d e m o n s t r a n d u m}. \quad (\mathrm {E n d o f P r o o f}). \ \end{array} $$

It is this last theorem that turns relation 5 into a "partial order", a partial order being defined as a binary relation that is reflexive, antisymmetric, and transitive. Partial orders are quite common; the reader may check that the relations of our examples - viz. "being a divisor of" and "lying inside"- are indeed transi- tive.

Theorem (16) also gives us the opportunity of connecting the two important concepts of "distribution" and "monotonicity".

"Application of $f$ distributes over $1 ^ { \prime \prime }$ means that for any $x, y$

(18) ${f}{\cdot}\left( {{x}^{ \uparrow }{y}^{ - }}\right) = {f}{\cdot x} \uparrow {f}_{\cdot y}$

(here we give the dot".of the function

"Function $f$ is monotonic with respect to $\varepsilon$ " means that for any $x,y$

$x \leq y \Rightarrow f.x \leq f.y$

The connection between these two con-

cepts is expressed by the

Theorem A function that distributes over $\uparrow$ is monotonic with respect to $\leq$ .

Proof We observe for any $f$ that is

$$ \begin{array}{l} = \begin{array}{l} f _ {x} \leq f _ {y} \ {(1 6) \mathrm {w i t h} x, y := f _ {x}, f _ {y} } \end{array} \ = \begin{array}{l} f _ {\cdot x} \uparrow f _ {\cdot y} = f _ {\cdot y} \ {\text {f d i s t r i b u t e s o v e r} \uparrow , \mathrm {i . e} (1 8) } \end{array} \ \begin{array}{r l} & {\quad f _ {!} (x \uparrow y) = \rho_ {!} y} \ {=} & {\quad {\mathrm {e q u a l s} \mathrm {f o r e q u a l s} }} \end{array} \ \equiv \begin{array}{l} x \uparrow y = y \ {1 6 } \end{array} \ x \leq y \quad (\mathrm {E n d o f P r o o f}). \ \end{array} $$

From the fact that is idempotent, symmetric, and associative follows

$$ z \uparrow (x \uparrow y) = (z \uparrow x) \uparrow (z \uparrow y). $$

i.e. by viewing $z \uparrow$ as a function application tion -viz.of the function such that for any $w$ ,f.w = z↑w - we see that it distributes over This observation makes the previous theorem applicable in the proof of the following

Theorem 1 is monotonic with respect to $\underline{E}$

in both its arguments, i.e. for any $x,x,y,{y}^{\prime }$

$x \leq {x}^{\prime } \land y \leq {y}^{\prime } \Rightarrow {x}^{\prime }y \leq {x}^{\prime }{y}^{\prime }$

a proof of which we leave to the inter-ested reader. (For several reasons it may help to compare (20) with the more fami- iar $a \leq {a}^{\prime } \land b \leq {b}^{\prime } \Rightarrow a + b \leq {a}^{\prime } + {b}^{\prime }$ .)

Now the time has come to confess that, so far, we have only told you half the story of lattice theory: to all we told about $\uparrow$ ,there is a dual story after the introduction of our fourth postulate,viz. that for any $x,y$ there exists a $w$ that -in analogy to (8)- satisfies

$\left\langle {\forall z : z \leq w \equiv z \leq x \land z \leq y}\right\rangle$ , which,as before,determinines for any the $w$ uniquely.

The combination of existence and uniqueness allows us to introduce the w-value satisfying (21) as another function of x and y . It is known under names like "the glb C = greatest lower bound) of x and y or " the meet op x and y ; we shall use the name "the infimum of x and y" and denote it

by $\left{ \begin{array}{l} x \downarrow y \ {21} \end{array}\right.$ (read: " $x$ down $y$ ). According

$$ \begin{array}{l} (2 2) \quad z \leq x \downarrow y \equiv z \leq x \land z \leq y \ \mathrm {W i t h o u t p r o o f w e l s t i t s p r o p e r t i e s :} \ (2 3) \quad \downarrow \quad i s i d e m p o t e n t, s y m m e t r i c, a s s o c i a t i v e \ (2 4) \quad x \downarrow y \leq x \quad \land \quad x \downarrow y \leq y \ (2 5) \quad x \leq x \downarrow y \equiv x \leq y \ (2 6) \quad x = x \downarrow y \equiv x \leq y \ (2 7) A f u n c t i o n t h a t d i s t r i b u t e s o v e r \downarrow i s \ (2 8) \downarrow i s m o n o t o n i c w i t h r e s p e c t t o 5 in b o t h i t s a r g u m e n t s. \ \end{array} $$

Let us return for a moment to our examples. With $x, y$ of type natural number and 5 meaning "being a divisor of" we run into a slight problem with the interpretation of the infimum : $x \downarrow y$ denotes the greatest common divisor of $x$ and $y$ provided at least one of the arguments is positive, but $0 \downarrow 0$ requires extra attention since there is no greatest divisor of 0 , each natural number being a divisor of 0 .

There are two ways out of the dilemma, either we define $0 \downarrow 0 = 0$ - a definition that is compatible with (22) - or we replace for $x,y$ the domain of the natural numbers (which includes zero) by that of the positive integers (which starts at one).

with $x,y$ circles in the plane and meaning "lying inside", $x \downarrow y$ would be the largest circle lying in the inter- section:

but what if the intersection of $x$ and

The answer is to extend the domain of all "visible" circles in the plane by, one extra element - called "bottom" and denoted by "⊥" or "L" - that by definition lies inside all circles (including itself). The defining relation for bottom is

$$ (2 9) \quad \langle \forall z:: \perp \subseteq z \rangle $$

Operators ↑ and ↓ are connected by the laws of Absorption

Proof We prove the first one by observing for any $x, y$

true (End of Proof.)

$$ \begin{array}{l} (3 0) \quad x = x \downarrow (x \uparrow y) \quad x = x \uparrow (x \downarrow y) \ x = x \downarrow (x \uparrow y) \ \equiv {(\mathrm {2 6}) \mathrm {w i t h} y := x \uparrow y } \ x \subseteq x ^ {\uparrow} y \ \equiv {1 4 } \ \end{array} $$

The other connection between ↑ and ↓ is that if the one distributes over the other, the other distributes over the one. (In this case of mutual distribution, people call the lattice "distributive". We shall show that ↓ distributes over ↑.

i.e. that for any $x,y,z$

$$ x \downarrow (y \uparrow z) = (x \downarrow y) \uparrow (x \downarrow z), $$

if $\uparrow$ distributes over $\downarrow$ ,i.e. for any $x,y,z$

$$ x \uparrow (y \downarrow z) = (x \uparrow y) \downarrow (x \uparrow z) $$

Proof We observe for any $x,y,z$

$$ \begin{array}{l} = \begin{array}{r l} & {(x \downarrow y) \uparrow (x \downarrow z)} \ & {{\uparrow \mathrm {o v e r t h e r i g h t m o s t} \downarrow }} \end{array} \ ((x \downarrow y) \uparrow x) \downarrow ((x \downarrow y) \uparrow z) \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {L a w o f A b s o r p h o n} } \ x \downarrow ((x \downarrow y) \uparrow z) \ = {\uparrow \mathrm {o v e r r i g h t m o s t} \downarrow } \ x \downarrow (x \uparrow z) \downarrow (y \uparrow z) \ = {(t h e o t h e r) ^ {J} L a w o f A b s o r p h i o n } \ x \downarrow (y ^ {\uparrow} z) \qquad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

For reasons of symmetry, the above four-step calculation establishes the following very general

Theorem For symmetric, associative. operators ↑ and ↓ that satisfy the Laws of Absorption (30), we have

$$ (\uparrow d i s t r i b u t e s o v e r \downarrow) \equiv (\downarrow d i s t r i b u t e s o v e r \uparrow). $$

(In the above proof, the appeals to symmetry and associativity were left as implicit as usual; I hope this did not confuse the reader.) The above proof has been included as a strong example of the power of calculation; anyone who still doubts is invited to try to establish the equivalence of our last theorem by means of a verbal argument, for the experience should quickly convert him.

We close this illustrative chapter with a last generalization, which will lead to another way of introducing $\bot$ (i.e. element "bottom" as defined by (29)).

Relation (10)

$$ x \uparrow y \equiv z \equiv x \le z \land y \le z $$

introduces the supremum x1y of the 2 elements x and y . Repeated appli-. cation gives the supremum for 3 elements u, x, y

$$ u \uparrow x \uparrow y \leq z \equiv u \leq z \land x \leq z \land y \leq z, e t c. $$

Now allow me for a moment to use ↑ as a unary operator on the set of values whose supremum should be taken, i.e. allow me for a moment to write uXy now as $\uparrow {u,x,y}$ By naming the set of values whose supremum should be taken, we can now generalize our last formula, i.e. express "etc.": for any $z$ and any set $X$

$$ (3 1) \quad \uparrow X \leq z \equiv \langle \forall x: x \in X: x \leq z \rangle , i. e. $$

the supremum of a set $X$ is under $z$ means that each element of $X$ is under $z$ . (In the right-hand side

of (31) we have used a notational extension that will be discussed more fully later. The $x \in X$ " - "x is an element of set $X$ " - between the two colons restricts the range of the dummy $x$ : the constraint $x \leq z$ , more precisely the constraint of being under $z$ , only applies to the elements that belong to $x$ .)

So far, (31) defines $\uparrow X$ certainly for any finite set $X$ of at least 2 elements. In fact, the "one-point rule" - which we used when we established the equivalence between (0) and (1) - allows us to interpret $\uparrow X$ when $X$ is a singleton set, ${y}$ say. We observe for any $y, z$

$$ \begin{array}{l} \begin{array}{r l} & {\uparrow {y } \subseteq z} \ {\equiv} & {{(3 1) \mathrm {w i t h} X := {y }} \ & {\langle \forall x: x \in {y }: x \subseteq z \rangle} \end{array} \ \begin{array}{r l} & {\equiv \quad {\mathrm {s e t t h e o r y :} x \in {y } \equiv x = y }} \ & {\langle \forall x: x = y: x \leq 2 \rangle} \end{array} \ \equiv \begin{array}{l} {\mathrm {o n e - p o i n t r u l e} } \ y \equiv z, \end{array} \ \end{array} $$

from which observation we conclude for any $y$

(32) $\uparrow { y} = y$

by Indirect Equality (7)

The case of infinite X we shall not pursue here, we shall , however, try to interpret $\uparrow X$ when $X$ equals The empty set $\varnothing$ . We observe for any $z$

$$ \begin{array}{l} \equiv \begin{array}{l} \left{ \begin{array}{l} (3 1) \mathrm {w i t h} X := \emptyset \end{array} \right} \ \langle \forall x: x \in \emptyset : x \subseteq z \rangle \end{array} \ \equiv \begin{array}{l} {\mathrm {s e t t h e o r y}: x \in \phi \equiv \mathrm {f a l s e} } \ \langle \forall x: \mathrm {f a l s e}: x \leq z \rangle \end{array} \ \begin{array}{r l} & {\equiv {\mathrm {e m p h y - r a n g e r u l e (f r o m p r e d i c a t e}} \ & {\qquad \mathrm {c a l c u l u s , s e e l a t e r)} }} \ & {\mathrm {t r u e},} \end{array} \ \end{array} $$

which observation we can rewrite as

i.e. $\uparrow \varnothing$ satisfies the defining relation (29) for

And this concludes our little bit of

lattice theory.

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