Fillers at a YoP-institute

EWD1017 · 1987–1991 · PDF · Source language: English. · Local OCR-derived source needs manual review.

Copyright Notice

The following manuscript,

EWD 1017: Fillers at a YoP-institute

was published as

Edsger W. Dijkstra, ed., Formal Development of Programs and Proofs. Addison-Wesley, 1990: 209-227.

Fermat and Wilson

From graph theory, we use

a finite, directed graph in which each node has both in-degree and out-degree $= 1$ consists of cycles; consider along a cycle a path of p edges; if the path ends at the node at which it starts, the length of the cycle -i.e. the number of nodes on it - is a divisor of p ; in particular, if p is prime, the cycle is of length p or is of length 1 (i.e. is a "self-loop").

We can use this to prove for natural $n$ and prime $p$

$$ (n ^ {p} - n) \mod p = 0 \quad (\mathrm {F e r m a t}) $$

$$ ((p - 1)! - (p - 1)) \mod p = 0 \quad (\mathrm {W i l s o n}) $$

For the proof of the theorem of Fermat we take as nodes the $n^p$ strings of $p$ characters from an alphabet of size $n$ , and introduce a directed edge from $Rr$ to $rR$ for any character $r$ and string $R$ (of length $p-1$ ). According to $\bullet$ , the graph consists of cycles of length $p$ and of self-loops. Because the self-loops correspond to the strings in which all characters are the same and because the size of the alphabet is $n$ , the number of nodes occurring in self-loops equals $n$ . The remaining $n^p-n$ nodes are therefore partitioned into cycles of length $p$ , which proves Fermat's theorem.

For the proof of the theorem of Wilson we take as nodes the $(p - 1)!$ cyclic arrangements of the numbers from 0 through $p - 1$ ; for each directed edge we obtain (the cyclic arrangement corresponding to) the target node by increasing each number in (the cyclic arrangement corresponding to) the source node by 1 modulo $p$ . According to $\bullet$ , the graph consists of cycles of length $p$ and of self-loops. Because the self-loops correspond to the cyclic arrangements with constant difference (modulo $p$ ) between adjacent numbers, and because 1 through $p - 1$ are the possible values of that difference, the number of nodes occurring in self-loops equals $p - 1$ . The remaining $(p - 1)!\cdot (p - 1)$ nodes are therefore partitioned into cycles of length $p$ , which proves Wilson's theorem.

Maximizing the product for given sum

Question How do we construct a bag of positive integers with given sum so that their product is as large as possible?

Answer Because with sum $\leq 1$ ,the bag is unique, we only analyse the cases with sum $\geq 2$ .

because $1 \cdot x < 1 + x$ ,and (because of sum $\geq 2$ ) our target bag differs from ${ 1}$ ,our target bag contains no 1 ;
because $2 \cdot \left( {x - 2}\right) \geq x \equiv x \geq 4$ ,our target bag need not contain integers $\geq 4$ ;
because $2 + 2 + 2 = 3 + 3$ and $2 \cdot 2 \cdot 2 < 3 \cdot 3$ ,our

target bag contains at most two 2's.

The above constraints are met by a bag of (2. sum) mod 3 2's and for the rest 3's . (End of Answer.)

Remark The predominance of 3's in the target bag reflects that 3 is the closest integer approximation of e -the base of the natural logarithm -, which is the solution of the corresponding continuous problem. For the same reason it is theoretically preferable to implement Heapsort with a ternary tree instead of a binary one. (End of Remark.)

On "Poor Man's Induction"

We consider n points along the circumference of a circular cake and cuts along all the chords between them, the points being chosen in such a way that all internal intersection points of pairs of chords are distinct. With f the number

of pieces , the above suggests $f = {2}^{n - 1}$ . The reader may verify that $n = 5$ indeed yields $f = {16}$ . However, $n = 6$ yields $f = {31}$ ! How does $f$ depend on $n$ ?

This problem is most easily solved in two steps:

the first step expresses $f$ in terms of $c =$ the number of chords, and $p =$ the number of internal intersection points

the second step expresses C and p in terms

for the increase $\Delta {f}^{\prime }$ of $f$ caused by a new

$\Delta f$

= the new chord cuts pieces into two

= {a piece is cut by a segment of the new chord} $= { {segments}$ are separated by intersection points $}$ = {internal intersection points of pairs of chords are distinct}

