The very first beginnings of lattice theory

The very first beginnings of lattice theory

of two infix operators $\uparrow$ ("up") and $\downarrow$ ("down") we are given that the are idempotent, symmetric, and associative, i.e. (in order)

(0) $x \uparrow x = x\;x \downarrow x = x$ ${xy} = y\overset{1}{ \downarrow }x$ $\left( 2\right) \left( {x \uparrow y}\right) \uparrow z = x \uparrow \left( {y \uparrow z}\right) \left( {x \downarrow y}\right) \downarrow z = x \downarrow \left( {y \downarrow z}\right) .$

Furthermore they satisfy the so-called absorption rules, i.e.

(3) $x \downarrow \left( {y \uparrow x}\right) = x$ ${y}^{ \uparrow }\left( {x \downarrow y}\right) = y$

From (3) alone we can conclude

${xy}$

Proof The proof is by mutual implication; here we only show ping, i.e. LHS $\Rightarrow$ RHS

$$ \begin{array}{l} = y ^ {\uparrow} {L H S o f (4) } \ y \uparrow (x \downarrow y) \ y \quad , \quad i. e. \quad p i n g. \ \end{array} $$

(End of Proof.)

We can now define relation

$x \leq y \equiv x \downarrow y = x\;$ or $x \leq y \equiv {y}^{ \uparrow }x = y$

According to (4), the two definitions are equivalent.

We observe

$$ \begin{array}{l} = \begin{array}{r l} & x \leqslant x \ & {(5) } \end{array} \ x \downarrow x = x \ = {() } \ t r u e \quad , \quad i. e. \leq i s r e f l e x i v e. \ x \leq y \land y \leq x \ x \downarrow y = x \wedge y \downarrow x = y \ y \downarrow x = x \wedge y \downarrow x = y \ \Rightarrow \quad {L e i b n i z } x = y, \mathrm {i . e .} \leq s i n t i s y m m e t r i c. \ \begin{array}{l} x \leq y \ \left{\left(5\right) \begin{array}{l} y \leq z \ t w i c e \end{array} \right} \end{array} \ x \downarrow y = x \wedge , y \downarrow z = y \ \Rightarrow \quad {\mathrm {L e i b n i z} } \ x \downarrow y = x \wedge x \downarrow (y \downarrow z) = x \ = {\left(2\right) } \ x \downarrow y = x \wedge (x \downarrow y) \downarrow z = x \ \Rightarrow \quad {L e i b n i z } \ x \downarrow z = x \ = {5 } \ x \leq z, i.e. \leq s t a n s i t i v e. \ \end{array} $$

A relation that is reflexive, antisymmetric, and transitive is called "a partial order"; we can summarize that $\leq$ , as introduced above, is a partial order.

Let us start with a tabula rasa at the other side. Of relation $\leq$ we are given

$x = y \equiv \times \leq y \land y \leq x,\;$ i.e. $\leq$

is reflexive and antisymmetric ;

(7) for all $x,y$ the equations

$\left( {7a}\right) \;w : \left\langle {\forall z : z \leq w \equiv z \leq x \land z \neq y}\right\rangle$

$\left( {76}\right) \;w : \left{ {\forall z : w \leq z \equiv x \leq z \land y \leq z}\right}$

are solvable.

To begin with we shall show that for fixed $x,y$ ,the solution of (7a) is unique. We observe for any $h,k,x,y$

h solves (7a) and k solves (7a)

$\left{ \left( {7a}\right) \right}$

$$ \langle \forall z: z \leq h \equiv z \leq x \land z \leq y \rangle \land $$

$$ \langle \forall z: z \le k \equiv z \le x \land z \le y \rangle $$

$\Rightarrow \;\left{ \begin{array}{l} \text{ Leibniz } \ \end{array}\right}$

$$ \langle \forall z: z \leq h \equiv z \leq k \rangle $$

$\Rightarrow \;\left{ {\text{with} \mathbf{z} \mathrel{\text{:=}} \mathbf{h};\text{with} \mathbf{z} \mathrel{\text{:=}} \mathbf{k}}\right}$

