Perry Moerland’s proof of Carel Scholten’s theorem

Perry Moerland's proof of Carel Scholten's theorem

At the last session of the ETAC, Perry Moerland showed a proof of a conjecture of Carel Scholten's (which neither Carel nor I had been able to prove). Perry's proof, which is very short, deserves recording because it has a few nice features.

About predicate transformers

(0) $f$ is monotonic (1) ${f}_{g}$ is the identity function (2) $g \circ f$ is the identity function , and we have to prove (3) $g$ is monotonic.

A few naive efforts suggest that the theorem would not hold for monotonicity with respect to an arbitrary partial order and that we have to take some special properties of the implication into account, such as its relation to the negation. One way of introducing the negation is by shunting, another one is by considering the conjugates - [f.x ≡ if.(iX)], etc.

We choose the latter, inspired by

(i) what is given about the pair ${f}_{g}$ ,also holds for the pair ${p}^{ * }{g}^{ * }$ ,and (ii) the conjugate allows us to rephrase (3) as

$\left\lbrack {X \vee Y}\right\rbrack \Rightarrow \left\lbrack {{g}^{ * }X \vee g \cdot Y}\right\rbrack$ for all $X,Y$ .

For the first bold step, it helps to remember the Mother of All Inference Rules

(4) $\left\lbrack {P \vee Q}\right\rbrack \land \left\lbrack {R \vee S}\right\rbrack \; \Rightarrow$

$$ [ P \vee (Q \wedge R) \vee S ] $$

which is used to introduce into the con- sequent of (3') the term $g.x$ -alterna- tively we could have introduced the other "in between term" $g^{*}.Y -$ :

$$ \begin{array}{l} [ g ^ {} X \vee g. Y ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ g ^ {}, X \vee (i g. X \wedge g. X), \vee g. Y ] \ = {\mathrm {d e f . o f} \mathrm {c o n j u g a t e} } \ [ g ^ {} X \vee (g ^ {} (X) \wedge g. X) \vee g. Y ] \ \Lleftarrow {4 } \ [ g ^ {} X \vee g ^ {} (X) ] \wedge [ g X \vee g Y ] \ \Leftrightarrow \quad {L e m m a 0, t w i c e } \ [ X \vee \neg X ] \wedge [ X \vee Y ] \ = \begin{array}{l} {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ X \vee Y ] \end{array} \ \end{array} $$

where we used

Lemma 0 for all $X, Y$

$$ [ X \vee Y ] \Rightarrow [ g. X \vee g. Y ] \qquad a n d $$

$$ [ X \vee Y ] \Rightarrow [ g ^ {} X \vee g ^ {} Y ] $$

Proof We only prove the first implication.

$$ [ g. X \vee g. Y ] $$

$\Leftrightarrow {$ lemma 1 with $X \mathrel{\text{:=}} g \cdot X \vee g \cdot Y}$

$$ [ f. (g. X \vee g. Y) ] $$

$\Leftrightarrow { \left( 0\right) ,i.e. f$ is monotonic

$$ [ f. (g. X) \vee f. (g. Y) ] $$

$= { \left( 1\right) ,i.e.\;{f}_{0}$ is identity function $}$

$$ [ X \vee Y ] \qquad \mathrm {(E n d o f P r o o p .)} $$

After the appeal to (4), the emergence of Lemma 0 is not too surprising, for it is just what we need. The same holds for the emergence of Lemma 1 in the last proof above; it is just what we need for we need to eliminate g-applications in a strengthening chain, and g can be eliminated by applying

Lemma 1 For all $X\colon [f.X]\Rightarrow [X]$ and

$$ [ f ^ {*} X ] \Rightarrow [ X ] $$

Proof Again, we only prove the first implication. This little proof, I think, is surprising. In a weakening chain we have to eliminate $f$ ;

(2) not having been used yet, $g$ -application is the appropriate mechanism for the elimination of $f$ . So little being known about $g$ , Leibniz's Principle has to justify the weakening in the step where $g$ is applied. This application is surrounded by introduction and removal of $\equiv$ . We observe for any $X$ :

$$ [ f, X ] $$

$$ \begin{array}{l} \Rightarrow {p r e d i c a t e c a l c u l u s } [ f. t r u e \Rightarrow f. x ] \ = \begin{array}{l} {\left{f \mathrm {m o n o t o n i c , i . e .} [ f. \mathrm {t r u e} \Leftarrow f. X ] \right}} \ {[ f. \mathrm {t r u e} \equiv f. X ]} \end{array} \ \Rightarrow \quad {\mathrm {L e i b n i z} } \ [ g. (f. t r u e) \equiv g. (f. x) ] \ = {(\mathbf {2}), \mathrm {i . e .} g ^ {\circ} f i s i d e n t i t y } \ = {p r e d i c a t e c a l c u l u s } [ X ] \ \end{array} $$

(End of Proof.)

This last proof is something to remember. (A short proof of the whole theorem has been published by J.C.S.P. van der Woude in "C.S. Schohen Dedicata".)

Nuenen, 27 December 1992

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