$$ \Delta C + \Delta p $$

From this and $c = 0 \Rightarrow p = 0 \land f = 1$ we derive by mathematical induction

$$ f = 1 + c + p $$

from the one-to-one correspondence between chords and pairs of points on the circumference we derive

$$ c = \left( \begin{array}{l} n \ 2 \end{array} \right) $$

from the one-to-one correspondence between internal intersection points and quadruples of points on the circumference we derive

$$ p = \binom {n} {4} $$

Combining the results from $\bullet \bullet$ we establish

$$ f = 1 + \binom {n} {2} + \binom {n} {4} $$

or -by properties of binomial coefficients - equi- valently

$$ f = \binom {n - 1} {0} + \binom {n - 1} {1} + \binom {n - 1} {2} + \binom {n - 1} {3} + \binom {n - 1} {4} $$

i.e. $f$ equals the sum of the first five values on a line of the Pascal triangle, lines which each add up to a power of 2 .

The above argument owes its extreme elegance to its high degree of disentanglement: the first blob is not concerned with $n$ and the second one not with $f$ , while their combination is no more than two substitutions. Note that this partitioning into two mutually independent blobs was only possible thanks to the introduction of $c$ and $p$ , which carry the interface.

Acknowledgement We owe the above beautiful solution to A. Blokhuis. (End of Acknowledgement.)

The binary search

Let $A$ be a non-empty, ascending, integer sequence of length $N$ , more precisely, let

$N > 0$ ,and

$$ (\underline {{A}} i, j: 0 \leqslant i < j < N: A. i \leqslant A. j) $$

let $X$ be an integer. We are requested to design a program solving the equation

$$ \mathrm {p r e s e n t}: (\mathrm {p r e s e n t} \equiv (\underline {{E}} i: 0 \leqslant i < N: A _ {i} = X)) $$

We distinguish two cases, $A.0 > X$ and $A.0 \leq X$ ; the latter case being the harder one, we deal with that one first.

It is hard to visualize an algorithm correctly establishing present, i.e. determining that the value $X$ indeed occurs in the sequence, without determining at the same time where $X$ occurs, i.e. without establishing for some integer, i say,

$$ A. i = X \land 0 \leq i < N $$

As intermediate result, this is too strong to aim for: if present is to be established, no such value for i exists. The best we can do in that case is to let i determine the pair of adjacent values in the sequence "between which X is missing", i.e. to establish

$$ A. i < X < A. (i + 1) \quad \land \quad 0 \leq i < N $$

for which purpose we define A.N so that

$$ X < A, N $$

Combining the two intermediate results we construct the more realistic target of establishing

$R : \;A,i \leq X < A.\left( {i + 1}\right) \; \land \;0 \leq i < N$

Our program can then have the form

$$ \begin{array}{l} \left[ \begin{array}{l} \text {v a r i : i n t} \end{array} \right] \ ; e s t a b l i s h \mathcal {R} \ ; \mathrm {p r e s e n t}: = A. i = X \ \begin{array}{c c} \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \hline \ \end{array} $$

For "establish $\mathbb{R}$ ",the precondition $A.0 \leq X < A.N$

suggests a repetition whose invariant P is

obtained from $R$ by replacing $\left( {i + 1}\right)$ by a

fresh variable, j say. I.e. with

$P : \;A.i \leq X < A.j\;\Lambda \;0 \leq i < j \leq N$

we suggest for "establish $R$ "

$$ \begin{array}{l} [ \underline {{v a r}} j: i n t ] \ i _ {0} j := 0, N {P } \ ; \underline {{d o}} j \neq i + 1 \rightarrow s h r i n k (j - i) {P } \underline {{o d}} {R } \ } {R } \ \end{array} $$

Let us now investigate for "shrink $(j - i)^{n}$ to what extent a change of $i$ will do the job. To this end we derive the weakest precondition such that $i = h$ decreases $(j - i)$ under invariance of $P$ :

$$ \begin{array}{l} j - h < j - i \ A, h \leq X < A, j \ \end{array} $$

which follows from

$P \land i < h < j \land {A}_{i}h \leq X$

For $j := h$ we derive in the same manner

$$ P \land i < h < j \land X < A. h $$

These two preconditions lead for "shrink $\left( {j - i}\right)$ "

