On partitioning predicates

On partitioning predicates

Let the predicates $\mathrm{{Bi}}$ satisfy

(0)

$$ [ (\text {E} _ {i}: B _ {i}) ] $$

and

(1)

$$ [ (\neg A _ {i, j}: i \neq j: \neg B _ {i} \vee \neg B _ {j}) ] $$

Such a set of predicates is called "a set of parti

Let functions $c$ and $d$ be defined by

(2) $\left\lbrack {cR \equiv \left( {\underline{A}i : 7\mathrm{{Bi}} \vee \mathrm{{Ri}}}\right) }\right\rbrack$ for any $R$ (3) $\left\lbrack {dR \equiv \left( {{E}{i} : {B}{i} \land {R}_{i}}\right) }\right\rbrack$ for any $R$

For partitioning predicates $B$ i we then have

(5) $\left\lbrack {c\mathcal{R} \equiv d\mathcal{R}}\right\rbrack$

which is an immediate consequence of

(6) $\left\lbrack {\left( {{E}{i} : {B}{i}}\right) }\right\rbrack \equiv \left\lbrack {{c}{R} \Rightarrow {d}{R}}\right\rbrack$ ,and (7) $\left\lbrack {\left( {{A}{i},j : i \neq j : i \in {B}{i} \vee i \in {B}_{j}}\right) }\right\rbrack \Rightarrow \left\lbrack {{dR} \Rightarrow {cR}}\right\rbrack$

Proof of (6)

$$ \begin{array}{l} [ (E _ {i}: B _ {i}) ] \ = {\text {p r e d . c a l c .} } \ [ (\operatorname {E i}:: (\operatorname {B i} \land \neg R _ {i}) \lor (\operatorname {B i} \land R _ {i})) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\exists i: B _ {i} \land \neg R _ {i}) \lor (\exists i: B _ {i} \land R _ {i}) ] \ = {\mathrm {p r e d . c a l c .} } \ \end{array} $$

$$ \begin{array}{l} [ (\underline {{A}} i: \neg B i \vee R i) \Rightarrow (E i: B i \wedge R i) ] \ = {(2) a n d (3) } \ [ c R \Rightarrow d R ] \ \end{array} $$

(End of Proof $\Rightarrow P\left( 6\right) .$ )

$$ \begin{array}{l} [ (\underline {{A}} i: \neg B i \vee R i) \Rightarrow (E i: B i \wedge R i) ] \ = {(2) a n d (3) } \ [ c R \Rightarrow d R ] \ P r o o f o f (7) \ [ (\underline {{A}} i, j: i \neq j: \neg B i \vee \neg B j) ] \ \Rightarrow {\mathrm {p r e d . c a l c} } \ [ (\underline {{A}} i, j: i \neq j: (\neg B i \vee \neg R i) \vee (\neg B j \vee R j)) ] \ = {\mathrm {p r e d . c a l c . : t h e a d d e d c o n j u n c t i s t h r u e} } \ [ (\underline {{A}} i, j: i \neq j: (\neg B i \vee \neg R i) \vee (\neg B j \vee R j)) \wedge \ (\underline {{A}} i, j: i = j: (\neg B i \vee \neg R _ {i}) \vee (\neg B j \vee R _ {j})) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{A}} i, j: ((\neg B i \vee \neg R i) \vee (\neg B j \vee R j)) ] \ = {\mathrm {d i s j u n c t i o n d i s t r i b u t e s o v e r u n i v e r s o l q u a n t i f i c a t i o n} } \ [ (\underline {{A}} i: \neg B i \vee \neg R i) \vee (\underline {{A}} j: \neg B j \vee R j) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{E}} i: B i \land R i) \Rightarrow (\underline {{A}} j: \neg B j \lor R j) ] \ = {(2) a n d (3) } \ [ d R \Rightarrow c R ] \ \end{array} $$

(End of Proof of (7).)

$$ \begin{array}{l} \begin{array}{l l} \mathrm {N e x t} & \mathrm {w e o b s e r v e} \end{array} \ \mathbf {f r u e} \ = {(5) } \ [ \neg c R \equiv \neg d R ] \ = {(3) } \ [ \neg c R \equiv \neg (E _ {i}: B _ {i} \land R _ {i}) ] \ = {\mathrm {p r e d . c a l c .} } \ [ \neg c R \equiv (\neg A i: \neg B i \vee \neg R i) ] \ = {(2) } \ \end{array} $$

(8) $\left\lbrack {\neg cR \equiv c\left( {\neg R}\right) }\right\rbrack$

$$ \begin{array}{l} t r u e \ = {(2) } \ [ c (P \wedge R) \equiv (\mathrm {A i} \dots \neg B \vdots v (P _ {i} \wedge R _ {i})) ] \ = {\mathrm {p r e d . c a l c} } \ [ c (P \land R) \equiv (\neg A i: (\neg B i \lor P _ {i}) \land (\neg B i \lor R _ {i})) ] \ = {p r e d, c a l c. } \ [ c (P \wedge R) \equiv (\underline {{A}} i: \neg B i v P _ {i}) \wedge (\underline {{A}} i: \neg B i v R _ {i}) ] \ = {(2) } \ \end{array} $$

(9) $\left\lbrack {c\left( {{P}^{ \land }R}\right) \equiv c{P}^{ \land }{C}^{ \land }R}\right\rbrack$

and similarly

(10) $\left\lbrack {d\left( {{P}^{v}R}\right) \equiv dP \vee {dR}}\right\rbrack$

From (5), (8), (9), and (10) we conclude that the function given by $c$ (or $d$ ) distributes over the logical connectives (as it should). So much on partitioning predicates.

Plataanstraa 5

5671 AL NUENEN

The Netherlands

23 July 1984

prof. dr. Edsger W. Dijkstra

Burroughs Research Fellow