A Relation-Algebraic Treatment of the Dedekind Recursion Theorem

The recursion theorem of Richard Dedekind is fundamental for the recursive definition of mappings on natural numbers since it guarantees that the mapping in mind exists and is uniquely determined. Usual set-theoretic proofs are partly intricate and become lengthy when carried out in full detail. We present a simple new proof that is based on a relation-algebraic specification of the notions in question and combines relation-algebraic laws and equational reasoning with Scott induction. It is very formal and most parts of it consist of relation-algebraic calculations. This opens up the possibility for mechanised verification. As an application we prove a relation-algebraic version of the Dedekind isomorphism theorem. Finally, we consider two variants of the recursion theorem to deal with situations which frequently appear in practice but where the original recursion theorem is not applicable.