$$ \begin{array}{r l}&\mathrm {I I} \underline {{v a r h : i n t}}\&{\quad ; \mathrm {s o l v e} h: (i < h < j)}\&{\quad ; \mathrm {i f} A. h \leq X \rightarrow i := h}\&{\quad \mathrm {I I} X < A. h \rightarrow j := h}\&{\quad \mathrm {f i}}\&{\quad ] 1}\end{array} $$

We observe, firstly, that, its guards being each other's complement, the alternative construct does not abort, and, secondly, that the precondition of shrink (j-i) - in particular: i $< j \land j \neq i + 1$ , or, equivalently, $i + 1 \leq j - 1$ implies that equation $h:(i < h < j)$ has at least one solution. For reasons of efficiency we don't implement "solve $h:(i < h < j)$ " by $h = i + 1$ or by $h:= j - 1$ , but rather by

$$ h := a v g. i j $$

The nice thing of the above derivation is that it makes it so clear that the termination of the repetition and the establishment of R are totally independent of the sequence A being ascending. Even if the algorithm establishes present we need not know that A is ascending; only the outcome present requires for its trustworthiness that A is indeed ascending.

In the case $A.0 > X$ , $A.0 > X \land 0 \leq i < N$ is an invariant and above program establishes present, as it should.

The Theorem of Pompeiu

Theorem Consider an equilateral triangle and an arbitrary point in the plane of the triangle. Then the three distances from the vertices of the triangle to the fourth point satisfy the triangular inequalities.

Proof The proof is by constructing a figure that contains a triangle with the three distances as its edge lengths. To this end we consider two instances of the triangle/point configuration, rotated over $60^{\circ}$ around one of the vertices of the triangle.

Because the triangle is equilateral, one instance of one of the other two vertices coincides with the other instance of the third vertex. The triangle formed by this point of coincidence and the two instances of the fourth point has the desired edge lengths, as we see as follows.

Because the rotation is over $60^{\circ}$ , the distance between the two instances of the fourth point equals their distance from the centre of rotation, which is one of the vertices. Because in the point of coincidence, different instances of the two remaining vertices coincide, its distances from the two instances of the fourth point are the distance from the fourth point to the two other vertices of the equilateral triangle. (End of Proof.)

Acknowledgement The above construction is due to G.R. Veldkamp. (End of Acknowledgement.)

Remark In my filler at the YoP Institute I used a picture, which was annoyingly overspecific: for instance, one cannot avoid choosing the fourth point inside or outside the triangle. Later in the institute, Jan L.A. van de Snepscheut showed how he could describe a class of mutual-exclusion algorithms with his hands in his pockets. The above presentation of Veldkamp's proof of the Theorem of Pompeiu has been inspired by that performance; it is a striking example of avoiding avoidable case analyses. (End of Remark.)

The monotonicity of extreme solutions

In the following, capital letters $P, Q, X, Y, Z$ denote predicates on some space. Universal quantification over that space is denoted by surrounding the universally quantified predicate by a pair of square brackets, known as "the everywhere operator". Lower case letters $f, g$ denote predicate transformers, i.e. functions from predicates (or predicate pairs) to predicates; functional application is denoted by an infix full stop.

Let $f$ be monotonic in both its arguments, i.e.

$$ \begin{array}{l} [ P \Rightarrow Q ] \Rightarrow \ [ f. P. Y \Rightarrow f. Q. Y ] \land [ f. X. P \Rightarrow f. X. Q ], f o r \ \end{array} $$

all $P,Q,X,Y$ .

Let, for all $X$ , $g.X$ be the strongest solution of the equation

$$ Y: [ f. X. Y \Rightarrow Y ] \quad , $$

i.e.

$$ \begin{array}{l} [ Z \Rightarrow f. X. (g. X) ] \Rightarrow [ Z \Rightarrow g. X ] \quad \mathrm {f o r a l l} X, Z \ (1) \quad [ f. X. Y \Rightarrow Y ] \quad \Rightarrow [ g. X \Rightarrow Y ] \quad \mathrm {f o r a l l} X, Y \ \end{array} $$

Remark Monotonicity of f in its second argument implies the existence of that strongest solution; (0) is equivalent to $[f. X. (g. X) \Rightarrow g. X]$ , i.e. it states that $g. X$ is a solution; (1) states that $g. X$ implies each solution. (End of Remark.)

