Junctivity of extreme solutions (with C.S.Scholten)

Junctivity of extreme solutions

by Edsger W.Dykstra and C.S.Schoften

Introduction

A predicate transformer that distributes over conjunction is called "conjunctive"; similarly, one that distributes over disjunction is called "disjunctive".

Example. Since for all $P, Q$

[ w p (S, P ∧ Q) \equiv w p (S, P) ∧ w p (S, Q) ] ,

${wp}\left( {S,?}\right)$ is conjunctive; we remind the reader that it is only disjunctive for deterministic $S$ . (End of Example.)

The notions of conjunctivity and disjunctivity can be generalized to distribution over universal and existential quantification respectively. The manners in which will be made more precise below.

In connection with repetitions it is customary to define a predicate transformer $g$ by a definition of the form "for all $X$ , $gX$ is the strongest (weak- est) solution of the equation $Y: [Y \equiv fXY]$ ".

The purpose of this note is to relate the junctivity of $g$ to the junctitivity of $f$ ; since $f$ is a function with 2 arguments, the notion of junctivity will be suitably extended.

Definitions

Associated with each predicate transformer is its so-called "conjugate"; the transition to the conjugate is denoted by adding an asterisk to the function symbol. The conjugate of a predicate transformer is (loosely) defined as the negation of that predicate transformer applied to the negated arguments, i.e.

[ g ^ {} X \equiv ¬ g (¬ X) ], [ f ^ {} X Y \equiv ¬ f (¬ X) (¬ Y) ] e k.

The relation is a mutual one: the conjugates of ${g}^{ * }$ and ${f}^{ * }$ are $g$ and $f$ respectively.

From the above it follows that a predicate trans-former over which negation distributes, e.g

[ ¬ f X Y \equiv f (¬ X) (¬ Y) ]

is its own conjugate.

Example For any program $s$ such that the final state is a total function of the initial state, i.e. any deterministic $S$ with [wp(S,false)], wp(S,?) is its own conjugate. Consequently, in order to appreciate the difference between a predicate transformer and its conjugate in programming terms, we have to include nontermination and/or nondeterminacy into our considerations. (End of Example.)

The notion of the conjugate is important for what follows because -as will be made more precise shortly- firstly, a conjunctive property of a predicate transformer is a disjunctive property of its conjugate

and, secondly, the conjugate of a strongest solution of an equation is the weakest solution of a "conjugate equation." This symmetry has been exploited for the sake of brevity.

Let $g$ be a predicate transformer with one argu- ment and $V$ a bag of predicates. By "g is conjunctive over $V$ " we mean

[ g (\underline {{A}} X: X _ {\underline {{\ln}} V}: X) \equiv (\underline {{A}} X: X _ {\underline {{\ln}} V}: g X) ]

Depending on the restrictions imposed on $V$ , six types of conjunctivity are introduced; note that, the stronger the restrictions on $V$ , the weaker the type of conjunctivity.

0 universal conjunctivity means conjunctivity over 0 unbounded conjunctivity means conjunctivity over o denumerable conjunctivly means conjunctivity over all non-empty denumerable V 0 (finite) conjunctivity means conjunctivity over all non-empty finite o and- continuity means conjunctivity over all non-empty V, the distinct elements of which can be ordered as a strengthening sequence 0 monotonicity means conjunctivity over all nonempty $V$ ,the distinct elements of which can

can be ordered as a finite strengthening sequence.

These types of conjunctivity have been listed in the order of decreasing strength, except finite conjunctivity and and- continuity, neither of which implies the other.

For the definition of the corresponding six types of disjunctivity - i.e. in order: universal, unbounded, denumerable, and finite disjunctivity, or continuity, and (again) monotonicity - two ways are open to us.

We can define that the disjunctivity of $g$ and

Alternatively we can define "g is disjunctive over $v$ " to mean

[ g (\underline {{E}} X: X _ {\underline {{i n}}} V: X) \equiv (\underline {{E}} X: X _ {\underline {{i n}}} V: g X) ] (0)