$$ \begin{array}{l} (h \le h \equiv h \le k) \land (k \le h \equiv k \le k) \ = {\leq i s r e f l e x i v e } \ h \le k \land k \le h \ \Rightarrow \quad {\leq i s a n h i s y m m e t r i c } \ h = k, \mathrm {i . e .} \mathrm {t h e s o l u t i o n o f (7 a)} \ \end{array} $$

$$ i s u n i q u e. $$

For (7b) we conclude similarly that its solution is unique. We denote the solutions by $x \downarrow y$ and $x \uparrow y$ respectively, i.e. we have for all $x, y, z$

$z \leq x \downarrow y \equiv z \leq x \land z \leq y$ ${x}^{\prime }y \leq 2 \equiv x \leq 2 \land y \leq 2$

Before further exploration of properties of $\downarrow$ and $\uparrow$ ,we establish that $\leq$ is transitive. To this end we observe

for arbitrary

$$ b \leq c \Rightarrow a \leq c $$

$= \left{ {\text{pred.}\operatorname{calc.},\text{heading for}\left( 9\right) }\right}$

$$ a \leq c \land b \leq c \equiv b \leq c $$

$= \left{ \begin{array}{l} \left( 9\right) \text{ with }x,y,z \mathrel{\text{:=}} a,b,c} \end{array}\right.$

$$ a \uparrow b \leq c \equiv b \leq c $$

[\left{ \begin{array}{l} \text{ Leibniz } \ \end{array}\right} ]

$$ a \uparrow b = b $$

$\Leftrightarrow \;{ \leq \text{ is antisymmetric }}$

$$ a \uparrow b \leq b \land b \leq a \uparrow b $$

$$ \begin{array}{l} = {1 0) w i t h x, y := a, b } \ a \uparrow b \leq b \ = {(\mathbf {9}) \mathrm {w i t h} x, y, 2 := a, b, b } \ a \leq b \land b \leq b \ = {\leq i s r e f l e x i v e } \ a \le b \ \end{array} $$

where

$$ (1 0) x \downarrow y \leqslant x, x \downarrow y \leqslant y, x \leqslant x \uparrow y, y \leqslant x \uparrow y $$

follows from (8) and (9) with $z \mathrel{\text{:=}} x \uparrow y$ and

Since $a \leq b \Rightarrow \left( {b \leq c \Rightarrow a \leq c}\right)$ equivalences

Remark The usual treatment immediately postulates that is a partial order. (End of Remark.)

Our next purpose is to prove (0) through (5) from (6) through (10)

$$ a d (0) \quad W e o b s e r v e f o r a n y x, z $$

$$ \begin{array}{l} x \uparrow x \leq 2 \ = {(9) } \ x \leq z \wedge x \leq z \ = {\wedge i d e m p o t e n t } \ x \leqslant z \ \end{array} $$

$$ f o r \downarrow s i m i l a r l y $$

ad (1) We observe for any $x,y,z$ ${x}^{\prime }y \leq 2$ for $\downarrow$ similarly $x \leq z \land y \leq z$ $y \leq z \land x \leq z$ $= { \left( 9\right) }$ $y \uparrow x \leq 2.$

ad (2) We observe for any $x,y,z,u$

$\left( {x + y}\right) \uparrow \leq u$ ${y}^{2} - {15}{y}^{2} + {15} = 0$ for $\downarrow$ similarly $\left{ \left( 9\right) \right}$

$$ \begin{array}{l} x \uparrow y \leq u \ {9 } \end{array} \land z \leq u $$

$$ \begin{array}{l} (x \le u \land y \le u) \land z \le u \ {\wedge \mathrm {a s s o c i a t i v e} } \ x \leq u \land (y \leq u \land z \leq u) \ = {(\mathfrak {g}) } \ x \leq u \land y ^ {\uparrow} z \leq u \ = {(9) } \ x \uparrow (y \uparrow z) \leq u \ \end{array} $$