Then, $g$ is monotonic, i.e. for all $P, Q$

$$ [ P \Rightarrow Q ] \Rightarrow [ g. P \Rightarrow g. Q ] $$

Proof We observe for any $P, Q$

$$ [ g, P \Rightarrow g, Q ] $$

$\Leftrightarrow \;\left{ \begin{array}{l} \text{ (1 ) with } \ X,Y \end{array}\right. = P,\;g.{Q}^{3}$

$$ [ f. P. (g. Q) \Rightarrow g. Q ] $$

$\Leftrightarrow { \left( 0\right)$ with $X,Z \mathrel{\text{:=}} Q,\rho .P.\left( {g,Q}\right) }$

$$ [ f. P. (g, Q) \Rightarrow f. Q. (g, Q) ] $$

$\Leftrightarrow { f\left( x\right)$ monotonistic in its 1st argument $}$

$$ [ P \Rightarrow Q ] $$

(End of Proof.)

The above 3-step proof is in a sense the shortest one possible: the first step takes into account that the function applied to $P$ is $g$ , the second step takes into account that the function applied to $Q$ is $g$ , and the third step uses that $f$ is monotonic in its 1st argument—and all three facts are indispensable.

It has, however, been included for more than its brevity alone; it has been included because it is the simplest example of the standard derivation of proofs of theorems involving extreme solutions.

The shape of the consequent. $[g.P\Rightarrow g.Q]$ immediately tells us that for the application of $g$ to $P$ , (0) is irrelevant, and (1) hence essential, and, conversely, that for the application of $g$ to $Q$ ,(1) is irrelevant and, hence,(0) is essential. The above heuristics all but dictate the design of such proofs. (We point out that these heuristics would have been hardly available, had the strongest solution been defined by "it is a solution and implies all other solutions" instead of by "it is a solution and implies all solutions".)

Finally we would like to point out that the use of $f$ the follows from symbol $\Leftarrow$ has enabled us to present the calculation without pulling a single rabbit out of a hat.

An algebraic approach to the predicate calculus

As in the previous filler, capital letters can be viewed as standing for predicates on some space, universal quantification over which is then denoted by a pair of square brackets. Because we wish to replace what is usually called "reasoning" whenever profitable by calculation, we here present the logical operators stressing their algebraic properties.

equality between predicates $X$ and $Y$ is expressed by "everywhere equivalent": $[X \equiv Y]$ .
function application is characterized by the Rule of Leibniz, i.e. by being equality-preserving:

$$ [ X \equiv Y ] \Rightarrow [ p. X \equiv p. Y ] $$

expressions are postulated to be functions of their subexpressions.

equivalence is postulated to be associative, i.e.

$$ [ ((X \equiv Y) \equiv Z) \equiv (X \equiv (Y \equiv Z)) ] $$

so that, from here on, parentheses in continued equivalences will be omitted - and to be symmetric, i.e.

$$ [ X \equiv Y \equiv Y \equiv X ] \quad . $$

Parsing the last formula as $[X \equiv (Y \equiv Y \equiv X)]$ and as $[(X \equiv Y \equiv Y) \equiv X]$ , we see that $\equiv$ has a left- and a right-identity element -viz. $Y \equiv Y -$ ; therefore $\equiv$ has a unique identity element, which we denote by true:

$$ [ X \equiv t r u e \equiv X ] $$

disjunction is postulated to be associative,i.e.

$$ [ (X \vee Y) \vee Z \equiv X \vee (Y \vee Z) ] $$

so that in continued disjunctions parentheses can be omitted-, to be symmetric, i.e.

$$ [ X \vee Y \equiv Y \vee X ] \quad , $$

to be idempotent, i.e.

$$ [ X \vee X \equiv X ] $$

and to distribute over equivalence, i.e.

$$ [ X \vee (Y \equiv Z) \equiv X \vee Y \equiv X \vee Z ] $$

0 [Xv true 3 true]

Proof We observe for any $X, Y$

$$ \begin{array}{l} X \vee \mathrm {t r u e} \ = {\mathrm {d e f . o f t r u e} } \ X \vee (Y \equiv Y) \ = {v d i s t r i b u t e s o v e r \equiv } \ X \vee Y \equiv X \vee Y \ = {\mathrm {d e f . o f t r u e} } \ t r u e \ \end{array} $$

(End of Proof.)

conjunction is defined in terms of equivalence and disjunction by

$$ [ X \land Y \equiv X \equiv Y \equiv X \lor Y ] \quad , $$

a formula known as the Golden Rule.

o conjunction is associative, symmetric and idempotent

Proof This is left to the reader. (End of Proof.)

$$ 0. \quad [ X \wedge (Y \equiv Z) \equiv X \wedge Y \equiv X \wedge Z \equiv X ] $$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} x \wedge y \equiv x \wedge z \ = {G o l d e n R u l e, t w i c e } \ X \equiv Y \equiv X \vee Y \equiv X \equiv Z \equiv X \vee Z \ = {\mathrm {r e a r r a n g i n g t e r m s o f c o n t i n u e d e q u i v a l e n c e} } \ \end{array} $$

