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 ∨ DThe 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)
|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,|
|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.|
|E:||there exists a mathematician that can communicate with more than three others,|
|G:||for each x, the equation x | u has at least five different solutions for u,|
E ∨ G (6)
|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,|
E ∨ H . (7)Applying rule (4) to assertions (6) and (7) we find E ∨ (G ∧ H) ,
|E ∨||"for each x, the equation x | y ∧ x | z ∧ y | z has at least one solution in y and z".|
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)
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
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.)
5671 AL NUENEN
27 February 1980
prof.dr. Edsger W. Dijkstra
Burroughs Research Fellow
Last revised on