Junctivity and massaging quantification

Junctivity and massaging quantification

To begin with, we discuss universal disjunctivity. That predicate transformer $f$ is universally disjunctive means that for any range of the dummy and any $p$ (of the appropriate type)

$\left\lbrack {f.\left\langle {\exists x\;\because p.x}\right\rangle \equiv \left\langle {\exists x\;\therefore f.p}\right\rangle }\right\rbrack$

The question we raise is whether uni- versal disjunctivity of $f$ follows from the fact that for any range of the dummy $y$

(1) $\left\lbrack {f \cdot \left{ {\exists y : y}\right} \equiv \left{ {\exists y : f \cdot y}\right} \end{array}\right\rbrack$

i.e. whether in order to demonstrate (0), it suffices to confine one's attention to the specific instantiation $p \mathrel{\text{:=}}$ "identify function".

The answer to this question is positive on account of the following theorem:

Theorem 0. For any (appropriately typed)

(2) $\left\lbrack {\langle \exists x : r.x : q.\left( {p \cdot x}\right) }\right\rangle \equiv \langle \exists y : C.r.p.y : q.y\rangle \rbrack$ (3) $\left\lbrack {\langle \forall x : r.x : q.p.\left( {p.x}\right) \rangle \equiv \langle \forall y : C.r.p.y : q.y\rangle }\right\rbrack$

where $C$ is given by

(4) $\left\lbrack {C.r.p.y \equiv \langle \exists x : r.x : \left\lbrack {p.x = y}\right\rbrack > }\right\rbrack$

Proof In order to prove (2), we observe for any $p,q,r$ - in great detail-

$$ \begin{array}{l} \langle \exists y: C. r. p. y: q. y \rangle \ = {\left(4\right) } \ \langle \exists y: \langle \exists x: r. x: [ p. x = y ] \rangle : q. y \rangle \ = {\text {t r a d i n g} } \ \langle \exists y: \langle \exists x: r. x: [ p. x = y ] \rangle \land 9. y \rangle \ = {\wedge o v e r \exists } \ \langle \exists y: \langle \exists x: r. x: [ p. x = y ] \land q. y \rangle \rangle \ = {t r a d i n g } \ \langle \exists y: \langle \exists x: r. x \land [ p. x = y ]: q. y \rangle \ = {\mathrm {i n t e r c h a n g e o f} q u a n t i f i c a l i o n s } \ \langle \exists x: r. x: \langle \exists y: [ p. x = y ]: q. y \rangle \rangle \ = {1 - p o i n t r u l e } \ \langle \exists x: r. x: q. (p. x) \rangle \ \end{array} $$

The crucial observation is that the new range C.r.p does not depend on $q$ . This allows us to prove (3) by instantiating (2) with $q = 79$ ,and then applying cle Morgan's Law.

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

And now the ground work has been done to derive (0) from (1), more precisely: we observe for an $f$ satisfying (1) for any range of the dummy $y$ , and any $r, p$ of the appropriate types

$$ \begin{array}{l} f. \langle \exists x: r. x: p. x \rangle \ = {2) w i t h q := i d } \ f: \langle \exists y: C. r. p. y: y \rangle \ = {(1) \mathrm {w i t h} r a n g e: C. r. p } \ \langle \exists y: C. r. p. y: f. y \rangle \ = {2) w i t h q := f } \ \langle \exists x: r. x: f. (p. x) \rangle \ \end{array} $$

I owe Theorem 0 to the ETAC, which considers it (I think) as a generalization of "splitting the range". My interest is here in the relation between (o) and (1). It is of the form

$$ \langle \forall p: B. p \rangle \equiv B. i d $$

to demonstrate B , one demonstrates the RHS ; to use B , one uses the LHS which can be instantiated as you like .

Situation (5) is common, and for metho-dological reasons we should know and recognize it. For instance

$$ \langle \forall x: [ c; x \Rightarrow x ] \rangle = [ c \Rightarrow J ] $$

gives us in the relational calculus two ways of expressing that $C$ is "a middle condition" (or "a monohype"). Similarly

$$ \langle \forall x: [ x; r \Rightarrow r ] \rangle \equiv [ t r u e; r \Rightarrow r ] $$

gives us two ways of expressing that $r$

is "a right condition". Finally

$$ \langle \forall i, j: i \leq j: A. i \leq A. j \rangle = \langle \forall i: A. i \leq A. (i + 1) \rangle $$

gives us two ways of expressing that the sequence $A$ is ascending.

The last three examples rely for LHS $\Leftarrow$ RHS on transitivity or monotonicity. This note has been written because the first example, i.e. the characterizations of junctivity, seems not to do so.

Austin, 21 October 1994

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