Exploring the lexical coupling

Exploring the lexical coupling

Let us try to forget for a moment everything we know about the lexical order and start afresh. Then we could consider something like the following problem.

Let $X, X'$ be of some type for which a binary relation has been given; let $Y, Y'$ be of some type for which a binary relation has been given; let us call these given relations the constituent relations. Question: how can we meaningfully define a binary relation - called the composite relation - on the ordered pairs $XY$ and $X'Y'$ in terms of the constituent relations?

Denoting all three relations by the same infix $\Delta$ ,we are considering how to define XYAXY in terms of ${X\Delta }{X}^{\prime },{X}^{\prime }{4X},{Y\Delta }{Y}^{\prime }$ ,and ${Y}^{\prime }{4Y}$ . Remembering a little bit of the lexical order, I propose to investigate the definition

(0) $X Y \triangleleft X^{\prime} Y^{\prime} \equiv X \triangleleft X^{\prime} V\left(\neg X^{\prime} \triangleleft X \land Y \triangleleft Y^{\prime}\right)$ ,

a definition which is interesting in its own right - i.e. independent of properties of the con- stituent relations -, as shown by the following two lemmata.

Duality lemma With relation $D$ defined by

(1) ${Z}{D}{Z}^{\prime } \equiv 7{Z}{A}{Z}^{\prime }\;$ ,for all $Z$ ,

$D$ satisfies for all $X,Y,{X}^{\prime },{Y}^{\prime }$

(2) $X \circledast X^{\prime}Y^{\prime} \equiv X \circledast X^{\prime} \wedge (\neg X^{\prime} \circledast X \vee Y \circledast Y^{\prime})$ .

Proof We observe for any $X, Y, X', Y'$

$$ \begin{array}{l} X Y _ {D} X ^ {\prime} Y ^ {\prime} \ = {(1) } \ \neg (X Y \triangleleft X ^ {\prime} Y ^ {\prime}) \ = {(0) } \ \lnot (X \triangleleft X ^ {\prime} \lor (\lnot X ^ {\prime} \triangleleft X \land Y \triangleleft Y ^ {\prime})) \ = {d e M o r g a n, t w i c e } \ \lnot X \triangleleft X ^ {\prime} \land (\lnot X ^ {\prime} \triangleleft X \lor \lnot Y \triangleleft Y ^ {\prime}) \ = {(1), t h r i c e } \ X \supset X ^ {\prime} \land (\neg X ^ {\prime} D X \lor Y \supset Y ^ {\prime}) \ \end{array} $$

(End of Proof.)

Notice that (1) allows us to rewrite (0) and (2) as

$\left( d\right) Y{Y}{\Delta }{X}^{\prime }{Y}^{\prime } \equiv {X}{\Delta }{X}^{\prime }v\left( {{X}^{\prime }{Dx} \land {Y}_{\Delta }{Y}^{\prime }}\right)$

$\left( {2}^{\prime }\right) X{Y}{D}{X}^{\prime }{Y}^{\prime } \equiv {X}{D}{X}^{\prime } \land \left( {{X}^{\prime }{A}^{v}X \vee {Y}_{D}{Y}^{\prime }}\right)$

Associativity lemma

(3) $\left( {X,Y}\right) Z \vartriangleleft \left( {{X}^{\prime }{Y}^{\prime }}\right) {Z}^{\prime } \equiv X\left( {Y,Z}\right) \vartriangleleft {X}^{\prime }\left( {{Y}^{\prime }{Z}^{\prime }}\right)$ (4) $\left( {X + Y}\right) Z \Rightarrow \left( {{X}^{\prime }{Y}^{\prime }}\right) {Z}^{\prime } \equiv X\left( {YZ}\right) \supset {X}^{\prime }\left( {{Y}^{\prime }{Z}^{\prime }}\right)$

Proof We shall demonstrate (3).

$$ (X Y) Z \triangleleft (X ^ {\prime} Y ^ {\prime}) Z ^ {\prime} $$

$$ = {0 ^ {\prime} \mathrm {w i t h} X, Y := X Y, Z } $$

$$ X Y \triangle X ^ {\prime} Y ^ {\prime} \vee (X ^ {\prime} Y ^ {\prime} \triangleright X Y \wedge Z \triangle Z ^ {\prime}) $$

$$ = {(0 ^ {\prime}); (2 ^ {\prime}) \mathrm {w i t h p r i m i n g i n v e r t e d} } $$

$$ X \circ X ^ {\prime} \vee (X ^ {\prime} \circ X \wedge Y \circ Y ^ {\prime}) \vee $$

$$ (X ^ {\prime} \triangle X \wedge (X \triangle X ^ {\prime} \vee Y ^ {\prime} \triangle Y) \wedge Z \triangle Z ^ {\prime}) $$

$$ = {\wedge d i s t r i b u t e s o v e r v } $$

$$ X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \triangleright X \wedge Y \triangleleft Y ^ {\prime}) \vee $$

$$ (X ^ {\prime} \triangleright X \land Y ^ {\prime} \triangleright Y \land Z \triangleleft Z ^ {\prime}) \lor $$

$$ (X ^ {\prime} \triangle X \wedge X \triangle X ^ {\prime} \wedge Z \triangle Z ^ {\prime}) $$

$$ = {\mathrm {a b s o r p t i o n w i t h f i r s t a n d l a s t d i s j u n c t} } $$

