Courtesy Rajeev Joshi

Courtesy Rajeev Joshi

Denoting for any relation universal quantification over its two arguments by enclosing it within a pair of square brackets, we can formulate the

Theorem For relations $Q,R$ of the same type we have

$$ \langle \forall a, b, A, B: a Q b \Rightarrow A Q B: a R b \Rightarrow A R B \rangle \equiv $$

$$ [ \neg R ] \vee [ Q \equiv R ] \vee [ R ] $$

Proof We observe for any $Q, R$

$$ \langle \forall a, b, A, B: a Q b \Rightarrow A Q B: a R b \Rightarrow A R B \rangle $$

$$ \equiv {[ x \Rightarrow y \equiv 7 x \vee y ]; r a n g e s p l i t; t r a d i n g } $$

$$ \langle \forall a, b, A, B:: a Q b \vee \neg a R b \vee \neg A R B \rangle \land $$

$$ \langle \forall a, b, A, B:: \neg A Q B \vee \neg a R b \vee \neg A R B \rangle $$

$$ \equiv {\mathrm {n e s t i n g}; \vee \mathrm {d i s t r i b u t e s o v e r} \forall ; [ ] \mathrm {c o n v e n t i o n :} $$

$$ \langle \forall a, b:: a Q b \rangle \equiv [ Q ] \rangle , e t c. } $$

$$ ([ Q \vee \neg R ] \vee [ R ]) \wedge ([ \neg R ] \vee [ \neg Q \vee R ]) $$

$$ \equiv {\wedge d i s t r i b u t e s o v e r v } $$

$$ ([ Q \vee \neg R ] \wedge [ \neg R ]) \vee ([ Q \vee \neg R ] \wedge [ \neg Q \vee R ]) \vee $$

$$ ([ R ] \wedge [ \neg R ]) \vee ([ R ] \wedge [ \neg Q \vee R ]) $$

$$ \equiv {\mathrm {a b s o r p t i o n}, \mathrm {m u t u a l} \mathrm {i m p l i c a t i o n}, \mathrm {p r e d . c a l c .} } $$

$$ [ r ] \vee [ Q \equiv R ] \vee [ R ] \qquad (\mathrm {E n d o f P r o o f .}) $$

The above proof (or something very close to it) emerged when Rajeev Joshi decided to design a calculational proof for the theorem of EWD1245, which the above yields with $Q_{i} = J$ . The first

calculus did not use Q or J , but expressed the range as " $a = b \Rightarrow A = {B}^{\prime }$ ; it was only after "=" had been replaced by "J" that it became patently obvious that none of J's properties had been used and that, therefore, J could be generalized to any rela-tion. It was a modest example of how notation can stimulate abstraction.

Reference

EWD1245

A kind of converse of Leibniz's Principle (17 September 1996)

Austin, 29 September 1996

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