A simple country dance for transitivity and shunting

A simple country dance for transitivity and shunting

Transitivity of the relation E (read "under")

(a) $a \leq b \land b \leq c \Rightarrow a \leq c$

with the converse relation 2 (read "above") satisfying $a \leq b \equiv b \geq a$ etc., and the symmetry of $\land$ ,we can rewrite (0) and reformulate the tran-sitivity by stating that for all a,b,c

$\Rightarrow c \equiv a\;{b}^{x} \equiv {c}^{y}$

in other words: of 5 and 3 , the one is as transitive as the other.

But in this note we shall exploit the symmetry differently, viz by ob-serving that there are two ways of rewriting (o) by shunting , viz.

$b \leq c \Rightarrow \left( {a \leq b \Rightarrow a \leq c}\right)$ $a \leq b \Rightarrow \left( {b \leq c \Rightarrow a \leq c}\right)$

and if we take for the implication,

$$ w e g e t $$

$\left( 4\right) \;\left( {b \Rightarrow c}\right) \Rightarrow \left( {\left( {a \Rightarrow b}\right) \Rightarrow \left( {a \Rightarrow c}\right) }\right)$ (5) $\left( {a \Rightarrow b}\right) \Rightarrow \left( {\left( {b \Rightarrow c}\right) \Rightarrow \left( {a \Rightarrow c}\right) }\right) ,$

i.e. implication is monotonic in its right-hand argument and antimonotonic in the other.

Here, however, we shall pursue that in (0), (2), and (3), one of the three dummies in the universal quantifica tion occurs only at one side of the (outer) implication. Universally quanti-fying (0), (2), (3) over b,a,c respec-tively, yields secundum regulas artis

$\left\langle {0,1}\right\rangle \Rightarrow \left\langle {{a}_{1} \leq b}\right.$ $\left( {2}^{\prime }\right) \Rightarrow \left\langle {\forall a : : a \leq b \Rightarrow a \leq c}\right\rangle$ $\left( {3}^{\prime }\right) \;a \leq b \Rightarrow \left\langle {\forall c\therefore b \leq c \Rightarrow a \leq c}\right\rangle$

This note is written because I observed people having difficulty with the first step of a reflexivity proof that started with

$\Leftrightarrow \left{ {\left( {5},D\right) \text{ with }c = a}\right}$ $\left\langle {\exists b : a \leq b \Rightarrow a \land a \leq b}\right\rangle$ [where (5,0) in the hint referred to $a \leq b \Rightarrow a \leq b \Rightarrow a \leq c.$

People wonder: "Why that existential quanfication?" Why not just write

$\Leftrightarrow \left{ \begin{array}{l} a \leq a \ c : \left( {5,\mathcal{D}}\right) \end{array}\right.$ with $c \mathrel{\text{:=}} a}$

But that would be a step that trans- forms an expression not depending on b into one depending on b. We can eliminate b as free variable by quantifying over it, and I used to justify the choice of the existential quanfication by the fact that this proof is building up a strengthening chain and that therefore the weaker intermediate result makes it easier to complete it. (Remember: in a strengthening chain, each intermediate result represents your remaining proof obligation.)

similarly, if in a weakening chain

a free variable threatens to be introduced we bind it by universal quantifications, because in a weakening chain, inter- mediate results stand for conclusions reached so far, and one wishes to formulate those as strong as possible.

If is these strategies that are nicely

Austin, 27 September 1998

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