$$ X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \triangleright X \wedge Y \triangleleft Y ^ {\prime}) \vee $$

$$ (X ^ {\prime} \circ X \wedge Y ^ {\prime} \circ Y \wedge Z \circ Z ^ {\prime}) $$

$$ {\wedge d i s t r i b u t e s o v e r v } $$

$$ X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \triangleright X \wedge (Y \triangleleft Y ^ {\prime} \vee (Y ^ {\prime} \triangleright Y \wedge Z \triangleleft Z ^ {\prime}))) $$

$$ = {(0 ^ {\prime}) \mathrm {w i t h} X, Y := Y, Z } $$

$$ X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \boxdot X \wedge Y Z \triangleleft Y ^ {\prime} Z ^ {\prime}) $$

$$ = {(0 ^ {i}) \mathrm {w i t h} Y := Y Z } $$

$$ X (Y Z) \triangleleft X ^ {\prime} (Y ^ {\prime} Z ^ {\prime}) $$

(End of Proof.)

Remark I am wondering whether I am missing something or have unwittingly fooled myself by some obfuscation, for I don't remember having ever written down such a strange proof about associativity. (End of Remark.)

The next thing to investigate is how properties of the constituent relations are related to properties of the composite relation. With

(5) $\left( {\underline{R}\text{ is reflexive}}\right) \equiv \left( {\underline{A}Z : Z\underline{R}Z}\right)$ (6) (R isirreflexive) $\equiv$ (A: : ZRz)

we can formulate the

Reflexivity lemma For non-empty domains

(composite $\Delta$ is irreflexive)

(constituent $\Delta$ ’s are irreflexive)

and

(composite $D$ is reflexive)

(constituent)

Proof. In view of (1), (5), and (6), the two statements above are equivalent. It suffices to demonstrate, say, the last one.

(composite $D$ is reflexive)

$$ \begin{array}{l} = {(5) } \ (\underset {\sim} {A} X, Y::: X Y \supset X Y) \ = {2 } \ (\neg X, Y: \quad X \triangleright X \land (\neg X \triangleright X \lor Y \triangleright Y)) \ = {\mathrm {l a w o f c o m p l e m e n t} } \ (\neg X, Y:: X \triangleright X \land Y \triangleright Y) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underset {\sim} {A} X, Y: \colon X \supset X) \wedge (\underset {\sim} {A} X, Y: \colon Y \supset Y) \ = {\mathrm {r a n g e} Y \mathrm {n o n - e m p l y}; \mathrm {r a n g e} X \mathrm {n o n - e m p l y} } \ (\underset {\sim} {A X}: X \supset X) \wedge (\underset {\sim} {A Y}: Y \supset Y) \ \end{array} $$

$$ = {(5) } $$

