The calculus of boolean structures (Part 1)

Copyright Notice

The following manuscript

EWD 1002: The calculus of boolean structures (Part 1)

is a draft of Chapter 5 (pp. 62-80) of

E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Permission to reproduce the manuscript here has been granted by Springer-Verlag New York.

The calculus of boolean structures (Part 1)

Universal quantification is a generalization of the conjunction. Its format is

(A dummies : range: term)

Here, "dummies" stands for an unordered list of local variables, whose scope is delineated by the outer parenthesis pair. In what follows, x and y will be used to denote dummies; they may be of any understood type. Components "range" and "term" are in general expressions of type "boolean structure"; their potential dependence on the dummies will be indicated explicitly by using a functional notation, i.e. if a range has the form r.x ∧ s.y, it is a conjunction of r.x, which does not depend on y, and s.y, which does not depend on x; similarly, Q would stand for a predicate that depends on none of the dummies. In the following, we shall use r, s, f and g to denote functions from (the types of) the dummies to boolean structures on the implicitly understood space or on the trivial one. (In the latter case, they are just boolean functions.) If range and term are boolean expressions, the whole quantification is a boolean expression, otherwise it is a boolean structure.

For the sake of brevity, the range true will be omitted. The following axiom tells us how ranges different from true can be eliminated

$$ (5 9) \quad [ (\underline {{A}} x: r. x: p. x) \equiv (\underline {{A}} x: r. x \vee p. x) ] $$

(Appeals to this axiom will be given by the catchword "trading", being short for "trading between range and term".)

Disjunction distributes in the same way over universal quantification as it does over conjunction, i.e. we postulate

$$ (6 0) \quad [ Q \vee (\underline {{A}} x: \underline {{f}}. x) \equiv (\underline {{A}} x: Q \vee f. x) ] $$

But now we observe for any $Q,r,p$

$$ \begin{array}{l} Q \vee (A x: r. x: f. x) \ = {\mathrm {t r a d i n g} } \ Q \vee (\neg x: \neg r. x \vee p. x) \ = {(6 0) } \ (\underline {{A}} x: \quad Q \vee \operatorname {I r}. x \vee f. x) \ = {\mathrm {t r a d i n g} } \ (A x: r. x: Q \vee f. x) \ \end{array} $$

Hence we have the more general

$$ (6 1) [ Q \vee (\underline {{A}} x: r. x: f. x) \equiv (\underline {{A}} x: r. x: Q \vee f. x) ] $$

An analogue of conjunctions associativity and symmetry is introduced by postulating

(62) $\left\lbrack {\left( {\underline{A} \times : : {P}{.} \times }\right) \land \left( {\underline{A} \times : : {g}{.} \times }\right) \equiv \left( {\underline{A} \times : : {P}{.} \land {g}{.} \land }\right) }\right\rbrack$

which invites us to observe for any $r,f,g$

$$ \begin{array}{l} (\underline {{A}} x: r. x: p. x) \wedge (\underline {{A}} x: r. x: g. x) \ = {\mathrm {t r a d i n g}, \mathrm {t w i c e} } \ (\underset {\sim} {A} x: \neg r. x \vee f. x) \wedge (\underset {\sim} {A} x: \neg r. x \vee g. x) \ = {(6 2) } \ (\underline {{A}} x: (\neg r. x \vee f. x) \wedge (\neg r. x \vee g. x)) \ = {\mathrm {p r e d . c a l c} } \ (\underline {{A}} x: \neg r. x \vee (f. x \wedge g. x)) \ = {\mathrm {t r a d i n g} } \ (\underline {{A}} x: r. x: \overline {{f}}. x \wedge g. x) \ \end{array} $$

Hence we have the more general

(63) $\left\lbrack {\left( {\underline{A}x}\right) : r.x : f.x}\right) \land \left( {\underline{A}x : r.x : g.x}\right) \equiv$

$$ (\underline {{A}} x: r. x: {p. x \wedge g. x }) ] $$

