Guided by necessity

Guided by necessity

It is our purpose to prove for a non-empty set $W$ of predicates

(0) $\left[(\underline{A} X: X \in W: X) \Rightarrow (\underline{E} Y: Y \in W: Y)\right]$

The restriction to non-empty $W$ is essential, for with $W := \varnothing$ , (0) reduces to [true $\Rightarrow$ false], which is false. Our demonstration of (0) therefore has to use the fact that $W$ is non-empty, more precisely, has to contain a valid step that would be invalid for empty $W$ . Well-known steps only valid for non-empty $W$ are the restricted distributions

$\left\lbrack {Q \land \left( {{A}^{x} : X \in W : X}\right) \equiv \left( {{A}^{x} : X \in W : Q \land X}\right) }\right\rbrack$ (2) $\left\lbrack {Q \vee \left( {{EY} : Y \in W : Y}\right) \equiv \left( {{EY} : Y \in W : Q \vee Y}\right) }\right\rbrack$ ,

and we propose to use (at least) one of the above two to demonstrate (0) in the form

(3) $\left\lbrack {\left( {{AX} : X \in W : X}\right) \vee \left( {{EY} : Y \in W : Y}\right) \equiv \left( {{EY} : {Y \in W} : Y}\right) }\right\rbrack$ .

To this end we observe for any non-empty $W$

$$ (\underset {X \in W: X} {\mathrm {A X}}) \vee (\underset {Y \in W: Y} {\mathrm {E Y}}) $$

$$ \begin{array}{l} = {2) \mathrm {w i t h} Q := (\underline {{A}} X: X \in W: X) \mathrm {a n d} W \mathrm {n o n - e m p l y} } \ (E Y: Y \in W: (A X: X \in W: X) \vee Y) \ = {\text {i n s t a n t i a t i o n} } \ (E Y: Y \in W: Y) \ \end{array} $$

The above proof is correct, but there is a little bit more to it. When we rewrite (1) and (2) as mutual implications we see that in both cases one of the two implications also holds for empty $W$ , and our proof has to use one of the others: for non-empty $W$

(A) $\left\lbrack {Q \land \left( {\underline{A}X : X \in W : X}\right) \Leftrightarrow \left( {\underline{A}X : X \in W : Q \land X}\right) }\right\rbrack$ (5) $\left\lbrack {Q \vee \left( {{EY} : Y \in W : Y}\right) \Rightarrow \left( {{EY} : Y \in W : Q \vee Y}\right) }\right\rbrack$

We have to use one of these, for (4) and (5) are the ones that are invalid for empty $W$ .

This immediately raises the question of whether our proof of (3) -phrased in terms of equivalences - can be viewed as a strengthening chain or a weakening one. Our demonstrandum

(3) is of the form $\left\lbrack {{P}^{v}Q \equiv Q}\right\rbrack$ ; since

$\left\lbrack {{PvQ} \Leftarrow Q}\right\rbrack$ follows from predicate calculus,our obligation is to show $\left\lbrack {{PvQ} \Rightarrow Q}\right\rbrack$ . Since

our proof of (3) starts at the left-hand side, it is therefore "really" a weakening chain. But that tells us that we can use (4) only to take $\mathbf{a} \cdot \mathbf{Q}$ outside a universal quantifica-

tion , and (5) only to bring a Q inside an existential one. And, indeed, the latter "weaken. ing" step is in essence the first step of our proof of (3).

There was something remarkable going on in the above. Under the condition $\tau \left( {W = \phi }\right)$ ,our proof obligation was of the form

(6)

$$ [ P \Rightarrow Q ] $$

we rewrite that as $\left\lbrack {{P}_{v}Q \equiv Q}\right\rbrack$ to eliminate the implication, and immediately reintroduced it again by writing our proof obligation as

(7)

$$ [ P \vee Q \Rightarrow Q ] $$

Since in the transition from (6) to (7) we have weakened the antecedent, it looks as if we have formally made things harder, but this is not the case: from a weakening chain from P to Q, we can construct a weakening chain from PvQ to QvQ and, thanks to the idempotence of v, also one from PvQ to Q. What the transition from (6) to (7) bought us, is that with (7) we have a clearly "more complicated side" to start with, which gives us more manipulative opportunities and hints.

(The alternative is to rewrite (6) as

(3)

$$ [ P \land Q \Leftarrow P ] $$

and to transform $P \land Q$ via a strengthening chain into $P$ .)

I do not exclude that on closer scrutiny we decide that the use of $\Rightarrow$ and $\Leftarrow$ in the data (4) and (5) and in the demonstrada (7) and (8) are to be considered as a misuse of notation. We could conclude that what we really would like to have is some sort of directed equivalence, say an equivalence between terms such that the implication in the one direction is a tautology.

Austin, 25 March 1991

Prof. Dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188

USA