A Cry for Generalization in Mathematics
In the Spring of 1981, A.J.M. van Gasteren and E.W. Dijkstra wanted to understand "how to tame the complexity of artefacts such as proofs and programs". In hindsight it is no surprise that Dijkstra's rallying cry for generalization in programming of the early 1960s is reflected in his work of the early 1980s with regards to proving mathematical theorems. Some examples below will illustrate this, based on AvG5/EWD788.
As a first example, Van Gasteren and Dijkstra mentioned that "the mathematical community still hesitates whether zero is a natural number". This hesitation became apparent to them after having asked mathematicians to prove a theorem about the p-ary representation of a natural number n. Van Gasteren and Dijkstra noted that:
[M]ost mathematicians introduced a case analysis depending on whether n+1 was divisible by p or not, unaware of the fact that the argument about the length of the train of trailing zeros of the p-ary representation of n+1 is also applicable when that train is empty. [AvG5/EWD788 - 2]
By generalizing the notion of natural number in order to include zero (as opposed to treating it as a special case) Van Gasteren and Dijkstra explained that the theorem could be proved without having to introduce case distinctions at all.
By discussing some more proofs conducted by their mathematical colleagues, Van Gasteren and Dijkstra showed that it is often unfavorable to treat zero as a special number. They also made the analogy with classical Greece: Euclid had to present two separate proofs for his greatest-common-divisor algorithm because, in those times, one was not treated as a natural number either. Extrapolating to natural language, Van Gasteren and Dijkstra provided one explicit reason to be formally rigorous:
It can be argued that our Western languages with their singular and plural forms keep these distinctions alive. The circumstance offers a further advantage of formal over verbal arguments. [AvG5/EWD788 - 3]