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



Resending, the cartoon didn’t come through
https://media.newyorker.com/cartoons/5e90ed84fe3260000878c2a7/master/w_1160,c_limit/200420_a23997_706.jpg <https://media.newyorker.com/cartoons/5e90ed84fe3260000878c2a7/master/w_1160,c_limit/200420_a23997_706.jpg>



> On May 13, 2020, at 10:59 AM, Richard Waldinger <waldinger at AI.SRI.COM> wrote:
> 
> 
> 
>> 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.