The transitivity of the implication

The transitivity of the implication

Let $\leq$ -read "below" - be a punctual relation on structures of some type, i.e.

$\left\lbrack {x = y \land u = z \Rightarrow \left( {x \equiv u \equiv y \equiv z}\right) }\right\rbrack$

(We have given $\in$ a higher binding power than the logical operators; universal quantification over free variables is left understood.)

Let $\xi$ be transitive, i.e.

$\left\lbrack {x \leq y \land y \leq z \Rightarrow x \leq z}\right\rbrack .$ To the usual definition (1), we prefer here the equivalent alternatives $\left\lbrack {x \leq y \Rightarrow \left( {y \leq z \Rightarrow x \leq z}\right) }\right\rbrack$ and with ${x}{1}{y}{1}z = {z}{1}{x}{1}{y}_{1} -$ $\left\lbrack {x \leq y \Rightarrow \left( {z \leq x \Rightarrow z \leq y}\right) }\right\rbrack$

Note that, if a relation is transitive, so is its transpose.

Punctual h is monotonic with respect to $s$ means $\left\lbrack {x \leq y \Rightarrow h.x \leq h.y}\right\rbrack ;$

punctual h is antimonotonic with respect to $\leq$ means analogously

[\left\lbrack {x \leq y \Rightarrow {h.y} \leq {h.x}}\right\rbrack ]

After all those general definitions, we now start with more specific observations. With functions $f$ and $g$ defined by

(6) $\left\lbrack {f \cdot \xi \equiv z \leq \xi }\right\rbrack$ and $\left\lbrack {g \cdot \xi \equiv \xi \leq z}\right\rbrack$ for all $\xi$ ,

we can rewrite (2) and (3) :

$\left\lbrack {x \leq y \Rightarrow \left( {g,y \Rightarrow g \cdot x}\right) }\right\rbrack$ (8) $\left\lbrack {x \leq y \Rightarrow \left( {f \cdot x \Rightarrow f \cdot y}\right) }\right\rbrack$

Comparing (7) with (5) - or (8) with (4) - we see that in the two positions where (5) - or (4) - has " $\equiv$ ", (7) - or (8) - has a " $\equiv$ " and a " $\Rightarrow$ " respectively. There is precisely one special case in which this difference disappears, viz. when for the punctual and transitive " $\leq$ " in (4) through (8) we choose the punctual and transitive " $\Rightarrow$ ". The choice gives for (2) and (3) respectively the well-known theorems

$\left\lbrack {\left( {x \Rightarrow y}\right) \Rightarrow \left( {\left( {y \Rightarrow z}\right) \Rightarrow \left( {x \Rightarrow z}\right) }\right) }\right\rbrack$ -i.e. the implication is antimonotonic in its antecedent - and $\left\lbrack {\left( {x \Rightarrow y}\right) \Rightarrow \left( {z \Rightarrow x}\right) \Rightarrow \left( {z \Rightarrow y}\right) }\right\rbrack$ -i.e. the implication is monotonic in its con-

sequent - .

And now we see why the implication is such a special relation: it is -with its transpose $\nVdash$ -the only relation whose transitivity can be expressed in terms of (anti)monotonic dependence on its arguments! It is this circumstance that justifies and ex- plains the urgent and wise advice w.H.J. Feijen gave me -more than once, as a matter of fact, for I was a little bit slow in the uptake-. The advice was to justify steps like

$A \Rightarrow B$ $\Leftarrow$ {hint why $\left\lbrack {A \Rightarrow C}\right\rbrack$ and how to use this} $C \Rightarrow B$

not in terms of transitivity of $\Rightarrow$ , but as strengthening by weakening the antecedent. To strengthen and to weaken we have to do anyhow; the elimination of implications transi- vity from the language of hints is a significant simplification.

Nuenen, 12 December 1992

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