Re: [isabelle] [EXTERNAL] new in the AFP: Recursion Theorem in ZF




> On May 13, 2020, at 10:38 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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://urldefense.com/v3/__https://www.isa-afp.org/entries/Recursion-Addition.html__;!!Nv3xtKNH_4uope0!2IPP6o6PVHRPP2wjTA5naVZLOniuj8Y0Be6PpoK-DvoLa3UZ8olbpwkBQdevY7c$ 
> 
> Larry Paulson
> 
> 
> 
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.