and introduce the six types of disjunctivity by re-writing the above with the following substitutions:

"disjunctivity" for "conjunctivity"

"or- continuity" for "and- continuity"

"weakening" for "strengthening".

Proof.

(0)

$= {$ negating both sides and de Morgan twice $}$

[ ¬ g. ¬ (\underline {{A}} X: X _ {\underline {{i n}}} V: ¬ X) \equiv (\underline {{A}} X: X _ {\underline {{i n}}} V: ¬ g X) ]

$= {$ definition of conjugate $}$

[ g ^ {} (\underline {{A}} X: X _ {\mathrm {i n}} ^ {\prime} V; \tau X) \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: g ^ {} \tau X) ]

$= {$ definition of ${V}^{ * }$ ,see below

[ g ^ {} (\underset {\mathrm {A}} {\bigvee} Y; Y _ {\mathrm {i n}} V ^ {}; Y) \equiv (\underset {\mathrm {A}} {\bigvee} Y; Y _ {\mathrm {i n}} V ^ {}; g ^ {} Y) ]

where ${V}^{ * }$ is defined by

(\underline {{A}} Z: (Z _ {\underline {{i n}}} V ^ {*}) \equiv (¬ 2) _ {\underline {{i n}}} V)

From the above relation between $V$ and ${V}^{ * }$ we immed

$V$ is non-empty $\equiv {V}^{ * }$ is non-empty

$V$ is denumerable $\equiv {V}^{ * }$ is denumerable

$V$ is finite $\equiv {V}^{ * }$ is finite

$V$ is a strengthening sequence $\equiv {V}^{ * }$ is a

weakening sequence

observations which conclude the proof. (End of Proof.)

In the sequel we shall confine ourselves to conjunctivity; in view of the above all our results can be mechanically translated into the corresponding results about disjunctivity.

For our next definitions and associated notational conventions we remind the reader of an earlier and now familiar generalization. Traditionally the logical operators (such as $¬ , ∧ , \lor , \equiv , \underline{\mathrm{A}}$ , and $\underline{\mathrm{E}}$ ) are defined on boolean variables. The next step is their generalization from propositions to predicates. To this end we consider boolean functions -called "predicates"- defined on some domain. Let $P$ and $Q$ be two such functions; then, for instance, "P∧Q" denotes a third similar function, defined by

(P \wedge Q) s \equiv P s \wedge Q s f o r a l l s i n t h e d o -

main; this device enabled us to manipulate predicates without all the time mentioning the dummy s.

In the same vein we now consider predicate-valued functions defined on some domain. Let $K$ and $H$ be two such functions; then, for instance, "K ∧ H" denotes a third similar function, defined by

[ (K \wedge H) u \equiv K u \wedge H u ] \mathrm {f o r a l l} u \mathrm {i n t h e}

domain_ where the square brackets denote as usual universal quantification over the domain of the anonymous $s -$

The name under which such a function like $K$ or $H$ is known depends on their domain: if $u$ ranges over predicates, they are known as predicate transformers; consequently, with $g$ and ${g}^{\prime }$ being two predicate transformers,we have now attached a meaning "g ^ $∧ {g}^{\prime }$ ".

If u ranges over the natural numbers (or a prefix thereof), they are known as infinite (or finite) predicate sequences: the usual parlance then refers to "element-wise" or "component-wise" application of the logical operators. Note that the logical connectives have been defined for functions on the same domain; predicate sequences thus connected should be of equal length.

If the domain of such a predicate-valued function is left unspecified the name "predicate generator" can be used.

Another way of viewing a predicate generator such as $K$ and $H$ is to regard it as a boolean function on the Cartesian product of the ranges of $u$ and $s$ . This view is reflected in our use of square brackets around predicate generators; for a predicate generator $K$ we define $[K]$ by

[ K ] \equiv (\underline {{A}} u: [ K u ])

Example. The commutativity -i.e. symmetry- of the conjunction when connecting predicate generators can now be expressed by

[ K ∧ H \equiv H ∧ K ] . (E n d o f E x a m p l e.)

Hope. May we not regret this overloading of the square brackets. (End of Hope.)

Having defined conjunctivity for $g$ ,i.e. a predicate transformer with one argument,we now turn our attention to $f$ ,a predicate transformer with two arguments. By " $f$ enjoys a certain type of conjunctivity in its first argument " we mean that $f?Y$ enjoys that same type of conjunctivity for all $Y$ ,and similarly for its second argument.

Besides $f$ 's conjunctivity in its individual argu- ments, we introduce its so-called "double conjunctiviy" -in the same six types-. In order to do so we associate with $f$ a function defined on one argument, which is an ordered predicate pair, i.e.

[ \tilde {f} (X, Y) \equiv f X Y ] \mathrm {f o r a l l} X, Y;

f enjoying some type of double conjunctivity means that f enjoys that type of conjunctivity. We could do so because an ordered predicate pair is an instance of a predicate sequence, which can be regarded as a predicate generator and for predicate generators on the same domain - here ${0,1} -$ the logical connectives have been defined.

Examples. With $g_0$ and $g_1$ enjoying some type of conjunctivity, $f$ defined by

[ f X Y \equiv g _ {0} X \wedge g _ {1} Y ]

enjoys the same type of double conjunctivity, so does

[ f \times Y = i f B \rightarrow g 0 X [ ] ¬ B \rightarrow g 1 Y [ f ]

(End of Examples.)

The results

Our first results relate for a predicate transformer $f$ with 2 arguments its type of double conjunctivity and the type of conjunctivity in its individual argu- ments.

Our first result is very simple, but negative: in the case of universal conjunctivity there is no relation, as is shown by the following two examples.

Examples. The function $f$ given by $\left\lbrack {{f}^{\prime }{X}^{\prime }Y}\right\rbrack$ is universally doubly conjunctive, but not universal- Iy conjunctive in its individual arguments: uni- versal conjunctivity of $g$ implies $\left\lbrack {g\text{true}}\right\rbrack$ ,but [f true Y], being [Y], certainly does not hold for all $Y$ .

The function $f$ given by $[fXY\equiv XvY]$ is universally conjunctive in its individual arguments since disjunction distributes over all forms of universal quantification, but not universally doubly conjunctive, not even finitely doubly conjunctive: $\tilde{f}$ is not conjunctive over the bag of predicate pairs ${(true,false),(false, true)}$ . (End of Examples.)

Remark. There is, in fact, only 1 if that is both universally conjunctive in both its arguments and universally doubly conjunctive; this even holds if "universally doubly conjunctive" is replaced by the much weaker "doubly conjunctive".

true

\begin{array}{l} \equiv {f i s u n v e r s a l l y c o n j u n c t i v e i n b o t h i s a r g u m e n t s } \ \underline {{\left(\underline {{A}} X , Y \right.}}: [ f X T ] \wedge [ f T Y ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} X, Y:: [ f X T \wedge f T Y ]) \ \equiv {f i s d o u b l y c o n j u n c t i v e } \ (\underline {{A}} X, Y:: [ f \overline {{X}} Y ]) \ \end{array}

(End of Remark.)

For the remaining types of conjunctivity we have, however, the following two results.

Theorem 0. An $f$ enjoying some type of double conjunctivity enjoys the same type of conjunctivity in both its arguments for all types, except universal conjunctivity.

Theorem 1. An $f$ that is and-continuous or monotonic in both its arguments enjoys the same type of double conjunctivity.

Remark. In view of Theorem 0, the formulation of Theorem 1 could have been extended with "and vice versa". (End of Remark.)

Before embarking on the proofs of Theorems 0 and 1, we state and prove

Lemma 0. In terms of a bag $V$ of predicates and a predicate transformer $p$ , bag $W$ of predicate pairs is defined by

(X, Y) _ {\underline {{\mathrm {i n}}}} W \equiv X _ {\underline {{\mathrm {i n}}}} V \wedge [ Y \equiv p X ] f o r a l l X, Y;

for any predicate transformer q with two arguments we then have

[ (\underline {{A}} (X, Y): (X, Y) _ {\underline {{\mathrm {i m}}}} W: q X Y) \equiv (\underline {{A}} X: X _ {\underline {{\mathrm {i m}}}} V: q X (p X)) ]

Proof. We observe for all $Z$

[ Z \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{\operatorname {i n} W : q X Y}}}}) ]

