{"id":3587,"date":"2013-09-02T08:18:06","date_gmt":"2013-09-02T06:18:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3587"},"modified":"2013-09-02T08:21:12","modified_gmt":"2013-09-02T06:21:12","slug":"a-mechanised-proof-of-godels-incompleteness-theorems-using-nominal-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-mechanised-proof-of-godels-incompleteness-theorems-using-nominal-isabelle\/","title":{"rendered":"A mechanised proof of G\u00f6del&#8217;s incompleteness theorems using Nominal Isabelle"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre metal\u00f3gica titulado <a href=\"http:\/\/www.cl.cam.ac.uk\/~lp15\/Pages\/G\u00f6del-ar.pdf\">A mechanised proof of G\u00f6del&#8217;s incompleteness theorems using Nominal Isabelle<\/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 <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> formalisation of <a href=\"http:\/\/en.wikipedia.org\/wiki\/G%C3%B6del%27s_incompleteness_theorems\">G\u00f6del\u2019s two incompleteness theorems<\/a> is presented. Aspects of the development are described in detail, including two separate treatments of variable binding: the <a href=\"http:\/\/www4.in.tum.de\/~urbanc\/Publications\/esop-11.pdf\">nominal package<\/a> and <a href=\"http:\/\/www.win.tue.nl\/automath\/archive\/pdf\/aut029.pdf\">de Bruijn indices<\/a>. The work follows <a href=\"http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html\">\u015awierczkowski\u2019s a detailed proof<\/a>, using <a href=\"http:\/\/ncatlab.org\/nlab\/show\/hereditarily+finite+set\">hereditarily finite set<\/a> theory.<\/p>\n<p>The machine proofs are fairly readable, thanks to the structured Isar proof language, and concise at under 14,000 lines for both theorems. The paper presents highlights of the proof, commenting on the advantages and disadvantages of the nominal framework and HF set theory. The proof reported here closely follows a detailed exposition by \u015awierczkowski. His careful and detailed proofs were indispensable, but significant deviations proved to be necessary. For the first time, we have complete, formal proofs of both theorems. They take the form of structured Isar proof scripts that can be examined interactively.<\/p>\n<p>The total proof length of 14000 lines comprises 5000 lines for the second theorem and 9000 lines for the first. (One could also include 3000 lines for HF set theory itself, but then we may as well also count the standard libraries of natural numbers.)<\/p>\n<p>This project took approximately one year, in time left available after fulfilling a Professor\u2019s usual teaching and administrative duties. The underlying set theory took only two weeks to formalise. The G\u00f6del development up to the proof formalisation condition took another five months. From there to the first incompleteness theorem took a further two months, mostly devoted to proving single valued properties. Then the second incompleteness theorem took a further four months, including much time wasted due to misunderstanding this perplexing material.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre metal\u00f3gica titulado A mechanised proof of G\u00f6del&#8217;s incompleteness theorems using Nominal Isabelle. Su autor es Lawrence C. Paulson (de la Universidad de Cambridge). Su resumen es A Isabelle\/HOL formalisation of G\u00f6del\u2019s two incompleteness theorems is presented. Aspects of the development are described in detail,&#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":[8,100],"tags":[217,144,216,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\/3587"}],"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=3587"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3587\/revisions"}],"predecessor-version":[{"id":3588,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3587\/revisions\/3588"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3587"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3587"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3587"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}