Mathematical Induction Made Calculational

摘要

Several concise formulations of mathematical induction are presented and provenequivalent. The formulations are expressed in variable-free relation algebra and thus are in terms of relations only, without mentioning the related objects. It is shown that the induction principle in this form lends itself very well for use in calculational proofs. As a non-trivial example a proof of a generalization of Newman's lemma is given. The paper begins with an introduction to relation algebra and is reasonably self-contained. The style is expository and suggestions for exercises are included. The basic concept underlying many of the calculations is the notion of a Galois connection, and the paper could be seen as an introductory tutorial in the use of this concept.