From the Hungarian Eotvos Competition, 1911

About the six real variables $a,b,c,A,B,C$ it has been given that

$\therefore {aC} - {2bB} + {cA} = 0,$ and ${ac} - {b}^{2} > 0$

prove that $AC - B^{2}\leq 0$

Proof We first massage the demonstrandum.

$$ \begin{array}{l} a C - 2 b B + c A = 0 \quad \wedge a c - b ^ {2} > 0 \quad \Rightarrow A C - B ^ {2} \leq 0 \ {s h u n t i n g, (0) } \ a c - b ^ {2} > 0 \land A C - B ^ {2} > 0 \Rightarrow a C - 2 b B + c A \neq 0 \ {\mathrm {a r i t h m e t i c}, (1) } \ \end{array} $$

$$ a c > b ^ {2} \land A C > B ^ {2} \Rightarrow a C + C A \neq 2 b B $$

Under exploitation of the antecedent we now demonstrate the consequent. We observe

$$ a C + c A \neq 2 b B $$

[\left{ \begin{array}{l} \text{Fegen's Law, a.k.a. Zinbiel's Principle, (2)} \ \end{array}\right} ]

$$ (a C + C A) ^ {2} \neq 4 b ^ {2} B ^ {2} $$

[\left{ \begin{array}{l} \text{arithmetic,}\left( 3\right) } \ \end{array}\right. ]

$$ (a C + c A) ^ {2} > 4 b ^ {2} B ^ {2} $$

$\Leftrightarrow \left{ {{ac} > {b}^{2} \geq 0 \land {AC} > {B}^{2} \geq 0 \Rightarrow {ac}{AC} > {b}^{2}{B}^{2},\left( 4\right) }\right}$

$$ (a C + c A) ^ {2} \geq 4 a c A C $$

[\left{ \begin{array}{l} \text{arithmetic} \ \end{array}\right} ]

$$ (a C - c A) ^ {2} \geq 0 $$

[\left{ \begin{array}{l} \text{arithmetic,}\left( 5\right) } \ \end{array}\right. ]

true

(End of Proof.)

Notes

(0) The hint "shunting" refers to appeals to the law

$$ [ P \land Q \Rightarrow R \equiv P \Rightarrow \neg Q \lor R ]. $$

This law is loved by the people that concoct problems for Mathematical Olympiads; they use it to make the problem statement as misleading as possible. Here, shunting is indicated to restore the symmetry between the upper and lower case variables.

(1) Writing $x - y > 0$ for $x > y$ is another wilful complication: $x$ is a nice binary relation that has nothing to do with the zero-element of the addition. The simplifications of the antecedent are obvious, that of the consequent has been guided by considerations of symmetry. (2) The use of Leibniz's Principle that for any $x,y,f$ $x = y \Rightarrow f \cdot x = f \cdot y$

is standard. I owe to W.H.J.Feyn the awareness that its contra-positive

$$ x \neq y \Leftarrow f \cdot x \neq f \cdot y $$

can be used to strengthen $x \neq y$ . The application of Zinbiels Principle gives us the freedom and the obligation to choose an appropriate $f$ . It is one of those steps that co ipso embodies an invention. Because in the antecedent $b$ and $B$ occur only in the form ${b}^{2}$ and ${B}^{2}$ ,choosing for $p$ the square

is in this case a minute invention.

(3) In view of

$$ [ x \neq y \equiv x < y \vee x > y ] $$

we can strengthen the expression by replacing $\neq$ by $<$ or by $>$ ,in the hope of implementing a monotonicity argument. This is, in general,a rather optimistic step; in this case,the step is strongly suggested by the fact that the antecedent gives upper bounds for ${b}^{2}$ and ${\mathbf{B}}^{2}$ . (4) This step is a very usual monotonicity argument. It appeals to the first one of

$$ \begin{array}{l} [ p > r \iff p \geq q \land q > r ] a n d \ [ p > r \iff p > q \land q \geq r ] \quad , \ \end{array} $$

where the bounds are exclusive in the left-hand side and in one of the conjuncts of the right-hand side. It is the standard way of exploiting the original antecedent

$ac > b^{2}$ and of doing justice to the fact that it is essential that in both conjuncts the bounds are exclusive. (Had the first conjunct been $ac\geq b^2$ , the instantiation $a,b,c:= 0,0,0$ would have revealed that the problem was a nontheorem.) The whole idea of the monotonicity argument is that it embodies a disentanglement in the

sense that, for an appropriate $q$ ,precisely one of the conjuncts depends on the original antecedent. Since we have to do justice to the fact that in the latter the bounds are exclusive, we derive from the original antecedent the conjunct with the exclusive bound (in this case $q > r$ ),and the remaining proof obligation -in this case ${\left( ac + cA\right) }^{2} \geq {4acAC} -$ has to be an inequality in which the bound is included.

If we wish to prove the hint in more detail, we may observe

$$ b ^ {2} B ^ {2} $$

$\leq \left{ \begin{array}{l} {ac} > {b}^{2} \end{array}\right.$ and ${B}^{2} \geq 0$ because $B$ is real $< { {AC} > {B}^{2}$ and ${ac} > 0\;$ because ${ac} > {b}^{2}$ and b is real}

(5) Here we use that the remaining four variables are real.

(End of Notes.)

The sole reason for recording the above proof with its underlying heuristics lies in the fact that these heuristics proved to be so effective. The other week, Anne Kaldeway showed me the problem after we had had dinner at his house. Within 7 minutes, in an easy chair and without

pencil and paper, I solved the problem as shown above. I did not feel brilliant at all; I remember observing with some satisfaction that, once more, the Rules of the Game had worked.

The experience gained significance when I later learned that even seasoned mathematicians could easily work on this problem for an hour or so (and not necessarily with success). Evidently, mathematics as "The Art and Science of Effective Reasoning" has still a long way to go.

Nuenen, 7 June 1989

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