Triggered by Wim Feijen’s treatment of “Exists Forall ⇒ Forall Exists”

Triggered by Wim Feijen's treatment of "exists $\Rightarrow \forall \exists$ "

In WF189, WHJ Feijen presents totally convincing heuristics for the derivation of Carroll Morgan's proofs of the well-known theorem from the predicate calculus

(0) $\left\lbrack {\langle \exists x : \langle \forall y : t.x.y\rangle \rangle \Rightarrow \langle \forall y : \langle \exists x : t.x.y\rangle \rangle }\right\rbrack$ .

These proofs use the laws of the Quantified. Constant - Wim Feijen regretted their anonymity, here is my suggestion for a name

(1a) $\left\lbrack {Q \Rightarrow \langle \forall z : Q\rangle }\right\rbrack$ for fresh z (1b) $\left\lbrack {Q \Leftrightarrow \langle {\exists z. : Q}\rangle }\right\rbrack$ and any range ,

and the laws of Instantiation, which are so well known that I won't write them down (now).

Reduced to its bare essentials, Carroll Morgan's proof is as follows

$$ \begin{array}{r l} & {\langle \exists x:: \langle \forall y:: t. x. y \rangle \rangle} \ {\Rightarrow} & {{\mathrm {Q u a n t i f i e d C o n s t a n t} }} \ & {\langle \forall y ^ {\prime}: \langle \exists x:: \langle \forall y:: t. x. y \rangle \rangle \rangle} \ {\Rightarrow} & {{\mathrm {I n s t a n t i a t i o n} y := y ^ {\prime} }} \ & {\langle \forall y ^ {\prime}: \langle \exists x:: t. x. y ^ {\prime} \rangle \rangle .} \end{array} $$

But, perhaps, this proof has been reduced a little bit too much, for we really did as if the unmentioned ranges were true, but

in its full glory, the theorem to be proved is

(2) $\left\lbrack {\langle \exists x : R.x : \langle \forall y : S.y : t.x.y\rangle }\right\rangle \Rightarrow$

$$ \langle \forall y: S. y: \langle \exists x: R. x: t. x. y \rangle \rangle ] $$

and the Laws of Instantiation which I now

give, are , when we include the ranges. (for instance)

(3a) $\left\lbrack {r.y \land \left\langle {\forall z : r.z : f.z}\right\rangle \Rightarrow {f}{.}y}\right\rbrack$ (3b) $\left\lbrack {f.y \Rightarrow \left( {{r}{.}y \Rightarrow \left\langle {\exists z : r.}z : f.{}_{z}\rangle }\right) }\right\rbrack$

For Carroll Morgan's proof, with ranges included, I suggest the following text:

$$ \langle \exists x: R. x: \langle \forall y: S. y: t. x. y \rangle \rangle $$

$\Rightarrow$ {Quantified Constant}

$$ \langle \forall y ^ {\prime}: S. y ^ {\prime}: \langle \exists x: R. x: \langle \forall y: S. y: t. x. y \rangle \rangle \rangle $$

$= \left{ {\text{Range Diffusion,see below}}\right}$

$$ \langle \forall y ^ {\prime}: S. y ^ {\prime}: \langle \exists x: R. x: S. y ^ {\prime} \land \langle \forall y: S. y: t. x. y \rangle \rangle \rangle $$

$\Rightarrow$ {Instantiation} $y \mathrel{\text{:=}} {y}^{\prime },$ according ${H}_{0}\left( {3a}\right) \rbrack$

$$ \langle \forall y ^ {\prime}: S, y ^ {\prime}: \langle \exists x: R, x: T, x, y ^ {\prime} \rangle \rangle $$

We observe for any punctual $f$ and predicates $Q,X,Y$

$$ \begin{array}{l} [ Q \wedge f. X \equiv Q \wedge f. Y ] \ = {\text {p r e d . c a l c .} } \ [ Q \Rightarrow f. X = Q \Rightarrow f. Y ] \ = {\text {p r e d . c a l c} } \ [ Q \Rightarrow (f. X \equiv f. Y) ] \ \end{array} $$

$$ \begin{array}{l} \Leftrightarrow \quad {f \mathrm {i s p u n c t u a l} } \ [ Q \Rightarrow (X \equiv Y) ] \ \Leftrightarrow \quad {\mathrm {p r e d . c a l c} } \ [ Y \equiv Q \land X ] \lor [ Y \equiv Q \Rightarrow X ] \ \end{array} $$

Eliminating $Y$ from the lines marked with a bullet,we conclude for punctual $f$

$$ \begin{array}{l} (4 a) [ Q \wedge f. X \equiv Q \wedge f. (Q \wedge X) ] \ (4 b) [ Q \wedge f. X \equiv Q \wedge f. (Q \Rightarrow X) ] \ (4 c) \quad [ Q \Rightarrow f. X \equiv Q \Rightarrow f. (Q \land X) ] \ (4 d) \quad [ Q \Rightarrow f. X \equiv Q \Rightarrow f. (Q \Rightarrow X) ] \ \end{array} $$

Note that the prefix $Q \land$ creates a predicate that depends monotonically on $Q$ , whereas $Q \Rightarrow$ creates antimonotonic dependence.

A consequence of (4) and trading- is that the value of a universal or an existential quantification remains unchanged if we select a subexpression on which the term depends punctually and strengthen that subexpression by the prefix "range" or weaken it by the prefix "range". This property is referred to by "Range diffusion".

In its applications it is, of course, useful to know that predicates built from $7, 7, \land, \Rightarrow$ , $\Leftarrow$ , $\equiv$ , $\neq$ , $\forall$ , $\exists$ depend punctually on their

subexpressions (but since this has to be proved by induction over the syntax, I am afraid that Gries and Schneider would call this a metatheorem).

When we have integer dummies i, with associated ranges osi and osj , we usually dont manipulate those ranges: we replace the ranges by (an invisible) true and declare the dummies to be of type natural number and allow this type information to diffuse all through their scope. That's how we do it.

Austin, 27 February 1995

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