__When a symmetric operator distributes over ↑ and ↓__

To begin with we postulate (0) and (1):

(0) relation ⊑ is reflexive and antisymmetric,

i.e., for all `x`, `y`

`x`=`y` ≡ `x`⊑`y` ∧ `y`⊑`x`

(1) for any `x`,`y` there exists a (unique) value, which we denote by `x`↑`y`, that satisfies for all `z`

`x`↑`y` ⊑ `z` ≡ `x`⊑`z` ∧ `y`⊑`z` .

__Remark__ Since the uniqueness can be proved, it need not be postulated; hence the parentheses.
(End of Remark.)

It then follows that (for all `x`,`y`)

(2) ↑ is idempotent, symmetric, and associative

(3) `x` ⊑ `x`↑`y`

(4) `x` = `x`↑`y` ≡ `y`⊑`x`

(5) ⊑ is transitive (hence —see (0)— ⊑ is what is known as “a partial order”)

(6) ↑ is monotonic

We'll just prove (6).

__Proof__ We calculate for any triple `x`,`y`,`z` :

`x`↑`z` ⊑ `y`↑`z`

≡ {(4)}

`y`↑`z` = (`y`↑`z`)↑(`x`↑`z`)

≡ {(2)}

`y`↑`z` = (`y`↑`x`)↑`z`

⇐ {Leibniz’s Principle}

`y` = `y`↑`x`

≡ {(4)}

`x` ⊑ `y`

To the above we add “the dual” (0′) through (6′) obtained from (0) through (6) by

(α) interchanging the arguments of ⊑ , and

(β) replacing ↑ by ↓ and vice versa.

__Remark__ The reader may note that, thanks to the symmetry of ∧ , (0′) is equivalent to (0).
The “and vice versa” has been added so as to make (β) —like (α)— its own inverse.
(End of Remark.)

And this concludes our summary of Lattice Theory.

* *

*

Now we are ready to formulate and prove the following simple theorem.

__Theorem__ Let the symmetric infix operator ● distribute over ↑ and ↓ Then

(7) (`x`↑`y`)●(`x`↓`y`) = `x`●`y`

__Proof__ To begin with we observe for any `x`,`y`

(`x`↑`y`)●(`x`↓`y`)

= {● distributes over ↑}

(`x`●(`x`↓`y`))↑(`y`●(`x`↓`y`))

= {● distributes over ↓, twice}

(`x`●`x` ↓ `x`●`y`)↑(`y`●`x` ↓ `y`●`y`)

⊑ {(3') and (6), twice}

`x`●`y` ↑ `y`●`x`

= {symmetry of ● , idempotence of ↑}

`x`●`y` ,

i.e.,

(8) (`x`↑`y`)●(`x`↓`y`) ⊑ `x`●`y` .
.

By dualization we conclude from (8):

(8′) `x`●`y` ⊑ (`x`↓`y`)●((`x`↑`y`) ,

and thanks to the symmetry of ● and (0), the conjunction of (8) and (8′) yields (7). (End of Proof).

* *

*

The above theorem and proof emerged yesterday afternoon when K. Rustan M. Leino joined the session of the ATAC and wanted to show us some aspects of his proof of the fact that the product of two natural numbers equals that of their GCD and their LCM (what he did). The decision to go from there to lattices in general was a minor step. Acknowledgements are further due to Dr Rajeev Joshi, who contributed to what we presented here.

Austin, 6 October 1999

prof. dr. Edsger W. Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA