A CALCULATIONAL APPROACH TO MATHEMATICAL INDUCTION

Several concise formulations of mathematical induction are presented a nd proved equivalent. The formulations are expressed in variable-free relation algebra and thus are in terms of relations only, without ment ioning the related objects, It is shown that the induction principle i n this form, when combined with the explicit use of Galois connections , lends itself very well for use in calculational proofs. Two non-triv ial examples are presented, The first is a proof of Newman's lemma. Th e second is a calculation of a condition under which the union of mio well-founded relations is well-founded. In both cases the calculations lead to generalisations of the known results. In the case of the latt er example, one lemma generalises three different conditions.