{"id":383,"date":"2021-07-26T11:05:42","date_gmt":"2021-07-26T11:05:42","guid":{"rendered":"http:\/\/synasc.ro\/2021\/?page_id=383"},"modified":"2021-11-23T09:53:24","modified_gmt":"2021-11-23T09:53:24","slug":"cristian-s-calude","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2021\/cristian-s-calude\/","title":{"rendered":""},"content":{"rendered":"\n<h2 class=\"has-text-align-center wp-block-heading\">G\u00f6del Incompleteness and Proof Assistants<\/h2>\n\n\n\n<h3 class=\"has-text-align-center wp-block-heading\">by Cristian S. Calude, University of Auckland, New Zealand<\/h3>\n\n\n\n<p class=\"has-text-align-center\"><strong>Abstract:<\/strong><\/p>\n\n\n\n<p>G\u00f6del&#8217;s first incompleteness theorem states that in every consistent system of axioms which contains a modicum of arithmetic&nbsp;&nbsp;and its theorems can be listed by an algorithm, there exist true statements about natural numbers that are unprovable in the&nbsp;&nbsp;system. The second incompleteness theorem states that such a system cannot demonstrate its own consistency. J. von Neumann&nbsp;&nbsp;called them &#8220;a landmark which will remain visible far in space and time.&#8221;<\/p>\n\n\n\n<p>The talk will briefly show that both incompleteness results follow from the undecidability of the Halting problem. Then we will discuss theoretically whether the incompleteness results give a &#8220;coup de gr\u00e2ce&#8221; to Hilbert\u2019s Programme. Finally, we will argue that the current practice of mathematics, which uses extensively proof-assistants, is changing the theoretical views about the impact of incompleteness.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>G\u00f6del Incompleteness and Proof Assistants by Cristian S. Calude, University of Auckland, New Zealand Abstract: G\u00f6del&#8217;s first incompleteness theorem states that in every consistent system of axioms which contains a modicum of arithmetic&nbsp;&nbsp;and its theorems can be listed by an algorithm, there exist true statements about natural numbers that are unprovable in the&nbsp;&nbsp;system. The second [&hellip;]<\/p>\n","protected":false},"author":23,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-383","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/pages\/383","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/users\/23"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/comments?post=383"}],"version-history":[{"count":3,"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/pages\/383\/revisions"}],"predecessor-version":[{"id":595,"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/pages\/383\/revisions\/595"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2021\/wp-json\/wp\/v2\/media?parent=383"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}