A bagatelle on implication’s transitivity

A bagatelle on implication's transitivity

We recall

Leibniz's Rule in the form $\left\lbrack {X \equiv Y}\right\rbrack \Rightarrow \left\lbrack {P \cdot X \equiv P \cdot Y}\right\rbrack$ - is symmetric and associative - $\vee$ is symmetric,associative,and idempotent; - ^ is defined by the Golden Rule. $[X\wedge Y\equiv X\equiv Y\equiv X\vee Y]$ ; it can be shown to be symmetric, associative, and idempotent.

We prove here

(0) $\left\lbrack {{X}{\Lambda }\left( {Y \equiv Z}\right) \equiv {X}{\Lambda }Y \equiv {X}_{\Lambda }Z \equiv X}\right\rbrack$

Proof

$$ \begin{array}{l} X \wedge (Y \equiv Z) \ = {\text {G o l d e n R u l e} } \ X \equiv Y \equiv Z \equiv X \vee (Y \equiv Z) \ = {v d i s t r i b u t e s o v e r \equiv } \ X \equiv Y \equiv Z \equiv X \vee Y \equiv X \vee Z \ = {\mathrm {s y m .} \& \mathrm {a s s . o f} \equiv } \ (X \equiv Y \equiv X \vee Y) \equiv (Z \equiv X \vee Z) \ = {\mathrm {G o l d e n R u l e}, \mathrm {t w i c e} } \ X \wedge Y \equiv X \wedge Z \equiv X \ \end{array} $$

(End of Proof.)

$\Rightarrow$ is defined by

$$ [ X \Rightarrow Y \equiv X \vee Y \equiv Y ] $$

or, by virtue of the Golden Rule, equivalently by

$$ [ X \Rightarrow Y \equiv X \land Y \equiv X ] $$

The remainder of this note is devoted to proving

$\left\lbrack {\left( {X \Rightarrow Y}\right) \land \left( {Y \Rightarrow Z}\right) \Rightarrow \left( {X \Rightarrow Z}\right) }\right\rbrack$

not because this is difficult, but because this proof gives me the opportunity of showing the considerations that guide its design.

*

The primary shape of our demonstrum (1) is of the form $\left\lbrack {P \Rightarrow Q}\right\rbrack$ as to how to eliminate the $\Rightarrow$ ,about which little has been established so far. We can either take the form of the antecedent into account and consider a demonstrum of the form

$$ [ P \land Q \Rightarrow R ] $$

or the form of the consequent, and consider a demonstrandum of the form

$$ [ P \Rightarrow (Q \Rightarrow R) ] $$

We choose the latter because of its nested implications about which we know so little yet: their elimination offers the hope of a "complicated"

expression whose structure almost dictates its simplification. We observe

$$ P \Rightarrow (Q \Rightarrow R) $$

$=$ {as the outer implication has a complicated consequent that we would not like to duplicate we opt for its conjunctive definition}

$$ P \land (Q \Rightarrow R) \equiv P $$

$=$ {because of the $\land$ in front of it, the remaining implication too is eliminated by its conjunctive definition}

$$ P \land (Q \land R \equiv Q) \equiv P $$

$= \left{ \begin{array}{l} \left( 0\right) \text{because that tells us how to deal with an equivalence as conjunct: (0) with} \ X,Y,Z \end{array}\right.$

$$ P \land Q \land R \equiv P \land Q $$

$= {$ conjunctive def. of $\Rightarrow }$

$$ P \land Q \Rightarrow R $$

Hence we have established

$\left\lbrack {P \Rightarrow \left( {Q \Rightarrow R}\right) \equiv P \land Q \Rightarrow R}\right\rbrack$

Applying this result (2), that tells us how to eliminate $a \Rightarrow$ from the consequent to our demonstrandum (1), we rewrite that as

(I) $\left\lbrack {\left( {X \Rightarrow Y}\right) \land \left( {Y \Rightarrow Z}\right) \land X \Rightarrow Z}\right\rbrack$

So far we have not taken into account that the antecedent of (1) was a conjunction; the

introduction of the conjunct X as in (1') draws attention to this fact: the time has come to take into account that the antecedent of (i) was a conjunction of implications. First and last conjuncts of the antecedent of (i') being the only pair in which only two variables occur, we investigate

$$ P \land (P \Rightarrow Q) $$

$= {$ conjunctive elimination of $\Rightarrow$ ,as before $}$ $= { \left( 0\right)$ with $X,Y,Z \mathrel{\text{:=}} P,{P}^{ \land }Q,P$ : that should give opportunity for simplification!

$$ P \wedge P \wedge Q \equiv P \wedge P \equiv P $$

$= {$ idempotence of $\land }$ $= {$ identif1y element of $\rho \equiv }$

hence

(3) $[P \wedge (P \Rightarrow Q) \equiv P \wedge Q]$

And now we are ready to tackle our original demonstrum

(1) $= {$ on account of (2): see (1) $}$

$$ [ X \wedge (X \Rightarrow Y) \wedge (Y \Rightarrow Z) \Rightarrow Z ] $$

$= { \left( 3\right)$ with $P,Q : X,Y}$

$$ \begin{array}{l} [ X \wedge Y \wedge (Y \Rightarrow Z) \Rightarrow Z ] \ = {(3) \mathrm {w i t h} P, Q := Y, Z } \ [ X \wedge Y \wedge Z \Rightarrow Z ] \ = {\mathrm {c o n j u n c h i v e d e f i n i t i o n} o p \Rightarrow } \ [ X \wedge Y \wedge Z \wedge Z \equiv X \wedge Y \wedge Z ] \ = {i d e m p o t e n c e o f \wedge ; i d e n t i b l y e l e m e n t o f \equiv 3 \ \end{array} $$

And this concludes the proof.

Why should I be interested in heuristics - even in woolly heuristics - to solve a problem so trivial? It is trivial in the technical sense that we have mechanical decision procedures for the propositional calculus. The point is -I hope!- that by willfully ignoring the mechanical decidability I can even use these technically "trivial" problems as proving ground for manipulation strategies.

Austin, 26 April 1988

prof.dn. Edsger W. Dgikstra

Department of Computer Sciences

The University of Texas at Austin

Aushin, TX 78712 - 1188

USA