Beware of the empty range

Beware of the empty range

Recently David Gries drew my attention to the problem of proving

(0) $\langle \exists x : \langle \forall y : p.x \equiv p.y \rangle \rangle \equiv \langle \exists x : p.x \rangle \equiv \langle \forall y : p.y\rangle$ , in which all quantifications are understood to be over the same range. As soon as I had seen the problem, I put David's text away and tackled the problem myself. In doing so I had a surprise; hence this little note.

￥

My surprise was, that I had to introduce a case analysis, as soon as I had decided to prove (0) by demonstrating (1) and (2):

(1) $\left\langle {\exists x : \left\langle {\forall y : p.x \equiv p.y}\right\rangle }\right\rangle \equiv \left\langle {\forall x,y : p.x \equiv p.y}\right\rangle$ (2) $\langle \exists x : p.x\rangle \equiv \left\langle {\forall y : p.y}\right\rangle \equiv \left\langle {\forall x,y : p.x}\right. \equiv {p.y} >$

while, because false $\equiv$ false $\equiv$ true,(0) definitely holds for empty ranges, (1) and (2) are false for empty ranges! So now we know that in the proofs of (1) and (2) the non-emptiness of the ranges has to be used. We use (half of) the

Lemma. For any $q$ and quantifications over the same range

(3) $\langle \exists z\therefore q.z\rangle \Leftrightarrow \langle \forall z\therefore q.z\rangle$ for non-empty range (4) $\langle \exists z : q.z\rangle \Rightarrow \langle \forall z : q.z\rangle$ for empty range

Proof of (3) We observe for any $q$ and non

$$ \langle \forall z:: q. z \rangle \Rightarrow \langle \exists z:: q. z \rangle $$

[\left{ \begin{array}{l} \text{predicate calculus; de Morgan} \end{array}\right} ]

$$ \langle \exists z:: 7 q. z \rangle \vee \langle \exists z:: q. z \rangle $$

[\left{ \begin{array}{l} \text{ combining terms } \ \end{array}\right} ]

$$ \langle \exists z: 7 q. z \vee q. z \rangle $$

$\left{ \begin{array}{ll} \text{ excluded middle } \ \end{array}\right}$

$$ \langle \exists z::: t r u e \rangle $$

[\left{ \begin{array}{ll} \text{ range non-empty } \ \end{array}\right} ]

$$ t r u e. $$

(End of Proof of (3).)

Proof of (1) We observe for any $p$ and non-empty ranges

$$ \langle \exists x:: \langle \forall y:: p. x \equiv p. y \rangle \rangle $$

$\equiv \;\left{ {\land \text{idempotent};\text{renamng the dummies}}\right}$

$$ \langle \exists z: \langle \forall y: p. z \equiv p. y \rangle \land \langle \forall x: p. z \equiv p. x \rangle \rangle $$

[\left{ {\text{ ranges }x,y,z\text{ the same }}\right} ]

$$ \langle \exists z: \langle \forall x, y: (p. z \equiv p. y) \land (p. z \equiv p. x) \rangle \rangle $$

$\Rightarrow$ {leibniz; quantifications are monotonic}

$$ \langle \exists z: \langle \forall x, y: p. x \equiv p. y \rangle \rangle $$

$\Rightarrow$ {quahshiftconstant}

$$ \langle \forall x, y: p. x \equiv p. y \rangle $$

$\equiv { {unnesting}}$

$$ \langle \forall x: \langle \forall y: p. x \equiv p. y \rangle $$

[\left{ \begin{array}{ll} \text{ range }x & \text{ non-empty,}\left( 3\right) } \end{array}\right. ]

$$ \langle \exists x: \langle \forall y: p. x \equiv p. y \rangle \rangle $$

First line, the line marked (*) and the last line prove for non-empty ranges (1) by mutual implication.

$$ (E n d o f P r o o f (1).) $$

Proof of (2) We observe for any $p$ and non-empty ranges

[\left{ \begin{array}{l} \text{ mutual implication, }; \text{ range non-empty, }\left( 3\right) } \ \end{array}\right. ]

$\left{ \begin{array}{l} \text{predicate calculus } \ \ \left\langle {\forall x,y : p \cdot x \Rightarrow p \cdot y}\right\rangle \end{array}\right.$

$\equiv \;\left{ {\land \text{idempotent};\text{renamng the dummies}}\right}$

$$ \begin{array}{l} \langle \exists x: p. x \rangle \equiv \langle \forall y: p. y \rangle \ \langle \exists x: p. x \rangle \Rightarrow \langle \forall y: p. y \rangle \ \end{array} $$

$$ \langle \forall x, y: p. x \Rightarrow p. y \rangle \land \langle \forall x, y: p. y \Rightarrow p. x \rangle $$

$\left{ \begin{array}{l} \text{ combining the terms; mutual implication } \ \ \left\langle {\forall x,y : p.x \equiv {p.y}}\right\rangle \end{array}\right}$

and thus (2) has been proved for non-empty

ranges.

(End of Proof of (2).)

Austin, 30 September 1996

prof. dr Edsger W. Dykgstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA