Why preorders are beautiful

Why preorders are beautiful

Preorders are relations that are reflexive and transitive, more precisely: $\leq$ is a preorder iff

(0) $\left( {A \times : \;x \subseteqq x}\right) \;,\;\;$ and (1) $\left( {\underline{A}x,y,z\therefore x \leq y \land y \leq z \Rightarrow x \leq z}\right)$

The combination of reflexivity and transitivity is beautiful because (0) is equivalent to $\left( 2\right) \;\left( {\underline{A}x,y : x \in y \Leftrightarrow \left( {\underline{A}z : y \leq z \Rightarrow x \leq z}\right) }\right)$

and (1) is equivalent to (3) $\left( {\underline{A}x,y\therefore x \leq y \Rightarrow \left( {\underline{A}z\therefore y \leq z \Rightarrow x \leq z}\right) }\right) ,$

so that, by taking their conjunction, we derive: is a preorder iff

$\left( 4\right) \;\left( {\underline{A}x,y : x \leq y \equiv \left( {\underline{A}z : y \leq z \Rightarrow x \leq z}\right) }\right) .$

Proof of $\left( 0\right) \Rightarrow \left( 2\right)$ We observe for any $x,y$

$$ \begin{array}{l} (\underline {{A}} z: y \leq z \Rightarrow x \leq z) \ \Rightarrow \quad {\mathrm {w i t h} z := y } \ y \leq y \Rightarrow x \leq y \ = {0) w i t h x := y; p r e d i c a t e c a l c u l u s } \ x \leq y \quad (\mathrm {E n d o f P r o o f o f} (0) \Rightarrow (2)). \ \end{array} $$

Proof of (0) $\Leftrightarrow$ (2) We observe for any $x$

$$ \begin{array}{c c c} \times & \sqsubseteq & \times \ \hline \end{array} $$

$$ \begin{array}{l} \Leftarrow \left{ \begin{array}{l l} (2) \mathrm {w i t h} y := x \end{array} \right} \ (A z: x \leq z \Rightarrow x \leq z) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ t r u e \ \end{array} $$

$$ (E n d o f P r o o f o f (0) \Leftarrow (2).) $$

$$ \mathrm {P r o o f} o p (1) \equiv (3) $$

$$ \begin{array}{l} (\underline {{A}} x, y, z: \quad x \leq y \land y \leq z \Rightarrow x \leq z) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} x, y, z: \quad x \leq y \Rightarrow (y \leq z \Rightarrow x \leq z)) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} x, y: \quad x \leq y \Rightarrow (\underline {{A}} z: \quad y \leq z \Rightarrow x \leq z)) \ (E n d o f P r o o f o f (1) \equiv (3)) \ \end{array} $$

with $\equiv$ ,the transpose of $\leq$ ,given by

(5) $\left( {x,y : x \geq y \equiv y \leq x}\right)$

we have

(6) $\;\left( {5\text{ is a preorder }}\right) \equiv \left( {2\text{ is a preorder }}\right)$

because

(7) (5 is reflexive) $\equiv$ (2 is reflexive) (8) (5 is transitive) $\equiv$ (2 is transitive)

$$ \mathrm {P r o o f s o f (7) a n d (8)} $$

$$ \begin{array}{l} (A \times :: X \subseteq X) \ = \begin{array}{l} {{(5) }} \ {(\underline {{A}} x: \underline {{\cdot}} x \geq x)} \end{array} \quad a n d \ \end{array} $$

$$ (A x, y, z: x \leq y \land y \leq z \Rightarrow x \leq z) $$

$$ = {(\mathfrak {s}) } $$

$$ (A x, y, z: \quad y \geq x \quad \land \quad z \geq y \Rightarrow z \geq x) $$

$$ = {\text {p r e d i c a t e c a l c u l u s} } $$

$$ (\exists x, y, z: z \geq y \land y \geq x \Rightarrow z \geq x) $$

$$ (E n d o f P r o o f s o f (7) a n d (8).) $$

As an alternative to (4) we now derive

$$ E \mathrm {i s a p r e o r d e r i f f} $$

(9) $\;\left( {\underline{A}x,y : : x \in y \equiv \left( {\underline{A}z : : z \in x \Rightarrow z \in y}\right) }\right)$

