A monotonicity argument revisited
EWD1014 · 1987–1991 · PDF · Source language: English. · Local OCR-derived source needs manual review.
A monotonicity argument revisited
(This is derived from Avg36/EWD 878 d.d. 22 Feb. 1984.)
Square brackets denote universal quantification over $x$ and $y$ . Function $f$ satisfies
$$ [ x < y \Rightarrow f. x. y < f. y. x ] \tag {0} $$
We observe
(0)
$$ \begin{array}{l} = {p < q \equiv q > p } \ [ y > x \Rightarrow f. y. x > f. x. y ] \ = {\mathrm {c h a n g e d u m m i e s} x, y := y, x } \ [ x > y \Rightarrow p. x. y > p. y. x ] \ \Rightarrow {\mathrm {p a i r - w i s e d i s j u n c t i o n w i t h} (0); \ p < q \vee p > q \equiv p \neq q } \ [ x \neq y \Rightarrow f _ {x} \cdot y \neq f _ {y} \cdot x ] \ = {\mathrm {c o n t r a p o s i t i v e} } \ [ x = y \Leftarrow f. x. y = f. y. x ] \ = {\mathrm {L e i b n i z}: [ x = y \Rightarrow f. x. y = f. y. x ] } \ [ x = y \equiv f. x. y = f. y. x ] \quad (1) \ \end{array} $$
Consider in triangle
We were taught two theorems
"The sides opposite to equal angles are equal" or
$$ [ a = \beta \Rightarrow a = b ] \tag {2} $$
"The angles opposite to equal sides are equal" or
$$ [ \alpha = \beta \Leftarrow a = b ] \tag {3} $$
The theorems were proved separately; both were geometrical proofs using congruent triangles. Prior to that it had already been shown that opposite to the larger angle lies the larger side, i.e.
$$ [ a < \beta \Rightarrow a < b ] \quad (4) $$
Consider now, for fixed $c$ ,a and $b$ functions of $\alpha$ and $\beta$ . For reasons of symmetry a is the same function of $\left( {\alpha ,\beta }\right)$ as $b$ is of $\left( {\beta ,\alpha }\right)$ ,i.e. for some $p$ we have
$$ a = f. \alpha . \beta \qquad a n d \quad b = f. \beta . \alpha $$
Substituting this in (4) we see that this $f$ satisfies (0), hence, on account of (1) we immediately get, as logical consequence
$$ [ \alpha = \beta \equiv a = b ] $$
i.e. the conjunction of (2) and (3): the geometrical proofs with the congruent triangles are superfluous. The proofs were an obfuscation.
A similar pair of theorems is
"An isosceles triangle has two angle bisectors of equal length and
"A triangle with two angle bisectors of equal length is isosceles".
The one is considered easy to prove, the other one difficult. Thanks to the above, both theorems are subsumed in "The larger angle has the shorter bisector.", which follows from the formula for the length of the bisector of $\alpha$ :
$$ \sqrt {b \cdot c \cdot (1 - (\frac {a}{b + c}) ^ {2})} $$
which is a decreasing function of $a$ and an increasing function of
The above suggests that, in the way in which geometry is taught, logic is underexploited. Historically understandable, but regrettable all the same.
22 October 1987
prof. d. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA