{"entities":{"Q2890695":{"pageid":2901420,"ns":120,"title":"Item:Q2890695","lastrevid":51488300,"modified":"2026-01-18T11:42:25Z","type":"item","id":"Q2890695","labels":{"en":{"language":"en","value":"Valentini's cut-elimination for provability logic resolved"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6045063"}},"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":"Q2890695$902F05FE-B153-41B5-8602-D65BB78B4F7B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f6182e3375a53682f2b9e5ce539788c3870a43b9","datavalue":{"value":"1254.03113","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$47642122-EA8F-4048-BC5F-8C72A909A004","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7c64a3b6fba5830bd9bd1dcd8d25e47658ca0b9d","datavalue":{"value":"10.1017/S1755020311000323","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$E9D1F272-FF48-4289-883D-2AEC2D6445BD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9764b5e3183836adae29ba3fef393bcd0832967e","datavalue":{"value":{"entity-type":"item","numeric-id":229747,"id":"Q229747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$948208E4-DF19-4439-8E25-63425C787737","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cd26fdbdfe1d2fb01e4aa125652a423d7111de5","datavalue":{"value":{"entity-type":"item","numeric-id":1709694,"id":"Q1709694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$3DD9157A-82D6-4733-ACC5-A8488C879E92","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"af0afed2c0d629b9762e7f6c9dfa985cdd4f9630","datavalue":{"value":{"entity-type":"item","numeric-id":2804470,"id":"Q2804470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$D0691D4A-F6C6-4121-B5D4-F8002752BF89","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b407bfdab7c0722e3633ce88dbddcd941cc491a9","datavalue":{"value":{"time":"+2012-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2890695$DC19250B-E956-4D5F-B79C-45E2EE4A6D17","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b638c7935436ccffba7a737e2b57436cbbd2533c","datavalue":{"value":"03F45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$FDC444B1-8A96-42D4-BEA9-B50BAE70AF7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$D407E9AB-81C1-4D32-94A6-1E15D747FEED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$A2737EEE-39C7-4CAC-8E55-61EBAFD3642E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d56c5d4764e9ba3e9ca3bec436e2c68f1cd9b97a","datavalue":{"value":"6045063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$4633A29E-9927-4A6B-9BB5-8A3CE880FC11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6de501434cb22f2101a61b9b99a0ca64a911288f","datavalue":{"value":"provability logic GL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2890695$950476C5-A323-4FEB-898D-B14041A6F4C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e72d7e810d991f073ed72f085597492a186cd22c","datavalue":{"value":"syntactical cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2890695$288CF413-34ED-41AE-9C91-099991B1E606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4605262f950382e87dc58df46038532164191769","datavalue":{"value":"contraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2890695$853EDFF6-E81E-449E-B3CD-6EC7E9D9FBA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9c8035cac10f9af1a18e8d6fcbe16ed68d97c9c8","datavalue":{"value":"L\u00f6b axiom","type":"string"},"datatype":"string"},"type":"statement","id":"Q2890695$267F6D9C-3519-4A81-A707-0C5EA2324B1E","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":"Q2890695$22F460D6-0059-4534-A8AF-504123929B34","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f866ce907de55bb6422915580ccdf6356e5fea7e","datavalue":{"value":{"entity-type":"item","numeric-id":4779590,"id":"Q4779590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$5033B433-B93B-4B34-875D-2C9F904E84B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f580077c20a971d5f9bd8188096db37f21f37730","datavalue":{"value":{"entity-type":"item","numeric-id":5187258,"id":"Q5187258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$15EF0840-51D0-481D-915D-1E05B2AF4768","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47e897bc8b0383e0be621508dc47975da8303b0c","datavalue":{"value":{"entity-type":"item","numeric-id":4487267,"id":"Q4487267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$A6C28B5D-3292-4B73-95AA-D269F408DF67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2c08abdce84bc42d9a4b1ba80fa892bde25ec2e","datavalue":{"value":{"entity-type":"item","numeric-id":3762309,"id":"Q3762309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$7D0780B4-9B82-475A-A6E9-1BF708A0ADF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ba513acce41afdadafe2075e4fa4f56dd7aa740","datavalue":{"value":{"entity-type":"item","numeric-id":3753985,"id":"Q3753985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$3A460DE5-5BAB-4704-B2BC-1172E3E77ED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9046092912369ae53c021eb53125c7bea4658d3d","datavalue":{"value":{"entity-type":"item","numeric-id":790809,"id":"Q790809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$1E39666F-4535-4AA2-B19F-90882DBE3F75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbba195f59bc845671d8c6b66b30c57697b93115","datavalue":{"value":{"entity-type":"item","numeric-id":2454875,"id":"Q2454875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$E9F93FA5-A3EF-4D69-99A0-74DD089C48F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65af634f8ea04e9717486b98f2f6b61acf5b154f","datavalue":{"value":{"entity-type":"item","numeric-id":1235695,"id":"Q1235695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$4438C2F2-32F3-4194-9EE0-FAF961CD2DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c77d029ca17e8cbeae5ff8bc11ecd94cb2895f59","datavalue":{"value":{"entity-type":"item","numeric-id":3714054,"id":"Q3714054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$94898232-3850-4407-954E-7BE8FE1C8A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c232a4ac94055e2cc6462047a2680a2578759dc","datavalue":{"value":{"entity-type":"item","numeric-id":3887437,"id":"Q3887437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$C86D8E8A-7C1A-4878-B62F-E09DA554DB03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b767d85950bf99e8910526fcfcbcb504d6a930ba","datavalue":{"value":{"entity-type":"item","numeric-id":1056745,"id":"Q1056745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$84A80029-9630-445F-87CA-E2E8A42F01DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5947643150d637319b5eba17184efd7e207af1cf","datavalue":{"value":{"entity-type":"item","numeric-id":5850981,"id":"Q5850981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$5C6396F0-ADD6-47DF-A406-1FCEF1CB5813","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3ce41d60cfb93a7d9f318710e34ad3627406dc9","datavalue":{"value":{"entity-type":"item","numeric-id":3580655,"id":"Q3580655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$42266530-E805-4094-AB40-FAED4F3631BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8546dfa3ee45536454a034a5905b0e5f07e2b82","datavalue":{"value":{"entity-type":"item","numeric-id":812101,"id":"Q812101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$0CDF3A62-50FE-489B-B78C-A2FBDDB804E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4196aa856e022b95d032a8421e5fadcfeb1922b9","datavalue":{"value":{"entity-type":"item","numeric-id":3914957,"id":"Q3914957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$82A3A399-F1FE-4BAD-AD81-02D56C796F44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2ff84a380859792f98a71b73007569735b0f24f","datavalue":{"value":{"entity-type":"item","numeric-id":5277766,"id":"Q5277766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$747AF3C7-2EE4-47EE-ADD5-B1DCC7C30BF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6fe9c7bc1afe6e3b7b77fad40b2f8f849bb4920","datavalue":{"value":{"entity-type":"item","numeric-id":4365323,"id":"Q4365323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$42E3B17C-411E-46CF-BF14-D70A2AC948BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"361e0f23746829e48ff0ff918b87727856cdb536","datavalue":{"value":{"entity-type":"item","numeric-id":5928308,"id":"Q5928308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$D160E82A-CDD6-46CA-AE3E-ED1AB3F09BF8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1e0e2bf6be5437c032175361b686730eb3d68b27","datavalue":{"value":"https://doi.org/10.1017/s1755020311000323","type":"string"},"datatype":"url"},"type":"statement","id":"Q2890695$DA51A89B-3C38-418D-858D-6AFEF12D66BC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7de2202449bb220f57ac7bf2a5a1b958d2d2ad78","datavalue":{"value":"W2102143997","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2890695$20E590E5-8082-4FF0-BE14-E008FFF2E033","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a2fd3a67e27cc79d07adda1f419fc2d24aea4538","datavalue":{"value":{"text":"Valentini's cut-elimination for provability logic resolved","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2890695$656AC8A6-0546-4D02-A811-8952BFB9E977","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8f8b5edc115cf1af9009656958ed1d3cb4f9967f","datavalue":{"value":"As for the problem of syntactical cut elimination in a sequent-style formulation of provability modal logic GL, there have been given various versions by several authors for their formulations with different methods, respectively, where some of them seem to leave ambiguity for details, as can happen sometimes in a proof by the so-called Gentzen method. Among others, the first one was proposed by Leivant, to which, however, Valentini showed soon a counterexample as well as another proof for a system based on sequents of formula sets by featuring a triple induction with the third parameter called ``width'' in addition to the usual ``degree'' and ``height (rank)'' of Gentzen. Afterwards, Moen claimed that Valentini's algorithms either do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. On the other hand, in general, the original mix (multi-cut) elimination method by Gentzen has also been revisited rather recently from the viewpoint to analyze such a problem brought about by structural rules. In this paper, the authors explain that Valentini's proof is not sufficient for manipulating the contraction rule explicitly, and then reconstruct the argument on the setting of multiset sequents with weakening and contraction, which is indeed carried out affirmatively but not straightly because of the global aspect of the third parameter ``width''. By analyzing the hidden role of structural rules in the argument thus, it is pointed out that Moen's claim is not correct; as a matter of fact, the algorithms used by him are essentially the same as those of Leivant. The authors discuss also the possibility of adapting their cut-elimination procedure to other logics axiomatizable by formulas of a syntactically similar form to the L\u00f6b axiom of GL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2890695$D7949183-D2D7-4E4E-A916-4714D827D43E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2890695$C738210F-1611-457E-85F5-3A21E2C778C0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c2adff1667a33ce714f216e8fc6d225e433a1f9","datavalue":{"value":{"entity-type":"item","numeric-id":3086940,"id":"Q3086940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d82e4a4139a673600181d3fbd9ad8b27e110445","datavalue":{"value":{"amount":"+0.9803253412246704","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":"Q2890695$5941FA9B-A802-404F-98B0-71116B07086C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"137ece3485bd94eb6384fe30979b166becb136e5","datavalue":{"value":{"entity-type":"item","numeric-id":790809,"id":"Q790809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67623c08c15c2a0bb89e2abb6a61c56ab0b2e24c","datavalue":{"value":{"amount":"+0.8134433627128601","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":"Q2890695$79A2B548-CE3C-4F84-BE20-61BD12C4451D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08d94c183b8a90d5604e28002e00d2bf7f110ebb","datavalue":{"value":{"entity-type":"item","numeric-id":288243,"id":"Q288243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b4f14da322c554a8eb8d3d4c33de8c5b50f14a9","datavalue":{"value":{"amount":"+0.7679793238639832","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":"Q2890695$203F1238-B4ED-4D18-99DF-AE4026A125C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c92618bc10caa6fee0fd91c49cc2d8a0e61babdf","datavalue":{"value":{"entity-type":"item","numeric-id":5884958,"id":"Q5884958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"221e56d5263b9662a7993e7f448dac70df0e08b3","datavalue":{"value":{"amount":"+0.7617204785346985","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":"Q2890695$56596B5A-29F3-499B-AD15-21313F6053E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d063d20ab7b79dc1022e3a70a0d5ca6d036a686","datavalue":{"value":{"entity-type":"item","numeric-id":798649,"id":"Q798649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52ff214e3b7c6b4721fbfd3efff1fc0d1f90099a","datavalue":{"value":{"amount":"+0.7615619897842407","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":"Q2890695$DDAE1E9D-CB6A-4A2F-A088-F47924E7BBB6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2890695","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2890695"}}}}}