ad (3) We observe for any $x,y$

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

$\left{ \begin{array}{l} \leq \text{ is antisymmetric } \ \end{array}\right}$ $x \leq x \downarrow {\left( y \uparrow x\right) }^{y}$

$$ = {(\mathbf {8}) } $$

and similarly

$$ x \leq x \land x \leq y ^ {\uparrow} x $$

for the other

$$ = {\leqslant r e f l e x i v e, (1 0) } $$

absorption rule

$$ t r u e $$

ad (4) This follows from (3)

ad (5) We observe for any $x,y$

$$ \begin{array}{l} = \begin{array}{r l} & x \downarrow y = x \ & {1 0 } \end{array} \ = \begin{array}{l} x \leq x \downarrow y \ {(\delta) } \end{array} \ = \begin{array}{r l} & x \leqslant x \land x \leqslant y, \ & {x \leqslant r e f l e x i v e } \end{array} \ x \leq y \ \end{array} $$

And this concludes the demonstration that the two ways of introducing lattices are equivalent. From now on- wards we feel free to use (0) through (10), independently of how lattices have been introduced.

We shall now give two different proofs of the monotonicity of $f$ , i.e.

$x \leq y \Rightarrow x \uparrow z \leq y \uparrow z$

Proof A In view of (9) we rewrite the

$$ \langle \forall u: y ^ {\uparrow} z \leq u \Rightarrow x ^ {\uparrow} z \leq u \rangle $$

and observe for any $x,y,z,u$ such that ${xxy}$

$$ = \begin{array}{l} y ^ {\uparrow z \leq u} \ {(9) } \end{array} $$

$y \leq u \land z \leq u$ $\left{ {\times {5y}, \leq \text{transitive}} }\right.$ $x \leq u \land z \leq u$

$$ = \begin{array}{l} {{(9) }} \ {x \uparrow z \leq u} \end{array} $$

(End of Proof $A$ )

Proof. Here we tackle the consequent directly, and observe for any $x, y, z$

$$ \begin{array}{l} = \begin{array}{r l} & x \uparrow z \leq y ^ {\uparrow z} \ & {(5) } \end{array} \ \begin{array}{r l} {(x \uparrow_ {2}) \uparrow (y \uparrow_ {2})} & {= y \uparrow_ {2}} \ & {\quad {\uparrow \downarrow \mathrm {c a l c u l u s , s u c h a s a s s o c i a t i v i t y o f} \uparrow }} \end{array} \ \begin{array}{r l} {(x \uparrow y) \uparrow z} & {= y \uparrow z} \ {{\mathrm {L e i b n i z} }} & \end{array} \ = \begin{array}{l} x \uparrow y = y \ {5 } \end{array} \ \begin{array}{l} x \leq y \ (\mathrm {E n d o f P r o o f B}) \end{array} \ \end{array} $$

I think I prefer proof B, probably because it does not depend on intermediate results depending monotonically on some of their subexpressions.

We conclude this short introduction with (half of) the proof of (I distributes over $\downarrow$ ) $\equiv$ ( $\downarrow$ distributes over $\uparrow$ )

We prove ping by observing for any $x,y,z$ $\left( {x \downarrow y}\right) \uparrow \left( {x \downarrow z}\right)$ $\left{ {\begin{array}{l} \uparrow \text{ over }\downarrow \ \end{array}\;\left( {\left( {x \downarrow y}\right) \uparrow x}\right) \downarrow \left( {\left( {x \downarrow y}\right) \uparrow z}\right) }\right.$ $= \left{ {\begin{array}{l} \text{absorption,}\uparrow \text{over}\downarrow \ \end{array}\;}\right}$ $x \downarrow \left( {x \uparrow z}\right) \downarrow \left( {y \uparrow z}\right)$ $= \left{ {\begin{array}{l} \text{absorption}\ x \downarrow \left( {y \uparrow z}\right) \end{array}\;}\right.$

Nothing in the above is new. This EWD has been written for my students to correct an error in last week's lectures.

Austin, 14 November 1994

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