\begin{array}{l} = {d e f i n i t i o n o f W } \ [ Z \equiv (\underline {{A}} X, Y: X _ {\mathrm {i n}} V \wedge [ Y \equiv p X ]: q X Y) ] \ \equiv {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} X: X \ln V: (\underline {{A}} Y: [ Y \equiv p X ]: q X Y)) ] \ \equiv {\text {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: q X (p X)) ] . (E n d o f P r o o f.) \ \end{array}

Proof of Theorem 0.

On account of the symmetry it suffices to show that $f$ enjoys the appropriate type of conjunctivity in its first argument, i.e.

[ f (\underset {\mathrm {A X}} {\cap} X _ {\mathrm {i n}} V; X) Y ^ {\prime} \equiv (\underset {\mathrm {A X}} {\cap} X _ {\mathrm {i n}} V; f X Y ^ {\prime}) ]

for any $Y^{\prime}$ and appropriate $V$ . To this purpose we construct for any $Y^{\prime}$ and $V$ an equally appro-priate bag W of predicate pairs and subsequently deduce from $\phi^{\prime}$ double conjunctivity over W its corresponding conjunctivity in its first argument. The crux of the argument is the construction of an appropriate W; we propose

(X, Y) \underline {{\mathrm {i n}}} W \equiv X _ {\underline {{\mathrm {i n}}}} V \wedge [ Y \equiv Y ^ {\prime} ] f o r a l l X, Y.