$$ \begin{array}{l} \frac {\mathrm {P r o o f}}{2} \ (\equiv \mathrm {i s a p r e o r d e r}) \ = {6 } \ (\exists i s a p r e o r d e r) \ = {(4) \mathrm {w i t h} x, y, \subseteq := y, x, \exists } \ (\underline {{A}} y, x: \quad y \geq x \equiv (\underline {{A}} z: \quad x \geq z \Rightarrow y \geq z)) \ = {5 } \ (\underline {{A}} x, y: \quad x \leq y \equiv (\underline {{A}} z: \quad z \leq x \Rightarrow z \leq y)) \ (\mathrm {E n d o f P r o o p}) \ \end{array} $$

Remark Formulae (4) and (9) are not difficult to memorize. In (4), the 2 occurrences of $x$ are at the same side of $\underline{5}$ and "hence" $x \leq z$ occurs as consequent, whereas the 2 occurrences of $y$ are at the different sides of $\underline{5}$ , and "hence", $y \leq z$ occurs as antecedent. Formula (9) follows the same pattern. (End of Remark.)

Let $W$ now be a nonempty subset of the domain on which our relation $E$ is defined, and let there exist an $x$ satisfying

(10) $\left( {A,y : y \in W : x \leq y}\right)$

From now on we shall pronounce the relation $\mathbf{E}$ as "under"; the jargon then captures the fact that $x$ satisfies (10) by saying that " $x$ is a lower bound of $W$ " In general, (10) is not a suitable way to define $x$ , because if (10), viewed as equation in $x$ , is solvable, it often has many solutions. We can be more stringent by requiring $x$ to satisfy (10) and (11) with (11) given by

$\left( {1 + 2}\right) \;\left( {1 - 2}\right) \Leftrightarrow \left( {1 + 2}\right) y = 1 - y$

By requiring that any lower bound $z$ of $W$ is under $x$ , $x$ becomes what the jargon calls "a highest lower bound of $W$ ".

Now, wouldn't it be nice if (10) were equivalent to (12), with (12) given by

(12) $\left( {\underline{A}z : z \leq x \Rightarrow \left( {\underline{A}y : y \in W : z \leq y}\right) }\right)$

You see, then (10)∧ (11) -the condition that x is a highest lower bound of W - becomes (12)∧ (11), which can nicely be simplified to

(13) $\;\left( {\underline{A}z : z \equiv x \equiv \left( {\underline{A}y : y \in W : z \leq y}\right) }\right)$

The equivalence aimed at holds for all preorders, more precisely

Lemma (Ax,W: (10) ≡ (12)) = (E is a preorder)

Proof The proof is by mutual implication.

$\therefore {LHS} \Rightarrow {RHS}$ We observe for any $x,y$

LHS

$\Rightarrow \;{$ with $x,W \mathrel{\text{:=}} x,{ y}$ and one-point rule $}$

$$ x \leq y \equiv (\underline {{A}} z: z \leq x \Rightarrow z \leq y)) $$

which observation establishes $\mathrm{{LHS}} \Rightarrow \mathrm{{RHS}}$ in view of (9).

LHS

(12)

$=$ {definition}; $Q \Rightarrow$ distributes over $A}$

$$ (\underline {{A}} z: (\underline {{A}} y: y \in W: z \leq x \Rightarrow z \leq y)) $$

$= \left{ {\text{interchange of quanthifications}}\right}$

$$ (\underline {{A}} y: y \in W: (\underline {{A}} z: z \leq x \Rightarrow z \leq y)) $$

$= \left{ {\mathrm{{RHS}},\text{ in particular (9) }}\right}$

$$ (A y: y \in W: x \leq y) $$

[\text{def.}} ]

(10)

(End of Proof.)

In view of (9), our lemma is of the form

$$ (\underline {{A}} x: p. x \equiv q. x) \equiv (A y: r. y \equiv s. y) $$

something I would not care to write down or like to manipulate without using the equivalence. Notice that in our proof only the outer equivalence is dealt with via mutual implication. Here it is not because the two directions depend on different properties -the proof of the lemma uses only the predicate calculus- but because of the universal quantifications:

$$ \begin{array}{r l} {\underline {{(A x :)}} \underline {{P x}}) \equiv (\underline {{A y}}: Q. y)} & {\equiv} \ {\underline {{(A y}}: (\underline {{A x}}: \underline {{P x}}) \Rightarrow Q. y)} & {\wedge (\underline {{A x}}: P. x \Leftarrow (A y: Q y))} \end{array} $$

and these conjuncs are dealt with separately.

(For unclear reasons this EWD took a long time to write. Strange, for writing it was a pleasure.)

Austin. 23 June 1991

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