For Bill Walker a sequel to EWD1099

When I showed to Bill Walker my arguments for demonstrating [R ] in the form [¬RR ], he said he would like to see an example. My first remark is that a proof by case analysis can serve as example:

QR ]   ∧   [QR ]   , hence [R ]    ;

taking the contrapositive of the first conjunct, and appealing to the transitivity of implication we get the scheme

RQ ]   ∧   [Q R ] ,  hence [¬RR ]     .

*                   *
*

Here is my example for Bill Walker (see EWD1053). Our universe of discourse is a Euclidean plane in which each point is red, white, or blue. Our proof obligation R is

R :      there exists a monochrome pair of points with mutual distance 1.

The intermediate predicate Q is

Q :      all pairs of points with mutual distance √3 are monochrome.

In the following pictorial hints, drawn lines connect points, distance 1 apart, and dotted lines points at distance √3.

Note Monochrome means "of equal colour". The only significance of equality is that it is preserved in function application (Leibniz). The only function defined on our colour domain is equality, and applying Leibniz's principle to it yields that equality is transitive. And that is why an appeal to the transitivity of = has to occur in this proof. (End of Note.)

  ¬R

⇒             { diamond shape with one solid diagonal and one dotted diagonal , pigeon-hole principle }

Q

⇒             {triangle with one solid side and two dotted sides , transitivity of equality }

R            .

          Nuenen, 10 July 1991

 

prof.dr. Edsger W.Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712–1188

USA

 


transcribed by Guy Haworth
revised Sat, 13 Dec 2008