Note that in the classification "non-empty/ denominator- able/finite/strengthening" $W$ has the same type as $V$ . We shall now derive the consequences of $P$ 's double conjunctivity over $W$ , i.e.

\begin{array}{l} [ f (\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: X) (\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: Y) \equiv \ (\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{\mathrm {i n}}}}} W: f X Y) ] \ \end{array}

Applying in this formula Lemma 0 with $Y^{\prime}$ for $pX$ and in succession $X, Y,$ and $pXY$ for $qXY$ and observing that for non-empty $V$

\begin{array}{l} [ (\underset {\sim} {A} X: X \mathrm {i n} V: Y ^ {\prime}) \equiv Y ^ {\prime} ] , w e i n d e e d o b t a i n \ [ f (\underline {{A}} X: X _ {\mathrm {i n}} V: X) Y ^ {\prime} \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: f X Y ^ {\prime}) ] \ (E n d o f P r o o f.) \ \end{array}

Proof of Theorem 1.

We associate with the strengthening sequence of predicate pairs $(X_i, Y_i)$ for $0 ≤ i ≤ N$ the strengthening sequences $X_i$ and $Y_i$ with the same non-empty range. Under the assumption of the appropriate conjunctivity in the individual arguments, we have to show

[ f (\underline {{A}} _ {i}: X _ {i}) (\underline {{A}} _ {i}: Y _ {i}) \equiv (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ]

To this end we observe for all $Z$

[ z \equiv f (\underline {{A}} i: X _ {i}) (\underline {{A}} i: Y _ {i}) ]

\equiv {f a p p r o p r a t e l y c o n j u n c t i v e i n i t s 1 s t a r g u m e n t }

[ Z \equiv (\underline {{A}} _ {i}: f (X _ {i}) (\underline {{A}} _ {j}: Y _ {j})) ]

\equiv {f a p p r o p r a t e l y c o n j u n c t i v e i n i t s 2 n d a r g u m e n t }

[ Z \equiv (\underline {{A}} i, j: P (X _ {i}) (Y _ {j})) ]

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

[ \dot {z} = (\underline {{a}} j, i: i ≤ j: f (x _ {i}) (r _ {j})) \wedge (\underline {{a}} i, j: j ≤ i: f (x _ {i}) (r _ {j})) ]

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

[ Z \equiv (\underline {{A}} _ {j}: (\underline {{A}} _ {i}: i ≤ j: f (x _ {i}) (Y _ {j}))) \wedge (\underline {{A}} _ {i}: (\underline {{A}} _ {j}: j ≤ i: f (x _ {i}) (Y _ {j}))) ]

\equiv {f \mathrm {i s m o n o t o n i c i n e i t h e r a g u m e n t} X _ {i} \mathrm {a n d}

r _ {j} a r e s t r e n t h e n i n g s e q u e n c e s }

[ 2 \equiv (\underline {{A}} _ {j}: f (X _ {j}) (Y _ {j})) \wedge (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ]

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

[ Z ^ {\prime} \equiv (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ]

(End of Proof of Theorem 1.)

Since $f$ given by $\left\lbrack {{f}^{\prime }{XY} \equiv X \vee Y}\right\rbrack$ is universally conjunctive in both its arguments but not finitely doubly conjunctive, Theorems O and 1 are as strong as possible.

We now consider, for any $X$ , the equation

Y: [ p \times Y \equiv Y ] ; \tag {1}

we confine ourselves to $f$ ’s that are monotonic in their $2^{nd}$ argument,so that -thanks to Knaster. Tarski- (1) has for all $X$ a strongest and a weakest solution,which we denote by $g\left( X\right)$ and h X respectively.Our purpose is to relate the conjunctivity properties of $g$ and h to those of $f$ . The above definitions of $g$ and h are formally captured by

[ f X (g X) \equiv g X ] \qquad \mathrm {f o r a l l} X \qquad (2)

\underline {{A}} Y: [ f X Y \equiv Y ]: [ g X ⇒ Y ]) \qquad \mathrm {f o r a l l} X \qquad (3)

[ f X (h X) \equiv h X ] \qquad \mathrm {f o r a l l} X \qquad (4)

(\underline {{A Y}}: [ f X Y \equiv Y ]: [ Y ⇒ h X ]) \mathrm {f o r a l l} X. (5)

Theorem 2. If $f$ is monotonic in its 1st argument as well, $g$ and $h$ are monotonic.

Proof. We observe for any $x_0$ and $x_1$

[ X 0 ⇒ X 1 ]

⇒ {f i s m o n o t o n i c i n i t s 1 ^ {s t} a r g u m e n t }

[ f \times_ {0} (g \times_ {1}) ⇒ f \times_ {1} (g \times_ {1}) ]

\equiv {\mathrm {i n v i e w o f} (2) }

[ f \chi_ {0} (g \chi_ {1}) ⇒ g \chi_ {1} ]

⇒ {(3) \mathrm {i n c o m b i n a t i o n w i t h k n a s t e r - T a r s k i} }

[ g X _ {0} ⇒ g X _ {1} ]

and similarly

\begin{array}{l} [ X _ {0} ⇒ X _ {1} ] \ ⇒ {f \mathrm {i s m o n o t o n i c i n i s} 1 ^ {\mathrm {s t}} \mathrm {a r g u m e n t} } \ [ f X _ {0} (h X _ {0}) ⇒ f X _ {1} (h X _ {0}) ] \ = {\mathrm {i n v i e w o f} (4) } \ [ h X _ {0} ⇒ f X _ {1} (h X _ {0}) ] \ ⇒ {(5) \mathrm {i n c o m b i n a t i o n w i t h k n a s t e r - T a r s k i} } \ [ h X _ {0} ⇒ h X _ {1} ] (\mathrm {E n d o f P r o o f .}) \ \end{array}

For the proofs of our next theorems we need a lemma; for the sake of brevity we introduce some abbreviations. For a bag $W$ of predicate pairs we define the predicates $Xw$ and $Yw$ by

\begin{array}{l} [ X _ {w} \equiv (\underline {{A}} (X, Y): (X, Y) _ {\mathrm {i n}} W: X) ] \ [ Y w \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: Y) ] \ \end{array}

Lemma 1. With $f$ doubly conjunctive over $W$ and $W$ such that

(\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{\operatorname {i n} W}}}}: [ f X Y \equiv Y ]) (6)

