A relational bagatelle

A relational bagatelle

The first observation is, that , given the ex- change rules in the form

(0) $\left\lbrack {x;y \Rightarrow z}\right\rbrack \equiv \left\lbrack {{72}^{ \circ }; \sim y \Rightarrow {7x}}\right\rbrack$ for all $x,y,z$ (1) $\left\lbrack {x;y \Rightarrow z}\right\rbrack \equiv \left\lbrack {\sim x;\neg z \Rightarrow \neg y}\right\rbrack$ for all $x,y,z$ , it stands to reason to rewrite " $\sim$ over; "

$$ [ \sim (x; y) \equiv \sim y; \sim x ] f o r a l l x, y $$

in the more similar form

(2) $\left\lbrack {x;y \Rightarrow z}\right\rbrack = \left\lbrack {\sim y;\sim x \Rightarrow \sim z}\right\rbrack$ for all $x,y,z$ .

Note We use freely -i.e. without mentioning it even - that $\sim$ is an involution that distributes over the logical connectives. (End of Note.)

The second, more important observation, which I owe to Rutger M. Dykstra, is that we can eliminate the 7-signs by (i) transforming the dummy z into 72 , and (ii) shunting the consequents towards the antecedents ; we then get for all $x,y,z$

$$ \begin{array}{l} [ x; y \land z \Rightarrow \mathrm {f a l s e} ] \equiv [ z; \sim y \land x \Rightarrow \mathrm {f a l s e} ] \ [ x; y \land z \Rightarrow \mathrm {f a l s e} ] \equiv [ \sim x; z \land y \Rightarrow \mathrm {f a l s e} ] \ [ x; y \land z \Rightarrow \mathrm {f a l s e} ] \equiv [ \sim y; \sim x \land \sim 2 \Rightarrow \mathrm {f a l s e} ] \ \end{array} $$

Remark This observation is of importance be- cause, besides eliminating many negation signs, it eliminates many calculational steps of taking the contrapositive by a simple appeal to the symmetry of $\land$ . Rutger went one step further and eliminated the "⇒false" by the introduction of the "somewhere operator", the conjugate of the "everywhere operator" [ ] (End of Remark.)

We now introduce 3 functions from triples (of predicates) to triples (of predicates), in which definitions " $\sim$ " denotes an involution:

$$ \begin{array}{l} L. (x, z, y) = (z, x, \sim y) \ R. (x, z, y) = (\sim x, y, z) \ C _ {1} (x, z, y) = (\sim y, \sim z, \sim x) \ \end{array} $$

It now follows that with $\alpha ,\beta ,\gamma$ any permutation of $L,R,C\therefore$

(i) $\alpha \circ \alpha =$ the identity function (ii) $\alpha = \beta \circ \gamma \circ \beta$

I find it a bit annoying that my proof

(i) requires showing that $\mathit{LOL}$ , $\mathit{ROR}$ , and $\mathit{COC}$ are all three the identity function, (ii) follows from the fact that LoR , RoC and coL are the same function.

By way of example we compute $\mathsf{L}\mathsf{o}\mathsf{L},\mathsf{L}\mathsf{o}\mathsf{R},\mathsf{R}\mathsf{o}\mathsf{C}$

$$ \begin{array}{l} (l o L). (a, b, c) \ = \begin{array}{l} {{\mathrm {d e f . o f} L \mathrm {w i t h} x, y, z := a, c, b }} \ {L. (b, a, \sim c)} \end{array} \ = \begin{array}{l} {{\mathrm {d e f . o f} L \mathrm {w i t h} x, y, z := b, \sim c, a }} \ {(a, b, \sim \sim c)} \end{array} \ = \left{ \begin{array}{l l} \sim 1 5 \mathrm {o n i n v o l u t i o n} \ (a, b, c) \end{array} \right} \ \end{array} $$

$$ \begin{array}{l} (L \circ R). (a, b, c) \quad (C \circ L). (a, b, c) \ = \begin{array}{l} {{\mathrm {d e f . o p} R }} \ {L. (\sim a, c, b)} \end{array} = \begin{array}{l} {{\mathrm {d e f . o p} L }} \ {C. (b, a, \sim c)} \end{array} \ = \left{ \begin{array}{l l} \mathrm {d e f . o p} L \ (c, \sim a, \sim b) \end{array} \right. = \left{ \begin{array}{l l} \mathrm {d e f . o p} C \ (c, \sim a, \sim b) \end{array} \right. \ \end{array} $$

And now we can, for instance, conclude

$$ \mathcal {R} $$

$$ \begin{array}{l} = \left{ \begin{array}{l} L O L \end{array} \right. i s t h e i d e n t i t y f u n c t i o n 3 \ = {L O R = C o L } \ \end{array} $$

From (ii): $\alpha = \beta \circ \gamma \circ \beta$ we conclude that of the triple $\left( 0\right) ,\left( 1\right)$ ,and(2),we can derive each from the two others,and that we can do so in (precisely) two ways. To show how,for instance (0) can be derived from (1) and (2),we observe

$$ \begin{array}{l} [ x; y \Rightarrow z ] \ = {(\mathbf {i}) } \ [ \sim x; \sim z \Rightarrow \sim y ] \ = {(2) } \ [ \sim 7 2; x \Rightarrow \sim 7 y ] \ = {(1) } \ [ 7 2; \sim y \Rightarrow \neg x ] \ \end{array} $$

$$ \begin{array}{l} [ x; y \Rightarrow z ] \ = {\left(2\right) } \ [ \sim y; \sim x \Rightarrow \sim z ] \ = {() } \ [ y; \sim 1 2 \Rightarrow \sim 1 x ] \ = {(\mathbf {2}) } \ [ \neg z; \sim y \Rightarrow \neg x ] \ \end{array} $$

a guise in which these proofs may look quite surprising, but now we know why they could be constructed on the principle "there is only one thing you can do".

The nice thing of this bagatelle is that the algebraic theorem $\alpha = \beta \circ \gamma \circ \beta$ yields the proof-theoretic result that (0), (1), and (2) are not independent results, as each follows from the other two.

Austin, 22 October 1992

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