Addendum to EWD969

Addendum to EWD 969

(To be inserted after " (End of Proof 5.6)" at EWD 969-16.)

Remark 5.6 can be extended. Let $P, Y$ be the strongest solution of

$$ X: [ p. (X, Y) \equiv X ] $$

i.e. our formal knowledge about $f$ is captured by

$\left( {20}^{\prime }\right) \;\left\lbrack {p.\left( {p,Y,Y}\right) \equiv p.Y}\right\rbrack$ $\left\lbrack {p,\left( {X,Y}\right) \Rightarrow X}\right\rbrack \Rightarrow \left\lbrack {p,Y \Rightarrow X}\right\rbrack$

Then, analogous to the conclusion $\left\lbrack {g.P \equiv Q}\right\rbrack$ , Theorem 5.6 allows us to conclude $\left\lbrack {P.Q \equiv P}\right\rbrack$ , i.e. $\left( {P,Q}\right)$ is a solution of

$$ (x, Y): [ (f. Y, g. X) \equiv (X, Y) ] $$

We shall now show that $(P,Q)$ is the strongest solution of the above equation, i.e. we shall show

$$ [ (P, Y, g, X) \equiv (X, Y) ] \Rightarrow [ (P, Q) \Rightarrow (X, Y) ] $$

To this end we observe for any $X, Y$ satisfying the antecedent

$$ \begin{array}{l} [ (P, Q) \Rightarrow (X, Y) ] \ \Leftarrow {1 9 } \ [ p. (X, Y) \Rightarrow X ] \land [ q. (X, Y) \Rightarrow Y ] \ = \begin{array}{l} {{\mathrm {t h e a n t e c e d e n t e q u i v a l e s} [ f. Y \equiv X ] \wedge [ g. X \equiv Y ] }} \ {[ p. (f. Y) \Rightarrow f. Y ] \wedge [ q. (X, g. X) \Rightarrow g. X ]} \end{array} \ = {(2 0) a n d (2 0 ^ {\prime}) } \ f r u e \ \end{array} $$

The next theorem will show that above $f$ and $g$ are monotonic. The theorem of Knaster. Tarski is therefore applicable and we have therefore that (P.O) is also the strongest solution of

$$ (x, y): [ (f. Y, g. X) \Rightarrow (X, Y) ] $$

Note how in the above we have proved the weaker implication, i.e. the one with the stronger antecedent: the middle step in the above proof makes essential use of the equivalence. (End of Remark.)

Austin, 27 April 1987

prop. dr. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188