Email Gateway (Aug 23 2022 at 09:08): Email Gateway (Aug 23 2022 at 09:08):From: Lawrence Paulson <lp15@cam.ac.uk>
You wait hours for a bus and then two come along at the same time. And so somehow, the first ever AFP entry for Isabelle/ZF has been followed by a second entry: "Recursion Theorem in ZF", by Georgy Dunaev:
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.
It’s online at https://www.isa-afp.org/entries/Recursion-Addition.html
Larry Paulson
Last updated: Apr 25 2024 at 16:19 UTC