we have $\left\lbrack {g{x}{w} ⇒ {y}{w}}\right\rbrack$ (7)

and $\left\lbrack {{Y}{W} ⇒ h{X}{W}}\right\rbrack$ (8)

Proof. We observe for any $z$

\begin{array}{l} [ Z \equiv \rho_ {X _ {w} Y _ {w}} ] \ \equiv {\mathrm {d e f i n i t i o n o f} X w \mathrm {a n d} Y w \mathrm {a n d} P ^ {\prime} s \mathrm {d o u b l e c o n j u n c h i v i t y} } \ [ Z \equiv (\underline {{A}} (X, Y): (X, Y) _ {\mathrm {i n}} W: f X Y) ] \ \equiv {\mathrm {i n v i e w o f (6) a n d d e f i n i t i o n o f Y w} } \ [ Z \equiv Y _ {w} ] , h e n c e \ [ f X _ {w} Y _ {w} \equiv Y _ {w} ], \mathrm {f r o m w h i c h (7) a n d (8) f o l l o w} \ \end{array}

by virtue of (3) and (5) respectively.

(End of Proof.)

In the sequel we shall appeal to Lemma 1 twice, each time with a well-chosen $W$ .

Theorem 3 If $f$ enjoys double conjunctivity of some type, $h$ enjoys conjunctivity of the same type.

