{"id":3829,"date":"2013-11-18T06:25:33","date_gmt":"2013-11-18T05:25:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3829"},"modified":"2013-11-18T06:35:03","modified_gmt":"2013-11-18T05:35:03","slug":"godels-incompleteness-theorems","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/godels-incompleteness-theorems\/","title":{"rendered":"G\u00f6del&#8217;s incompleteness theorems"},"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 metal\u00f3gica titulado <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Incompleteness\/document.pdf\">G\u00f6del&#8217;s incompleteness theorems<\/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>\nG\u00f6del&#8217;s two incompleteness theorems are formalised, following a careful <a href=\"http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html\">presentation by Swierczkowski<\/a>, in the <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/the-hereditarily-finite-sets\/\">theory of hereditarily finite sets<\/a>. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/afp.sourceforge.net\/entries\/Incompleteness.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-Incompleteness-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 metal\u00f3gica titulado G\u00f6del&#8217;s incompleteness theorems. Su autor es Lawrence C. Paulson (de la Universidad de Cambridge). Su resumen es G\u00f6del&#8217;s two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted&#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\/3829"}],"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=3829"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3829\/revisions"}],"predecessor-version":[{"id":3834,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3829\/revisions\/3834"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3829"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3829"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3829"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}