{"entities":{"Q5928308":{"pageid":8105110,"ns":120,"title":"Item:Q5928308","lastrevid":47591869,"modified":"2026-01-02T04:09:53Z","type":"item","id":"Q5928308","labels":{"en":{"language":"en","value":"A proof of Gentzen's \\textit{Hauptsatz} without multicut"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1582391"}},"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":"Q5928308$9A9FE447-85D2-4EF7-8A7A-3C3F85C3C956","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0b4a18947378213c2ba6344d3034f90898f64703","datavalue":{"value":{"text":"A proof of Gentzen's \\textit{Hauptsatz} without multicut","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5928308$BD0024EA-0445-49DF-84C4-063F507F90DA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"74fdd275a9736715de461b941ca66d8c92f860fd","datavalue":{"value":"0968.03065","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5928308$AC96D03D-C7B8-4EFC-AB4F-9FB009D1C4E2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cc8bf89138092366dba76fbdf018c3e853b377d","datavalue":{"value":{"entity-type":"item","numeric-id":167888,"id":"Q167888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5928308$6C956E9B-24B8-4B57-AA5C-EEDFC26DC449","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":"Q5928308$2D3C1729-CCA9-4658-8355-26DB931AABD8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"910b748a15c45cd335bff2eb974340b10444976e","datavalue":{"value":{"time":"+2001-03-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5928308$EDC07C68-63B1-4292-8934-161B88FBC0DD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cc1fec5ca4adb2e23ec47a3de4de91b8fd942e49","datavalue":{"value":"The celebrated Gentzen's cut elimination theorem does not really eliminate cuts themselves, but multicuts (Mischung). The reason is the following. If one eliminates cuts one at a time, the case when the cut formula is the result of contraction causes difficulty, because ranks of cuts may increase, and so the inductive procedure does not work. In this paper, the author overcomes this difficulty by using the familiar inversibility result. The case when the cut formula is \\(A\\& B\\) and the logic is intuitionistic is the clearest for seeing the point. If \\(\\Gamma\\to A\\& B\\) is derivable, then certainly \\(\\Gamma\\to A\\) and \\(\\Gamma\\to B\\) are. Also when \\(A\\& B\\), \\(\\Gamma\\to \\Delta\\) is derived without cut, its proof can be inverted to that of \\(A,B,\\Gamma \\to\\Delta\\), even if \\(A\\& B\\) was the principal formula of contraction. So, instead of cutting \\(A\\& B\\), one can cut the simpler formulas \\(A\\) and \\(B\\). And these cuts are eliminable according to the induction hypothesis. For the cases of other connectives and quantifiers, and of classical logic, the formulations take more complex forms, but the idea is the same.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5928308$77FF5AD6-06A3-49FF-8AC0-6105E78D537F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5928308$4BC0EBDA-675B-4E4D-BAE4-706E261BE4D8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"89f34375803396603d727719ec3a257e5a337bb7","datavalue":{"value":"1582391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5928308$9813F62A-1661-46F2-8927-E49FDD3E9F2E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5928308$62912646-CECD-4B28-9C56-C7031AC54D24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4080b483fd9f575e4eff0edc14e0f1330693728","datavalue":{"value":"multicuts","type":"string"},"datatype":"string"},"type":"statement","id":"Q5928308$08BCAB22-A062-46B6-8FB1-6A06D504A0DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca014d7f91a21cec3920bc6bda739018c248476a","datavalue":{"value":"inversibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q5928308$F9FD7E39-5117-4F74-B0AF-083956416431","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":"Q5928308$31D2CF46-C690-4787-969B-A3908659AB89","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"acdbb72cb7b2725761191b4d16666be6d6aed355","datavalue":{"value":"https://doi.org/10.1007/s001530050170","type":"string"},"datatype":"url"},"type":"statement","id":"Q5928308$ECBBF154-07EB-457B-B51F-F2A30DD57590","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc33d2f6c3624b6afd1ffe58e5cae723b764ca0f","datavalue":{"value":"W2014377715","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5928308$DB545475-B737-437E-9133-9785D857B4AA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b94b27018235ac3f4b22f7a944b6059a34e2f0cc","datavalue":{"value":"10.1007/S001530050170","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5928308$AE33B9C8-73C4-46D0-8ACC-13F54CA1ACB8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec41fbcf6227cb9b98d3720513a93678334e98b2","datavalue":{"value":{"entity-type":"item","numeric-id":4451468,"id":"Q4451468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22411c752df0546ccda9a9bf2013893690e59d52","datavalue":{"value":{"amount":"+0.8319708704948425","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":"Q5928308$0A22DE59-3ACA-49FA-B53C-5D145F1EE480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b8dcd8df300661aa3bb06e3c099f7fcec67e20b","datavalue":{"value":{"entity-type":"item","numeric-id":1304543,"id":"Q1304543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eef45eb3d2d85b18209f2b8630ef31c00ce65802","datavalue":{"value":{"amount":"+0.8146675229072571","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":"Q5928308$A5A7BF3E-7DDC-4694-A0F1-38F94CF6A5EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1fb3f97197cc5507bdb6e9313478f714e3311063","datavalue":{"value":{"entity-type":"item","numeric-id":1204120,"id":"Q1204120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b98ea803c530e63f945f72e2bdac787e11f4002e","datavalue":{"value":{"amount":"+0.8128722310066223","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":"Q5928308$22959BD6-90D3-4531-A618-1607957B8FC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18a1363b9fb4769d2729b14d5535843556213fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5221860,"id":"Q5221860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c98161647c809c2471435cc83b9e5056202884d9","datavalue":{"value":{"amount":"+0.802382230758667","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":"Q5928308$3BCA401B-D924-4856-81C3-AA3434DB8ED6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc833c0de071a9374a09b3209df6f501c8bc0cf6","datavalue":{"value":{"entity-type":"item","numeric-id":4487267,"id":"Q4487267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f9ba71c2d82b8ae11efb3344dd4edb6de3a98f1","datavalue":{"value":{"amount":"+0.7889178395271301","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":"Q5928308$B42836F2-0701-474E-A126-E95BE6869135","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5928308","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5928308"}}}}}