$$ \begin{array}{l} X \equiv Y \equiv Z \equiv X \vee Y \equiv X \vee Z \equiv X \ = {v d i s t r i b u t e s o v e r \equiv } \ X \equiv (Y \equiv Z) \equiv X \vee (Y \equiv Z) \equiv X \ = {\mathrm {G o l d e n R u l e} } \ X \wedge (Y \equiv Z) \equiv X \quad . \qquad (\mathrm {E n d o f P r o o f}). \ \end{array} $$

$$ \begin{array}{l} \left. \begin{array}{l} 0 \ [ X \wedge (U \equiv Y \equiv Z) \equiv X \wedge U \equiv X \wedge Y \equiv X \wedge Z ] \end{array} , \right. \ i. e. " \wedge d i s t r i b u t e s o v e r \equiv \equiv " \ \end{array} $$

Proof This is left to the reader. (End of Proof.)

$$ \begin{array}{l} 0 \quad [ X v (Y \wedge Z) \equiv (X v Y) \wedge (X v Z) ] \qquad a n d \ \left[ X \wedge (Y \vee Z) \equiv (X \wedge Y) \vee (X \wedge Z) \right], i. e. \ \end{array} $$

disjunction and conjunction distribute over each other.

Proof To prove the last one we observe for any $X, Y, Z$

$$ \begin{array}{l} (X \land Y) \lor (X \land Z) \ = {\text {G o l d e n R u l e} } \ (X \wedge Y) \wedge (X \wedge Z) \equiv X \wedge Y \equiv X \wedge Z \ = {\Lambda \mathrm {i s a s s o c i a t i v e}, \mathrm {s y m m e t r i c , a n d i d e n i p o t e n t} } \ X \wedge (Y \wedge Z) \equiv X \wedge Y \equiv X \wedge Z \ = {\wedge d i s t r i b u t e s o v e r \equiv \equiv } \ X \wedge (Y \wedge Z \equiv Y \equiv Z) \ = {\mathrm {G o l d e n R u l e} } \ X \wedge (Y \vee Z) \ \end{array} $$

The preceding one can be proved similarly. (End of Proof.)

$\left\lbrack {{X\wedge }\left( {{X\vee Y}}\right) \equiv X}\right\rbrack$ and $\left\lbrack {{Xv}\left( {X \land Y}\right) \equiv X}\right\rbrack$ ,known as the

Laws of Absorption

Proof. To prove the first one - the second one can be proved similarly- we observe for any $X, Y$

$$ \begin{array}{l} X \wedge (X \vee Y) \ = {\text {G o l d e n R u l e} } \ X \equiv X \vee Y \equiv X \vee (X \vee Y) \ = {\mathrm {a s s o c i a t i v i t y a n d i d e m p o t e n c e o f} v } \ X \equiv X \vee Y \equiv X \vee Y \ = {\mathrm {i d e n t i t y e l e m e n t o f} = } \ X \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

Finally we derive for the conjunction

0 []

Proof We observe for any $X$

$$ \begin{array}{l} X \wedge t r u e \ = {\mathrm {G o l d e n R u l e} } \ X \equiv \mathrm {t r u e} \equiv X v \mathrm {t r u e} \ = {\mathrm {t r u e i s z e r o - e l e m e n t o f} v } \ X \equiv \mathrm {t r u e} \equiv \mathrm {t r u e} \ = {\mathrm {i d e n t i f y e l e m e n t o f} \equiv } \ X \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

implication is defined in terms of equivalence and disjunction by

$$ [ X \Rightarrow Y \equiv X \vee Y \equiv Y ] $$