Proof. For a bag $V$ of predicates, which is of the appropriate type, we construct a bag $W$ of predicate pairs by

(x, y) _ {\mathrm {i n}} W \equiv X _ {\mathrm {i n}} V \wedge [ Y \equiv h X ]

We want to show first that if $V$ is of some appropriate type, $W$ is of that type as well. As far as the classification "non-empty/denumerable/finite" is concerned this is obvious. Furthermore, to a $V$ ordered as a strengthening sequence corresponds a $W$ which is a strengthening sequence: $f$ being doubly conjunctive (of some type), it is doubly monotonic, hence -by Theorem 0 - monotonic in both its arguments, and therefore -Theorem 2 - $h$ is monotonic.

In order to prove conjunctivity of $h$ over $V$ , i.e.

[ h (\underline {{A}} X: X \underline {{\operatorname {i n}}} V: X) \equiv (\underline {{A}} X: X \underline {{\operatorname {i n}}} V: h X) ]

we show that either side implies the other.

(i) Because $h$ is monotonic -see above-we have $\left\lbrack {h\left( {{A}^{\prime }X : {X}{\text{in }}V : X}\right) ⇒ \left( {{A}^{\prime }X : {X}{\text{in }}V : hX}\right) }\right\rbrack$ .

(ii) Because $f$ is doubly conjunctive over $W$ , and $W$ satisfies -on account of (4)- condition (6),

Lemma 1 is applicable. Now we observe for any $Z$

\begin{array}{l} [ Z \equiv (\underset {\sim} {A} X: X _ {\mathrm {i n}} V: h X) ] \ \equiv {\mathrm {d e f i n i t i o n o f} W, \mathrm {l e m m a 0 w i t h h f o r} p \mathrm {a n d} Y \mathrm {f o r} q X Y } \ [ Z \equiv (\underset {\sim} {A} (X, Y): (X, Y) _ {\mathrm {i n}} W: Y) ] \ \equiv {\mathrm {d e f i n i t i o n} o p Y _ {w} } \ [ Z \equiv Y _ {w} ] \ ⇒ {\mathrm {i n v i e w o f} (8) \mathrm {o f L e m m a 1} } \ [ 2 ⇒ h X _ {w} ] \ \equiv {\mathrm {d e f i n i t i o n} o f X w } \ [ 2 ⇒ h (A (X, Y); (X, Y) _ {\mathrm {i n} W: X}) ] \ \equiv {\mathrm {d e f i n i t i o n o f} W, \mathrm {L e m m a O w i t h h f o r} p \mathrm {a n d} X \mathrm {f o r} q X Y } \ [ Z ⇒ h (\underline {{A}} X: X _ {\underline {{i n}}} V; X) ] \ (E n d o f P r o o f.) \ \end{array}

