A universal quantification revisited (with C.S.Scholten)

An universal quantification revisited

by C.S.Schoften and Edsger W.Dykgstra

For any bag B and any boolean function $b$ defined on the elements of $B$ we claim (AX: XnB: bx) defined as usual. Our first purpose is to define as a predicate

(0) $\left( {A \times : X\text{ in }B : fX}\right)$

where $f$ is a function from the elements of $B$ to predicates on some space. (If the elements of $B$ are predicates on that same space, $f$ is traditionally known as a predicate transformer.)

A traditional way of defining the predicate (o) is by pointwise definition: in each point of state space the ${f}_{X}$ stand for boolean values for which universal quantification over $B$ is defined. We should like to develop a predicate calculus as far as possible without explicit reference to points of the space; we would like to define it by means of a set of rules for the manipulation of formulae.

We postulate expressions of form (0) to satisfy the following two rules - where a pair of square brackets, if so desired, may be interpreted as universal quantification: over the points of space-

(1) $\left( {{\underline{A}X} : X\underset{\text{ in }}{ = }B : \left\lbrack {fX}\right\rbrack }\right) \equiv \left\lbrack {\left( {{A}^{2}X : X\underset{\text{ in }}{ = }B : fX}\right) }\right\rbrack$ (2) $\left\lbrack {\left( {{\underline{A}X} : X\text{ in }B : Q \vee {fX}}\right) \equiv Q \vee \left( {{\underline{A}X} : X\text{ in }B : fX}\right) }\right\rbrack$ for

any predicate Q .

Note that in the case of a finite bag $B$ ,(1) and (2) are consistent with the interpretation of (0) as the conjunction of ${f}_{X}$ over the elements of $B$ .

For the sake of brevity, the range " $x$ in $B$ " will be omitted in the sequel.

We observe for any $z$

true

\begin{array}{l} = {\mathrm {s u b s t i t u t i o n o f} 7 2 \mathrm {f o r} Q \mathrm {i n} (2) } \ [ (\underline {{A}} X:: ¬ Z \vee f X) \equiv ¬ Z \vee (\underline {{A}} X:: f X) ] \ ⇒ {\mathrm {l e i b n i z ' s} R u l e } \ [ (\underline {{A}} X: ¬ Z \vee f X) ] \equiv [ ¬ Z \vee (\underline {{A}} X: f X) ] \ = {(1) a n d t h e d e f i n i t i o n o f ⇒ } \ (3) (\underline {{A X}}: [ Z ⇒ f X ]) \equiv [ Z ⇒ (\underline {{A X}}: f X) ] \ \end{array}

One of the consequences of (3) is that (0) is the weakest solution of

(4) Z: (\underline {{A}} X:: [ Z ⇒ f X ])

because, firstly, any solution of (4) substituted for $Z$ in (3) reduces its left-hand side to true and, hence, implies (0), and, secondly, (0) substituted for $Z$ in (3) reduces its right-hand side to true and, hence, is a solution of (4).

Consider in addition to $B$ a bag of elements $Y$ and let $g$ be a predicate-valued on the Cartesian product of $B$ and $C$ . For any $Z$

true

\begin{array}{l} = {\mathrm {s u b s t i t u t i o n o f} g X Y \mathrm {f o r} f X \mathrm {i n} (3) } \ (\underline {{\mathrm {A}}} Y: (\underline {{\mathrm {A}}} X: [ Z ⇒ g X Y ]) \equiv [ Z ⇒ (\underline {{\mathrm {A}}} X: g X Y) ]) \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} Y: (\underline {{A}} X:: [ Z ⇒ g X Y ]))) \equiv (\underline {{A}} Y:: [ Z ⇒ (\underline {{A}} X:: g X Y) ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} X: (\underline {{A}} Y: [ Z ⇒ g X Y ]) \equiv (\underline {{A}} Y: [ Z ⇒ (\underline {{A}} X: g X Y ] ]) \ = {(3) } \ (\underline {{A}} X: [ Z ⇒ (\underline {{A}} Y: g X Y) ]) \equiv (\underline {{A}} Y: [ Z ⇒ (\underline {{A}} X: g X Y) ]) \ = {(3) a p p l i e d t o b o t h s i d e s } \ [ Z ⇒ (\underline {{A X}}:: (\underline {{A Y}}:: g X Y)) ] \equiv [ Z ⇒ (\underline {{A Y}}:: (\underline {{A X}}:: g X Y)) ] \ \end{array}

Hence

(5) [ (\underline {{A}} X:: (\underline {{A}} Y:: g X Y)) \equiv (\underline {{A}} Y:: (\underline {{A}} X:: g X Y)) ],

i.e. also when the terms are predicates, the order of universal quantifications is immaterial.

\mathrm {C o r o l l a r y} \varphi (5)

[ (\underline {{A}} X:: f X \wedge g X) \equiv (\underline {{A}} X:: f X) \wedge (\underline {{A}} X:: g X) ]

Note that from this corollary the monotonicity of univer

Slightly shifting notational gears we consider (0) with for $f$ the identity function and for $B$ the bag of solutions of the equation

(6) X: [ g X ]

where $g$ is some predicate transformer, i.e. $X$ and $gX$ are predicates on the same space. For the sake

of reference, the resulting expression is denoted by

$\left\lbrack {Q \equiv \left( {\underline{A}X : \left\lbrack {gX}\right\rbrack : X}\right) }\right\rbrack$

Rewriting (3) we observe for any $z$

(8) $\underset{⏜}{\left( A X : [g X] : [Z ⇒ X]\right) } \equiv \left\lbrack {Z ⇒ Q}\right\rbrack$

with the corollary

(g) (A $X\colon [gX]\colon [Q⇒ X])$

We are now ready to prove

Lemma 0. In terms of (6) and (7) the following three assertions are equivalent

(i) ① is a solution of (6) (ii) $Q$ is the strongest solution of (6) (iii) a strongest solution of (6) exists.

Proof. Formally expressed the assertions are

(i) [gQ] (ii) $\left\lbrack {gQ}\right\rbrack ∧ \left( {A \times \left\lbrack {gX}\right\rbrack : \left\lbrack {Q ⇒ X}\right\rbrack }\right)$ (iii) $\left( {\underline{\underline{\mathbf{E}}}\mathbf{P} : \left\lbrack {\mathbf{g}\mathbf{P}}\right\rbrack : \left( {\underline{\underline{\mathbf{A}}}\mathbf{X} : \left\lbrack {\mathbf{g}\mathbf{X}}\right\rbrack : \left\lbrack {\mathbf{P} ⇒ \mathbf{X}}\right\rbrack }\right) }\right)$

The equivalence $\left( i\right) \equiv \left( {i \cdot i}\right)$ follows immediately from

(g). Further we observe

\begin{array}{l} (c c c) \ = {\mathrm {d e f i n i t i o n o f (i i i) a n d (8) w i t h P f o r 2} } \ (E P: [ g P ]: [ P ⇒ Q ]) \ = {o n a c c o u n t o f (g) } \ (E P: [ g P ]; [ P ⇒ Q ] ∧ [ Q ⇒ P ]) \ \end{array}

EWD844-4

= {\text {p r e d i c a t e c a l c u l u s} }

(E P: [ g P ]: [ P \equiv Q ])

= {\text {p r e d i c a t e c a l c u l u s} }

[ g Q ]

= {\mathrm {d e f i n i t i o n} \varphi (i) }

（）

(End of Proof.)

Remark 0. Note that Lemma 0 holds without any further assumptions about predicate transformer $g$ . (End of Remark 0.)

We mention a special consequence of Lemma 0. In order to prove that (6) has a strongest solution, one shows for instance that $Q$ - the conjunction of all solutions of (6) - is a solution of (6). Sometimes one can prove a somewhat stronger property of $g$ , viz. that the conjunction of any bag of solutions of (6) is again a solution of (6). Such is the case in the following two examples.

Example 0. For monotonic $h$ ,the equation

(1 0) X: [ h X ⇒ X ]

has a strongest solution.

Proof. In view of the above it suffices to show that $\left( {AX : X\text{ in }B : X}\right)$ solves (10) for $B$ any bag of solutions of (10).

true

\begin{array}{l} = {\mathrm {d e f i n i t i o n} o f B } \ (A \stackrel {\prime} {X}: X _ {\mathrm {i n}} B: [ h X ⇒ X ]) \ \end{array}

$⇒ {$ monotonicity of universal quantificati $}$

[ (\underset {\mathrm {A X}} {\backslash} \cdot X _ {\mathrm {i n}} \mathcal {B}: h X) ⇒ (\underset {\mathrm {A X}} {\backslash} \cdot X _ {\mathrm {i n}} \mathcal {B}: X) ]

$⇒$ {monotonicity of $h$ ,see next page}

[ h (\underset {\mathrm {A X : X i n}} {\wedge} \mathcal {B}: \mathcal {X}) ⇒ (\underset {\mathrm {A X : X i n}} {\wedge} \mathcal {B}: \mathcal {X}) ]

(End of Proof.)

(Note that Example 0 states "half" of the Theorem of Knaster-Tarski.)

Example 1. For universally conjunctive $h$ ,the equation

$X : \left\lbrack {P \vee hX}\right\rbrack$

has a strongest solution for any predicate $P$ .

Proof. For any bag $B$ of solutions of (11) we have

t r u e

= {d e f i n i t i o n o B }

(A X: X \underline {{\operatorname {i n}}} B: [ P v h X ])

= {\mathrm {p r e d i c a t e c a l c u l u s} }

[ (\underline {{A}} X: X _ {\mathrm {i n}} B: P \vee h X) ]

= {\mathrm {o n a c c o u n t o f} (2) }

[ P v (A X: X _ {i n} B: h X) ]

= {\mathrm {u n i v e r s a l c o n j u n c t i v i t y} _ {h} }

[ P v h (A X: X _ {i n} B: X ^ {2}) ]

(End of Proof.)

The last transition in the proof of Example 0 relies on

(11) For monotonic $h$ and any $\operatorname{bag} B$ $\left\lbrack {h\left( {{AX} : X\text{ in }B : X}\right) ⇒ \left( {{AX} : X\text{ in }B : hX}\right) }\right\rbrack$

Proof true

\begin{array}{l} \begin{array}{l} {= {(3) \mathrm {w i t h} f \mathrm {t h e i d e n t i t y a n d} (\underline {{A Y : Y _ {\mathrm {i n}} B : Y}}) \mathrm {f o r} Z }} \ {(A X: X _ {\mathrm {i n}} B: [ (A Y: Y _ {\mathrm {i n}} B: Y) ⇒ X ])} \end{array} \ ⇒ {\mathrm {m o n o t o n i c i t y} h } \ (¬ X: X \in B: [ h (¬ Y: Y \in B: Y) ⇒ h X ]) \ = {(3) } \ [ h (\underline {{A}} Y: Y _ {\mathrm {i n}} B: Y) ⇒ (A X: X _ {\mathrm {i n}} B: h X) ] \ = {\mathrm {r e n a m i n g t h e d u m m y} } \ \end{array}

(End of Proof.)

The conclusion we drew from the Corollary of (5), viz. the monotonicity of universal quantification, was a bit rash. The statement of the monotonicity -and in this version we used it in the proof of Example 0 - is

(12) $\left( {{\underline{\mathrm{A}}}{\mathrm{X}} : {\mathrm{X}}{\text{in }}\mathcal{B} : \left\lbrack {{\mathrm{f}}^{\mathrm{X}} ⇒ \mathrm{g}\mathrm{X}}\right\rbrack }\right) ⇒ \left\lbrack {\left( {{\underline{\mathrm{A}}}{\mathrm{X}} : {\mathrm{X}}{\text{in }}\mathcal{B} : {\mathrm{f}}^{\mathrm{X}}}\right) }\right\rbrack ⇒ \left( {{\underline{\mathrm{A}}}{\mathrm{X}} : {\mathrm{X}}{\text{in }}\mathcal{B} : {\mathrm{g}}^{\mathrm{X}}}\right) \rbrack$

For the formal proof of (12) we need an extension of Leibniz's Rule, viz.

(13) $\left( {\underline{A}X : {X}{\text{in}}B : \left\lbrack {{P}^{X} \equiv gX}\right\rbrack }\right) ⇒ \left\lbrack {\left( {\underline{A}X : {X}{\text{in}}B : P}X\right) \equiv \left( {\underline{A}X : {X}_{\text{in}}B : gX}\right) }\right\rbrack$ .

The proof of (12) is then as follows - for the sake

\begin{array}{l} (\underline {{A}} X: [ f X ⇒ g X ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} X: [ f X = f X \wedge g X ]) \ ⇒ {(1 3) } \ [ (\underline {{A X}}: f X) \equiv (\underline {{A X}}: f X \wedge g X) ] \ = {\mathrm {C o r o l l a r y} o f (5) } \ [ (\underline {{A}} X:: f X) \equiv (\underline {{A}} X:: f X) \wedge (\underline {{A}} X:: g X) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A}} X:: f X) ⇒ (\underline {{A}} X:: g X) ] \ (E n d o f P r o o f.) \ \end{array}

26 November 1982

dMrs. C.S. Scholten

ScienriPic Advisor

Philips Research Laboratories

5600JA EINDHOVEN

The Netherlands

prof. dr. Edsger W. Dgkstra

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

The Netherlands