Using the Golden Rule the reader may derive

$$ 0 \quad [ X \Rightarrow Y \equiv X \land Y \equiv X ] $$

and using the laws of Absorption

$$ \begin{array}{l} 0 \quad [ X \Rightarrow X \vee Y ] \qquad a n d \ 0 \qquad [ X \land Y \Rightarrow X ] \qquad . \ \end{array} $$

We shall prove

$$ 0 \quad [ X \Rightarrow (Y \Rightarrow Z) \equiv X \land Y \Rightarrow Z ] $$

Proof We observe for any $X, Y, Z$

$$ X \Rightarrow (Y \Rightarrow Z) $$

$$ \begin{array}{l} = \left{ \begin{array}{l l} \mathrm {r e l a t i o n b e t w e e n} \Rightarrow \mathrm {a n d} \wedge \ X \wedge (Y \wedge Z \equiv Y) \equiv X \end{array} \right. \ = {r e l a t i o n b e t w e e n \wedge a n d \equiv } \ = {\mathrm {r e l a t i o n b e t w e e n} \Rightarrow \mathrm {a n d} \land } \ X \land Y \Rightarrow Z \qquad \mathrm {(E n d o f P r o o f)} \ \end{array} $$

Proof We observe for any $X, Y$

$$ \begin{array}{l} 0 \quad [ X \wedge (X \Rightarrow Y) \equiv X \wedge Y ] \ X \wedge (X \Rightarrow Y) \ = {\mathrm {r e l a t i o n b e t w e e n} \Rightarrow \mathrm {a n d} \land } \ X \wedge (X \wedge Y \equiv X) \ = {\mathrm {r e l a t i o n b e t w e e n} \land \mathrm {a n d} \equiv } \ X \wedge X \wedge Y \equiv X \wedge X \equiv X \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {i d e m p o t e n c e} o f \wedge } \ X \wedge Y \equiv X \equiv X \ = {\mathrm {i d e n t i t y e l e m e n t o f} = } \ x \wedge y \ \end{array} $$

(End of Proof.)

Implication is transitive, i.e.

$$ 0 \quad [ (X \Rightarrow Y) \land (Y \Rightarrow Z) \Rightarrow (X \Rightarrow Z) ] $$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} [ (X \Rightarrow Y) \land (Y \Rightarrow Z) \Rightarrow (X \Rightarrow Z) ] \ = {\mathrm {p r e p r o v i o u s t h e o r e m} } \ [ X \wedge (X \Rightarrow Y) \wedge (Y \Rightarrow Z) \Rightarrow Z ] \ = {\mathrm {p r e v i o u s t h e o r e m} } \ [ X \wedge Y \wedge (Y \Rightarrow Z) \Rightarrow Z ] \ = {\mathrm {p r e v i o u s t h e o r e m} } \ [ X ^ {\prime} \wedge Y \wedge Z \Rightarrow Z ] \ = {\mathrm {L a w o f A b s o r p h i o n i n i m p l i c a t i v e v e r s i o n} } \ t r u e \ \end{array} $$

(End of Proof.)

