{"entities":{"Q40326":{"pageid":40382,"ns":120,"title":"Item:Q40326","lastrevid":105427346,"modified":"2026-10-09T10:07:24Z","type":"item","id":"Q40326","labels":{"en":{"language":"en","value":"Incompleteness Theorems"}},"descriptions":{"en":{"language":"en","value":"AFP entry Incompleteness"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"71200051a4f6a200d77e2cd8d616b1e5277d0c74","datavalue":{"value":"28612","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40326$DD6B13AF-C32D-409C-8BA5-2E1B408E6791","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$41A53952-D129-41E4-8EC9-51A3E023F4FA","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"cefc4d0c54875679b8a395b2540497b75755f056","datavalue":{"value":"https://www.isa-afp.org/entries/Incompleteness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40326$A2A8A5D0-715E-4599-B557-8752F5306BF1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40326$E6CA6ED3-CBD2-4B60-9EBF-E71B98209C4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40326$5212DF59-D54E-435A-B1CA-80F11A5D3BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40326$FCE85242-26BC-4FF1-A9B9-FE4EBA0641A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40326$B16DA408-7A99-455C-906C-0C7800F23FD8","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$92D50B24-09F7-4941-9F20-5BF2F1A07E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$D0B871F3-B889-41B8-9B78-EF2D93D7815A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$8C2FD622-E730-4B47-BBDF-C33EA5C7C112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f1bbc3872a55b3dfa074c96d37fd46f076f92caa","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$24BFF2D9-B7B3-4462-A7CE-E49B4575DB67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"493c5144a9d14f0b980d45769fb4b197b51b453c","datavalue":{"value":{"entity-type":"item","numeric-id":40555,"id":"Q40555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$B4272A35-0D2A-4FD3-875F-2D2DE0C5BB65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"37701d360bad336addd4a826712aca6608c48c21","datavalue":{"value":{"entity-type":"item","numeric-id":40554,"id":"Q40554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$44F3644F-4B67-4D55-8329-E7FE9D421ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b677ab36580483ca33e96c40f998e187dadaa8b2","datavalue":{"value":{"entity-type":"item","numeric-id":40553,"id":"Q40553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$2155C14F-128E-45F4-B43B-900D38A43746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$D304ED26-67CC-41D6-944B-4A524AC6631F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6953b82ed35a5241d6fb5d47b5912e5553edbeaf","datavalue":{"value":{"entity-type":"item","numeric-id":40298,"id":"Q40298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$6ED17173-CF53-46CE-9590-EC10FBC38CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"861e34f6b532f04d877297070a58fb137923d509","datavalue":{"value":{"entity-type":"item","numeric-id":40509,"id":"Q40509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$4280D1E3-A34D-48C0-A67F-C582F1D64ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0a329d132b963c571723538ca5cd1b467b324fe","datavalue":{"value":{"entity-type":"item","numeric-id":40325,"id":"Q40325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$002DC91F-FF5A-4A68-8343-C60E0E9C6F20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0204f081facf570c6ab1a272475183b48ae5e4f2","datavalue":{"value":{"entity-type":"item","numeric-id":40286,"id":"Q40286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$27A826C9-7081-4DE0-8E26-50A4D7DCAB92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7ef1082544496cdbd626aabd0ffce07a1cf4d46a","datavalue":{"value":{"entity-type":"item","numeric-id":40285,"id":"Q40285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$6C3DEF69-3666-4801-8072-CD974B601BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab75a27745b95bbc51eed60e2ef7157b7c449125","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$F7C1BAF7-0FDD-472B-B789-6FD68E2F3338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9a2aad95369d69c08086a6600b609b3220c2705e","datavalue":{"value":{"entity-type":"item","numeric-id":40276,"id":"Q40276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$04056F93-87F1-422C-825C-5F1B918EAC18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a3d1e0e198e45cd480c75f3cdc16c51aa12a9827","datavalue":{"value":{"entity-type":"item","numeric-id":43931,"id":"Q43931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$3911B686-292C-4CEA-A5E8-BC857F9D55A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"90ccaf8bd8cd77886514793cbc9a0a922682a7f1","datavalue":{"value":{"entity-type":"item","numeric-id":31430,"id":"Q31430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$C8112866-BFED-4B2F-980D-B549DD20B705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1da83e82f563b21e91a419cb34e11d3be154209f","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$23D0A17F-8263-4CDB-9146-6D29569530F4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d867865e18fbf0f82e20aabe69abb54999e3f8ba","datavalue":{"value":"https://isa-afp.org/entries/Incompleteness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40326$AA742E72-1271-40FC-9415-C68A14299852","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7479166f83b44c07c9a493479bd3c0ed2c72ef23","datavalue":{"value":"Lawrence C. Paulson","type":"string"},"datatype":"string"},"type":"statement","id":"Q40326$79AF3373-206B-41AC-B3C8-FFDEAF56951E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f38f8279d7035817b3b00bc0178d2aa1efba272c","datavalue":{"value":"G\u00f6del'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 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. L\u00f6b's theorem states that we have that $\\mathsf{HF} \\vdash \\mathsf{PfP}(\\ulcorner \\varphi \\urcorner) \\rightarrow \\varphi$ implies $\\mathsf{HF} \\vdash \\varphi$, where the formula $\\mathsf{PfP}(x)$ is the standard provability predicate for $\\mathsf{HF}$. It is a strengthening of G\u00f6del's second incompleteness theorem, which can be recovered via $\\varphi := \\bot$. The formalised argument follows a modern textbook presentation of L\u00f6b's argumentation by Smith via the Hilbert-Bernays-L\u00f6b derivability conditions. The formalisation of L\u00f6b's theorem is part of Janis Bailitis's Bachelor's thesis completed at Saarland University in 2024.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40326$39898AB8-1ACE-40CE-A76C-A49B8EE88072","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"845969487dd8e0c91747e5b0285df64cc79ce670","datavalue":{"value":{"entity-type":"item","numeric-id":4397069,"id":"Q4397069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$96C91548-DE18-4AE4-AAF6-38AD188C97F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cec0c6339a6656b04c8db9d9f87d70c68dd44245","datavalue":{"value":{"entity-type":"item","numeric-id":571218,"id":"Q571218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$52239919-5ADC-4DE4-8AF4-6E3CCC6C8A84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d14e6969de02cf5a19417906c0c5f01258599367","datavalue":{"value":{"entity-type":"item","numeric-id":5772177,"id":"Q5772177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$ED75C973-D343-441C-B691-1C941E62E266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55f8c2b319d70b60be30ee404d4dbd182565eb7","datavalue":{"value":{"entity-type":"item","numeric-id":3423150,"id":"Q3423150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$8696401A-7D31-4F6B-BBD7-D8E64EB558CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac1103109f5e36aeeaaf4d39c1229005c3254b87","datavalue":{"value":{"entity-type":"item","numeric-id":3227564,"id":"Q3227564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$D5EEE69F-B591-4AA7-A88B-BC8253C6960C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c05aa45210aebb87236e38d8954563df144e4d","datavalue":{"value":{"entity-type":"item","numeric-id":2940885,"id":"Q2940885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$F9902C5E-024A-42BE-865D-E66EE9A3BE52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aab84f6aaf590fa756248847abc358b761eb7958","datavalue":{"value":{"entity-type":"item","numeric-id":286772,"id":"Q286772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$0151D182-05B8-4D2C-92EC-3A2CC4250BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43d16eadd7d770e36314c60d303dfa1744d54a29","datavalue":{"value":{"entity-type":"item","numeric-id":5109248,"id":"Q5109248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$ADF556E1-6B74-4830-B78C-DA8BA3152603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a251d54cb8d77477d7b56edd116f203ae2ce0345","datavalue":{"value":{"entity-type":"item","numeric-id":4829437,"id":"Q4829437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$5E3A48F8-EF3A-4B1D-9435-3033EA361FB7","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"76069a6d59279efa1dd2eb6eeafe6968fbde0cc3","datavalue":{"value":{"entity-type":"item","numeric-id":7361169,"id":"Q7361169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$FC0AD655-6482-4C82-AC85-1D327B9E0FB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"947633d77ac0c595dad38098201be725b355abe0","datavalue":{"value":{"entity-type":"item","numeric-id":7361006,"id":"Q7361006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$75BDEE98-2BB8-42C6-B394-698239470D19","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3a591a0a7680cf5422afb615fc9041972e3bd7c4","datavalue":{"value":{"time":"+2013-11-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40326$6418743A-8EA7-4E3A-B410-41AED3FA9853","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"678098e70e6ea2192dd0a13a13f6052adbcbc35a","datavalue":{"value":{"text":"G\u00f6del's Incompleteness Theorems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40326$C38B1893-3BC4-453B-888E-3E6BDACDDF06","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$22251E5F-2960-4BF4-BF51-C4EA9414B697","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40326$F3607C8C-2045-4DF0-B3B7-E66571BD5964","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Incompleteness Theorems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Incompleteness_Theorems"}}}}}