This concludes our treatment of the conjunctivity properties of the weakest solution of $Y$ : $[fXY \equiv Y]$ . We now turn our attention to the strongest solution of that equation.

Our first result about $g$ is

Theorem 4 With $f$ enjoying universal, unbounded, denumerable, or finite double conjunctivity,

with $W$ a bag of predicate pairs that is of the appropriate type and satisfies (6), i.e.

(\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{\operatorname {i n}}} W}}: [ f X Y \equiv Y ])

and $x_{w}$ and $Y_{w}$ defined as before, i.e.

\begin{array}{l} [ X _ {w} \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: X) ] \ [ Y _ {W} \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: Y) ] \ \end{array}

we have

(\underline {{A}} (X, Y): (X, Y) _ {\underline {{m}}} W: [ g X _ {w} \equiv Y _ {w} ∧ g X ])

Proof. We show that either side of the equivalence implies the other.

(i) All conditions of Lemma 1 being satisfied, we have

[ g X _ {w} ⇒ Y _ {w} ]

Since $f$ is doubly conjunctive (of some type), it is doubly monotonic, hence - Theorem 0 - monotonic in both its arguments, and therefore - Theorem 2- $g$ is monotonic, from which we conclude

[ g X w ⇒ g X ] f o r a l l X o c c u r r i n g i n X w.

Combining these two results we get

(\underline {{A}} (X, Y): (X, Y) _ {\underline {{\mathrm {i n}}}} W: [ g X w ⇒ Y w ∧ g X ])

(ii) The crux of the proof of $\left\lbrack {{Yw} ∧ gX ⇒ {gXw}}\right\rbrack$ consists of rewriting this as $\left\lbrack {{gX} ⇒ {gXw}v¬ {Yw}}\right\rbrack$ , and showing -see (3)- that $g{Xw}v¬ {Yw}$ satisfies the equation of which $g$ is the strongest solution.

true

\begin{array}{l} \equiv {(2) } \ [ f X _ {w} (g X _ {w}) \equiv g X _ {w} ] \ ⇒ {f \mathrm {i s m o n o t o n i c i n i t s} 2 ^ {n d} \mathrm {a r g u m e n t} } \ [ f ^ {\prime} X _ {w} (g X _ {w} \wedge Y _ {w}) ⇒ g X _ {w} ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ (A ^ {\prime} (P, Q): (P, Q) _ {\mathrm {i n}} W: [ f X _ {w} (g X _ {w} ∧ Y _ {w}) ⇒ g X _ {w} ]) \ \equiv {\mathrm {d e f i n i t i o n o f} X _ {w} \mathrm {a n d p r e d i c a t e c a l c u l u s} } \ \end{array}

$(A(P,Q):(P,Q))_{in}W$

[ f (P \wedge X _ {w}) ((g X _ {w} \vee Y _ {w}) \wedge Y _ {w}) ⇒ g X _ {w} ])

$\equiv { f {also} {double}$ conjunctive over the union of $P$ ${W}_{\text{and the single }}$ set $\left{ {\left( {P,gXw} \vee {Yw}\right) }\right}$ ; definition of ${Xw}$ and ${Yw}}$

(H,P,Q): (P,Q) in $W$ :

[ f P (g X _ {w} v \cap Y _ {w}) ∧ (\underline {{A}} (X, Y): (X, Y) _ {\ln} W: f X Y) ⇒ g X _ {w} ])

$\equiv { W$ satisfies (6) and definition of ${Y}_{W}}$

(\underline {{A}} (P, Q): (P, Q) _ {\mathrm {i n}} W: [ f P (g ^ {\prime} X _ {w} \vee Y _ {w}) \wedge Y _ {w} ⇒ g X _ {w} ])

[\equiv { \text{predicate calculus}} ]

(\underline {{A}} (P, Q): (P, Q) _ {\underline {{\mathrm {i n}}}} W: [ F P (g X w \vee ¬ Y w) ⇒ g X w \vee ¬ Y w ])

