Proving an implication via its converse

Proving an implication via its converse

This note deals with a theorem that is often used - for instance in as different areas as equational theory, geometry, and functional programming. but rarely mentioned explicitly. It first gives and proves the theorem, and then illustrates its use with a (famous!) geometric example.

In the following, variables x,y range over some - possibly unusual, but wellunderstood-type , while boolean functions f,g are predicates on that type. (Function application being denoted by an infix dot, this means that for instance f.x and g.y are boolean expressions. Below, each equation is denoted by its boolean expression, prefixed by its unknown, followed by a colon.)

With the above conventions we can now formulate the

Theorem Let predicates $f, g$ satisfy

(0) $f \cdot x \Rightarrow g \cdot x\;$ for all $x$ ;

let equation $x : f\left( x\right)$ have at least

(1) $\left\langle {\exists x : f \cdot x}\right\rangle$

let equation $x : y.x\;$ have at most

1 solution, i.e.

(2) $g \cdot x \land g \cdot y \Rightarrow x = y\;$ for all $x,y$ .

Then we may conclude the converse $\phi (0),\ldots$

(3) $g \cdot y \Rightarrow p \cdot y$ for all $y$ .

Proof In order to establish (3), we observe for arbitrary $x$

[{y}_{\left( 1\right) }\left( {x,y}\right) = \left( {{ax} + b}\right) y]

$$ \begin{array}{l} \langle \exists x: f. x \rangle \land g. y \ \equiv {\text {p r e d i c a t e} \quad \text {c a l c u l u s} } \ \langle \exists x: f. x, \land g. y \rangle \ \equiv {0, w h i c h m e a n s } \cdot x \equiv f. x \wedge g. x } \ \langle \exists x: f. x \land g. x \land g. y \rangle \ \Rightarrow {(2) a n d m o n o t o n i c i t y o f \exists } \ \langle \exists x: f. x \wedge x = y \rangle \ \equiv {\mathrm {o n e - p o i n t} r u l e } \ f \cdot y \ \end{array} $$

(End of Proof.)

*

By way of illustration we'll sketch the structure of the shortest proof (see [0]) of Morley's Theorem, which deals with the shape of figures of the following topology!

In the application of our theorem, the "possibly unusual, but well-understood type" over which $x, y$ range comprises all figures of the above topology - PQR inside ABC such that the lines drawn above partition △ABC into the 7 small nondegenerate tri- angles shown -, where the size of the figure is irrelevant: only the angles matter.

Morley's Theorem states that, if the angles at $A,B,C$ are trisected, triangle PQR is equilateral.

Predicates $p$ and $g$ are formulaled in terms of the angles $\alpha ,\beta ,\gamma$ that satisfy

(4) $\alpha + \beta + r = \pi /3\;$ and $\alpha ,\beta ,r$ are positive. Predicate $f$ prescribes the angles around

Predicate $f$ satisfies condition (1) thanks

(5) $\begin{array}{l} \left( {\alpha + \pi /3}\right) + \left( {\beta + \pi /3}\right) < \pi \ \text{clically} \end{array}$ (and ${cy} =$ (6) $\left( {\beta + \pi /3}\right) + \left( {\pi /3}\right) + \left( {\alpha + \pi /3}\right) > \pi$ (and

when we extend the above figure with

Predi cate Prescribes the angles around A,B,C:

To verify that $g$ satisfies condition (2) we observe that, thanks to (4), a triangle ABC with angles ${3\alpha },{3\beta },{3\gamma }$ exists,that the shape of a triangle is fixed by its angles, and that with respect to that triangle the positions of their angle trisectors, and hence of their points of intersection $P,Q,R$ are uniquely determined.

Because $f.y$ implies that in $y$ triangle PQR is equilateral, $g.y \Rightarrow f.y$ -i.e. (3)- implies Morley's Theorem. The proof in [0], however, establishes $f.x \Rightarrow g.x$ -i.e. (0)- (using the Rule of Sines, followed by a monotonicity argument). The appeal to the above theorem and the facts that the existence condition (1) and the uniqueness condition (2) are satisfied are swept under the rug by the rug by the sentence "We start in our proof not with the arbitrary triangle [ABC], but with the equi- lateral one [PQR]." Regretably, this way of committing the sin of omission is only

too common, and it is no wonder that people get confused about the distinction between consequent and antecedent.

This note has been written because, only a few years ago, I had been unable to identify without pencil and paper the precise logical structure of the sketched proof of Morley's Theorem (though, at the time obviously taking a lot for granted, I had designed that proof myself). The two hurdles I failed to take were (i) the realization that an unusual type might (and was) needed, and (ii) the parameterization -by $\alpha ,\beta ,\gamma$ of $f$ and $g$ , which is essential for the application but need not show up in the theorem presented in this note.

[0] "EWD538 A Collection of Beautiful Proofs" in Edsger W. Dijkstra, "Selected Writings on Computing: A Personal Perspective," 174-183, Springer-Verlag New York Heidelberg Berlin, 1982

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