{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:58Z","timestamp":1774984078751,"version":"3.50.1"},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,4,3]],"date-time":"2014-04-03T00:00:00Z","timestamp":1396483200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2014,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A formalization of G\u00f6del\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 \u015awierczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of this theory is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalization itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.<\/jats:p>","DOI":"10.1017\/s1755020314000112","type":"journal-article","created":{"date-parts":[[2014,4,3]],"date-time":"2014-04-03T13:22:50Z","timestamp":1396531370000},"page":"484-498","source":"Crossref","is-referenced-by-count":19,"title":["A MACHINE-ASSISTED PROOF OF G\u00d6DEL\u2019S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS"],"prefix":"10.1017","volume":"7","author":[{"given":"LAWRENCE C.","family":"PAULSON","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,4,3]]},"reference":[{"key":"S1755020314000112_ref6","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610026"},{"key":"S1755020314000112_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"S1755020314000112_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569883"},{"key":"S1755020314000112_ref15","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"S1755020314000112_ref1","volume-title":"The Logic of Provability","author":"Boolos","year":"1993"},{"key":"S1755020314000112_ref10","unstructured":"Paulson L. C . (2013). A mechanised proof of G\u00f6del\u2019s incompleteness theorems using Nominal Isabelle. Submitted for publication."},{"key":"S1755020314000112_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"S1755020314000112_ref13","unstructured":"Shankar N . (2013). Shankar, Boyer, Church-Rosser and de Bruijn indices. E-mail."},{"key":"S1755020314000112_ref8","first-page":"245","volume-title":"TPHOLs","volume":"3603","author":"O\u2019Connor","year":"2005"},{"key":"S1755020314000112_ref11","volume-title":"Proof-checking Metamathematics","author":"Shankar","year":"1986"},{"key":"S1755020314000112_ref14","doi-asserted-by":"publisher","DOI":"10.4064\/dm422-0-1"},{"key":"S1755020314000112_ref3","volume-title":"Kurt G\u00f6del: Collected Works","volume":"I","author":"Feferman","year":"1986"},{"key":"S1755020314000112_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S1755020314000112_ref16","volume-title":"From Insight to Proof \u2014 Festschrift in Honour of Andrzej Trybulec","volume":"10","author":"Wenzel","year":"2007"},{"key":"S1755020314000112_ref9","volume-title":"Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory","author":"O\u2019Connor","year":"2009"},{"key":"S1755020314000112_ref4","doi-asserted-by":"publisher","DOI":"10.1201\/b10700"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020314000112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T01:08:03Z","timestamp":1555895283000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020314000112\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,3]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["S1755020314000112"],"URL":"https:\/\/doi.org\/10.1017\/s1755020314000112","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,3]]}}}