A few addenda to EWD1192

A few addenda to EWD1192

(This text is not self-contained. You should have EWD 1192: "The very first beginnings of lattice theory" at hand.)

Before "twinkle, twinkle, little star" on page EWD 1192-2, I should have drawn one further conclusion from axioms (0) through (3) and definition (5), viz.

$\left( {5a}\right) - z \leq x \downarrow y \equiv z \leq x \land z \leq y$ and its dual

$\left( {56}\right) \;{x}^{2}{y}^{2} \leq z \equiv x \leq z \land y \leq z\;\therefore$

Proof of (5a) We observe for any $x,y,z$

$$ \begin{array}{l} z \leq x \land z \leq y \ = {(\mathbf {5}), \leq \mathrm {i n} \mathrm {t e r m s} o f \downarrow } \ x \downarrow z = 2 \land y \downarrow z = 2 \ = {\mathrm {L e i b n i z} } \ x \downarrow y \downarrow z = z, \wedge y \downarrow z = z \ = {\mathrm {L e i b n}; z } \ x \downarrow y \downarrow z = z \wedge y \downarrow x \downarrow y \downarrow z = z \ = {0, (1), a n d (2) } \ x \downarrow y \downarrow z = 2 \wedge x \downarrow y \downarrow z = 2 \ = {\mathrm {i c l e m p o t e n c e} o f ^ {\prime} \wedge , (5) } \ z \leq x \downarrow y \ \end{array} $$

(End of Proof of 5(a))

The proof of (5b) is mutatis mutandis the same (replace $\downarrow$ by $\uparrow$ and $\leq {by} \geq$ ).

The importance of (5a) is that it proves the solvability of equation (7a); similarly for (5b) and equation (7b). And this repairs my omission of showing that axiom (7) of the second system is a theorem of the first system.

Jan L.A. van de Snepscheut drew my at- ten tion to the fact that, in the first sys- tem, we don't need to postulate (0), the idempotence of $\uparrow$ and $\downarrow$ ,because it follows from the laws of absorption. (Depending on how the laws of absorption are defined, one might need the symmetry. Associativity is not involved.)

We observe for any $p,q$

P P

$= \left{ {\begin{array}{l} \text{ left }L.\rho A. \ \text{ p }\uparrow \left( {p \downarrow \left( {q \uparrow p}\right) }\right) \end{array}\text{ with }x,y \mathrel{\text{:=}} p,q}\right.$ $\left{ \begin{array}{l} \text{ right } \ \text{ of }\;A. \ B. \end{array}\right.$ with $x,y := \left( {q \uparrow p}\right) ,p$ and symmetry of $\downarrow 3$

p

By interchanging or not the arguments of $\uparrow$ and/or of $\downarrow$ , each law of absorption and theorem (4) can be written in 4 ways. For each formulation of (4) we can formulate the laws of absorption in such a way that (4) can be proved without appeal to (1), the symmetry of $\uparrow$ and $\downarrow$ , but none of those formula-tions allows us to prove the idempotence of $\uparrow$ and $\downarrow$ without an appeal to (1). As a matter of fact, we then need the symmetry of $\uparrow$ to demonstrate the idempotence of $\downarrow$ , and vice versa. (Please don't ask me how I established these last results. It was rather ugly, but polishing up the argument is insufficiently rewarding. Thank you for not asking.)

Austin, 2 October 1995

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