{"entities":{"Q892146":{"pageid":893994,"ns":120,"title":"Item:Q892146","lastrevid":52397333,"modified":"2026-01-22T13:38:15Z","type":"item","id":"Q892146","labels":{"en":{"language":"en","value":"Normalization proof for Peano arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6511009"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$314A840F-B6AE-4261-B1FE-CA3957666468","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bb44e60c35c05b3f0373f0b969971ef59d8f7fbf","datavalue":{"value":{"text":"Normalization proof for Peano arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q892146$D1196656-2D86-4EE4-9699-D01568F0F78D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d0966f95201469bbe3d75ef12fc1d3ae61841205","datavalue":{"value":"1339.03050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$7FFFECE2-8B41-451B-9A6C-D9CE8FB2B426","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$139F77D8-F04A-430C-9797-D5EF4FDCA1AF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"482b7978385e0be0d8ea5afcf93e349a724cc633","datavalue":{"value":{"time":"+2015-11-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q892146$9A5E86BF-DE02-4263-A79C-22D0A50013F4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d755e43d82df9968c20ffb585e611d7cff78b9de","datavalue":{"value":"The main purpose of the paper is to prove normalization of Peano arithmetic formulated in a standard natural deduction with an ordinal assignment originating in Howard's normalization proof for G\u00f6del's T. The result is a generalization of an argument found in an earlier paper by \\textit{A. Kanckos} [Math. Log. Q. 56, No. 6, 611--624 (2010; Zbl 1219.03072)] where a consistency proof for Heyting arithmetic was given.","type":"string"},"datatype":"string"},"type":"statement","id":"Q892146$FB5214E0-C3D2-4120-B9C7-6DFEC0EF3F50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$0BD2B678-F20D-4941-AB26-CABA41B3F4BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$FD62978E-9608-45F3-B717-6582E3184B6A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"23b8496f9a8e14598a9757b2eda0668f690a1152","datavalue":{"value":"6511009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$D9BD2A80-A1E7-41C6-84B4-E237D09A7A22","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4296281254337308ad2c5f734043898466afdb58","datavalue":{"value":"normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q892146$39E2E4B7-6765-4D80-9C64-4FC2BD8FF8AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q892146$7C9B4455-0108-4924-A5A0-ED590FB18958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q892146$BD90160E-B005-47E0-81F8-1FFAB71879F1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ea68be1d5bbf01a939b97478f823720bfc73a97b","datavalue":{"value":{"entity-type":"item","numeric-id":1734261,"id":"Q1734261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$1DC9E9AF-3684-423C-884E-920A88B37658","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"c45938d3b1c1a5c68183caabb02f42934d9ff682","datavalue":{"value":{"entity-type":"item","numeric-id":588140,"id":"Q588140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$CD21D69B-D4C4-4ACB-8B0C-C73AA6FD8844","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$221401B6-4DBE-4201-B0D8-6A11F568BC24","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b8037150331658871391d325d6f4d5436e34dc22","datavalue":{"value":"https://doi.org/10.1007/s00153-015-0450-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q892146$3058934A-3D73-46D0-99EF-0FB6AEB31FAD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d050313b802873352c0c5491ac71fab073f1e559","datavalue":{"value":"W2188987066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$C1A34255-0CA9-4EC0-AF76-991F6C85DBE0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"197f75f5cd86020e5cc4ef15f910d8be341c9f00","datavalue":{"value":{"entity-type":"item","numeric-id":5606582,"id":"Q5606582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$9BD764D6-4F65-40B3-B419-29675BE3C9A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69db4f067537cf0b31837c2e33b8f5372d860fa8","datavalue":{"value":{"entity-type":"item","numeric-id":3066292,"id":"Q3066292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$DC36686B-9AD8-4028-A47B-26130F07AB3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$4DE0EDD0-5721-4AAE-A447-1C31D36B61D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"507357060ccf4ffd97307cff2b14103f61ed17de","datavalue":{"value":{"entity-type":"item","numeric-id":5361247,"id":"Q5361247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$338F6E10-7208-46D4-9A41-3640034C13D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7562aac9e55441da819b7300f30f0118e747a6a8","datavalue":{"value":{"entity-type":"item","numeric-id":2377348,"id":"Q2377348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q892146$9A8DD0A5-9767-4A19-8727-7136F7C1E1B5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"663314a5920bea0b95e52acba7469f3a0f563c19","datavalue":{"value":"10.1007/S00153-015-0450-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q892146$322B7E57-D8DD-440D-8FD5-83C1AA4CA2F9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea5f5bb423a10705dd76c66bf44abada43e76174","datavalue":{"value":{"entity-type":"item","numeric-id":5361247,"id":"Q5361247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2750edb92ddc38882d18b9565b561589c3c5b25f","datavalue":{"value":{"amount":"+0.8241832852363586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q892146$792C8E53-A142-4252-9819-4D46DAEA5EF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"945ff30d1bfaf814e2be4227312eea6ee3a8471d","datavalue":{"value":{"entity-type":"item","numeric-id":3066292,"id":"Q3066292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d71c774490fc729404e615efdffba926b546a9e5","datavalue":{"value":{"amount":"+0.7614820003509521","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q892146$E6BE1788-037E-4401-9C3B-A2CFCDDAE39B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4ccc37c0744196bfba574342b120191f55749e1","datavalue":{"value":{"entity-type":"item","numeric-id":3999386,"id":"Q3999386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"335719d7d441fd2ce5b696498c5a3bdb4f1cee2d","datavalue":{"value":{"amount":"+0.7486891746520996","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q892146$EAE6CD90-9672-497E-BF1D-A2BCE2319063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30d1fc8028bcdbfe91e535c9e35c30ce392d1950","datavalue":{"value":{"entity-type":"item","numeric-id":4304806,"id":"Q4304806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"229139a8cc2a1b0d06d8499d5788e11a18acf700","datavalue":{"value":{"amount":"+0.7313673496246338","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q892146$1ACFAEFA-681B-4BBE-8ED6-D5743E34531E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d348a38c7a1069e80a95427043d7d77b16e16eb5","datavalue":{"value":{"entity-type":"item","numeric-id":2367413,"id":"Q2367413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"229139a8cc2a1b0d06d8499d5788e11a18acf700","datavalue":{"value":{"amount":"+0.7313673496246338","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q892146$0D88B5EA-A193-44DC-BA3D-F9036D203E95","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:892146","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:892146"}}}}}