A tough experiment with the triangle calculus
EWD1280 · 1995–2000 · PDF · Source language: English. · Local OCR-derived source needs manual review.
A tough experiment with the triangle calculus
Here we see 7 points so situated that they give rise to 6 collinear triples. They have been partitioned into the 4 vertices $a,b,c,d$ of a quadrilateral and the 3 points of inter- section of the 3 pairs of "diagonals".
Note We don't wish to distinguish between "the" pair of diagonals and a pair of opposite sides, for the distinction disappears when of the 4 points, 1 lies inside the convex hull of the other 3. (End of Note)
The theorem I want to prove is that $p,q,r$ are not collinear if, of $a,b,c,d$ , no three are collinear.
Now it so happens that
$\left( {x,y,z\text{are collinear}}\right) \equiv \left( {0 = \text{area of}\Delta {xyz}}\right)$ ,
so the whole theorem can be formulated in terms of areas being 0 or not. The purpose
of this note is to explore whether we can prove the theorem not in terms of the boolean function "collinear" but in terms of the real function "area". (The boolean criterion "collinear" is too crude to erect a calculus on, whereas signed areas have been shown to be a valuable tool in eliminating case analyses generated by the distinction inside/outside.)
We shall use $a, b, c, d, h, k, p, q, r, x, y, z$ to denote points and $\Delta xyz$ to denote in formulae the area of triangle $xyz$ . (We know that we can only do this as long as we avoid multileter names.) Our simplest axiom is
$$ (0) \quad \Delta x y z = \Delta y z x \quad \wedge \quad \Delta x y z = - \Delta z y x, $$
i.e. subjecting the arguments to an odd permutation changes the sign of the area. This has a mathematical consequence, viz.
$$ (1) \quad x = y \Rightarrow \triangle x y z = 0 $$
Note The formulation of this consequence did confront me with a dilemma: should I rather have written
$$ (1) \quad x = y \vee y = z \vee z = x \Rightarrow \Delta x y z = 0 \quad ? $$
When I think it is not confusing, I'll stick to the simplest formulation, hoping that the
reader will supply the appeals to (0). [This is a decision very similar to the one we took in the predicate calculus when we decided not to spend separate steps to the symmetry and associativity of the logical operators.]
There is a kind of converse of (1), viz. that for arbitrary real value $R$
$x \neq y \Rightarrow \left\langle {\exists z : R = \Delta x{yz}}\right\rangle$
Having other concerns in this note, I don't expect to use it explicitly.
For the next axiom - the additive axiom. I shall give three different formulations. The first formulation is completely symmetric in the four points:
$\left( {3}^{1}\right) \cdot \Delta {xyz} + {\Delta h2y} + {\Delta zhx} + {\Delta yxh} = 0$
(For any pair of triples in the above, the shared points occur in the same positions, but interchanged.)
In the next formulation of the same axiom, one point -here $h$ - plays a special role:
$\left( {3}^{\prime }\right) \cdot \Delta {xyz} = {\Delta h}^{2}z + {\Delta xh}^{2} + {\Delta xyz}$
The symbol dynamics" here are that the
triples of the right-hand side are formed by replacing the points in the triple at the left in turn by a fourth point.
In the last formulation, the four points are separated into two pairs, viz $\left( {x,y}\right)$ versus (h,k)
$\left( {3}^{n}\right) \cdot \Delta = {h}^{2} + {\Delta kx} = {\Delta h}^{2} + {\Delta kxh}$
Please note how the triples have been taken from the cycle (xhyk)
An immediate consequence of the additive axiom (3) - most easily derived from (3") - is lemma
${\Delta xyz} = 0 \Rightarrow {\Delta xhy} + {\Delta yh2} = {\Delta xh2}$
This is an important lemma because it provides a way of exploiting the collinearity of xyz and then equates an expression containing $y$ . to an expression without
Our next and probably last axiom is the multiplicative axiom
(5) ${\Delta xyz} = 0 \Rightarrow \left( {{\Delta hx}{y}^{\prime }}\right) \cdot \left( {{\Delta k}{x}_{2}}\right) =$ $\left( {{\Delta k} \times y}\right) \cdot \left( {{\Delta h} \times z}\right)$
(Here the high infix dot . denotes multiplic
tion.) The mathematical charm of (s) is that it does not matter at all if some of the five points coincide, and that is why I tried to use it in this form, but that was a pain in the neck: symbol dynamics with 5 points really becomes complicated.
We can replace (5) by
(6) ${\Delta xyz} = 0 \land x \neq z \Rightarrow$
$$ \langle \exists \lambda : \langle \forall h: \Delta h x y = \lambda \cdot \Delta h x z \rangle \rangle $$
This is better disentangled than (5) because it makes clear that there is a relevant quan- tity -viz. the λ that does the job- that only depends on the triple xyz
Note I did not name the function whose value equals that λ , nor did I define it by means of an operator , say,
$$ \lambda = x y: x 2, $$
because I am currently not in the mood to introduce partial functions. (End of Note.)
The time has come to try whether we can now prove our original theorem.
We are given:
4 primary points a,b,c,d and 3 secondary points p,q,r satisfying
(7) (i) ${\Delta apd} = 0$ (ii) ${\Delta bpc} = 0$ (8) (i) ${\Delta aqb} = 0\;\left( {ii}\right) {\Delta cqd} = 0$ (9) (i) $\bigtriangleup {arc} = 0\;\left( {ii}\right) \bigtriangleup {brd} = 0$
and furthermore (at least)
(10) ${\Delta abc} \neq 0 \land {\Delta bcd} \neq 0 \land$
$$ \Delta c d a \neq 0 \land \Delta d a b \neq 0 $$
Note. Thanks to (1), (10) implies that the 4 primary points are all distinct. (End of Note.)
We are requested to show $\bigtriangleup {pqr} \neq 0$ .
I propose to do this in 2 steps. In the first step I hope to express $\Delta$ pqr in terms of $\Delta$ abc, $\Delta$ bcd, $\Delta$ cda, $\Delta$ dab , and in the second step I hope to show that this expression differs from 0 . (I know that I may possibly do too much work to establish just 1 bit of information, but this time I do not mind.)
We have to relate "the secondary triangle"
$\Delta$ pqr to the 4 triangles with primary points only, and I propose to do so in 3 steps, in each step reducing the number of second ary points in the triples by 1 .
From 3 secondary points to 2 is easy: applying (3") with xyz := p q r a we get
(11) ${\Delta p q r} = {\Delta a q r} + {\Delta p a} + {\Delta p q a},$
the choice of " $a$ " having been arbitrary. We now proceed for the time being with one of the new triangles, say ${\Delta aqr}$ .
The pair $a +$ occurs in(x,i),the pair ar in (9.i).Arbitrarily we choose to concentrate on the former. Because of ${\Delta aqb} = 0 \land a \neq b\;$ we can instantiate
(6) with $xyz \coloneqq aqb$ , and then instantiate the consequent with $h := r$ , $h := c$ and $h := d$ , i.e. there is a $\lambda$ satisfying
$$ \Delta r a g = \lambda \cdot \Delta r a b $$
$$ \Delta c a q = \lambda \cdot \Delta c a b $$
$$ \Delta d a q = \lambda^ {\bullet} \Delta d a b $$
$$ o r \quad \Delta q a c = - \lambda \cdot \Delta a b c $$
(The other possible instantiations of) h don't give helpful results.) From the last 2
equalities we can eliminate 9 - the only secondary point occurring in them! by
observing
$$ \begin{array}{l} \lambda \cdot (\Delta d a b - \Delta a b c) \ = {\mathrm {l a s t} 2 \mathrm {e q u a l i t i e s} \mathrm {a b o v e} } \ \Delta d a q + \Delta q a c \ = {(4) \mathrm {w i t h} x y z h := d q c a \mathrm {a n d} (8, 1 1) } \ \Delta d a c \ = \quad \left{ \begin{array}{l} (0) \end{array} \right} \ \Delta c d a [ S e e F i p p e n d i x ] \ \end{array} $$
Eliminating $\lambda$ we now arrive at
$$ (1 2) \quad \Delta r a g = (\Delta r a b) \cdot (\Delta c d a) / (\Delta d a b - \Delta a b c), $$
which leaves us with the obligation of eliminating
The occurrence of points us to (9), arbitrarily we select (9,i) to begin with; $\Delta \operatorname {arc} = 0\land a\neq c$ invites us to use (6) with $xyz\coloneqq \operatorname {arc}$ and to obtain with $h:=b$ and $h:=d$ the existence of a $\mu$ such that
$$ \begin{array}{l} \Delta b a r = \mu \cdot \Delta b a c \quad o r \quad \Delta r a b = \mu \cdot \Delta a b c \ \Delta d a r = \mu \cdot \Delta d a c o r \Delta d a r = \mu \cdot \Delta c d a. \ \end{array} $$
Now we observe
$$ \begin{array}{l} \mu \cdot (\Delta c d a + \Delta a b c) \ = {\mathrm {l a s t} 2 \mathrm {e q u a l i t i e s} \mathrm {a b o v e} } \ \Delta d a r + \Delta r a b \ = {(4) \mathrm {w i t h} x y z h := d r b a \mathrm {a n d} (9, i i) } \ \Delta d a b \quad [ S e e A p p e n d i x ] \ \end{array} $$
which enables us to eliminate $\mu$ :
$$ (1 3) \quad \Delta r a b = (\Delta a b c) \cdot (\Delta d a b) / (\Delta c d a + \Delta a b c). $$
And now elimination of $\Delta$ rab from (12) and (13) yields
$$ (1 4) \quad \Delta a g r = \frac {\Delta a b c \cdot \Delta d a b \cdot \Delta c d a}{(\Delta c d a + \Delta a b c) \cdot (\Delta d a b - \Delta a b c)} $$
Before -see (11)- we start computing $\Delta$ par and $\Delta$ pqa,we introduce 4 abbreviations, viz.
$$ A = \triangle b c d B = \triangle c d a $$
$$ C = \Delta d a b D = \Delta a b c $$
which allow us to shorten ( $A$ ) to
$$ (1 4 ^ {\prime}) \quad \Delta a q r = \frac {D \cdot C \cdot B}{(B + D) \cdot (C - D)} $$
To compute $\Delta$ par we observe that the substitution ${pgbd} = {qpdb}$ leaves our theorem unchanged as it only interchanges (7) and (8). In terms of ABCD the substitution becomes
$$ A, B, C, D := - A, - D, - C, - B $$
and since ${\Delta par} = - {\Delta apr}$ we derive ${f}_{\text{rom }}\left( {14}\right)$
$$ (1 5) \quad \Delta p a r = \frac {B \cdot C \cdot D}{(D + B) \cdot (C - B)} $$
To compute $\bigtriangleup {pqa}$ from (14),we per- form the substitution prcd := rpdc,which only interchanges (7) and (9). In terms of ABCD it is
$$ A, B, C, D := - A, - B, D, C $$
and since ${\Delta pqa} = - {\Delta aqp}$ we derive from (4')
$$ (1 6) \quad \Delta p q a = \frac {C \cdot D \cdot B}{(C - B) \cdot (D - C)} $$
$$ \mathrm {C o l l e c t i n g} \quad (1 1), (1 4 ^ {\prime}), (1 5), (1 6) \qquad \mathrm {w e g e t} $$
$$ \Delta p q r = \frac {B \cdot C \cdot D \cdot ((C - B) + (C - D) - (B + D))}{(B + D) (C - D) (C - B)} $$
Because of (3) we have
$$ (1 7) \quad A + C = B + D $$
and we can simplify this to
(18) ${\Delta p q r} = \frac{2 \cdot A \cdot B \cdot C \cdot D}{\left( {B + D}\right) \cdot \left( {D - C}\right) \cdot \left( {C - B}\right) }$
which thanks to (17) has all the required symmetries. $\bigtriangleup {pqr} \neq 0$ indeed follows.
Epi Iogue
I have been thinking about this problem for months, it was only last month that I did a few notational calculation experiments and only last week when I started in earnest. I started without notes and not certain at all that I would succeed, this EWD first got a provisional number (in pencil). I worked on it on 4 or 5 dif- ferent days but each time I had to masster all my courage for I was apprehen-sive that it would become an unmanageable mess. Earlier experiments with formal, calculational geometry had been discouraging.
It was a true experiment in calculation in the sense that I never used the picture on the front page: the picture is only there to distract the reader. (When I introduced p,q, r in (7), (8), (9), I checked that picture and calculation used the same nomenclature, that was all.) There are too many pictorial cases : of $a,b,c,d$ ,one point may lie inside the convex hull of the other three or not , and in any case the symmetry between p,q,r is pictorially destroyed. One purpose was to show
how calculation with signed areas can elimi- nate case analyses.
I selected the problem because
(i) thanks to Sylvester I knew that the problem was not completely trivial. (ii) I did not know that, as in (18), ${\Delta p q r}$ could be expressed in terms of (iii) it challenges one to exploit symmetryries without notational aids to express them
I observe that the introduction of iden- tifiers $\left( {p,q,r,\lambda ,\mu }\right)$ with listed relations they satisfy - rather than using expressions with proper lies- served me well. So did the translation of a substitution for the points into a substitution for A,B,C,D .
When I completed this calculation two hours ago, I was very pleased with the
Austin, 1 February 1999
Appendix (with acknowledgement to the ETAC)
After having chosen the primary points $a,b,c,d$ ,I could have defined the secun- dary ones $p,q,r$ as the points of inter-
section between the appropriate pairs of lines through the primary points, a pro- cedure that closely corresponds to the way in which I constructed the picture at the opening of this note, but it would immediately raise the question "but what if such a pair of lines were parallel?" All this I circumvented by "giving" 7 points satisfying (7) through (10), ig- noring the question whether such septuples exist. (Rightly so, for that is a separate problem.)
The fact that (Δdab - Δabc), the denominator of the right-hand side of (12), differs from zero, follows from the preceding relation
$$ \lambda \cdot (\Delta a b - \Delta a b c) = \Delta c d a $$
whose derivation used the existence of $g$ (The above denominator ${\Delta dab} - {\Delta abc}$ equals zero if ab//cd.) That the denominator of the right-hand side of (13) differs from zero follows similarly. Austin, March 1999
Prof. Dr Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188, USA