A bagatelle on total orders

A bagatelle on total orders

If $\geq$ is postulated to be reflexive, antisymmetric, and transitive - for definitions, see later - it induces what is called a partial order. If, moreover, (Aa,b:: a≥b v b≥a), the order is total. For a total order $\geq$ we can define another relation $>$ by

$a > b \equiv 7\;b \geq a\;\therefore$

relation $>$ is then transitive as well. We even have the stronger theorems

$\Rightarrow a > b$ (1) $\Rightarrow a > c\;b < 0$

informally known as "Dyckstra's Laws". (These theorems need a name because they have proved themselves to be of considerable heuristic value.) This bagatelle is devoted to their demonstration (which turned out be harder than I had ex- pected).

Introduction Let predicates $P, Q, R$ satisfy

(2) $\left\lbrack {P \vee Q \vee R}\right\rbrack$ (3a) [IP v IP] (3b) $\left\lbrack {{7Q} \vee {7R}}\right\rbrack$ (3c) $\left\lbrack {{7R} \vee {7P}}\right\rbrack$

then $[\mathsf{P}vQ\equiv \mathsf{iR}]$ and cyclically.

Proof As (2) expresses that the predicates are weak enough and (3) that the are strong enough, we prove the demonstrandum by mutual implication. We observe

$$ \begin{array}{l} [ P \vee Q \Leftarrow \neg R ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \vee Q \vee R ] \ = {(2) } \ t r u e \ [ P \vee Q \Rightarrow \neg R ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \Rightarrow \neg R ] \land [ Q \Rightarrow \neg R ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ \neg R \vee \neg P ] \wedge [ \neg Q \vee \neg R ] \ = {(3 c); (3 b) } \ t r u e \ \end{array} $$

$$ \begin{array}{l} (E n d o f P r o o f) \ (E n d o f I n t r o d u c t i o n) \ \end{array} $$

In order to avoid possibly misleading connotations with the linear order of the reals, we introduce for our relation the new symbol $\mathbf{D}$ . Let $\mathbf{D}$ satisfy for all $a,b,c$

(4) $a > a$

(reflexivity)

(5) $a > b \land {b}^{ \land }a \Rightarrow a = b$

(cant isometry).

(6) $a > b \land {b}^{c} \Rightarrow a > c$

(transitivity)

(7) $a > b > v > b > a$

(linearity)

In terms of relation $D$ we define relation $A$ by

(8) $a \Delta b \equiv 7{a}^{2} > b$

This enables us to rewrite (5) and (7) as

(9) $a < b \vee b < a \vee a = b$ (10a) aaab v 7b4a

Since (4) is equivalent -one-point rule- to $a = b \Rightarrow {a}^{2}b\;$ or $a = b \Rightarrow b > a$ ,we deduce

[\left( {10b}\right) \;{7b} \div a\;v\;7a = b] $\left( {10c}\right) {7a} = b\;v\;{7a} < b$

With $P,Q,R\coloneqq a\bar{a} b,b\bar{a} a,a = b,(9)$ and (10) are an instantiation of (2) and (3), and thus we have derived -with rewriting (8)-

(11) $a \Delta b \vee a = b \equiv b \Rightarrow a\;;$ negating both sides of (11) yields (with (8) and de Morgan) (12) $a \nmid b \land a \neq b \equiv b \nmid a\;.\;$

In analogy to (1) and (2) we now have to prove

(13) $b \triangleleft a \land {b}^{2}c \Rightarrow c \triangleleft a$ (14) $a < b \land c > b \Rightarrow a < c$

Proof of (13) We observe for any $a,b,c$

$b < a \land b > c$

$$ \begin{array}{l} = {(1 2); \mathrm {e x c l u d e d m i d d l e}; \wedge \mathrm {d i s t r i b u t e s o v e r} v } \ (a \triangleright b \land a \neq b \land b \triangleright c \land a \neq c) \lor \ (a \triangleright b \land a \neq b \land b \triangleright c \land a = c) \ = {\mathrm {s e e b e l o w} } \ a \triangleright b \land a \neq b \land b \triangleright c \land a \neq c \ \Rightarrow {(6); p r e d i c a t e c a l c u l u s } \ a \geq c \land a \neq c \ = {(1 2) \mathrm {w i t h} b := c } \ c \triangle a; \ \end{array} $$

to see that the omitted disjunct is false, we observe

$$ \begin{array}{l} a \Delta b \wedge a \neq b \wedge b \Delta c \wedge a = c \ {\mathrm {L e i b n i z} } \ a \triangleright b \land a \neq b \land b \triangleright a \land a = c \ \Rightarrow \quad {(5) } \ a \neq b \land a = b \land a = c \ = {\mathrm {p r e c i l i c a t e c a l c u l u s} } \ f ^ {\prime} a l s e \ \end{array} $$

(End of Proof of (13))

The proof of (14) truly follows the same pattern and is not included here. (The need to appeal once more to the antisymmetry came somewhat as a surprise.)

Finally we observe for any $a, b, c$

$a < b \land b < c$

$$ \begin{array}{l} = {(1 2) \mathrm {w i t h} a := c } \ a \triangleleft b \wedge c \triangleright b \wedge c \neq b \ \Rightarrow {1 4; p r e d i c a t e c a l c u l u s } \ a \triangleleft c \ \end{array} $$

i.e. also relation $\Delta$ is transitive: for all $a,b,c$

(15) $a \Delta b \land b \Delta c \Rightarrow a \Delta c$

Theorem Let relations $\triangleright$ and $\triangleleft$ be coupled by (8), i.e. the one is the negation of the other. If $\triangleright$ satisfies (4), i.e. is reflexive, and $\triangleleft$ is transitive, i.e. satisfies (15), $\triangleright$ satisfies (7), the linearity requirement.

Proof We observe for any $a, b$

$$ a > b \lor b > a $$

$$ \begin{array}{l} = {4 } \ a > b \vee b > a \Leftarrow a > a \ = {(8), c o n t r a p o s i t i v e a n d d e M o r g a n } \ a \triangleleft b \wedge b \triangleleft a \Rightarrow a \triangleleft a \ = {(1 5) \mathrm {w i t h} c := a } \ t r u e \ \end{array} $$

(End of Proof.)

Austin 9 January 1989

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA