{"id":3827,"date":"2013-11-18T06:23:36","date_gmt":"2013-11-18T05:23:36","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3827"},"modified":"2013-11-18T06:27:09","modified_gmt":"2013-11-18T05:27:09","slug":"the-hereditarily-finite-sets","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/the-hereditarily-finite-sets\/","title":{"rendered":"The hereditarily finite sets"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento aproximado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL<\/a> sobre la teor\u00eda de conjuntos titulado <a href=\"http:\/\/afp.sourceforge.net\/entries\/HereditarilyFinite.shtml\">The hereditarily finite sets<\/a>.  <\/p>\n<p>Su autor es <a href=\"https:\/\/www.cl.cam.ac.uk\/~lp15\/\">Lawrence C. Paulson<\/a> (de la Universidad de Cambridge). <\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nThe theory of hereditarily finite (HF) sets is formalised, following the <a href=\"http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html\">development of Swierczkowski<\/a>. An HF set is a finite collection of other HF sets; they enjoy an induction principle and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated. All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers, functions) without using infinite sets are possible here. The definition of addition for the HF sets follows <a href=\"http:\/\/faculty.baruch.cuny.edu\/lkirby\/mlqarticlejan2007.pdf\">Kirby<\/a>. <\/p>\n<p>This development forms the foundation for the Isabelle proof of G\u00f6del&#8217;s incompleteness theorems, which has been <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/godels-incompleteness-theorems\/\">formalised separately<\/a>.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/afp.sourceforge.net\/entries\/HereditarilyFinite.shtml\">The Archive of Formal Proofs<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/afp.sourceforge.net\/release\/afp-HereditarilyFinite-current.tar.gz\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento aproximado en Isabelle\/HOL sobre la teor\u00eda de conjuntos titulado The hereditarily finite sets. Su autor es Lawrence C. Paulson (de la Universidad de Cambridge). Su resumen es The theory of hereditarily finite (HF) sets is formalised, following the development of Swierczkowski. An HF set is a finite collection&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3827"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3827"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3827\/revisions"}],"predecessor-version":[{"id":3831,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3827\/revisions\/3831"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3827"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3827"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3827"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}