An improvement on EWD912

An improvement on EWD912

In my final comments on EWD912 I suggest that Theorem 5.0 would admit a shorter proof. Here is a suggestion.

Proof Th.5.0 With $f$ enjoying some type of conjunctivity, $f$ is monotonic; hence - Lemma 5.8 -

In order to show that $h$ is conjunctive over some $V$ , i.e.

[ h. (\underline {{A}} X: X \in V: X) \equiv (\underline {{A}} X: X \in V: h. X) ]

we show that either side implies the other.

(i) Because $h$ is monotonic,we have

[ h. (\underline {{A}} X: X \in V: X) ⇒ (\underline {{A}} X: X \in V: h. X) ]

(ii) To show the implication in the other direction, it suffices to show in view of (11) that

[ (\underline {{A}} X: X \in V: h. X) ⇒ f. ((\underline {{A}} X: X \in V: X), (\underline {{A}} X: X \in V: h. X)) ].

or, since quantification distributes over pair forming

(14) $\left\lbrack {\left( {{\underline{A}X} : X \in V : h.X}\right) ⇒ {f}_{c}\left( {{\underline{A}X} : X \in V : \left( {X,h.X}\right) }\right) }\right\rbrack$

To this end we construct a bag $W$ of predicate pairs by

\left(\mathrm {I S} ^ {\prime}\right) (X, Y) \in W \equiv X \in V \wedge [ Y \equiv h. X ]

and observe that - see Lemma to be inserted in ch.3- V and W are of the same junctivity type since h is monotonic. Hence, suffices to show (14') under the assumption that f is conjunctive over W .

\begin{array}{l} (A X: X \in V: h. X) \ = {(1 0) } \ (¬ X: X \in V: f. (X, h. X)) \ = {\mathrm {o n e - p o i n t} r u l e } \ (\underline {{A}} X: X \in V: (\underline {{A}} Y: [ Y \equiv h. X ]: f. (X, Y))) \ = {(1 5 ^ {\prime}) } \ (A X, Y: (X, Y) \in W: f. (X, Y)) \ = {f \mathrm {c o n j u n c t i v e o v e r} W } \ = {(1 5 ^ {\prime}) } \ p. (\underline {{A}} X: X \in V: (\underline {{A}} Y: [ Y \equiv h. X ]: (X, Y))) \ = {\mathrm {c n e - p o i n t r u l e} } \ P (\underline {{A}} X: X \in V: (X, h, X)) \ \end{array}

(End of Proof Th. 5.0)

Austin, 9 April 1985

prof. dr. Edsger W. Dyrksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 United States of America