A short sequel to EWD842

I think I have now found a formulation of the required generalization of Leibniz's Rule. As it stood it described how a new formula may be generated "in the presence of $P \equiv R$ ".

The generalization describes how a new formula may be generated "in the presence of $A \lor B$ ",es- sentially by interpreting the presence of $A \lor B$ as the presence of at least 1 from the bag ${A,B}$ .

If $F$ may be generated (presumably in the presence of $A$ but) without using $B$ and $F$ may be generated (presumably in the presence of $B$ but) without using $A$ , then $F$ may be generated in the presence of $A \lor B$ .

In particular - but this is only a special case-: if $G$ may be generated using $A$ but not $B$ , whereas we don't succeed generating $G$ using $B$ but not $A$ , we can form a formula $F$ that satisfies the second requirement as well, by choosing for $F$ the formula $B \vee G$ .

Note. In EWD842 -and I remember that I hesi- tated when I did so!- I defined the disjunction v (and consequently the conjunction A) only on bags containing at least 2 operands . The proper extension is of course to define the dis- junction (and the consequently the conjunction) of a bag of 1 operand as that operand, (and to define the disjunction of the empty bag in view of Theorem 5 as 7black , and its conjunction as black). The equivalence on a bag of 1 operand should be defined as that operand, The equivalence on an empty bag should, in view of Theorem o be defined as black

Leibniz's Rule in the presence of an equivalence is now recursively defined according to the syn-

\begin{array}{l} < \mathrm {e q u i v a l e n c e} >: = < \mathrm {d i s j u n c t i o n} > {\equiv < \mathrm {d i s j u n c t i o n} > } ^ {} \ < \mathrm {d i s j u n c t i o n} > := < \mathrm {t e r m} > {V < \mathrm {t e r m} > } ^ {m} \ < \mathrm {f e r m} > := {7 } ^ {} < \mathrm {p r i m a r y} > \ < \mathrm {p r i m a r y} > := < \mathrm {p r e d i c a t e v a r i a b l e} > \ \end{array}

Remark At least the associativity of could have been expressed syntactically by

\begin{array}{r l} {\langle \mathrm {e q u i v a l e n c e} \rangle} & {:= \langle \mathrm {d i s j u n c t i o n} \rangle} \ & {| \langle \mathrm {e q u i v a l e n c e} \rangle \equiv \langle \mathrm {e q u i v a l e n c e} \rangle ,} \end{array}

etc.(End of Remark.)

(End of Note.)

Note that we did not interpret the presence of $A \lor B$ as a promise that eventually at least 1 formula from the bag ${A,B}$ can be generated! In a common application, $A \lor B$ takes the form - which we can generate in view of Theorem 2 for any $A -$ ,and the rejected interpretation would exclude the existence of undecidable formulae - i.e. formulae $A$ such that neither $A$ nor $?A$ can be generated - .

The above use of the presence of $A \lor ¬ A$ in the case of undecidable $A$ does not bother me at all. In that case we can add either $A$ or $¬ A$ to our set of Axioms, thus creating two different systems. Our usage of $A \lor ¬ A$ genera- ates what those two systems have in common. So I prefer not to be bothered; undoubtedly I am very naive, but I definitely prefer to remain so as long as possible.

Plataanstraat 5 5671 AL NUENEN The Netherlands

25 October 1982 prof. dr. Edsger W. Dgkstra Burroughs Research Fellow