Transitivity as an (unexpected?) consequence

Transitivity as an (unexpected?) consequence

All variables in this note are of an unspecified type on which a relation $\leq$ is defined.

A standard technique for function definition is to define the function as the solution of an equation. We would like to define the solution of

(0) $w : \left\langle {\forall z : w \leq z \equiv x \leq z \land y \leq z}\right\rangle$

as function of $x$ and $y$ . This only works provided

(i) solutions of (0) are always unique, and (ii) solutions of (1) always exist.

To begin with, we investigate what to postulate about so that we can prove unicity. Let $a,b$ be solutions of (0); we then observe for arbitrary $x,y$

$$ t r u e $$

$$ = \left{ \begin{array}{l} \text {p r e d . c a l c .} \ \langle \forall z: x \leq z \land y \leq z \equiv x \leq z \land y \leq z \rangle \end{array} \right. $$

$$ = {a a n d b ^ {2} b o t h s o l v e (0) } $$

$$ \langle \forall z: a \leq z \equiv b < z \rangle $$

$\Rightarrow$ { instantiated with $2 : = a\;{and}\;{with}\;z : = b}$ $= \left{ {\begin{array}{l} \bullet \text{ assume } \leq \text{ to be reflexive. } \ \end{array}\text{ }}\right}$

$$ \begin{array}{r l} & {\mathrm {b} \leq a \land a \leq b} \ {\Rightarrow} & {{\bullet \mathrm {a s s u m e} \leq t o b e a n t i s y m m e t r i c }} \ & {\mathrm {a} = b.} \end{array} $$

In view of the above argument we postulate our $\leq$ to be reflexive and antisymmetric.

Remark 2.1. Antisymmetric 2020.

(1) $\left\lbrack {x = y \equiv x \leq y \land y \leq x}\right\rbrack \;\therefore$

where we use [...] to denote universal quantification of the enclosed expression over its free variables. As the above argument shows,

(1) implies

$\left\lbrack {x = y \equiv \left{ {\forall z : x \leq z \equiv y \leq z}\right} \end{matrix}\right\rbrack \;$ and $\left\lbrack {x = y \equiv \left{ {\forall z : z \leq x \equiv z \leq y}\right} \end{array}\right\rbrack$

(End of Remark.)

Besides (1) we now postulate (ii), viz. that (0) is always solvable. The rest of this note is devoted to the proof that (1) $\land$ (ii) implies the transitivity of $\leq$ .

The proof, totally elementary and built from well-known components - see, for instance, [0] -

is rather indirect: following Feijen, we use (0)'s unique solution to define an infix. operator, of which we prove a number of properties using (1) and (2). Finally, the transitivity of is shown. Here we go.

We denote (0)'s solution by ${x}^{\prime }y$ , i.e. define the infx operator

$\left\lbrack {{x}^{2}y \leq z \Rightarrow x \leq z \land y \leq z}\right\rbrack$

Lemma 0: ↑ is associative .

[\text{Proof.}\left( {a \uparrow b}\right) \uparrow c \leq z]

$$ \begin{array}{l} = {(4) _ {a}: x, y := (a \uparrow b), c } \ (a \uparrow b) \leq z \land c \leq z \ = {4): x, y := a, b } \ (a \leq z \land b \leq z) \land c \leq z \ = {\wedge i s a s s o c i a t i v e } \ a < z \land (b \leq z \land c \leq z) \ = {4): x, y := b, c } \ a \le z \land (b \uparrow c) \le z \ = {(4): x, y := a, (b \uparrow c) } \ a \uparrow (b \uparrow c) \leq z \ \end{array} $$

on account of (2)

$$ [ (a \uparrow b) \uparrow c \equiv a \uparrow (b \uparrow c) ] $$

now follows. (End of Proof.)

Lemma 1: $\left\lbrack {x \leq x \uparrow y \land y \leq x \uparrow y}\right\rbrack$

Proof We observe for any $x,y$

$$ \begin{array}{l} = \begin{array}{r l} & x \leq x \uparrow y, \wedge y \leq x \uparrow y \ & {(4): z := x \uparrow y } \end{array} \ = \begin{array}{r l} & x \uparrow y \leq x \uparrow y \ & {x \leq r e f p e x i v e } \end{array} \ t r u e \ \end{array} $$

(End of Proof.)

$$ \mathrm {L e m m a} 2 [ x \uparrow y = y \equiv x \leq y ] $$

Proof We observe for any $x,y$

$$ \begin{array}{l} = \begin{array}{r l} & x \uparrow y = y \ & {1: x := x \uparrow y } \end{array} \ = \begin{array}{l} x \uparrow y \leqslant y \wedge y \leqslant x \uparrow y \ {\text {L e m m a} 1 } \end{array} \ = \begin{array}{r l} & x \uparrow y \leq y \ & {4: z := y } \end{array} \ = \begin{array}{r l} & x \leq y \ & {x \leq r e f l e x i v e } \end{array} \ x \leq y \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

Theorem: $\leq$ is transitive.

Proof We observe for any $a,b,c$

$$ \begin{array}{l} a \leq b \land b \leq c \ = {\mathrm {L e m m a} 2: x, y := a, b \mathrm {a n d} x, y := b, c } \ a \uparrow b = b \wedge b \uparrow c = c \ \end{array} $$

$$ \begin{array}{l} \Rightarrow \quad {\text {L e i b o n i z} } \ (a \uparrow b) \uparrow c = c \wedge b \uparrow c = c \ = {\text {L e m m a} o } \ \end{array} $$

$$ \begin{array}{l} a \uparrow (b \uparrow c) = c \wedge b \uparrow c = c \ \Rightarrow \quad {L e i b n i z } \ a \uparrow c = c \ = {\text {L e m m a} 2: x, y := a, c } \ a \leq c \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

The proofs have been included to make this note self-contained (and perhaps also because it is always a pleasure to write them down). It is instructive to check how essential use has been made of equality. (Lemma 2, replaced, for instance, by $[x \uparrow y \leq y \equiv x \leq y]$ or $[x \uparrow y = y \Leftarrow x \leq y]$ , would not have sufficed for the proof of the Theorem.)

[0] W.H. J. Feijen, "Exercises in Formula Manipulation" in Formal Development of Programs and Proofs (Edsger W. Dgiksha, Ed.), Addison-Wesley Publishing Company, Inc., 1990

Austin, 20 October 1993

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