Equivalence versus mutual implication; junctivity and monotonicity

Equivalence versus mutual implication; junctivity and monotonicity

There are two complementary ways of expressing equivalence, viz.

$\left\lbrack {X \equiv Y \equiv \left( {{iX} \vee Y}\right) \land \left( {{X}^{2} \vee {iY}}\right) }\right\rbrack$ and (1) $\left\lbrack {X \equiv Y \equiv \left( {\neg X \land \neg Y}\right) \vee \left( {X \land Y}\right) }\right\rbrack$

There has been a time - not even so very long ago! - at which I was very familiar with (0) and hardly aware of (1). The greater popularity of (0) - i.e. expressing equivalence as mutual implication - is explained by the observation

$$ \begin{array}{l} [ X \equiv Y ] \ = {(0) \mathrm {w i t h r e w r i t t e n c o n j u n c t s} } \ [ (X \Rightarrow Y) \land (X \Leftarrow Y) ] \ = {\left[ \right] d i s t r i b u t e s o v e r \Lambda } \ [ X \Rightarrow Y ] \land [ X \Leftarrow Y ] \ \end{array} $$

Hence, (0) enables us to express the boolean scalar $[X = Y]$ in terms of two (simpler or weaker) boolean scalars. Because the "everywhere" operator $[]$ does not distribute over $v$ , (1) is much less useful. (I am pleased to observe that I owe this insight to $[]$ and its algebraic properties: in binary logic, where $[]$ is the identity operator, the above observation is void.)

Until quite recently I used to prove that a finitely conjunctive predicate transformer $f$ , i.e. one for which

(2) $[f.(X\wedge Y)\equiv f.X\wedge f.Y]\quad$ holds for all $X,Y,$ is monotonic, i.e (3) $\left\lbrack {P \Rightarrow Q}\right\rbrack \Rightarrow \left\lbrack {f.P \Rightarrow f.Q}\right\rbrack$ for all $P,Q$ , in the following way. Observe for any $P,Q$

$$ [ f, P \Rightarrow f, Q ] $$

$$ \begin{array}{l} = {\left{f r o m \Rightarrow t o \wedge \right} \ [ f. P \wedge f. Q \equiv f. P ] \ = {2) \mathrm {w i t h} X, Y := P, Q } \ [ f. (P \land Q) \equiv f. P ] \ \Leftrightarrow \quad {L e i b n i z } \ [ P, Q \equiv P ] \ = {\mathrm {f r o m} \land t o \Rightarrow } \ [ P \Rightarrow Q ] \ \end{array} $$

To which I can add that I liked this proof so much that my eloquence sufficed to convince many an audience that the above proof can be designed on the principle that "there is only one thing you can do". I honestly believed that the above proof was all but forced. The other month, though, I had a shock!

I rewrote (2) as the conjunction of

(4) $\left\lbrack {f \cdot \left( {X \land Y}\right) \Rightarrow f \cdot X \land f \cdot Y}\right\rbrack$ for all $X,Y$ and

