{"entities":{"Q790809":{"pageid":792657,"ns":120,"title":"Item:Q790809","lastrevid":48688561,"modified":"2026-01-05T15:05:02Z","type":"item","id":"Q790809","labels":{"en":{"language":"en","value":"The modal logic of provability: cut-elimination"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3849224"}},"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":"Q790809$0D22665D-A214-47ED-8164-8C3AD7FC723B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"124a53944e84f7adcd86519579c2c62b48bbb043","datavalue":{"value":{"text":"The modal logic of provability: cut-elimination","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q790809$85B9DAA8-8751-4FC4-A260-D7150725AFE8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"327ee8303505af6b46692ee87a5bc40de4b28dc0","datavalue":{"value":"0535.03031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q790809$D9C36C56-AAE3-4340-9209-8272F9495334","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"42c681697b3f6edd8245e6af22ed921841d62394","datavalue":{"value":"10.1007/BF00249262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q790809$5D65D125-24F5-4308-A658-4D32CFA250D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6d0979bbcd7d577f2b6333689cfdba669a470be","datavalue":{"value":{"entity-type":"item","numeric-id":651320,"id":"Q651320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q790809$CE8DB74A-DD7F-4E84-806F-0507EFF69295","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e692f569038e7bcb7d3e72ba14d8d8e224046270","datavalue":{"value":{"entity-type":"item","numeric-id":169434,"id":"Q169434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q790809$1ACD9042-234C-4249-A898-9A3DB7041544","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0136733d5dd7d9f4d36f24c87a0b8375ae1cb2fd","datavalue":{"value":{"time":"+1983-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q790809$C01B717D-46E5-4C5E-85C4-A97096C0EA26","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fa0e507d0cb528f3f876f5f1c50d38e9da13af26","datavalue":{"value":"\\textit{D. Leivant} [J. Symb. Logic 46, 531--538 (1981; Zbl 0464.03019)] outlined a cut-elimination procedure for the formulation of the provability logic GL based on the only modal rule \\(X,\\square X,\\square A\\to A/\\square X\\to \\square A\\). The author and \\textit{G. Sambin} [J. Philos. Logic 11, 311--342 (1982; Zbl 0523.03014)] gave a model-theoretic proof of the cut-elimination theorem for this formulation. An example is presented in the paper under review showing that Leivant's procedure can go in a loop. An additional reduction step is defined and the termination of the new procedure is proved.","type":"string"},"datatype":"string"},"type":"statement","id":"Q790809$B5D3621B-601B-4CAC-826A-9BF6DC5FC9D3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q790809$DD57AF48-E772-4AAE-A201-B9A20D284ED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q790809$E9C98DDC-DFE6-40FA-91CF-FA31F4D8E910","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7076021061b69602278667018608cadad60e9b56","datavalue":{"value":"3849224","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q790809$6A1691AC-0ECE-4D32-BF26-B7A5A0C95C88","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6de501434cb22f2101a61b9b99a0ca64a911288f","datavalue":{"value":"provability logic GL","type":"string"},"datatype":"string"},"type":"statement","id":"Q790809$4EFB194B-4E9E-4E1B-B96E-DDC9D56AA403","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q790809$7E7B3228-B4DF-4E8E-ADFB-CDFBDC1ED8C5","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":"Q790809$8E91DC83-B77B-4F1A-97D4-5D08C3FFA632","rank":"normal"}],"P223":[{"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":"Q790809$2FE87244-5EF3-4BC8-85E5-860A14E3FAF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71681916ff11f8a3fc6dbd9d1ba8a9a2a0b03154","datavalue":{"value":{"entity-type":"item","numeric-id":4724618,"id":"Q4724618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q790809$1917506E-B569-42C0-BDAE-2B6F4ADF7DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9210648c2da7d5773e848b729398c42f3567a36c","datavalue":{"value":{"entity-type":"item","numeric-id":4196401,"id":"Q4196401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q790809$3F9FF2AC-B988-407B-9155-FC1E421CF606","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":"Q790809$4610335B-5DB4-48FE-8F98-D758D612A28B","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":"Q790809$3C047A55-BC31-4805-9C69-D7C7A6EE6B01","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47f1ad10844ce984c8adb76ea61b2f97e4093499","datavalue":{"value":{"entity-type":"item","numeric-id":2890695,"id":"Q2890695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e8302ea1fdf715b18b5f3651d32865821859b6a","datavalue":{"value":{"amount":"+0.8637704253196716","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":"Q790809$CBB27AB6-C718-4BC3-AA77-CA9C1C6FFD0C","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":"c4ba4cd042205d1ccee2e9538eed4c637a8595b9","datavalue":{"value":{"amount":"+0.8578522205352783","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":"Q790809$0FCC40EF-6AB0-44F1-B735-39DB3BAF033D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dedff2a5fd0ec7cd0603ee32671f98cefcfa47f6","datavalue":{"value":{"entity-type":"item","numeric-id":5850981,"id":"Q5850981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28d929e88227c2b7dc501508fe5a05bda4320305","datavalue":{"value":{"amount":"+0.8194348812103271","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":"Q790809$51B1C20C-FBC7-41F7-B713-09AB0BE17D86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df7982ab060501728ce0f2208c041f28be535a51","datavalue":{"value":{"entity-type":"item","numeric-id":2343897,"id":"Q2343897"},"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":"Q790809$31F68D6A-4586-4296-A595-40D7A284E8D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53464fe7062b7899f2178a31102927db92a9632f","datavalue":{"value":{"entity-type":"item","numeric-id":2193977,"id":"Q2193977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa40e97333631f240c0a2452b5f00c3e9cfdb4c7","datavalue":{"value":{"amount":"+0.8120256662368774","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":"Q790809$1BBE8B8D-5341-4F32-8FA7-2639F8DD2A86","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:790809","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:790809"}}}}}