{"id":3796,"date":"2013-11-03T07:29:37","date_gmt":"2013-11-03T06:29:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3796"},"modified":"2013-11-03T07:29:37","modified_gmt":"2013-11-03T06:29:37","slug":"a-machine-assisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-machine-assisted-proof-of-godels-incompleteness-theorems-for-the-theory-of-hereditarily-finite-sets\/","title":{"rendered":"A machine-assisted proof of G\u00f6del&#8217;s incompleteness theorems for the theory of hereditarily finite sets"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle<\/a> titulado <a href=\"http:\/\/www.cl.cam.ac.uk\/~lp15\/Pages\/G\u00f6del-logic.pdf\">A machine-assisted proof of G\u00f6del&#8217;s incompleteness theorems for the theory of hereditarily finite sets<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/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>\nA formalisation of G\u00f6odel\u2019s incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows <a href=\"http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html\">\u015awierczkowski (2003)<\/a>, who gave a detailed proof using hereditarily finite set theory. The adoption of HF is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle titulado A machine-assisted proof of G\u00f6del&#8217;s incompleteness theorems for the theory of hereditarily finite sets. Su autor es Lawrence C. Paulson (de la Universidad de Cambridge). Su resumen es A formalisation of G\u00f6odel\u2019s incompleteness theorems using the Isabelle proof assistant is described. This is apparently&#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":[100],"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\/3796"}],"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=3796"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3796\/revisions"}],"predecessor-version":[{"id":3797,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3796\/revisions\/3797"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3796"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3796"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3796"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}