EWD731 - 0

An experiment in mathematical exposition.

Many people feel attracted to the implication on account of the simplicity of the associated inference rules 

           A ⇒ B          (1)
           B ⇒ C
        -----------
           A ⇒ C

           A ⇒ B          (2)
           C ⇒ D
        -----------
        A ∧ C ⇒ B ∧ D

           A ⇒ B          (3)
           C ⇒ D
        -----------
        A ∨ C ⇒ B ∨ D
The transitivity of (1), and the symmetry of (2) and of (3) are clearly appealing. Rule (1), however, is a direct consequence of, and rules (2) and (3) are merely two different transcriptions of the same 

           A ∨ B          (4)
           C ∨ D
        -------------
        A ∨ C ∨ (B ∧ D)       ,
a rule, which --on account of the symmetry of the disjunction-- can be applied in four different ways to the two given antecedents. Rules (2) and (3) give only two of the four. Rule (1) emerges as the special case

EWD731 - 1

           A ∨ B
           C ∨ ¬B
        -------------
           A ∨ C       .
I called this "a direct consequence" because --perhaps somewhat arbitrarily-- I would like to distinguish between inference rules (different applications of which may yield results that are not equivalent) and simplifications that are possible according to boolean algebra --such as replacing B ∧ ¬B by false and A ∨ C ∨ false by A ∨ C-- , but never change the value of the boolean expression.
* *
*

The above caused me to revisit the problem of the nine mathematicians visiting an international congress, and about whom we are invited to prove 

          A ∨ B ∨ C                     (5)

with

A:there exists a triple of mathematicians that is incommunicado (i.e. such that no two of them have a language in common)
B:there exists a mathematician mastering more than three languages
C:there exists a language mastered by at least three mathematicians.

Very much like the introduction of (named!) auxiliary lines or points in geometry proofs, I propose to introduce named auxiliary propositions, such that

EWD731 - 2

we can prove lemmata connecting them to the above propositions, such as
D:there exists a mathematician that can communicate with more others than he masters languages,
for which we can prove
Lemma 1 C ∨ ¬D.
Proof Obvious. With this qualification we mean here that we can start as well with observing
C ∨ "each mathematician communicates in different languages with those others he can communicate with", etc.
as with observing
¬D ∨ "there exists a mathematician that shares a language with at least two others", etc.
(End of proof of Lemma 1.)

With
E:there exists a mathematician that can communicate with more than three others,
we can prove
Lemma 2. A ∨ E.
Proof Let "x | y" here stand for "x and y are two different mathematicians that have no language in common. With
G:for each x, the equation x | u has at least five different solutions for u,
we observe (obviously) 

        E ∨ G                  (6)

With

EWD731 - 3

H:with y and z constrained to belong to an arbitrary quintuple, the equation y|z has at least one solution in y and z,
we observe (equally obviously) 

        E ∨ H        .        (7)
Applying rule (4) to assertions (6) and (7) we find     E ∨ (G ∧ H)   ,
hence
E ∨ "for each x, the equation x | y ∧ x | z ∧ y | z has at least one solution in y and z".
(End of proof of Lemma 2.)

Applying rule (4) to Lemmata 1 and 2 we infer the
Corollary.     A ∨ C ∨ (E ∧ ¬D)   .

Remembering rule (4) we see that (5) has been proved when we can prove B ∨ ¬(E ∧ ¬D)
or, equivalently
Lemma 3. B ∨ D ∨ ¬E.
Proof. Obvious. (End of proof of Lemma 3).

* *
*

Note that in the above the Corollary was only used for heuristic purposes. Once Lemmata 1, 2, and 3 have been established we could have inferred 

          A ∨ E
          B ∨ D ∨ ¬E
        ---------------
          A ∨ B ∨ D
and 
          A ∨ B ∨ D
          C ∨ ¬D
     ---------------
          A ∨ B ∨ C

EWD731 - 4

and our two individual inferences would have been of the traditional form of the transitive implication.

* *
*

I know that firm believers in the so-called "natural deduction" will state that, in the case of Lemma 2, I am just "deducing naturally" that A follows from the "assumption" ¬E. In this appreciation they will find themselves strengthened by the observation that in that proof all assertions start with "E ∨". They have a point, but the point is weak. Look at the structure of the proof as a whole. Lemmata 1, 2, and 3 capture it; from there rule (4) does the job, and at that level it is very arbitrary to subdivide assertions into assumptions and conclusions.

Remark. Observing the seven triples xyz for a pair (x,y) such that x | y , the argument proving Lemma 2 can equally well be phrased in terms of assertions starting with "A ∨". In the sense used above also Lemma 2 is obvious. (End of remark.)

Plataanstraat 5
5671 AL NUENEN
The Netherlands		 27 February 1980
prof.dr. Edsger W. Dijkstra
Burroughs Research Fellow

Transcription by John C Gordon

Last revised on Tue, 24 Jun 2003.