A theorem of Scholten’s once more (see EWD1048)

The other week I stumbled across EWD1048, which records how the ATAC had proved a theorem of Carel Schohen's. Seeing the theorem and its proof I felt that we should now be able to design a much simpler proof, and that is what the ETAC did on 1992.08.18.

To begin with, we reformulated the theorem, introducing as many implications as possible so as to ease monotonicity considerations.

Let $p$ and $q$ satisfy

(0) $\left\lbrack {p \cdot X \Rightarrow Y}\right\rbrack \equiv \left\lbrack {X \Rightarrow q \cdot Y}\right\rbrack$ for all $X,Y$ .

Note The original theorem formulated the relation between $p$ 's conjugate and $q$ , and instead of the implications in (0), it had disjunctions. With Galois connections en vogue as they are, formulation (0) now seems preferable. (End of Note.)

Let $h.x$ be the strongest solution of

$$ Y: [ X \vee p. Y \Rightarrow Y ] $$

Because it follows from (0) that $p$ is mono-tonic, this strongest solution exists.

Note In the original theorem, the equation had

an $\equiv$ where our equation has an $\Rightarrow$ . Knaster-Tarski tells us that the two equations have the same strongest solution. (End of Note.)

In formula, we know that h.x implies all solutions, i.e. -with some predicate calculus -

(1) $\begin{array}{l} \left\lbrack {X \Rightarrow Y}\right\rbrack \land \left\lbrack {p,Y \Rightarrow Y}\right\rbrack \Rightarrow \left\lbrack {h.X \Rightarrow Y}\right\rbrack \ \text{for all} X,Y \end{array}$

and that $h.x$ is a solution, i.e.

(2a) $\left\lbrack {X \Rightarrow h.X}\right\rbrack$ for all X $\left\lbrack {p,h,x} = \Rightarrow h.x\right\rbrack$ for all $X$ .

Let $k \times n$ be the weakest solution of

$$ Y: [ Y \Rightarrow X \land q. Y ] $$

i.e. (similarly)

$\left\lbrack {Y \Rightarrow X}\right\rbrack \land \left\lbrack {Y \Rightarrow q,Y}\right\rbrack \Rightarrow \left\lbrack {Y \Rightarrow k,X}\right\rbrack$

$$ f o r a l l X, Y $$

(4a) $\left\lbrack {k.X \Rightarrow X}\right\rbrack$ for all $X$

$\left\lbrack {k,X \Rightarrow q.k}\right) \rbrack$ for all $X$ .

Then

$\left\lbrack {h.A \Rightarrow B}\right\rbrack \equiv \left\lbrack {A \Rightarrow k.B}\right\rbrack$ for all $A,B$ .

Proof We show LHS $\Rightarrow$ RHS: we observe for any $A,B$

$$ [ A \Rightarrow k, B ] $$

$$ \begin{array}{l} \Leftrightarrow \quad \left{ \begin{array}{l} (2 a) \text {w i t h} X := h. A \end{array} \right} \ [ h. A \Rightarrow k. B ] \ \Leftrightarrow \quad {(3) \mathrm {w i t h} X, Y := B, h. A } \ [ h. A \Rightarrow B ] \land [ h. A \Rightarrow q. (h. A) ] \ \Leftarrow {0) \Rightarrow , w i t h X, Y := h. A, h. A } \ [ h. A \Rightarrow B ] \land [ p. (h. A) \Rightarrow h. A ] \ = {(2 b) w i t h x := A } \ [ h. A \Rightarrow B ] \ \end{array} $$

The proof LHS RHS uses similarly (0) $\Leftarrow$ (1),

(4a) and (4b).

(End of Proof.)

This is a very satisfactory proof: the complete proof consists of 8 steps, each of them using 1 of the 8 independent givens, each of which is therefore appealed to once. (In the original EWD1048 version it was clearer that $\delta = 4 + 4$ : the symmetry between $\Rightarrow$ and $\Leftarrow$ was more obvious.)

In the above, we have constructed a strengthen- ing chain in which $k$ is eliminated -via (3)- and $h$ is introduced -via (2a)-, but please note the order! In (3), the consequent is an (anti)motonic function of $Y$ , while the antecedent is not. When you start your proof with

$$ \begin{array}{l} [ A \Rightarrow k, B ] \ \Leftrightarrow \quad {(3) \mathrm {w i t h} X, Y := B, A } \ [ A \Rightarrow B ] \land [ A \Rightarrow q, A ] \ \end{array} $$

you can continue strengthening by weaking the

$$ \begin{array}{l} \Leftrightarrow {2 a \mathrm {w i t h} X := h. A } \ [ h. A \Rightarrow B ] \land [ h. A \Rightarrow q. A ] \ \end{array} $$

but now you are stuck because (the consequent in) the second conjunct is too strong, and there is no nonweakening way of transform- ing q.A into q. (h.A).

The moral of the story is: when appealing to the extremal property - in this example (1) or (3) -, be aware of the loss of (anti)monotonicity - here in Y- when going from con- sequent to antecedent.

Austin, 29 August 1992

prof. dr. Edsger W. Dgiksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188

USA