Formula (61) relates two quantifications with the same range, (63) relates three quantifications with the same range. It is, in fact, not uncommon that all through a longer manipulation a given dummy has always the same range; for brevily's sake, such constant ranges are stated once and for all and subsequently not repeated over and over again. (This opportunity for abbreviation was, in fact, one of the reasons for introducing the notion of the range in the first place.)

This last formula has a partner, in hints referred to as "splitting the range"

(64) $\left\lbrack {\left( {\underline{A}x}\right) : r.x : {P}{1}x}\right) \land \left( {\underline{A}x : s.x : {P}{2}x}\right) \equiv$

$$ (\underline {{A}} x: r. x \vee s. x: f. x) ] $$

Proof We observe for any $r,s,f$

$$ \begin{array}{l} (\underline {{A}} x: r. x: f. x) \wedge (\underline {{A}} x: s. x: p. x) \ = {\mathrm {t r a d i n g}, 4 \mathrm {t i m e s} } \ (\underset {A} {A} x: 7 p. x: 7 r. x) \wedge (\underset {A} {A} x: 7 p. x: 7 s. x) \ = {6 3 \mathrm {w i t h} r, f, g := 7 f, 7 r, 7 s } \ (A x: \neg f. x: \neg r. x \land \neg s. x) \ = {\mathrm {t r a d i n g}, \mathrm {t w i c e} } \ (\underline {{A}} x: \pi (\pi \tau . x \wedge \pi s. x): f _ {x}) \ = {d e M o r g a n } \ (\underline {{A}} x: r. x \vee s. x: f. x) \ \end{array} $$

(End of Proof.)

Another manifestation of associativity and symmetry is the postulate

(65) $\left\lbrack {\left( {\underline{A}x\because \left( {\underline{A}y\because f.x.y}\right) }\right) \equiv \left( {\underline{A}y\because \left( {\underline{A}x\because f.x.y}\right) }\right) }\right\rbrack$ ,

which invites us to observe for any $r,s,p$

$$ \begin{array}{l} (\underline {{A}} x: r. x: (\underline {{A}} y: s. y: f. x. y)) \ = {\mathrm {t r a d i n g}, \mathrm {t w i c e} } \ (\underline {{A}} x: \quad 7. 5 x \vee (\underline {{A}} y: \quad 7. 5 y \vee f. x. y)) \ = {v d i s t r i b u t e s o v e r \bar {A} } \ (\underline {{A}} x: (\underline {{A}} y: 7. 1. x \vee 7. 5. y \vee f. x. y)) \ = {(6 5) } \ \end{array} $$

