{"entities":{"Q691121":{"pageid":692970,"ns":120,"title":"Item:Q691121","lastrevid":63755883,"modified":"2026-04-11T15:20:16Z","type":"item","id":"Q691121","labels":{"en":{"language":"en","value":"A simple proof that super-consistency implies cut elimination"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6111344"}},"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":"Q691121$4D029A69-B1E0-4BA2-991A-E19ADA69B928","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a64f78c62f45ad22aa74fcadb13254f8099a7976","datavalue":{"value":{"text":"A simple proof that super-consistency implies cut elimination","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q691121$36F6BD89-57DB-4EE4-8C36-C4912AACB2D4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6dfcd4923fecb904c802847dc3449419221b0b4f","datavalue":{"value":"1270.03120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$374A20C0-21AA-4485-A2E0-6FE694FBF0CA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c11dd57c540527f3cbe4f0dd82236e860c1074c5","datavalue":{"value":"10.1215/00294527-1722692","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$7EEE5D90-4CEE-449F-B52D-7BAAB5FF02F3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$895FBC2C-84BC-43D9-9D67-E5502088BF8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5c8810b28319eddf2176b081cd070119a2cf8c13","datavalue":{"value":{"entity-type":"item","numeric-id":281285,"id":"Q281285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$6AA5CFC1-6F33-403C-9FFB-19A0E14775AB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$98317544-6F98-467C-A6B9-7E5E08A2DD3D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dd1dd78b610951b080ce7917880823f8267fcfa0","datavalue":{"value":{"time":"+2012-11-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q691121$164C9A14-86B5-4B30-8BF8-963C70C92A90","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0332559ccd3383b72a6e954d73c06149e34b004e","datavalue":{"value":"https://projecteuclid.org/euclid.ndjfl/1352383225","type":"string"},"datatype":"url"},"type":"statement","id":"Q691121$CF72F29D-7EBC-4A64-B5D5-ED5BEB226D65","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$D4C3E9C4-2D0D-4E32-90FD-3ED67CB2CB31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$65772455-9767-4D29-8B7A-73AFE4A93EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed0e9d16aabdfc4de2754948a872b6ceb30bba56","datavalue":{"value":"03C90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$1C8500F9-BB06-4F9E-BC93-E7886B67289E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6fa4c52bc53d188453da7bc2e6f6ef47a3eedd43","datavalue":{"value":"6111344","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$1665B6D2-E479-4EDD-84E3-D1A625B85C39","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"908a412ea1d66c8c3e12f690543d47d72647ae57","datavalue":{"value":"deduction modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q691121$022EA067-3B88-4E8A-81E8-ABA9F3229A52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"94fe175cdf9cd60f2d45f3b2a38cb419c178c78f","datavalue":{"value":"super-consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q691121$7536B9FC-7B81-4146-AEDF-64E02061CA2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q691121$1B53E9E7-2AED-4A2A-A130-220D02B171EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50ac0247726491e51a1a9dad4fadbff313f8e488","datavalue":{"value":"simple type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q691121$4055D867-71BB-4AAE-9488-3D46CFD79B26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q691121$AF46CC3F-2A8F-4A49-8770-574EA1118510","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":"Q691121$1D253C84-2675-4D64-8EFA-3C1DDEBA1901","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5182b3016e0964d966d60fb16b47c1c8876bc44c","datavalue":{"value":"W2081303576","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q691121$2BA00739-6435-457F-AB66-9B6C91875DB4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0021eb1ef45a5b93ce1d9b7eb620338bc69ad123","datavalue":{"value":{"entity-type":"item","numeric-id":5638281,"id":"Q5638281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$7FD77653-32E2-4398-9193-F97912EAF53D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$7938DE6D-C6D2-4931-80EB-96A480F7DA3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"491d79ebb333824e2a1d28fa415eece5d0654a36","datavalue":{"value":{"entity-type":"item","numeric-id":3371147,"id":"Q3371147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$48682FAA-54C4-466A-8173-586B7E8E411E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74d4e38bc26a617ad6c486910865ea965b523631","datavalue":{"value":{"entity-type":"item","numeric-id":3612439,"id":"Q3612439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$E7E79B28-6380-409A-A50A-D69627191778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a571653cb6ab1fa29a33b3cbc9d3383816e568e","datavalue":{"value":{"entity-type":"item","numeric-id":2713352,"id":"Q2713352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$31C19D76-13AD-43EF-8C58-3716F84310BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$9B4192CA-8DD3-4E4A-BD94-090183454DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00050bf08d8c66ff630f04c504e55da93f3d3677","datavalue":{"value":{"entity-type":"item","numeric-id":5432335,"id":"Q5432335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$F20995F8-EC5F-4FC5-9D3B-E772B6EB33BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e52f792aed007740441efa3e7b7b70e2d7b6c5c","datavalue":{"value":{"entity-type":"item","numeric-id":4650285,"id":"Q4650285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$D035511C-FFA2-41DB-BE2C-373262FC72A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2cede8cff36dcae45222f51a4a5b72320348ad0","datavalue":{"value":{"entity-type":"item","numeric-id":3540178,"id":"Q3540178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$6F1BC3BD-F5B6-464A-AA78-C8AC68CD1B03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9160d425354d4baf854c7de7521e20ecca21697","datavalue":{"value":{"entity-type":"item","numeric-id":3553922,"id":"Q3553922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$0B16D11B-510B-4522-8EE4-4F2D73F52AE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76c47ac64788248a40d8543304d3dd3bc25cb13b","datavalue":{"value":{"entity-type":"item","numeric-id":1603701,"id":"Q1603701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$3F9284B6-3E6C-4E06-AED3-AE127EC9956A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"341cf25e1331e9c3d9b625066b41f81f88fc1449","datavalue":{"value":{"entity-type":"item","numeric-id":5549033,"id":"Q5549033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$4E17EA47-48E6-4AA2-BA77-D9DE96538B95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce3dbb8e924086eb69a5a6a156183accae6efe07","datavalue":{"value":{"entity-type":"item","numeric-id":3845367,"id":"Q3845367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$6A0F531C-ABF4-4F57-B238-7CE57DCD4EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6424e891ec3320cd9100f08f39833a24c09ba9b7","datavalue":{"value":{"entity-type":"item","numeric-id":5596744,"id":"Q5596744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$0B6AC9F3-B3A5-4C7D-AB78-904584911318","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24e9a7126fd3647b4929f8ad5e5b5d84f4d827a2","datavalue":{"value":{"entity-type":"item","numeric-id":2542723,"id":"Q2542723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$32EB3E50-C5DF-4F80-99CB-215C7AB87724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q691121$3E8F692B-9A62-41F6-BEFD-4E3E84418F06","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"322f173fb3575a797ce385c52c033636a0af7c95","datavalue":{"value":{"entity-type":"item","numeric-id":5432335,"id":"Q5432335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e211a963f50184d41c810363b92937cff8947082","datavalue":{"value":{"amount":"+0.98847633600235","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":"Q691121$82939D51-5D8D-4651-8C13-C75E1F75BD8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00e975208f045c148481934fdcb20eeb35938a2d","datavalue":{"value":{"entity-type":"item","numeric-id":2870144,"id":"Q2870144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39bf92cabdc3588479543224209bdca5c4bd7466","datavalue":{"value":{"amount":"+0.8291102051734924","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":"Q691121$3450028F-3D64-411A-937F-3DC22F6D6C9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fb85740cec58ec7a36ef91932ed08f036161c0a","datavalue":{"value":{"entity-type":"item","numeric-id":3644841,"id":"Q3644841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73ac0907e3073a0acb33c529a99256f55cfe6ad3","datavalue":{"value":{"amount":"+0.8102133274078369","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":"Q691121$15B134ED-3C4D-42B5-8439-C0E2B9C808D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3fceebb954c3f3eb9ff32d939250be2deb621261","datavalue":{"value":{"entity-type":"item","numeric-id":3638252,"id":"Q3638252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1a1130bac33d506a99554caea2c10d28ec7d51c","datavalue":{"value":{"amount":"+0.7670531272888184","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":"Q691121$11469A97-7C43-4E33-ADAB-5ABCFC4EFE67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27f1a0ef4645d2bf4ef1332b9480367de0b3f497","datavalue":{"value":{"entity-type":"item","numeric-id":4650285,"id":"Q4650285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93e9a657243ca02e034b629dfa0bf7a496731773","datavalue":{"value":{"amount":"+0.756343424320221","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":"Q691121$A125C8AB-9D27-4692-A9D7-EA87567B8167","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A simple proof that super-consistency implies cut elimination","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_simple_proof_that_super-consistency_implies_cut_elimination"}}}}}