A chutzpah

A chutzpah

In EWD1073 "How Computing Science created a new mathematical style" - published in [0] -, I included W.H.J. Feijen's proof

$$ a + b \geq a \uparrow b \equiv a \geq 0 \land b \geq 0 $$

using for the definition of $\upharpoonright$ that for all

$\Rightarrow \;w \geq {a}^{ \uparrow }b \equiv w \geq a \land w \geq b\;\therefore$

$$ \begin{array}{l} a + b \geq a ^ {\prime} b \ = {(0) \mathrm {w i t h} w := a + b } \ a + b \geq a \land a + b \geq b \ = {\mathrm {a r i t h m e t i c} } \ b \ge 0 \land a \ge 0 \ \end{array} $$

is considered a single character.)

The other day I received a letter from a colleague, who was not convinced by this example. Using the definition of max

$$ \max (a, b) = \left{ \begin{array}{l l} a & i f a \geq b \ b & i f b \geq a \end{array} \right. $$

he proved the

Proposition. Let $a$ and $b$ be real numbers. Then the following are equivalent

(i) $a + b \geq \max \left( {a,b}\right)$ (ii) $a \geq 0\;{and}\;b \geq 0$ .

Proof. Since both (i) and (ii) are symmetric in $a$ and $b$ ,we may assume Wlog that $a \geq b$ . Then both (i) and (ii) are equivalent to " $b \geq 0$ ".

a proof of 101 characters. My correspond

"This is surely no longer than the argument you write out, and has the advantage of being easily readable by a human being rather than a computer."

This is what I call a chutzpah! I am not making this up; here my correspondent will remain anonymous, but as of "the other day" my files contain the physical evidence that he really exists. (And he isn't a nobody either: I knew his name very well before I received his letter.)

About my correspondent's proof we can remark

• that an argument "WLOG" - which I counted for 4 instead of for 23 characters has the disadvantage of usually appealing to an unformulated theorem that the proof does not mention that

it relies on the fact that max (a,b) = max(b,a). (It also relies on the facts that + and A are symmetric operators, but that we may classify under the headdings "arithmetic" and "predicate calculus" respectively.)

that his proof requires a demonstration

$$ a \geq b \Rightarrow (a + b \geq m a x (a, b) \equiv b \geq 0), $$

in the degree of detail of Fege's

$$ \begin{array}{l} a + b \geq a \uparrow b \ = {\mathrm {d e f . o f} \uparrow , a \geqslant b } \ a + b \geq a \ = {\mathrm {a r i t h m e t i c} } \ b \geq 0 \ \end{array} $$

a subproof of about 30 characters.

• that this 'proof requires a demonstration

of

$$ a \geq b \Rightarrow (a \geq 0 \land b \geq 0 \equiv b \geq 0), $$

in the degree of detail of Feyer's

proof for instance

$$ \begin{array}{l} a \geq 0 \land b \geq 0 \equiv b \geq 0 \ = {\mathrm {p r e d . c a l c . 3} \ b \geq 0 \Rightarrow a \geq 0 \ \leqslant {\mathrm {t r a n s i t i v i l y} \phi \geqslant 3 \ a \geq b \ \end{array} $$

a subproof of about another 30 characters (at least).

It seems more appropriate to summarize the comparison as follows:

"The calculational argument is shorter and more detailed than the proof my correspondent wrote out, and, besides being easily readable by humans, has the additional advantage of being amenable to mechanical verification as well."

One step of Feigen's proof uses the defini- nition of in order to eliminate it; this step is unavoidable. It's other step is arithmetical and also unavoidable since + has to be eliminated. In that sense, Feigen's proof is the shortest proof possible. Yet my correspondent thought he could produce a shorter proof!

This is the more amazing since EWD1073 states "that the calculational proofs are almost always more effective than all in-formal alternatives", and the next paragraph explains: "When I called calculational proofs more 'effective', I meant that they tend to be shorter, more explicit, and so complete

that they can be read and verified without. pencil and paper." So he was warned!

A couple of days after the fact I realize that the receipt of my colleague's letter has been a shocking experience, that reminds me of what I learned from Brian Randell: "There is none so blind as them that won't see."

[0] Mitteilungen der Mathematischen Gesellschaft in Hamburg, Band XII, Heft 4, 1991, pp. 897-905

Austin, 16 April 1994

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