$$ \begin{array}{l} (\underline {{A}} y: (\underline {{A}} x: \neg r. x \vee \neg s. y \vee f. x. y)) \ = {v d i s t r i b u t e s o v e r A } \ (\underline {{A}} y: \pi s. y \vee (\underline {{A}} x: \pi r. x \vee f. x. y)) \ = {\mathrm {t r a d i n g}, \mathrm {t w i c e} } \ (\underline {{A}} y: s. y: (\underline {{A}} x: r. x: f. x. y) \ \end{array} $$

Hence, we have the more general

(66) $\left\lbrack {\left( {\underline{A}x.\;r.x}\right) : \left( {\underline{A}y.\;s.y}\right) : f.x.y}\right\rbrack \equiv$

$$ (\underline {{A}} y: s. y: (\underline {{A}} x: r. x: f. x. y) ] $$

In hints, these formulae are referenced by "interchange of quantifications". Notice that in (66) each dummy carries with it its own range; hence we don't run into trouble here when we leave ranges unmentioned.

Often we don't care which is the outer and which is the inner quantification. We cater to that by admitting a list of dummies following

(67) $\left\lbrack {\left( {\underline{A}x,y : f.x.y}\right) \equiv \left( {\underline{A}x : \left( {\underline{A}y : f.x.y}\right) }\right) }\right\rbrack$ ,

which admits the analogous generalization

(68) $L\left( {\underline{A}x,y;1.x \land s.y;f. x.y}\right) =$

$$ (\underset {\sim} {A} x: r. x: (\underset {\sim} {A} y: s. y: {\underset {\sim} {p}. x. y)) ] $$

In hints we refer to these transformations by "nesting" or "unnesting". The proof of

(68) is left to the reader.

Finally we mention a special case of interchange of universal quantification

$$ (6 9) \quad [ (\underline {{A}} x: [ r. x ]: f. x) ] \equiv (\underline {{A}} x: [ r. x ]: [ f. x ]) $$

note that in this case, the range is not allowed to be a full-blown boolean structure.

From (61) we derive with $Q :=$ true

$$ (7 0) [ t r u e \equiv (\underline {{A}} x: r. x: t r u e) ] $$

and from that with $r \mathrel{\text{:=}} 7p$ and trading

$$ (7 1) [ t r u e \equiv (\underline {{A}} x: f a l s e: f. x) ] $$

From our formalization of the universal quantification, something is still lacking: all our postulates would be satisfied if each quantification were equivalent to true! This is remedied by the postulation of what is known as the "one-point rule", viz. that we have for any $f$ and $y$

$$ (7 2) \quad [ (\underline {{A}} x: [ x = y ]: f. x) \equiv f. y ] $$

Substituting in the above for $p$ the constant function false,we get

$$ (7 3) \quad (\underline {{A}} x: [ x = y ]: \mathrm {f a l s e}) \equiv \mathrm {f a l s e} $$

Remark An alternative would have been to postulate (73) and then to derive (72). The exercise

is left to the reader. He may also wish to verify that another possibility would have been to postulate

$$ (7 4) \quad (\underset {x:} {A} x: \neg (x \in V)) \equiv V = \phi $$

(End of Remark.)

Next we observe for any $y$

$$ \begin{array}{l} (A x: f. x) \wedge f. y \ = {\mathrm {o n e - p o i n t r u l e} } \ (\underline {{A}} x: \mathbf {p}. x) \wedge (\underline {{A}} x: [ x = y ]: \mathbf {p}. x) \ = {\text {r a n g e s p l i t i n g} } \ (\underline {{A}} x: \mathrm {t r u e} v [ x = y ]: f. x) \ = {p r e d i c a t e c a l c u l u s } \ (\underline {{A}} x: \quad f. x) \ \end{array} $$

Hence we have for any $y$

$$ (7 5) \quad [ (\underline {{A}} x: f. x) \Rightarrow f. y ] $$

and, because of ${\left\lbrack \cdot \right\rbrack }^{\prime }\mathrm{s}$ monotonicity and (69),

$$ (7 6) \quad (\underline {{A}} x: [ f. x ]) \Rightarrow [ f. y ] $$

It is this formula that allows us to identify the phrase "We have, for any $x$ , $[p.x]$ " with "We have $(A x::[p.x])$ ": both allow us to conclude, for any $y$ , that we have $[p.y]$ . From an operational point, the two phrases are equivalent. The reader may generalize (76) into

$$ (7 7) \quad (\underline {{\exists x : [ r . x ]}}: [ p. x ]) \Rightarrow ([ r. y ] \Rightarrow [ p. y ]) $$

We have for any $f,g,h$

(78) $\left( {\underline{A} \times \because \left\lbrack {f.x = g.x}\right\rbrack }\right) \Rightarrow \left\lbrack {\left( {\underline{A} \times \therefore h.\left( {f \cdot x}\right) }\right) \equiv \left( {\underline{A} \times \therefore h.\left( {g \cdot x}\right) }\right) }\right\rbrack$ .

This formula is of importance because it shows how Leibniz's principle can be applied to quanti-

Proof To begin with we observe for any $f, g, h$

(78)

$$ \begin{array}{l} = {(4 4); (5 8) } \ [ (\underline {{A}} x:: [ f. x = g. x ]) \Rightarrow ((\underline {{A}} x:: h. (f. x)) \equiv (\underline {{A}} x:: h. (g. x))) ] \ = {[ X \Rightarrow (Y \equiv Z) \equiv X \land Y \equiv X \land Z ]; (6 2) } \ [ (\underline {{A}} x: [ f. x = g. x ] \land h. (f. x)) \equiv \ (\underline {{\exists}} x: [ p. x = g. x ] \land h. (g. x)) ] \ = {[ [ a = b ] \wedge h. a \equiv [ a = b ] \wedge h. b ] \mathrm {w i t h} a, b := p. x, g. x } \ [ (\underline {{A}} x: [ P. x = g. x ] \land h. (P. x)) \equiv \ (\underline {{\underline {{\theta}}}} x: [ \underline {{\underline {{\phi}}}} x = g. x ] \land h. (\underline {{\underline {{\phi}}}} x)) ] \ = {\mathrm {p r e d . c a l c} } \ f r u e \ \end{array} $$

(End of Proof.)

And now we should be ready to show that universal quantification is monotonic, i.e.

(79) $\left( {\underline{\mathrm{A}}\mathrm{x} : \left\lbrack {\mathrm{f}.\mathrm{x} \Rightarrow \mathrm{g}.\mathrm{x}}\right\rbrack }\right) \Rightarrow \left\lbrack {\left( {\underline{\mathrm{A}}\mathrm{x} : \mathrm{f}.\mathrm{x}}\right) \Rightarrow \left( {\underline{\mathrm{A}}\mathrm{x} : \mathrm{g}.\mathrm{x}}\right) }\right\rbrack$

Proof We observe for any $f, g$

$$ \begin{array}{l} [ (\underline {{A}} x:: \mathbf {p}. x) \Rightarrow (\underline {{A}} x:: \mathbf {g}. x) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{A}} x: p. x) \wedge (\underline {{A}} x: g. x) \equiv (\underline {{A}} x: p. x) ] \ = {(6 2) } \ \end{array} $$