(the constituent $D$ 's are reflexive).

(End of Proof.)

From now onwards, we restrict ourselves in view of the above to non-empty domains.

What about anti-symmetry? We recall

(7) (R is antisymmetric) $\equiv$

$$ (\exists z, z ^ {\prime}: z \overline {{R}} z ^ {\prime} \land z ^ {\prime} \underline {{R}} z: z = z ^ {\prime}) $$

Since antisymmetry is closely connected to reflexivity, we investigate the antisymmetry of $D$ . To begin with we observe for any

$$ X Y \circledast X ^ {\prime} Y ^ {\prime} \wedge X ^ {\prime} Y ^ {\prime} \circledast X Y $$

$= \left{ {\left( 2\right) ;\left( 2\right) \text{ with priming inverted }}\right}$

$$ X \circ X ^ {\prime} \wedge (\neg X ^ {\prime} D X \vee Y _ {D} Y ^ {\prime}) \wedge $$

$$ X ^ {\prime} \circ X \wedge (\neg X \circ X ^ {\prime} \vee Y ^ {\prime} \circ Y) $$

$= {$ law of complement, twice; rearranging

$$ (X \triangleright X ^ {\prime} \wedge X ^ {\prime} \triangleright X) \wedge (Y \triangleright Y ^ {\prime} \wedge Y ^ {\prime} \triangleright Y) $$

We now observe

(the composite $\triangleright$ is antisymmetric)

$= { \left( 7\right) ;\frac{5}{2} + \frac{1}{2};\frac{3}{2}}$

$$ X Y = X ^ {\prime} Y ^ {\prime} \equiv X = X ^ {\prime} \wedge Y = Y ^ {\prime} b y d e f i n i t i o n } $$

$$ \begin{array}{l} (\exists X, X ^ {\prime}, Y, Y ^ {\prime}: (X \supset X ^ {\prime} \land X ^ {\prime} \supset X) \land (Y \supset Y ^ {\prime} \land Y ^ {\prime} \supset Y): \ X = X ^ {\prime} \wedge Y = Y ^ {\prime}) \ \end{array} $$

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ (A X ^ {\prime}, X ^ {\prime}, Y, Y ^ {\prime}: (X \triangleright X ^ {\prime} \wedge X ^ {\prime} \triangleright X) \wedge (Y \triangleright Y ^ {\prime} \wedge Y ^ {\prime} \triangleright Y): X = X ^ {\prime}) \wedge \ (\neg X, X ^ {\prime}, Y, Y ^ {\prime}: (X \supset X ^ {\prime} \land X ^ {\prime} \vdash X) \land (Y \vdash Y ^ {\prime} \land Y ^ {\prime} \vdash Y): Y = Y ^ {\prime}) \ = {\mathrm {r a n g e s f o r} Y, Y ^ {\prime} \mathrm {a n d f o r} X, X ^ {\prime} \mathrm {n o n - e m p l y , s e e b e l o w} } \ (A X, X ^ {\prime}: X \triangleright X ^ {\prime} \wedge X ^ {\prime} \triangleright X: X = X ^ {\prime}) \wedge \ (A Y, Y ^ {\prime}: Y D Y ^ {\prime} \wedge Y ^ {\prime} D Y: Y = Y ^ {\prime}) \ = {(7) } \ \end{array} $$

(the constituent $D$ 's are antisymmetric).

The simplest way of ensuring that ranges of the form ${Z}^{D}{Z}^{\prime } \land {Z}^{\prime }{Z}^{D}$ are non-empty - remember that we are restricting ourselves to non-empty domains - is requiring $D$ to be reflexive. Thus we have derived the

Antisymmetry lemma If the (constituent) dis are reflexive,

(the composite $D$ is antisymmetric) $\equiv$ (the constituent $D$ 's are antisymmetric)

Remark Independent of reflexivity we have

(8) (the composite $D$ is antisymmetric) $\Leftrightarrow$ (the constituent ${D}^{\prime }$ 's are antisymmetric)

This because of $[(\underline{A}_i: P_i \wedge Q) \Leftarrow (\underline{A}_i: P_i) \wedge Q]$ , independently of range emptiness. (End of Remark.)

What about transitivity? In order to explore this, let us work out the formal expression for the transitivity of the composite $\triangleright$ :

(the composite $\Rightarrow$ is transitive) $=$ {definition of transitivity}

$$ (A X Y, X ^ {\prime} Y ^ {\prime}, X ^ {\prime \prime} Y ^ {\prime}): X Y D X ^ {\prime} Y ^ {\prime} \wedge X ^ {\prime} Y ^ {\prime} D X ^ {\prime \prime} Y ^ {\prime}; $$

$$ X Y \supset X ^ {\prime \prime} Y ^ {\prime \prime}) $$

$= \left{ {\text{pair-forming};\left( {2}^{\prime }\right) }\right}$

$$ \begin{array}{l} (\underline {{A}} X, Y, X ^ {\prime}, Y ^ {\prime}, X ^ {\prime \prime}, Y ^ {\prime \prime}; \ X \triangleright X ^ {\prime} \wedge (X ^ {\prime} \triangleleft X \vee Y \triangleright Y ^ {\prime}) \wedge X ^ {\prime} \triangleright X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangleleft X ^ {\prime} \vee Y ^ {\prime} \triangleright Y ^ {\prime \prime}): \ X \triangleright X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangleleft X \vee Y \triangleright Y ^ {\prime \prime})) \ \end{array} $$

For reflexive $D$ 's and, hence, irreflexive $A$ 's,

we obtain by instantiating the above with ${Y}{2}^{\prime }{Y}^{\prime \prime } = {Y}{2}Y$

$$ (\neg X, X ^ {\prime}, X ^ {\prime \prime}: X \triangleright X ^ {\prime} \wedge X ^ {\prime} \triangleright X ^ {\prime \prime}: X \triangleright X ^ {\prime \prime}) $$

whereas the instantiation ${X}^{\prime },{X}^{\prime \prime } \mathrel{\text{:=}} X,X$ yields

$$ (\underset {\sim} {A Y}, Y ^ {\prime}, Y ^ {\prime \prime}: Y _ {D} Y ^ {\prime} \wedge Y ^ {\prime} D Y ^ {\prime \prime}: Y _ {D} Y ^ {\prime \prime}) $$

Hence we have established the

First transitivity lemma For reIeXive $D^{\prime}s$

(the composite $\Rightarrow$

(the constituent $D$ 's are transitive)

and

(the composite $\Delta$ is transitive) $\Rightarrow$

(the constituent $A$ ’s are transitive)

The second half is proved similarly, with (0') instead of (2'), i.e with $\land , \triangleright$ interchanged with $\lor , \triangleleft$ .

How can we derive transitivity of the composite relations? To this end we observe for any $X, Y, X', Y', X'', Y''$

$$ \begin{array}{l} X Y _ {D} X ^ {\prime} Y ^ {\prime} \wedge X ^ {\prime} Y ^ {\prime} D X ^ {\prime \prime} Y ^ {\prime \prime} \ = {(2 ^ {\prime}) } \ X \triangleright X ^ {\prime} \wedge (X ^ {\prime} \triangleleft X \vee Y \triangleright Y ^ {\prime}) \wedge X ^ {\prime} \triangleright X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangleleft X ^ {\prime} \vee Y ^ {\prime} \triangleright Y ^ {\prime \prime}) \ \Rightarrow {\mathrm {D i g k s t r a} ^ {\prime} \mathrm {L a w s}: X ^ {\prime} \triangle X \wedge X ^ {\prime} \triangle X ^ {\prime} \Rightarrow X ^ {\prime} \triangle X \quad \mathrm {a n d} \ X \triangleright X ^ {\prime} \wedge X ^ {\prime \prime} \triangleleft X ^ {\prime} \Rightarrow X ^ {\prime \prime} \triangleleft X \rbrace \ X \triangleright X ^ {\prime} \wedge (X ^ {\prime \prime} \triangle X \vee Y \triangleright Y ^ {\prime}) \wedge X ^ {\prime} \triangle X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangle X \vee Y ^ {\prime} \triangleright Y ^ {\prime \prime}) \ = {\text {r e a r r a n g i n g ;} v \text {d i s t i b u t e s o v e r} \land } \ (X \triangleright X ^ {\prime} \land X ^ {\prime} \triangleright X ^ {\prime \prime}) \land (X ^ {\prime \prime} \triangleleft X \lor (Y \triangleright Y ^ {\prime} \land Y ^ {\prime} \triangleright Y ^ {\prime \prime})) \ \Rightarrow {\mathrm {t h e c o n s t i t u e n t} D \mathrm {a r e t r a n s i t i v e} } \ X \triangleright X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangleleft X \vee Y \triangleright Y ^ {\prime \prime}) \ = \left{\left(2 ^ {\prime}\right) \right} \ X Y \supset X ^ {\prime \prime} Y ^ {\prime \prime} \ a n d s i m i l a r l y (t h o u g h n o t q u i t e) \ X Y \triangleleft X ^ {\prime} Y ^ {\prime} \wedge X ^ {\prime} Y ^ {\prime} \triangleleft X ^ {\prime \prime} Y ^ {\prime \prime} \ = {0 ^ {\prime} } \ (X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \triangleright X \wedge Y \triangleleft Y ^ {\prime})) \wedge (X ^ {\prime} \triangleleft X ^ {\prime \prime} \vee (X ^ {\prime \prime} \triangleright X ^ {\prime} \wedge Y ^ {\prime} Y ^ {\prime \prime})) \ \Rightarrow {D y k s t r a i s l a w s a n d t r a n s i t i v i t y o f 4 o n \ \mathrm {t h e} \times \mathrm {d o m a i n}) \ (X _ {\Delta} X ^ {\prime \prime}) \vee (X ^ {\prime} D X \wedge Y _ {\Delta} Y ^ {\prime})) \wedge (X _ {\Delta} X ^ {\prime \prime} \vee (X ^ {\prime \prime} D X ^ {\prime} \wedge Y _ {\Delta} ^ {\prime} Y ^ {\prime})) \ = {v d i s t r i b u t e s o v e r \wedge ; r e a r r a n g i n g } \ X \triangleleft X ^ {\prime \prime} \vee (X ^ {\prime} \triangleright X \wedge X ^ {\prime \prime} \triangleright X ^ {\prime} \wedge Y _ {\triangleleft} Y ^ {\prime} \wedge Y _ {\triangleleft} ^ {\prime} Y ^ {\prime \prime}) \ \Rightarrow {\triangleright \mathrm {t r a n s i t i v e} X \mathrm {d o m a i n}, \triangleleft \mathrm {t r a n s i t i v e} Y \mathrm {d o m a i n} } \ X \triangle X ^ {\prime \prime} \vee (X ^ {\prime \prime} \triangleright X \wedge Y \triangle Y ^ {\prime \prime}) \ = {(\mathbf {0} ^ {\prime}) } \ X Y \triangleleft X ^ {\prime \prime} Y ^ {\prime \prime} \ \end{array} $$

