The wife-swapping couples once more (See EWD1103 and EWD1115)

The wife- swapping couples once more (See EwD1103 and EwD1115)

Here is the problem. About a positive number of couples, we are given

(0) the maximum age among the husbands equals the maximum age among the wives, and (1) were two couples to engage in a wife swap, then the minimum age in the one new combination would equal the minimum age in the other new combination, and now have to demonstrate (2) in each couple, husband and wife are of the same age.

The standard argument is as follows. Lemma There exists a couple of which both husband and wife are of maximum age.

Proof Select a husband of the maximum age $H$ ; select a wife of the maximum age $W$ ( $= H$ , according to (0)). Either these two form a couple, and we are

done, or there are two couples $(H, w)$ and $(h, w)$ , from whose existence (1) allows us to conclude

$$ H \downarrow W = h \downarrow W $$

because $H = W$ , $H > h$ ,and $W > w$ ,we con- clude $H = h$ and $W = w$ : a person of maximum age has a spouse of maximum age. (End of Proof.)

To prove (2) we now consider an arbitrary couple $(h, w)$ , other than the couple $(H, W)$ , whose existence is guaranteed by the Lemma. From (1) we now conclude

$$ H \downarrow W = h \downarrow W, $$

but because of $H = W \geq w$ and $W = H \geq h$ , this simplifies to

$$ w = h $$

quod erat clemonsstrandum.

The above argument is ugly: Methusalem and his equally old wife are treated differently from the others, and , consequently, the argument appeals to (1) twice. To remedy the situation, we are going to have a second look at (1).

To dissociate ourselves from the previous argument, let us introduce new iden- tifiers: variables $x,y$ are of type "couple", m.x denotes the age of the male in couple x , and f.x denotes the age of the female in couple x . In this terminology we can express (1) by stating that

(3) $m \cdot x \downarrow {f}{y} = m \cdot y \downarrow {f}{x}$

holds for any pair of couples x and y. But we can drop the constraint $x \neq y$ because (thanks to Leibniz's Principle)

(3) also holds in the case $x = y$ . (This generalization of (1), which significantly contributes to the greater simplicity of the alternative arguments, is hard to express verbally; this simple example strikingly illustrates what formulae can do for you.) In EWDII03 - and in EWDII15 with much more comments- (0) is expressed as

$$ \langle \uparrow y:: m. y \rangle = \langle \uparrow y:: f. y \rangle $$

and the calculational demonstration of $m.x = f.x$ then uses of the $\uparrow \downarrow$ -calculus the Law of Absorption and that $\downarrow$ distributes over $\uparrow$ . The heuristics, as given in EWD1115, for the design of the calculation are quite

convincing.

Today we play a different game and explore what we can derive, starting from (3) all by itself. Formula (3) is amazingly symmetric: because of the symmetry of $\downarrow$ , left-hand side and right-hand side get inter-changed under the substitution $m, f := f, m$ , but also under the substitution $x, y := y, x$ . As a consequence of the latter symmetry and the fact that (3) is universally quantified over $x, y$ , our given is not weakened when we replace (3) by the formally weaker

$m \cdot x \downarrow {f}{y} \leq m \cdot y \downarrow {f}{x}$

Having thus destroyed the symmetries, we can explore what we can derive about one of the couples, y say. Here we had better use the properties of $\downarrow$ and $\leq$ . We observe,for any $x,y$

true $\left{ \begin{array}{l} \left( 4\right) } \ m \cdot x \downarrow f \cdot y \leq m \cdot y \downarrow f \cdot x \ \Rightarrow \left{ \begin{array}{l} p \downarrow q \leq p \ m \cdot x \downarrow f \cdot y \leq m \cdot y \end{array}\right. \end{array}\right.$

$$ m. x \downarrow f. y \leq m. y $$

$$ \Rightarrow \quad {\mathrm {p r e d . c a l c . a n d L e i b n i z} } $$

$$ m \cdot x \downarrow f \cdot y = f \cdot y \Rightarrow f \cdot y \le m \cdot y $$

$$ = {p \downarrow q = q \equiv q \downarrow p } $$

$$ (5) p. y \leq m. x \Rightarrow p. y \leq m. y $$

Conclusion (5) holds for any $x,y$ ,i.e. for any mrs.y we conclude that the existence of a single husband at least her age implies that her own husband is at least her age.

From (5) and the $m/f$ symmetry of (3) we conclude

(6) $m.y \leq {p.x} \Rightarrow m.y \leq {p.y}$

and, with (5) and (6), (0) evidently

allows us to conclude $m.y = {Fy}$ for

any $y$ .

Austin, 20 April 1996

pror. dr. Edsger W. Dgksta

Department of Computer Sciences The University of Texas at Aust

Austin, TX 78712 - 1188

USA