$$ [ (\underline {{A}} x: {p. x \wedge g. x) \equiv (\underline {{B}} x: p. x) ] $$

$$ \Leftrightarrow {(\gamma_ {8}) } $$

$$ (\underline {{\underline {{A}}}} x: [ f. x \wedge g. x = f. x ]) $$

$$ = {\text {p r e d . c a l c .} } $$

$$ (\underline {{A}} x: [ f. x \Rightarrow g. x ]) $$

(End of Proof.)

An important manipulation relies on

(80) for any invertible function $f$

$$ [ (\underline {{A}} x: r. x: p. x) \equiv (\underline {{B}} y: r. (t. y): p. (t. y)) ] $$

In hints, we refer to this manipulation as "trans- Forming the dummy"; in the special case that t is the identity function, "renaming the dummy" is the usual hint.

We prove (80) by mutual implication from the fact that we have for any -not necessarily invertible - t

(81) $\left\lbrack {\left( {\underline{A}x}\right) : r.x : f.x}\right) \Rightarrow \left( {\underline{A}y : r.\left( {t.y}\right) : f.\left( {t.y}\right) }\right) \rbrack$

which we shall prove subsequently. Using trading we see that it suffices to prove these formulae with the range true

Proof of (80) We prove (80) by mutual implication. In the one direction the implication is stated by

(81). For the implication in the other direction, we observe for any $\beta$ and invertible $t$

$$ \begin{array}{l} (\underline {{A}} y: f. (t. y)) \ \Rightarrow {(\theta 1) \mathrm {w i t h} x, y, f, t := y, x, f _ {0} + t ^ {- 1} } \ (\underline {{A}} x: f. (f. (f ^ {- 1} x))) \ = {\mathrm {t o t} ^ {- 1} i s \mathrm {t h e i d e n t i t y f u n c t i o n} } \ (\underline {{A}} x: \rho . x) \ \end{array} $$

(End of Proof of (80).)

Proof of (81) We observe for any $f, t$

$$ \begin{array}{l} [ (\underline {{A}} x:: f. x) \Rightarrow (\underline {{A}} y:: f. (f. y)) ] \ = {\forall Q \Rightarrow \forall d i s t r i b u t e s o v e r A } \ [ (\underline {{A}} y: (\underline {{B}} x: f. x) \Rightarrow f. (t. y)) ] \ = {(7 5) \mathrm {w i t h} y := t. y } \ [ (\exists y: \quad t r u e) ] \ = {(\gamma_ {0}) } \ \end{array} $$

true

(End of Proof of (81).)

We close our discussion of the universal quantification with two monotonicity theorems.

We have for any monotonic predicate transformer

