Recursion Theorem in ZF

Georgy Dunaev 📧

May 11, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This document contains a proof of the recursion theorem. This is a mechanization of the proof of the recursion theorem from the text Introduction to Set Theory, by Karel Hrbacek and Thomas Jech. This implementation may be used as the basis for a model of Peano arithmetic in ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development is much easier to follow.


BSD License


Session Recursion-Addition