$⇒ \left{ \begin{array}{l} \text{ (3 ) and Knaster-Tarski } \ \end{array}\right}$

(\underline {{A}} (P, Q): (P, Q) \mathrm {i n} W: [ g P ⇒ g X w \vee Y w ])

$\equiv {$ predicate calculus and renaming of the dummies $}$

(\underline {{A}} (X, Y): (X, Y) \underline {{\in}} W: [ Y _ {w} ∧ g X ⇒ g ^ {\prime} X _ {w} ])

(E n d o f P r o o f.)

Remark. Theorem 4 is as strong as possible in the sense that it can not be extended to and-continuity and monotonicity; $[fXY \equiv XvY]$ and the strengthening sequence (true, true), (false, true) provide the counterexample. (End of Remark.)

In view of the definition of $Y_{w}$ , Theorem 4 has the following

Corollary 0. With the antecedents and definitions as in Theorem 4 we have

(\underline {{E}} (X, Y): (X, Y) _ {\underline {{i n}}} W: [ Y \equiv g X ]) ⇒ [ g X _ {w} \equiv Y _ {w} ]

The conjunctivities of $f$ and $g$ are connected by

Theorem 5. If $f$ enjoys unbounded, denumerable, or finite double conjunctivity, $g$ enjoys conjunctivity of the same type.

Proof. For a bag $V$ of predicates, which is of the appropriate type, we construct a bag $W$ of predi- cate pairs by

(X, Y) _ {\underline {{\operatorname {i n}}}} W \equiv X _ {\underline {{\operatorname {i n}}}} V \wedge [ Y \equiv g X ]

To start with we observe that $W$ is of the same type as $V$ ; next we observe that this $W$ satisfies (6). Hence Theorem 4 is applicable. Since $W$ is not empty, Corollary O yields

[ g X _ {w} \equiv Y _ {w} ] (g).

Finally we observe - similarly to the proof of Theorem 3- for any $z$

[ Z \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: g X) ]

[\left. \begin{array}{l} \equiv \left{ {\text{ definition of }W;\text{ Lemma }0,\text{ with }g\text{ for }p,andY\text{ for }p}\right} \ g \in Y \end{array}\right} ]

[ Z \equiv (\underline {{A}} (X, Y): (X, Y) _ {\underline {{\mathrm {i n}}}} W: Y) ]

$\equiv \left{ {{\text{ definition of }}_{Yw}}\right}$

[ Z \equiv Y _ {W} ]

$\equiv { \langle g\rangle }$

[ Z \equiv g X _ {W} ]

[\left. \equiv \left{ {\text{ definition of }X}\right} \right. ]

[ Z \equiv g (\underline {{A}} (X, Y): (X, Y) _ {\mathrm {i n} W: X}) ]

$\equiv {$ def. of $W;$ Lemma 0,with $g$ for $p$ and $X$ for $q \times r}$ $\left\lbrack {2 \equiv g\left( {\underline{A}X : X\overset{.1}{1}\mathrm{ V} : X}\right) }\right\rbrack$

(End of Proof.)

Remark. We remind the reader that $g$ 's inheritance of monotonicity has already been established in Theorem 2. Neither universal conjunctivity nor and-continuity are in general inherited by $g$ . (End of Remark.)

Two final remarks. The above exclusively deals with conjunctivity. By switching to the conjugates, similar disjunctivity results are obtained.

Secondly, $X$ and $Y$ stood for predicates; they can, however, be taken as predicate generators. As an example, the above theorems tell us how the double conjunctivity properties of weakest and strongest solutions of $Z$ : $\left\lbrack {c \times Y \cdot Z \equiv Z}\right\rbrack$ are inherited from the triple conjunctivity properties of $c$ .

15 April 1983

drs. C.S. Scholten Scientific Advisor Philips Research Laboratories 5600 JA EINDHOVEN The Netherlands

prof. dr. Edsger W. Dgksra Burroughs Research Fellow Plataanstraat 5 5671 AL NUENEN The Netherlands