$$ (8 2) \quad [ f. (\underline {{A}} X: X \in V: X) \Rightarrow (\underline {{A}} X: X \in V: f. X) ] $$

Proof We observe for any monotonic $F$ and any $V$ , the range $X \in V$ being understood

$$ \begin{array}{l} [ f. (\underline {{\partial}} X:: X) \Rightarrow (\underline {{\partial}} X:: f. X) ] \ = {^ {\prime \prime} Q \Rightarrow^ {\prime \prime} d i s t r i b u t e s o v e r \underline {{A}} } [ (\underline {{A}} X:: f. (\underline {{A}} X:: X) \Rightarrow f. X) ] \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ (\underline {{A}} X:: [ f. (\underline {{A}} \overline {{X}}:: X) \Rightarrow f. X ]) \ \Leftrightarrow {f _ {i s m o n o t o n i c}; s o i s A } \ (\neg X:: [ (\neg X:: X) \Rightarrow X ]) \ = {(7 5); (7 0) } \ t r u e \ \end{array} $$

(End of Proof.)

For an $f$ with a natural argument "the p.i. form a strengthening sequence" means

$$ (\underline {{A}} i, j: 0 \leqslant i < j: [ f. i \Leftarrow f. j ]) $$

For $f$ and $g$ such that the $f.i$ and $g.j$ form strengthening sequences, we have

$\left\lbrack {\left( {\underline{A}}{i} : 0 \leq i : {f}{i}}\right) \vee \left( {\underline{A}}{j} : 0 \leq j : {g}{j}}\right) }\right\rbrack \equiv$

$$ (\exists i: 0 \leq i: {i \vee g _ {i} ^ {2} }) $$

Proof To begin with we observe for any $f$ and $g$

$$ \begin{array}{l} (\underline {{A}} i: 0 \leq i: f _ {i}) \vee (\underline {{A}} j: 0 \leq j: g _ {j}) \ = {v d i s t r i b u t e s o v e r A } \ (\underline {{A}} i: 0 \leq i: f. i \vee (\underline {{A}} j: 0 \leq j: g. j)) \ = {v d i s t r i b u t e s o v e r A } \ (\underline {{A}} i: 0 \leq i: (\underline {{A}} j: 0 \leq j: f _ {i} \vee g _ {j})) \ = {\mathrm {u n n e s t i n g} } \ (\exists i, j: 0 \leq i \land 0 \leq j: f. i \vee g. j) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} i, j: 0 \leq i \leq j v 0 \leq j \leq i: f _ {i} v g. j) \ = {\text {s p l i t i n g t h e r a n g e} } \ (\underline {{A}} i, j: 0 \leq i \leq j: f _ {i} \vee g, j) \wedge (\underline {{A}} i, j: 0 \leq j \leq i: f _ {i} \vee g, j) \ \end{array} $$

Focussing our attention on the left conjunct we observe

left conjunct above

$= {$ predicate calculus $}$

$$ (\underline {{A}} i, j: 0 \leq i \leq j \land 0 \leq j: f _ {i} \vee g. j) $$

$=$ [nesting the quantrificati ${n}_{2}$

$$ (\underline {{A}} j: 0 \leq j: (\underline {{A}} i: 0 \leq i \leq j: f. i \vee g. j)) $$

$= { v$ distributes over $A}$

$$ (A _ {j}: 0 \leq j: (A _ {i}: 0 \leq i \leq j: f _ {i}) \vee g _ {j}) $$

$= { f$ strengtthening $}$

$$ (\underline {{A}} j: 0 \leq j: f _ {j} \vee g _ {j}) $$

For reasons of symmetry, the other conjunct has the same value, which combined observations -the conjunction being idempotent - conclude the proof. (End of Proof)

(End of Proof.)

Existential quantification is the generalization of the disjunction and can now be defined by the analogue of de Morgan's Law:

$$ (8 4) [ (\underline {{E}} x: r. x: f. x) \equiv \neg (\underline {{A}} x: r. x: \neg f. x) ] $$

If has all the properties you would expect it to have. The derivation of the formulae that are the dual of the ones we gave for universal quanti. fication is left to the reader.

Austin, 1 March 1987

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