All this is quite messy. When the ATAC read my earlier version -which was less messy-, Edgar Knapp detected an error in my calculations -I had treated a strengthening as if it were a weakening: peccavi! -; shortly thereafter, Josyula R. Rao established that Dgksha's Laws for the X domain provided a way out. In EWD1038 -which was written while I worked on this note- I had established that Dgksha's Laws hold in a linear order, that is

$$ z > z $$

(Reflexivity)

$$ Z \supset Z ^ {\prime} \land Z ^ {\prime} D Z \Rightarrow Z = Z ^ {\prime} $$

(Anisymmetry)

$$ z \triangleright z ^ {\prime} \wedge z ^ {\prime} \triangleright z ^ {\prime \prime} \Rightarrow z \triangleright z ^ {\prime \prime} $$

(Transitivity)

$$ 2 \triangleright 2 ^ {\prime} \vee 2 ^ {\prime} \triangleright 2 $$

(Linear)

EWD1038 also shows that for reflexive $D$ and transitive $\Delta$ , $D$ satisfies the linearity requirement $Z \nrightarrow {Z^{\prime}} \lor Z^{\prime} \nrightarrow {Z}$ . Collecting all our observations, we had better formulate, instead of a second transitivity lemma, the

Linear order lemma

(the constituent $D$ 's are linear orders)

(the composite $D$ is a linear order).

The moral of the story is that, in connection with lexical coupling, there is little point in studying transitivity in isolation, and that even the partial order - i.e. reflexive, antisymmetric, and transitive, but not necessarily linear- is not a relevant concept.

This moral is fine with me. As will transpire in the remainder of this note, a much more inter-reshing link is the connection between lexical coupling and well-foundedness and -as W.H.J.Fegen had already pointed out to me - the latter notion has nothing to do with transitivity. The usual term "lexical order" is an overspecific misnomer!

For a set $C$ and a relation $D$ defined on that set we have by definition

$$ ((C, D) i s w e l l - f o u n d e d) \equiv $$

$$ (\underline {{A}} S: S \neq \varnothing : (\underline {{E}} Z ^ {\prime}: Z ^ {\prime} \in S: (\underline {{A}} Z: Z \in S: Z \supset Z ^ {\prime})) $$

where the dummy S ranges over the subsets of C. Notice that (p,p) is trivially well-founded. Further, more, by instantiating $S\coloneqq {Z^n}$ for any $Z^{\prime \prime}\in C$ we derive

$$ \begin{array}{l} ((C, D) i s w e l l - f o u n d e d) \ = {\mathrm {d e f i n i t i o n o f w e l l - f o u n d e d n e s s} } \ (\neg A S: S \neq \emptyset : (\exists Z ^ {\prime}: Z ^ {\prime} \in S: (\neg A Z: Z \in S: Z \triangleright Z ^ {\prime})) \ \Rightarrow \quad {\mathrm {i n s t a n t i a t e} S := {z ^ {\prime \prime} } \mathrm {w i t h} z ^ {\prime \prime} \in C, \mathrm {h e n c e} \ {Z ^ {\prime \prime} } \subseteq C \quad a n d {Z ^ {\prime \prime} } \neq \varnothing } \ (\underline {{A}} Z ^ {\prime}: Z ^ {\prime} \in C: (\underline {{E}} Z ^ {\prime}: Z ^ {\prime} \in {Z ^ {\prime} }: (\underline {{H}} Z: Z \in {Z ^ {\prime} }: Z \triangleright Z ^ {\prime})) \ = {Z \in {Z ^ {\prime \prime} } \equiv Z = Z ^ {\prime \prime}; \mathrm {o n e - p o i n t r u l e t w i c e} } \ (A Z ^ {\prime \prime}: Z ^ {\prime \prime} \in C: Z ^ {\prime \prime} \supset Z ^ {\prime \prime}) \ = {\mathrm {d e p i n i t i o n o f r e f l e x i v i l y} } \ (D \mathrm {i s r e f l e x i v e}) \ \end{array} $$

Thus we have established

Well-foundedness $\Rightarrow$ reflexivity lemma:

Let us now try to relate the well-foundedness of the composite $D$ to the well-foundedness of the constituent $D$ 's. With $X$ ranging over $\overline{X}$ and $Y$ over $\overline{Y}$ , $XY$ ranges over the Cartesian product $\overline{X} \times \overline{Y}$ . In the following, $W$ ranges over the subsets of $\overline{X} \times \overline{Y}$ and we shall restrict our-selves to non-empty $\overline{X} \times \overline{Y}$ , i.e non-empty $\overline{X}$ and non-empty $\overline{Y}$ .

What can we conclude from well-foundedness of the composite $D$ ? Let us explore

$$ \begin{array}{l} ((C, D) \mathrm {i s w e l l - f o u n d e d}) \Rightarrow \ (\Delta \mathrm {i s r e f l e x i v e}) \ ((\overline {{X}} \times \overline {{Y}}, \triangleright) i s w e l l - f o u n d e d) \ = {\mathrm {d e f i n i t i o n o f w e l l - f o u n d e d n e s s}; \mathrm {p r e v i o u s l e m m a} } \ (\underline {{A}} W: W \neq \phi : (\underline {{E}} X ^ {\prime} Y ^ {\prime}: X ^ {\prime} Y ^ {\prime} \in W: (\underline {{A}} X Y: X Y \in W: X Y \triangleright X ^ {\prime} Y ^ {\prime})) \land \ (c o m p o s i t e \triangleright i s r e f l e x i v e) \ \Rightarrow \quad {\mathrm {I n s t a n t i a t e w i t h} \ W := (\underline {{S E T}} X: X \in U: X Y ^ {\prime \prime}) \mathrm {w i t h} U \subseteq \overline {{X}}, Y ^ {\prime \prime} \in \overline {{Y}} \quad \mathrm {a n d} \ W := (\mathrm {S E T} Y: Y \in V: X ^ {\prime \prime} Y) \mathrm {w i t h} V \subseteq \bar {Y}, X ^ {\prime \prime} \in \bar {X} \ (\underline {{A}} U: U \neq \varnothing : (\underline {{E}} X ^ {\prime}: X ^ {\prime} \in U: (\underline {{A}} X: X \in U: X Y ^ {\prime \prime} D X ^ {\prime} Y ^ {\prime})))) \wedge \ (\underline {{A}} V: V \neq \varnothing : (\underline {{E}} Y ^ {\prime}: Y ^ {\prime} \in V: (\underline {{A}} Y: Y \in V: X ^ {\prime \prime} Y \supset X ^ {\prime \prime} Y ^ {\prime})) \land \ (c o m p o s i t e \Delta) i s r e f l e x i v e) \ = {(2 ^ {1}) \mathrm {a n d R e f l e x i v i t y l e m m a} } \ (\underline {{A}} U: U \neq \varnothing : (\underline {{E}} X ^ {\prime}: X ^ {\prime} \in U: (\underline {{A}} X: X \in U: \ X \triangleright X ^ {\prime} \wedge (X ^ {\prime} \triangleleft X \vee Y ^ {\prime \prime} Y ^ {\prime \prime}))))) \wedge \ \end{array} $$

$$ \begin{array}{l} (A V: V \neq \emptyset : (E Y ^ {\prime}: Y ^ {\prime} \in V: (A Y: Y \in V: \ X ^ {\prime \prime} \triangleright X ^ {\prime \prime} \wedge (X ^ {\prime \prime} \triangleleft X ^ {\prime} \vee Y _ {\triangleright} Y ^ {\prime})))) \wedge \ \end{array} $$

$$ (t h e c o n s t i t u e n d i s a r e r e f l e x i v e) $$

$$ \begin{array}{l} \Rightarrow (\neg U: U \neq \phi : (\exists X ^ {\prime}: X ^ {\prime} \in U: (\neg X: X \in U: X \triangleright X ^ {\prime})))) \land \ (\underset {\sim} {A} V: V \neq \varnothing : (\underset {\sim} {E} Y ^ {\prime}: Y ^ {\prime} \in V: (\underset {\sim} {A} Y: Y \in V: Y \supset Y ^ {\prime}))) \ = {\mathrm {d e f i n i t i o n o f w e l l - f o u n d e d n e s s} } \ ((X, \triangleright) i s w e l l - f o u n d e d) \land \ ((\bar {Y}, \Delta) i s w e l l - f o u n d e d) \ \end{array} $$

Thus we have established our

First well-foundedness lemma For nonempty domains

(the composite $D$ is well-founded) $\Rightarrow$

(the constituent $D$ 's are well-founded)

(Here we treat well-foundedness as a property of the relation, leaving each time the domain understood.)

The next question to tackle is -not surprisingly how we can conclude that the composite $D$ is well-founded. We propose to demonstrate that $(\overline{X} \times \overline{Y}, D)$ is well-founded by constructing for "non-empty $W \subseteq \overline{X} \times \overline{Y}$ a "witness" for the existential quantification, i.e. we shall construct a $X''Y''$ such that

(9) ${X}^{\prime \prime }{Y}^{\prime \prime } \in W$

and

(10) $\underset{\sim }{A}{X}_{Y} : {XY} \in W : XY \circ {X}^{\prime \prime }{Y}^{\prime \prime }$ )

With (2') and predicate calculus, we can rewrite (10) as the conjunction of

(10 a) $\left( {A,{X}_{Y} : X{Y}^{c} \in W : X \upharpoonright {X}^{\prime }}\right)$ and $\left( {1,0,b}\right) \;\left( {\underline{A}X,Y : XY \in W : {X}^{\prime \prime }A{X}^{\prime }V{Y}^{\prime }D{Y}^{\prime \prime }}\right)$

Requirement (10a) is a good start, because it does not contain $Y''$ . Let us therefore isolate dummy $Y$ as well:

(10 a) $= {$ nesting and trading $}$

$$ (\neg X: (\neg A Y: \neg X Y \in W \lor X \triangleright X ^ {\prime})) $$

$= { v$ distributes over $A}$

$$ (A X: (A Y: \neg X Y \in W) \vee X D X") $$

[\left{ \begin{array}{l} \text{trading} \ \end{array}\right} ]

$$ (\exists X: \because (E Y: X Y \in W): X \triangleright X") $$

$= \left{ \left( {11}\right) }$

$$ (\neg X:: X \in U: X \triangleright X") $$

For non-empty $U$ such that $U \subseteq \bar{X}$ and well-founded $\left( {\bar{X},D}\right)$ we can thus choose an ${X}^{\prime \prime }$ satisfying ${X}^{\prime \prime } \in U$ and (10a); $U$ is non- empty and a subset of $\bar{X}$ because $W$ is a non-empty subset of $\bar{X} \times \bar{Y}$ and $U$ is given by

(11) $X \in U \equiv (\exists Y: X Y \in W)$ .

We note that, since $X'' \in U$ , (11) implies

(12) (EY: X"YεW).

We now restrict ourselves to well-founded $\left( {\bar{X},\bar{D}}\right)$ ,so an ${X}^{\prime \prime }$ can be chosen. With the chosen ${X}^{\prime \prime }$ ,we rewrite (10b) as the conjunction of

(10c) $\left( {\underline{A}X,Y : XY \in W \land X = {X}^{\prime } : X\prime \Delta X \vee Y\prime Y}\right)$ and $\left( {1,0}\right) \;\left( {1,2}\right) : X \neq X\left( {1,3}\right) : X \neq X$

because we can now eliminate dummy $X$ from (10c)

(10c) $= \left{ \begin{array}{ll} \text{one - point rule } \ \end{array}\right}$

$\left( {A{Y}{1} : {X}^{\prime \prime }{Y}{1} \in W : {X}^{\prime \prime }{A}^{\prime }{X}^{\prime \prime } \vee {Y}_{1}{Y}^{\prime \prime }}\right)$ $= \left{ {\left( {\bar{X},\bar{D}}\right) \text{ well - founded ,hence reflexive }}\right}$

$\left( {A{Y}_{1} : {X}^{\prime \prime }{Y}^{\prime } \in W : Y \supset {Y}^{\prime \prime }}\right)$

Because of (12), the range $X''Y \in W$ is nonempty; because $W \subseteq \overline{X} \times \overline{Y}$ , its solution set is a subset of $\overline{Y}$ ; for well-founded $(\overline{Y}, D)$ , we can thus choose a $Y''$ , satisfying $X''Y'' \in W$ and $(10c)$ . We now restrict ourselves to well-founded $(\overline{Y}, D)$ as well, and deem $Y''$ chosen. Notice that, in the mean time, (9) has been satisfied as well; (10d), however has still to be demonstrated (10d) [\left{ \text{predicate calculus}\right} ]

(HXY: XY∈W ∧ X≠X": X"ΔX)

$= {$ trading $;\left( 1\right) }$ (HXY:XYeW:1X"DXvX=X")

(13)

$$ \begin{array}{r l} & {\mathrm {(A X Y : X Y \in W : X _ {D} X ^ {\prime \prime})}} \ {=} & {{(1 0 a) }} \ & {\mathrm {f r u e}} \end{array} $$

with

$$ (1 3) \quad (\neg X. X ^ {\prime \prime}:: X \triangleright X ^ {\prime \prime} \land X ^ {\prime \prime} \triangleright X \Rightarrow X = X ^ {\prime \prime}) $$

i.e. on $\overline{X}$ ,the constituent relation $D$ is antisymmetric. Thus we have derived - see (8)-

Second well-foundedness lemma

(the constituent $D$ 's are well-founded and antisymmetric) $\Rightarrow$ (the composite $D$ is well-founded and antisymmetric)

Note We only proved it for non-empty $\overline{X} \times \overline{Y}$ ; for empty $\overline{X} \times \overline{Y}$ , the theorem is trivially correct. (End of Note)

Combining the lemmata on reflexivity, anti-symmetry and well-foundedness, we conclude the

Lexical Theorem For non-empty domains

(the constituent $D$ are reflexive,antisymmetric, and well-founded)

(the composite $D$ is reflexive,antisymmetric, and well-founded)

(Reflexivity, however, is implied by well-foundedness.)

Reflexivity of $D$ ,usually expressed as

$$ z > z $$

can equivalently be expressed by

$$ z = z ^ {\prime} \Rightarrow z > z ^ {\prime} \land z ^ {\prime} > z $$

Since antisymmetry states

$$ z = z ^ {\prime} \Leftrightarrow z \triangleright z ^ {\prime} \land z ^ {\prime} \triangleright z $$

(4) (D is reflexive and antisymmetric) $\equiv$

$$ (\neg Z, Z ^ {\prime}: \quad Z = Z ^ {\prime} \equiv Z \triangleright Z ^ {\prime} \land Z ^ {\prime} \triangleright Z) $$

which enables us to rewrite (0') for reflexive,

antisymmetric

$$ \begin{array}{l} X Y \triangleleft X ^ {\prime} Y ^ {\prime} \ = {0 ^ {\prime} } \ X \triangleleft X ^ {\prime} \vee (X ^ {\prime} \triangleright X \wedge Y \triangleleft Y ^ {\prime}) \ = {\mathrm {L a w o f C o m p l e m e n t} } \ X \triangleleft X ^ {\prime} \vee (\neg X \triangleleft X ^ {\prime} \wedge X ^ {\prime} \triangleright X \wedge Y \triangleleft Y ^ {\prime}) \ = \left{ \begin{array}{l} (1) \end{array} \right} \ X \triangle X ^ {\prime} \vee (X \triangle X ^ {\prime} \wedge X ^ {\prime} \triangle X \wedge Y \triangle Y ^ {\prime}) \ = {(1 4): D \mathrm {i s r e f l e x i v e a n d a n t i s y m m e t r i c} } \ X \triangleleft X ^ {\prime} \vee (X = X ^ {\prime} \wedge Y \triangleleft Y ^ {\prime}) \ \end{array} $$

which is the more familiar way in which the lexical coupling is defined. Note that transitivity and linearity - i.e. ${Z}^{D}{Z}^{\prime } \vee {Z}^{\prime }{Z}^{ - }$ still do not enter the picture.

￥

For the sake of completeness we mention that the important theorem

$$ ((C, \triangleright) i s w e l l - f o u n d e d) \equiv $$

(all decreasing chains in $C$ are finite)

is independent of further properties of $\pmb{\theta}$ . A decreasing chain is a sequence of elements $K_n$ from $C$ such that

$$ (\exists n: n \geq 0: K. (n + 1) \triangleleft K. n) $$

To establish this theorem, we negate both sides and apply the definition of well-foundedness

$$ (E S: S \neq \varnothing : (A Z ^ {\prime}: Z ^ {\prime} \in S: (E Z: Z \in S: Z \triangleleft Z ^ {\prime})) \equiv $$

(there exists an infinite decreasing chain in $C$ )

Proof LHS $\Rightarrow$ RHS

Let $S^n$ be a witness for the LHS. We can choose an arbitrary element of $S^n$ for $K, O$ ; instantiating $Z' := K.n$ , the LHS states that we can choose an element $Z$ of $S^n$ as $K.(n+1)$ such that $K.(n+1) \triangleleft K.n$ .

LHS

Let $K$ be a witness for the RHS, i.e. let $K.n$ be an infinite decreasing chain in $C$ . Then $S'' = {S} n: n \geqslant 0: K.n}$ is a witness for the LHS.

(End of Proof.)

Concluding remarks

There were a variety of reasons for writing this note.

Firstly, it has been written "for the record" in the sense that I felt that the lexical coupling is of interest in its own right, while I had never seen a decent theory developed for it. Hence it seemed worthwhile to develop such a theory and record its results, thus creating a little work of reference.

Secondly, I knew from earlier experiences - perhaps as much as ten years ago, when I derived some isolated results- that it is only too easy to make a mess of a formal treatment. Let me describe some of the pitfalls for the better appreciation of the complications I avoided this time.

One can start with integer sequences $X, X'$ of length $N$ and define the lexical order $X \prec X'$ by

$$ \begin{array}{l} X \prec X ^ {\prime} \equiv (\underline {{E}} _ {j}: 0 \leq j \land j < N: X _ {j} < X ^ {\prime}. j \land \ (\underset {\sim} {A} i: 0 \leq i \land i < j: X. i = X ^ {\prime}. i)) \ \end{array} $$

I once did that - after all, this was the way in which I was introduced to the notion of lexical order. The nett effect is that one finds oneself manipulating quantified expressions all the time, splitting ranges, shifting origins and the whole lot. Hence, elimination of the "subscripts" was one of my first

goals.

With $X, {X}^{\prime }$ still standing for integer sequences of some length, and ${Y}_{1}{Y}^{\prime }$ similarly interpreted. I found myself considering

$$ X Y \prec X ^ {\prime} Y ^ {\prime} \equiv X \prec X ^ {\prime} \vee (X = X ^ {\prime} \wedge Y \prec Y ^ {\prime}) $$

but immediately two warning signals start flashing. Firstly, for one-character sequences $x,x^{\prime}$ ,one has to define

$$ x < x ^ {\prime} \equiv x < x ^ {\prime}; $$

Secondly, by the time one considers the associativity of the lexical coupling, one has to define - not unnat

urely, but yet!

$$ X Y = X ^ {\prime} Y ^ {\prime} \equiv X = X ^ {\prime} \wedge Y = Y ^ {\prime} $$

Note The second warning signal is a red herring.

which is a different pattern of relating constituent relations with the composite relation.

When I started on this note, I knew that I wanted to focus on the associative lexical coupling rather than on the lexical order of pairs of sequences of arbitrary length. I expected order -in particular transitivity- to play a less central role than I had tacitly assumed; the reason for this expectation was the close connection between the lexical coupling and well-foundedness, together with the -rather recent- insight that well-foundedness has nothing to do with transitivity. Finally I was annoyed by

the equality sign in (15). You see, it immediately raises the question how to define $<$ in terms of $2$ , viz.

$$ x < y \equiv y \geq x \land \neg x = y \quad \mathrm {o r} \quad x < y \equiv \neg x \geq y $$

Without equality, the latter definition is forced upon us. Because of the connotations of $<$ and $>$ with the real number line, where the above distinction is irrelevant, I chose $<$ and $>$ respectively, where the former would be reserved for the reflexive relation, and the latter one for the reflexive relation.

I have experimented with different symbols for the constituent relations and the composite one; at one time, (o) defined all in terms of $a$

$$ X Y \triangleleft X ^ {\prime} Y ^ {\prime} \equiv X \triangleleft X ^ {\prime} \vee (\neg X ^ {\prime} \triangleleft X \wedge Y \triangleleft Y ^ {\prime}) $$

but this was a forseeable -though not forseen- notational mistake: as soon as I had to deal with associativity, the inner $\Delta$ had to play the role of an outer $\Delta$ . I abolished the symbol $\Delta$ at the price of introducing the adjectives "consti-tuent" and "composite". (Since these terms are now introduced right at the beginning, you can conclude that some work was done before I started on this note. The trick shows the greater abstractive power of two adjectives versus the absence or presence of a vertical stroke: the adjectives can be omitted, or,

as the case may be, implied by the context.)

In order not to interrupt the flow of the presentation, I have proposed (0) as an unmitigated rabbit, but the occurrence of the term $7 \times 4 X$ is not as sur- prising as it might seem at first sight. Firstly, be- cause negation and interchange of the arguments are each its own inverse, their combination is so as well. Secondly, if $A$ is transitive, it is "weakening" with respect to its right-hand argu- ment and "strengthening" with respect to its left-hand argument:

$$ a \triangleleft b \wedge b \triangleleft c \Rightarrow a \triangleleft c $$

can be equivalently expressed as

$$ \begin{array}{l} b \triangle c \Rightarrow (a \triangle b \Rightarrow a \triangle c) \qquad o r \quad a s \ a \triangle b \Rightarrow (a \triangle c \Leftarrow b \triangle c) \ \end{array} $$

Both negation and interchange of the arguments invert this sense of monotonicity; their combination leaves this sense of monotonicity intact. Thus the - sweetly reasonable- desire to make $X$ a $X^{\prime}Y^{\prime}$ (usually) a monotonic function of $X$ and $Y$ . It makes (0) somewhat less of a rabbit. All this is suitably vague, as hunches usually are. The Duality lemma would have survived the omission of the negation in (0) (and accordingly in (2)); the Associativity lemma would not have done so.

In formula (1) I introduced $D$ besides $A$ .

A minor benefit is the reduction of the number of negation signs that have to be written down. The major benefit is that it enables us to maintain the symmetry and to talk about the pair of relations $\Delta$ and $D$ without considering the one more "fundamental" than the other. (Note that, without both of them being available, for instance the Second transitivity lemma would have been an ugly one to formulate.)

The attentive reader will have noticed that by the time the first page of this note had been written, all important decisions had been taken; the scene having been set, the rest was formal routine in the sense that the symbols did the work.

Writing this note was an instructive experience: it so happened that I had hardly done any formal mathematics for about a month and I noticed that I needed several pages of manipulation before the necessary hand-eye coordination was back. Thereafter, this note was a relaxing joy to write.

Austin, 16 January 1989

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 United States of America

PS. With thanks to ATAC! EWD