A little bit of lattice theory

A little bit of lattice theory (Replaces EWD1240)

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 convex figures in a plane. We shall mostly use the later letters of the lower-case alphabet , 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 \equiv y$ . (In the jargon this notational convention is captured by saying that " $\equiv$ is an infix operator.") Depending on the definition of $\equiv$ and the values of $x$ and $y$ , $x \equiv y$ is true or not.

Examples If the type is that of the natural numbers and E means "is a divisor of", then 3515 is true, but 6 15 is not true (or "is false" as we are used to say). If the type is that of the convex figures in a plane, and E means "lies inside", let $x,y,z$ then be situated as shown:

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 $\mathfrak{E}$ 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-

$$ \langle \forall x:: x \in x \rangle \tag {0} $$

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 convex figure 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}{r l} & {\langle \forall x, y: x \leq y \land y \leq x \Leftrightarrow x = y \rangle} \ {\equiv} & {{\mathrm {n e s t i n g} }} \ & {\langle \forall x: \langle \forall y: x \leq y \land y \leq x \Leftrightarrow x = y \rangle \rangle} \ {\equiv} & {{\mathrm {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} & {{\mathrm {o n e - p o i n t r u l e} }} \ & {\langle \forall x: x \leq x \land x \leq x \rangle} \ {\equiv} & {{\mathrm {a n d i d e m p o t e n t} }} \ & {\langle \forall x: x \leq x \rangle} \end{array} $$

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 $\langle$ "and $\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 $\langle$ to the last $\rangle$ -, while the scope of y extends over the inner bracket pair - from the second $\langle$ to the first $\rangle$ - The 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::$ " 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 $\mathbf{E}$ . It states that $\underline{\underline{\mathbf{E}}}$ 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

$\left\langle {\forall x,y : x \leq y \land y \leq x \Rightarrow x = y}\right\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 may indeed conclude that $x$ equals $y$ . (This last statement requires a proof which is not included here.) Similarly, with $x$ and $y$ denoting convex figures, we note that if $x$ lies inside $y$ and $y$ lies inside $x$ , we may indeed conclude that $x$ and $y$ denote the same convex figure. (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) $\langle \forall x,y\therefore x \leq y \land y \leq x \equiv x = y\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 $\underline{\underline{\mathbf{E}}}$ 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 \in x \Rightarrow z \subseteq y}\right\rangle \Rightarrow x \subseteq 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$

$\Rightarrow \;\left{ \begin{array}{l} \text{ instantiated};\;z \mathrel{\text{:=}} x} \ \end{array}\right.$

$\left{ {5\text{ reflexive }}\right}$

$\equiv \;\left{ {{pred}\;{cate}}\right.$ calculus: (true $\Rightarrow p$ ) $\equiv p}$

$$ \begin{array}{l} \langle \forall z: z \leq x \Rightarrow 2 \leq y. \rangle \ x \leq x \Rightarrow x \leq y \ t r u e \Rightarrow x \leq y \ x \leq 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

$$ \mathrm {t r u e} \Rightarrow p \quad \mathrm {t r u e} \equiv p \quad \mathrm {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 \subseteq$ 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 \equiv x \equiv z \equiv y}\right\rangle \Rightarrow x = y$ $\left\langle {\forall z : x \leq z \equiv y \leq z}\right\rangle \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$

$\langle {\forall z\therefore {25} \leq x \leq {25} \leq y}\rangle$ $\Rightarrow$ ${$ instantiate twice: $z = x$ and $z = y}$ $\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} \mathrm {c a l c u l u s} } \ x \equiv y \wedge y \equiv x \ \equiv {\left(3\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.

$$ \frac {\mathrm {P r o o f}}{\mathrm {a n d} \mathrm {l e t}} \mathrm {L e t}, \mathrm {f o r g i v e n} 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$ ..

$$ \begin{array}{l} w \leq 2 \ = {(8) } \ x \leq z, y \leq z \ = {(9) } \ \end{array} $$

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

thus establishing $\left\langle {\forall z\therefore \omega \leq z \equiv {w}^{\prime } \leq z}\right\rangle$ ,

from which $\omega = {\omega }^{\prime }$ 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 w satisfying (8), in all its formal glory:

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

The combination of uniqueness and existence of the w satisfying (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 to (8),the defining relation for $\uparrow$ is that for any $x,y,z$

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

Let us illustrate this with our earlier examples. With $x,y,z$ being natural numbers and $\subseteq$ meaning "is a divisor of", (10) reads "xTsy is a divisor of z, if and only if x and y are both divisors of z", telling us that xTsy is the smallest common multiple of x and y . With x,y,z convex figures and $\subseteq$ meaning "lies inside", xTsy is the convex hull of x and y (see Appendix for a proof):

Having introduced the operator $\uparrow$ via (10), we can now prove all sorts of properties of it. The first one is the Theorem $\uparrow$ 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 ↑ inherits these three properties from the conjunction $\land$ ,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$

$\left( {x \uparrow y}\right) \uparrow z \leq w$ $\left{ {\left( {10}\right) \text{with}x,y,z = {x}{1}{y}{1}z,{w}_{1}}\right}$ $\left( {x \uparrow y}\right) \leq w \land z \leq w$ [\left( {x \leq w \land y \leq w}\right) \land z \leq w] $\equiv \left{ \begin{array}{l} \land \text{ is associative } \ \end{array}\right}$ $x \leq w \land \left( {y \leq w \land z \leq w}\right)$ $\equiv \left{ \begin{array}{l} \left( {10}\right) \text{ with }x,y,z \mathrel{\text{:=}} y,z,w \ x \leq w \land \left( {{y}^{ \uparrow }z \leq w}\right) \end{array}\right.$ $\equiv \left{ \begin{array}{l} \left( {10}\right) \text{ with }y,z \mathrel{\text{:=}} y \uparrow z,w \ x \uparrow \left( {y \uparrow z}\right) \leq w \end{array}\right. ,$

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 has therefore to be removed. Similarly for the 1 in (x1y). 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) $x \leq x \uparrow y\; \land y \leq x \uparrow y$

Proof We observe for any $x, y$

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

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

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

$$ (1 5) 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 \equiv y \ {\equiv \text {i s r e f} \end{array} \ x \equiv y \wedge \mathrm {t r u e} \ = {\text {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

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

$$ \begin{array}{l} x \uparrow y = y \ \equiv {5 \mathrm {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}, \ i. e. (3) \mathrm {w i t h} x := x \upharpoonright y \ x \uparrow y \leq y \land y \leq x \uparrow y \ \equiv {1 5; (1 4), 2 n d \mathrm {c o n j u n c t} } \ 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} $$

$$ \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} $$

$$ \begin{array}{l} \mathrm {T h e o r e m .} E \mathrm {i s 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} $$

$$ \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 \wedge y \uparrow z = z \Rightarrow x \uparrow z = z $$

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

$$ \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} $$

It is this last theorem that turns relation $\varepsilon$ 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}^{n}$ 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 res-pect to 5 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} \equiv \begin{array}{r l} & f _ {x} \leq f _ {y} \ & \left{\left(1 6\right) \mathrm {w i t h} x, y := f _ {x}, f _ {y} \right} \end{array} \ = \left{f _ {i} ^ {} x \uparrow f _ {i} ^ {} y = f _ {i} ^ {*} y \right. \ f _ {1} (x \uparrow y) = f _ {2} y \ \Leftrightarrow \quad {\mathrm {e q u a l s} \mathrm {f o r e q u a l s} } \ \equiv \begin{array}{r l} & x \uparrow y = y \ & {(1 6) } \end{array} \ x \leq y \ \end{array} $$

(End of Proof.)

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 ${2}^{ \uparrow }$ as a function application

$d$ istributes over $\uparrow$ . This observation makes the previous theorem applicable in the proof of the following

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

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

${x}^{2}{y}^{2} + 5{y}^{2} = 4 \Rightarrow {x}^{2}{y}^{2} - {5y} + 4 = 0$

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\leqslant a^{\prime}\land b\leqslant b^{\prime}\Rightarrow a + b\leqslant 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 ↑, 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( {2,1}\right) \;\left\langle {\forall z\therefore z \leq w \equiv z \leq x\land z \leq y}\right\rangle$ ,

which, as before, determines for any $x,y$ 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 (= greatest lower bound) of $x$ and $y$ " or "the meet of $x$ and $y$ "; we shall use the name "the infimum of $x$ and $y$ " and denote it

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

(22) ${z5} \times \downarrow y \equiv {z5x} \land {z5y}$

Without proof we list its properties:

(23) $\downarrow$ is idempotent,symmetric,associative (24) $x \downarrow y \leq x \land x \downarrow y \leq y$ (25) $x \leq x \downarrow y \equiv x \equiv y$ (26) $x = {x}^{ \downarrow }y \equiv {x5y}$ (27) A function that distributes over $\downarrow$ is monotonic with respect to $\underline{\underline{\mathbf{E}}\cdot\cdot\cdot}$ (28) $\downarrow$ is monotonic with respect to $\leq$ in both its arguments.

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 this dilemma. Either we restrict the domain of $x,y$ to the positive integers (thus excluding zero), or we define $0 \downarrow 0 = 0$ ,a definition which is compatible with (22). I prefer the latter.

With $x,y$ convex figures in the plane and meaning "lying inside", $x \downarrow y$ would be the largest convex figure lying inside both, i.e. lying inside their intersection. But since the intersection of two convex figures is itself convex, $x \downarrow y$ is the intersection of $x$ and $y$

But what if the intersection of $x$ and $y$ is empty? The answer is to extend the domain of all "visible" convex figures by one extra element - called "bottom" and denoted by "⊥" or "⊥" - that by definition lies inside all convex figures (including itself). One could visualize it as "the empty convex figure"; its defining relation is (29)

Operators ↑ and ↓ are connected by the laws of Absorption

$\left( {30}\right) \;x = x \downarrow \left( {x \uparrow y}\right)$ $x = x \uparrow \left( {x \downarrow y}\right)$

Proof We prove the first one by observing for

true (End of Proof.)

$$ \begin{array}{l} x = x \downarrow (x \uparrow y) \ \equiv {(2 6) \mathrm {w i t h} y := x \uparrow y } \ x \leq x \uparrow y \ = {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$

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

$= \left{ {{}^{1}\;{over}\;{the}\;{rightmost}}\right}$

$$ ((x \downarrow y) \uparrow x) \downarrow ((x \downarrow y) \uparrow 2) $$

$$ \begin{array}{l} = {\mathrm {L a w o f A b s o r p h i 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) ^ {T} L a w o f A b s o r p h i o n } \ x \downarrow (y \uparrow z) \ \end{array} $$

(End of Proof.)

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

(↑ distributes over $\downarrow$ ) $\equiv \left( {\downarrow \text{distributes over} \uparrow }\right)$ .

(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 $\perp$ (i.e. element "bottom" as defined by (29)).

Relation (10)

$$ x \uparrow y \le 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 $1 \in {X}^{\prime \prime } - 1$ is an element of set $X$ ”- between the two colors restricts the range of the dummy x : the constraint $\frac{1}{2}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$

$$ \upharpoonright {y } \subseteq z $$

$$ \begin{array}{l} \equiv \quad {(3 1) \mathrm {w i t h} X := {y } } \ \langle \forall x: x \in {y }: x \leq z \rangle \ \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 \ \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

to interpret $\uparrow X$ when $X$ equals

empty 'set $\varnothing$ . We observe for any $z$

$$ \uparrow \phi \subseteq z $$

$$ \equiv \left{ \begin{array}{l l} (3 1) & \text {w i t h} X := \emptyset \end{array} \right} $$

$$ \langle \forall x: x \in \phi : x \leq z \rangle $$

$$ \equiv {\mathrm {s e t t h e o r y}: x \in \phi \equiv \mathrm {f a l s e} } $$

$$ \langle \forall x: f a l s e: x \leq z \rangle $$

$$ \equiv \begin{array}{l} {\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} \ \mathrm {c a l c u l u s , s e e l a t e r)} } \end{array} $$

$$ t r u e $$

which observation we can rewrite as

$$ \langle \forall z:: 1 \phi \leq z \rangle $$

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

for 上 . In other words, bottom and

the supremum of the empty set are

the same element (which, as we have

seen,need not exist).

And this concludes our little bit of

lattice theory.

Appendix

We have to show that for all convex

(AO) ${x}^{ \uparrow }y \leq z \equiv \times \leq z \land y \leq z\;,\;$

where ${x}^{\prime }y$ is defined as the convex hull

For brevity's sake we denote the union of $x$ and $y$ - i.e. every thing in side $x$ , inside $y$ or inside both-by

$\left( {A + 1}\right) h = x{U}_{y}$

From set theory and the notion "inside" we can now deduce for the right-hand side of (A0)

$\left( {A}_{2}\right) \;x \leq z\;w{\;y} \leq z\;h \leq z\;\cdots$

To tackle the left-hand side of (A0) we equate $x \uparrow y$ to $P$ ,where $P$ is the lowest (smallest) convex figure that contains both $x$ and $y$ . That a

convex $P$ contains both $x$ and $y$ is -see (A2)- expressed by

(A3) $h \leq P \land \operatorname{convex}.P$

while the fact that $P$ is the lowest (smallest), i.e. that $P$ lies inside any (other) convex figure $Q$ that contains

$\left( {A \downarrow }\right) \;h \subseteq Q \land \operatorname{convex.}Q \Rightarrow P \subseteq Q\;\left( {\text{for all}Q}\right) .$

Note (A3) and (A4) are here taken for granted. The demonstration that for any $h$ there exists a $P$ satisfying (A3) and (A4) would require a more detailed definition of the predicate "convex". (End of Note.)

With $P$ satisfying (A3) and (A4), our proof obligation (Ao) can now be rewritten that for any $h, z$

(A5) convex. $z \Rightarrow \left( {{P}_{\sum }z = h\sum z}\right)$ .

We prove (A5) by mutual implication, i.e. we demonstrate separately

${P}_{\sum }z \Rightarrow h \leq z\;,\;\left( {1,2}\right)$

Pong: $h \leq 2 \Rightarrow P \leq 2$

each time using whatever we need from (A3), (A4), and (A5)'s antecedent convex.z

Ping We observe for any $h, z$

$$ \begin{array}{l} p \le 2 \ \equiv {\mathrm {1 s t c o n j u n c t o f} (A _ {3}) } \ h \subseteq P \land P \subseteq Z \ \Rightarrow \quad {\equiv i s t r a n s i t i v e } \ h \leq z. \ \end{array} $$

Pong We observe for any $h,z$

$$ h \leq z $$

$$ \begin{array}{l} \equiv {\mathrm {a n t e c e d e n t} o f (A S) } \ h \in z \wedge c o n v e x. z \ \Rightarrow \quad \left{\mathrm {(A 4) i n s t a n t i a t e d w i t h} Q := 2 \right} \ P \subseteq 2 \ \end{array} $$

(End of Appendix.)

I am indebted to Rutger M. Dyrkstra for pointing out that in an earlier version, one of the examples was wrong.

Austin, 8 January 1998

prof. dir Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188, USA