A supplement to EWD878

A supplement to EWD878

In EWD878, A.J.M. van Gasteren and I showed that for any $p$

[ x < y ⇒ f \cdot x y < f \cdot y \cdot x ] ⇒ [ x = y \equiv f \cdot x y = f \cdot y \cdot x ]

(where universal quantification over $x$ and $y$ is denoted by a pair of square brackets).

We then remarked without further comment that

(0) "An isosceles triangle has to equal angles" and (1) "A triangle with two equal angles is isosceles" immediately follow from "opposite to the larger angle lies the larger side", the latter being of the form $[\alpha < \beta ⇒ a < b]$ , and the conjunction of (0) and (1) being of the form $[\alpha = \beta \equiv a = b]$

This, however was a bit brief, as we failed to show how $a$ and $b$ were functions of $\alpha$ and $\beta$ . The answer is to consider triangles with fixed $c$ and with $\alpha$ and $\beta$ satisfying $0 ≤ \alpha , 0 ≤ \beta , \alpha + \beta < \pi$ :

Without showing a function $f$ that does the job, the appeal to our former result is unwarranted.

There is an alternative approach that does not require the functional dependence. Let the square brackets denote universal quantification over $a, b, \alpha$ and $\beta$ ; let $R$ be symmetric in the pairs $(a, \alpha)$ and $(b, \beta)$ , i.e.

[ R \equiv R _ {b, \beta , a, \alpha} ^ {a, \alpha , b, \beta} ]

Then

(2) $\left\lbrack {R ⇒ \left( {\alpha < \beta \equiv a < b}\right) }\right\rbrack ⇒ \left\lbrack {R ⇒ \left( {\alpha = \beta \equiv a = b}\right) }\right\rbrack$

\begin{array}{l} \mathrm {P r o o f} [ R ⇒ (\alpha < \beta \equiv a < b) ] \ = {\text {p r e d . c a l c} } \ [ R ⇒ (\alpha ≥ \beta \equiv a ≥ b) ] * \ = {\mathrm {s y m m e t r y} o p R } \ [ R ⇒ (\beta ≥ a \equiv b ≥ a) ] \ = {\mathrm {p r o p .} \varphi ≥ \mathrm {a n d} ≤ } \ [ R ⇒ (a ≤ b \equiv a ≤ b) ] \ ⇒ {\mathrm {c o n j u n c t i o n w i t h} * } \ [ R ⇒ (\alpha = \beta \equiv a = b) ] \ \end{array}

(End of Proof.)

The convenience of (2) is that we need no bother about functional dependence: $R$ could be "a and b are in a triangle the sides opposite to $\alpha$ and $\beta$ respectively". The antecedent, however, contains an equivalence.

Austin, 2 October 1986

prof. dr. Edsger W. Dyrksta

Department of Computer Sciences The University of Texas at Austin

Austin, TX 78712- 1188, USA