Monotonicity and quantification

Monotonicity and quantification

Predicate transformer $f$ is monotonic means

[ X ⇒ Y ] ⇒ [ f X ⇒ f Y ]

Let Xi and Yi stand for predicates on some space S for any i from a domain D . Then Xi and Yi define two predicates X and Y respec-tively on the Cartesian product S x D , according

[ \tilde {X} (I / i) \equiv X I ] f o r a l l I \mathrm {i n} D.

(Here, the square brackets denote universal quanti. fication over $S_{j}$ $\tilde{X} (I / i)$ denotes $\tilde{\chi}$ with I substituted for i, the formal definition of which is given by

In this notation $\left\lbrack {\widetilde{X} ⇒ \widetilde{Y}}\right\rbrack$ is defined by

[ \tilde {X} ⇒ \tilde {Y} ] = (\underline {{A}} i: i \underline {{i n}} D: [ X i ⇒ Y _ {i} ])

(According to our habits and conventions, the square brackets in the left-hand side are over S x D, those in the right-hand side over S.)

We draw attention to the fact that universal quantification and existential quantification are monotonic, i.e.

and

[ \tilde {X} ⇒ \tilde {Y} ] ⇒ [ (\underline {{A}} _ {i}: X _ {i}) ⇒ (\underline {{A}} _ {i}: Y _ {i}) ]

[ \tilde {X} ⇒ \tilde {Y} ] ⇒ [ (\exists i: X _ {i}) ⇒ (\exists i: Y _ {i}) ]

(Note that quanltiCaiHion over i represents a func tion from predicates over SxD to predicates over s.)

Let Xi stand for a predicate on some space for any i from some domain. We then have for any I from that domain

[ (\underline {{A}} i: X i) ⇒ X I ]

hence we have for monotonic $f$ for any I

[ f (Q _ {i}: X _ {i}) ⇒ f (X I) ] ,

and since this holds for any $I$ from the do-

[ f (\underline {{A}}; \cdot : X _ {i}) ⇒ (\underline {{A}}; \cdot : f (X _ {i})) ] (0).

Let $Y_{j}$ stand for a predicate on some space. for any j from some domain. We then have for any J from that domain

[ Y J ⇒ (\exists j: Y _ {j}) ] ;

hence we have for monotonic $h$ for any $J$

[ h (Y J) ⇒ h (\underline {{E}} _ {j}: Y _ {j}) ]

and since this holds for any $J$ from the domain, we conclude for monotonic

[ (\underline {{E}} _ {j}: h (Y _ {j})) ⇒ h (\underline {{E}} _ {j}: Y _ {j}) ] . (1)

For some obscure reason, formula (1) is less well known than formula (0). Both formulae are of importance, since they allow us to deal with predicate transformers that are mono-tonic but of whose junctivity properties we know nothing.

Finally, we combine these two results. Let, for any $i$ from ${D}{i}$ and any $j$ from ${D}{j}$ ,

Let then, for any $i$ from ${D}{i}$ ,the predicate $X = \left{ {{D}{j} : j \in I}\right}$ is a predicate on $S \times {D}_{j}$ defined by

[ (X _ {i}) (j / j) \equiv z _ {i} j ] \mathrm {f o r a n y} J \mathrm {p r o m} D _ {j}.

Applying (0) with for $f$ existential quanltipication over

[ (\underline {{E}} _ {j}: (\underline {{A}} _ {i}: Z _ {i j})) ⇒ (\underline {{A}} _ {i}: (\underline {{E}} _ {j}: Z _ {i j})) ] (2)

Alternately, we could have defined, for any $j$ from $D_{j}$ , $Y_{j}$ to be a predicate on $S \times D_{i}$ , satisfying $[(Y_{j})(I / i) \equiv Z I_{j}]$ for any $I$ from $D_{i}$ .

Applying (1) with for $h$ universal quantifica- tion over i - which is monotonic- also yields (2). Had we chosen for $h$ existential quantificaiton over i, we would have gotten from (1)

[ (\underline {{E}} _ {j}: (\underline {{E}} _ {i}: Z _ {i j})) ⇒ (\underline {{E}} _ {i}: (\underline {{E}} _ {j}: Z _ {i j})) ] ;

with the inverse implication holding for reasons

[ (\underline {{E}} _ {j}: (\underline {{E}} _ {i}: Z _ {i j})) \equiv (\underline {{E}} _ {i}: (\underline {{E}} _ {j}: Z _ {i j})) ] ,

i.e. existential quantificats commute. Similarly, one can derive from (b) that universal quanti-fications commute.

Notational Remark. In the introduction I had to distinguish between the predicates $X_{i}$ on $S$ and the predicate $\tilde{X}$ on $S \times D$ , with $D$ the domain of $i$ . I wrote the somewhat pompous

" [ \tilde {X} (I / i) \equiv X I ] f o r a l l I i n D".

not quite daring to write the so much simpler

[ \tilde {X} \equiv X _ {i} ]

Here the square brackets denote universal quantification over $S \times D$ . But this is tricky. We are supposed to "understand" -or: to "remember"- that $\tilde{X}$ contains i as free variable and we are confronted with two conflicting interpretations of $X_{i}$ : for any i a predicate on S versus a predicate on $S \times D$ .

what we call "a predicate on $S$ " is some- thing of the type

$S \rightarrow$ bool, which stands for a boolean-valued expression in

in the coordinates of $S$ ; these coordinates are deemed to be named, though the names have been left unmentioned.

When we write that "for any $i$ from $D$ ,

D \rightarrow (S \dot {\to} b _ {0 0 1})

Were I to explain $\tilde{X}$ ,I would probably say that it was something of the type

(D _ {i} \times S) \rightarrow b o o l

the subscript on D mentioning the name of the free variable i that has entered the boolean- valued expression. Should we make a notational distinction between the two interpretations of $X_{i}$ and indicate, for instance, explicitly the coordinate with which the space has been extended, e.g.

[ \tilde {X} \equiv (\underset {\mathrm {v a r i}: i \mathrm {i n} D: X _ {i}} {\mathrm {v a r i}: i \mathrm {i n}}) ] ?

(End of Notational Remark.)

Turned out to be a notational question!

Plataanstraat 5

5671 AL NUENEN

The Netherlands

30 January 1984

prof. dr. Edsger W. Dgiksha

Burroughs Research Fellow