(5) $\left\lbrack {f\left( {X \land Y}\right) \Leftrightarrow f\left( {X \land f\left( {Y\text{}}\right) }\right\rbrack }\right.$ for all $X,Y$

and observed for any $P,Q$ such that $\left\lbrack {P \Rightarrow Q}\right\rbrack$

$$ f. p $$

$$ \begin{array}{l} = {\mathrm {s i n c e} [ P \land Q \equiv P ] \mathrm {a n d l e i b n i z} } \ f: (P \wedge Q) \ \Rightarrow \quad {(4) \mathrm {w i t h} X, Y := P, Q } \ f. P \wedge f. Q \ \Rightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ f. Q \ \end{array} $$

Please note that our latter proof does not appeal to (5) !

Unimportant remark The latter proof could have been rendered equivalently as

$$ [ f, p \Rightarrow f, q ] $$

$$ \begin{array}{l} = {\mathrm {s i n c e} [ P \land Q \equiv P ] \mathrm {a n d L e i b n i z} } \ [ f. (P \wedge Q) \Rightarrow f. Q ] \ \end{array} $$

$$ \begin{array}{l} \Leftarrow {p r e d i c a t e c a l c u l u s } \ [ f. (P \wedge Q) \Rightarrow f. P \wedge f. Q ] \ = {(4) \mathrm {w i t h} X, Y := P, Q } \ t r u e \ \end{array} $$

(End of Unimportant remark.)

The next question was whether, using only (4) instead of (2), a proof in the style of our former proof could be constructed. Note that our latter proof "uses" $\left\lbrack {P \Rightarrow Q}\right\rbrack$ ,whereas our first proof starts with $\left\lbrack {f.p \Rightarrow f.Q}\right\rbrack$ and strong-

thens it to $\left\lbrack {P \Rightarrow Q}\right\rbrack$ without using it on the way. Along that strengthening path we have to eliminate the occurrences of $f$ . Since we cannot elim- minate all occurrences of $f$ by appealing to (4),the only thing left to appeal to is the Rule of Leibniz

$$ [ X \equiv Y ] \Rightarrow [ f. X \equiv f. Y ] $$

I thought this forced the use of (2) but Lincoln

A. Wallen showed me how it could be done with (4):

$$ \begin{array}{l} [ f. P \Rightarrow f. Q ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ f. P \Rightarrow f. P \land f. Q ] \ \Leftrightarrow {\mathrm {t r a n s i t i v i t y} o f \Rightarrow 3 \ [ f. P \Rightarrow f. (P \land Q) ] \land [ f. (P \land Q) \Rightarrow f. P \land f. Q ] \ = {(2) \mathrm {w i t h} X, Y := P, Q } \ [ f. P \Rightarrow f. (P \land Q) ] \ \Leftarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ f. P \equiv f. (P \wedge Q) ] \ \Leftarrow {\mathrm {L e i b n i z} } \ [ P \equiv P _ {\wedge} Q ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \Rightarrow Q ] \ \end{array} $$

We have introduced conjunctivity properties of

a predicate transformer $f$ to characterize the degree in which $f$ -application distributes over conjunction and universal quantification - on syntactic grounds, some might prefer "commutes with universal quantification". We defined " $f$ is conjunctive over $V$ " as

(6) $\left\lbrack {f.\left( {{\Delta X} : X \in V : X}\right) \equiv \left( {{\Delta X} : X \in V : f{.}^{2}X}\right) }\right\rbrack$

and introduced conjunctivity types expressing that $f$ is conjunctive over all $V's$ , over all non-empty $V's$ , over all non-empty denumerable $V's$ , all non-empty and linear $V's$ , etc.

But was this the correct notion? We could have split (6) into two independent properties

(7) $\left\lbrack {f.\left( {{A}^{x};x \in V;X}\right) \Rightarrow \left( {{A}^{x};X \in V;f.X}\right) }\right\rbrack$ and (8) $\left\lbrack {f.\left( {\underline{A}X : X \in V : X}\right) \Leftrightarrow \left( {\underline{A}X : X \in V : f.X}\right) }\right\rbrack$

Rewriting (7) as

(7') (A: Y∈V: [f. (AX: X∈V: X) ⇒ f.Y])

we see immediately that each monotonic $f$ satisfies (7'), and that each $f$ satisfying (7') for all $V$ of some conjunctivity type is monotonic. Construct for $P, Q$ such that $[P \Rightarrow Q]$ a $V$ such that $[(A X: X \in V: X) \equiv P] \land Q \in V$ . For none of our conjunctivity types this construction is a problem.)

Perhaps we should have expressed (8) for instance

as " $f$ contracts over $V$ " and -similarly (9) $\left\lbrack {f.\left( {\underline{E}X : X \in V : X}\right) \Rightarrow \left( {\underline{E}X : X \in V : P \cdot X}\right) }\right\rbrack$

as "f expands over V". "f is conjunctive over V" then becomes "f is monotonic and contracts over V". "f is universally conjunctive" becomes "f is monotonic and universally contracting", the point being that the qualifier "universally" is only of relevance for the contraction, and not for the monotonicity. The isolation of the unqualified monotonicity makes sense: negation is not monotonic, but it is both positively con-tracting and positively expanding.

Not only does it make sense, it helps. Reformulation of van der Woudel's theorem (and of Scholten's generalization) in terms of monotonicity, expansion, and contraction makes the design of the proof much more straightforward. This is for later.

PS. Xerox is to be blamed for having sold blotting paper to write upon.

Austin, 31 October 1988

Prof. Dr. Edsger W. Dykstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 United States of America