Andrew’s challenge once more (see EWD1247)

Andrews's challenge once more (see EWD1247)

Since I wrote EWD1247, I received several proofs of its theorem - dubbed "Andrews's challenge" by David Gries - in which my case analysis on the emptiness of the range had been avoided. I got two proofs from the Netherlands - one by the ETAC and one by Carel S. Scholten- and one proof from here which had been designed independently by Rajeev Joshi and by Kedar Sharad Namjoshi; it is their proof which is rendered below.

In the following, all quantifications are to be understood to be over the same, possibly empty range. To save some ink, we introduce the following abbreviations for boolean function $t$

$\left( {0a}\right) \;\left\langle {\forall z : t.2}\right\rangle \equiv \left\lbrack t\right\rbrack \;\left( {\text{read} : \text{everywhere}t}\right)$ (0b) $\langle 3 : t,z\rangle \equiv < t >$ (read: "somewhere ").

From predicate calculus we use

$\left( {1a}\right) \;x = y \equiv \left( {\neg x \vee y}\right) \land \left( {x \vee {7y}}\right)$ $\left( {1 + b}\right) + x = y \equiv \left( {x \land y}\right) \vee \left( {{7x} \land {7y}}\right) \quad ,$

the equivalence of the two right-hand sides

(2) ${\left( 7p \vee x\right) }^{ \land }\left( {p \vee y}\right) \equiv \left( {p \land x}\right) \vee \left( {7p \land y}\right) .$

Furthermore we use the mutual distributions between the junctions and the quantifications.

The theorem to be proved is that for any $p$

$$ \langle \exists x: \langle \forall y: p. x \equiv p. y \rangle \rangle \equiv < p > \equiv [ p ] $$

We observe to this end for any $p$

$$ \begin{array}{l} \langle \exists x: \langle \forall y: p. x = p. y \rangle \rangle \ \equiv {(1 a) \mathrm {w i t h} x, y := p. x, p. y } \ \langle \exists x: \langle \forall y: (\neg p. x \vee p. y) \wedge (p. x \vee \neg p. y) \rangle \rangle \ \equiv {\forall o v e r \wedge } \ \langle \exists x: \langle \forall y: \neg p. x \vee p. y \rangle \wedge \langle \forall y: p. x \vee \neg p. y \rangle \rangle \ \equiv {\vee o v e r \forall a n d (0 a), t w i c e } \ \langle \exists x: ((p. x \vee [ p ]) \wedge (p. x \vee [ p ]) \rangle \ \equiv {(2) \mathrm {w i t h} p, x, y := p. x, [ p ], [ 7 p ] } \ \langle \exists x: (p. x \land [ p ]) \lor (\neg p. x \land [ \neg p ]) \rangle \ \equiv {\exists o v e r v } \ \langle \exists x: p. x \wedge [ p ] \rangle \vee \langle \exists x: 7 p \wedge [ 7 p ] \rangle \ \equiv {\wedge \mathrm {o v e r} \exists \mathrm {a n d} (0 b), \mathrm {t w i c e} } \ (< p > \land [ p ]) \lor (< \neg p > \land [ \neg p ]) \ \equiv \left{c l e M o r g a n, t w i c e \right} \ (< p > \land [ p ]) \lor (\neg [ p ] \land \neg < p >) \ \equiv {(1 b) w i t h x, y := < p >, [ p ] } \ \langle p \rangle \equiv [ p ] \ \end{array} $$

which completes the proof.

The longer one looks at this proof, the more satisfactory it becomes. It uses exactly once each of the four ways in which, for unrestricted range, the junctions distribute over the quantifications and vice versa. In the 1st step, (1a) rather than (1b) is chosen so as to enable the distribution of $\forall$ ; in the 4th step, the distribution of $\exists$ is enabled by the use of (2), which links (1a) to (1b), which is used in its own right in the last step; in the 7th step, [ ] and <> are linked -as usual - by the Morgan. Why did not all of us find this proof without any detours?

Austin, 18 October 1996

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