(E y :: (A x :: p . x . y )) ⇒ (A x :: (E y :: p . x . y ))

$$ (E y: (A x: p. x. y)) \Rightarrow (A x: (E y: p. x. y)) $$

The other day, while reading Tarshi's article at the ATAC, we encountered the above theorem and wondered for a while how to prove it. We did not see it immediately and went on. The purpose of this note is not to prove it - though we shall do so as we go along - but to show - once more! - that in designing that proof, "there is only one thing we can do".

Since, in isolation, neither antecedent nor consequent presents an invitation to manipulation, we start with the whole theorem, renaming the dummies at one side (for safety's sake)

$$ (E _ {y}: (A x: p. x. y)) \Rightarrow (\underline {{A}} h: (E k: p. h. k)) $$

= [rewrite the implication in disjunctive form; this (i) for my convenience, as I dislike the (quasi) distributions of the implication, and (ii) I like to see that disjunction as we have to explain a difference between existential and universal quantification]

$$ (\underline {{A}} y: (\underline {{E}} x: \neg p. x. y)) \vee (\underline {{A}} h: (\underline {{E}} k: p. h. k)) $$

this is nicely symmetric! Fortunately v distributes over A; in order not destroy the symmetry, we distribute about both

$$ (\underline {{A}} y, h: (\underline {{E}} x: - p. x y) \vee (\underline {{E}} k: p. h. k)) $$

[\left{ \begin{array}{l} \text{ now we should head for the excluded middle, } \ \text{ which we can do via proper (inverse) instantiation. } \end{array}\right. ]

$$ \begin{array}{l} (\underline {{A}} y, h: \neg p. h. y \vee p. h. y) \ = \left{ \begin{array}{l l} \text {e x c l u d e d m i d d l e} \ \text {t r u e} \end{array} \right. \ \end{array} $$

The theorem is, of course, very simple; almost too simple to devote an EWD to. The point is that, if the theorem is really so simple, we should know how to design without hesitation a proof for it. And that is precisely what we did.

The little experience was just satisfactory enough to be recorded.

Austin, 3 September 1986

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