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

```           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

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

 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 ```

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.