$$ 0 \quad [ (X \Rightarrow Y) \vee (Y \Rightarrow Z) ] $$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} [ (X \Rightarrow Y) \vee (Y \Rightarrow Z) ] \ = {\mathrm {r e l a t i o n b e t w e e n} \Rightarrow \mathrm {a n d} v } \ [ (X \vee Y \equiv Y) \vee (Y \vee Z \equiv Z) ] \ = {v d i s t r i b u t e s o v e r \equiv } \ [ X v Y v Y v Z \equiv X v Y v Z \equiv Y v Y v Z \equiv Y v Z ] \ = {\mathrm {i d e m p o t e n c e o f} v; \mathrm {i d e n t i l y e l e m e n t o f} = 3 \ t r u e \ \end{array} $$

(End of Proof)

$$ 0 \quad [ (X \Rightarrow Y) \land (Y \Rightarrow X) \equiv X \equiv Y ] $$

Proof We observe for any $X, Y$

$$ (X \Rightarrow Y) \land (Y \Rightarrow X) $$

$= {$ Golden Rule; previous theorem $}$

$$ X \Rightarrow Y \equiv Y \Rightarrow X $$

$= \left{ {{\text{ definition of }}^{f} \Rightarrow }\right}$

$$ X _ {v} Y \equiv Y \equiv X _ {v} Y \equiv X $$

$= {$ identity element of $p \equiv 3$

$$ X \equiv Y $$

(End of Proof.)

So much for the implication. Note that conjunction and implication have been defined in terms of equivalence and disjunction. In order to introduce the negation we therefore postulate its properties with respect to the latter two connectives only; its properties with respect to conjunction and implication can then be derived.

negation and equivalence are postulated to be connected by

$$ [ \neg (X \equiv Y) \equiv \neg X \equiv Y ] $$

0 [1X=Y X=Y]

Proof We observe for any $X, Y$

$$ \lnot X \equiv Y $$

$= {$ connection between $T$ and $\bar{x}}$

$$ i (X \equiv Y) $$

$= \left{ {{\text{connection between}}j\text{and}i \in {symmetry} \circ P \equiv j}\right}$

$$ X \equiv \neg Y $$

(End of Proof.)

Substitution $Y \mathrel{\text{:=}} 7X$ in the above yields

$\left\lbrack {X \equiv {77}X}\right\rbrack$

negation and disjunction are postulated to be connected by the law of the Excluded Middle, i.e.

$$ [ X \vee \neg X ] $$

Exploring what we can derive from the above two postulates for the negation, we observe for any $X,Y$

true

$$ \begin{array}{l} = {X \in Y: X := X \equiv Y } \ = \left{ \begin{array}{l l} \mathrm {r e l a t i o n b e t w e e n ? a n d} \equiv 3 \ [ (X \equiv Y) v (\neg X \equiv Y) ] \end{array} \right. \ = \left{ \begin{array}{l} v \text {d i s t i b u t e s o v e r} \equiv \end{array} \right} \ \begin{array}{l} = \quad {\text {E x c l u d e d M i d d l e}; \text {i d e m p o t e n c e o f v} } \ 0 \quad [ i X v Y \equiv X v Y \equiv Y ] \end{array} \ \end{array} $$

Confronting the above theorem with the definition of the implication we get

$$ 0 \quad [ X \Rightarrow Y \equiv \neg X \vee Y ] $$

We can furthermore use it to derive the Laws of de Morgan:

$$ \begin{array}{l} 0 \quad [ i X \vee i Y \equiv i (X \wedge Y) ] \ 0 \quad [ i X \wedge i Y \equiv i (X \vee Y) ] \ \end{array} $$

Proof We shall prove the first one. To this end we observe for any $X, Y$

$$ \begin{array}{l} \begin{array}{l} \vdash X \lor \vdash Y \end{array} \ = {\mathrm {r e c e n t t h e o r e m w i t h} Y _ {i} = i Y } \ X \vee \neg Y \equiv \neg Y \ = {\mathrm {s a m e t h e o r e m w i t h} X, Y := Y, X } \ X \vee Y \equiv X \equiv \neg Y \ = {\mathrm {r e l a t i o n b e t w e e n} \neg \mathrm {a n d} \equiv } \ \lnot (X \lor Y \equiv X \equiv Y) \ = {\mathrm {G o l d e n R u l e} } \ i (X \wedge Y). \ \end{array} $$

(End of Proof.)

We leave to the reader the derivation of

$$ 0 \quad [ \neg X \land Y \equiv X \land Y \equiv \neg Y ] $$

Etc.

The above text is somewhat more elaborate than what I showed as filler at the YoP Institute; also here the manipulation of formulae with explicit quantification has been omitted. The material has been included because it deserves to be better known than it is. We regret that classical logic has not yet become a daily, calculational tool of the working mathematician, for we find it indispensable.

The reason why logic is so little used is probably that it has been presented in the wrong way, viz. as formalization of how mathematicians "think" instead of a calculus in its own right. As the

reader will have noticed, we have allowed the equivalence to play a very central role. For a calculational approach, this is essential: the notion of function application is defined by the fact that it is equality-preserving. And it is precisely the equivalence that is the logical connective that is the hardest to render in natural language; we have the "if and only if", but its deficiencies are clearly displayed in the following sentence: "John sees with both eyes if and only if John sees with one eye if and only if John is blind." By all linguistic standards, this sentence is total gibberish.

The purpose of logic is not to mimic verbal reasoning but to provide a calculational alter- native.

Nuenen, 21 December 1987

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