{"entities":{"Q2144620":{"pageid":2155363,"ns":120,"title":"Item:Q2144620","lastrevid":56771331,"modified":"2026-03-23T13:29:05Z","type":"item","id":"Q2144620","labels":{"en":{"language":"en","value":"A note on cut-elimination for classical propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7541623"}},"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":"Q2144620$EBE43129-E9BB-45F0-991D-0EF970A99717","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8ab35ca534e627a78b8096654e16147d29da6a48","datavalue":{"value":{"text":"A note on cut-elimination for classical propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2144620$2F6D7D4D-6E51-41F7-9439-24CCECA81280","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5c7c3f0674b316aba3a56e377c4ea2774c16e928","datavalue":{"value":"1506.03121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$4F4E3C3D-891F-4B06-A0A0-4660BEB319F7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a4bdba2590022c90a202dc79d5f2fc1152466ada","datavalue":{"value":{"entity-type":"item","numeric-id":472803,"id":"Q472803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$B32EBAB7-3EFD-494D-A01C-E3D552291FA6","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":"Q2144620$18B7BE8C-51C6-44DD-ABD4-FF7888745C5D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ea330d22ab57957bacb34bf65b5f953b0504c328","datavalue":{"value":{"time":"+2022-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2144620$A712951C-BD7F-4F89-9F87-22E8814A7108","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e97b1c20f7576415a44d92e601a34a55f7d2f076","datavalue":{"value":"The article presents a simplification of Schwichtenberg's cut elimination procedure for classical first-order logic when restricted to the propositional case. The method is based on Tait's cut elimination for a one-sided sequent system, which is restricted to conjunction, disjunction, and negation as a complement.  The proof of the Hauptsatz is based on a height-preserving permutation argument which lets us assume that the cut formula is principal in each rule deriving the cut premises. The Hauptsatz is then proven through a double induction on the maximal cut complexity, with a side induction on the number of maximal cut-applications, by reducing a topmost maximal cut.  The proof does not extend to predicate logic. However, clear bounds on the size of the cut-free derivation can be provided based on the complexity of the conclusion.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2144620$7D9EA0EB-53D1-4425-AEA7-89ADA884F596","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"4c3bf1f68faacb3686e363b11483d45d0338454b","datavalue":{"value":{"entity-type":"item","numeric-id":1734261,"id":"Q1734261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$8B9BACB4-AEA7-41A9-9781-59C0D072F20E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$AAB365A0-51E4-41CE-BB0A-B7F3F34FD3CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$FB5BC5F3-B6B8-4382-876C-A9B7D34034C7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7199b655ab051fcf9e31897a1d579413a36f9214","datavalue":{"value":"7541623","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$A47B2255-7EF4-46F3-948D-0727A62F9DD4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e7e45de5f0961d0cf7470a7b0dd939d5c4c581f3","datavalue":{"value":"classical propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2144620$DBBCCD87-B939-462C-A602-31FA26C3CE61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2144620$4351E7E5-6D43-4E1A-8E87-C0D46A0241E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2144620$6C74142F-B6E1-4810-80FA-1B96AD3BAE3F","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":"Q2144620$AA91CE87-3AE1-4E96-9120-7BCB21AE0CF2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"66ef18dd18d2dfe7c3a69e5b342f17cecf27fc25","datavalue":{"value":"https://doi.org/10.1007/s00153-021-00800-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2144620$21F9EB2A-3EE7-4FF9-8C6C-DA101CF756F4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"eb00cb3fcdd9cd7acc2d437adee6441b410710f4","datavalue":{"value":"W3215149402","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$87EE834D-196C-410E-A549-7BDFEC4DFF23","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2a8a36327ea86df5522203c0e0180d9b3bcc5cb","datavalue":{"value":{"entity-type":"item","numeric-id":1311413,"id":"Q1311413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$34E025D7-0105-42F0-8F1F-0A2A6E73C3BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$42029702-B0E3-4801-B7F2-1D3B966C5C25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c89e08f8e981b15d9e994bd9b66679f47871eb79","datavalue":{"value":{"entity-type":"item","numeric-id":5528627,"id":"Q5528627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$ED3CD4AE-E3AA-459C-A699-6F66C8D69743","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"727533a3d0d816797bcc34128bff8fa0002535b8","datavalue":{"value":{"entity-type":"item","numeric-id":5883190,"id":"Q5883190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$E3F93103-E7ED-45AD-8685-E20964F1A19B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$E5C3C659-536E-486C-9F17-B4AE6591DDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be85b3951fe2b4ee7f07bf10003c515b5749abc6","datavalue":{"value":{"entity-type":"item","numeric-id":5605873,"id":"Q5605873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$DF21F9EA-7D64-4FDF-8C27-01C008742624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$C2DEA3A5-9CEC-440E-BA07-E665DB483B1C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7ef86098baa55326f8ff8c4acb8488add2bfc930","datavalue":{"value":"10.1007/S00153-021-00800-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2144620$5C48B738-AF64-42B9-B759-B7D926A95942","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba67e2817f44d9f3978eab80105f1e99842b107f","datavalue":{"value":{"entity-type":"item","numeric-id":5450573,"id":"Q5450573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ffff0dc7ab6ea4989fd09fb51ef78493d832bb8d","datavalue":{"value":{"amount":"+0.93423545","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$2FEC3DA2-D7A5-4DA7-9593-68ECEFE85EAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa561b8b5342ab318639cadc68c91a52aafd256f","datavalue":{"value":{"entity-type":"item","numeric-id":3475264,"id":"Q3475264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3eac29f5fff68a981b7491c91f871e48c27a6c51","datavalue":{"value":{"amount":"+0.93309927","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$9A4008D7-FCC3-4CFF-8961-986A9E09BA7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad9d2696e1f31a0e1464593f59c0b0b850cd43a7","datavalue":{"value":{"entity-type":"item","numeric-id":4327830,"id":"Q4327830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e41c1095d5eccff8fee262f54304a14aec7449e","datavalue":{"value":{"amount":"+0.92972815","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$D42FCE31-9D11-43AB-8E5F-5175F18A3156","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":"f9a8d7dde6eb345db21f449d61ea1f070ef1d876","datavalue":{"value":{"amount":"+0.9233285","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$2AC5B08D-F858-48F6-B635-15EB72EA0DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb90401d55c678683cbf98b496a29ffaad068fb7","datavalue":{"value":{"entity-type":"item","numeric-id":4644486,"id":"Q4644486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c54bbd0dac1c81ec47123a862c1584a4229844bb","datavalue":{"value":{"amount":"+0.9200094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$416B96D0-C992-4FBA-8A4F-FD704999D0E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c76f77ea149ac341d5cf455fcbd6b85ee4566ec","datavalue":{"value":{"entity-type":"item","numeric-id":1854335,"id":"Q1854335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58fd606a0bfafae7552ab076ce37968c8ee152f3","datavalue":{"value":{"amount":"+0.91896534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$0C6ECC45-E25D-4A9D-BFA6-0ACE58B26EAC","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":"8c79feba5a9e2e12003170a1ea2bc260a7ef557f","datavalue":{"value":{"amount":"+0.91825384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$27960F7D-7FAE-4416-817C-10D4D26F7F11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8acb201e4f84be34fd78b46d2ae7a9888529e0c","datavalue":{"value":{"entity-type":"item","numeric-id":3997528,"id":"Q3997528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c79feba5a9e2e12003170a1ea2bc260a7ef557f","datavalue":{"value":{"amount":"+0.91825384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$E28ECDE6-BE39-49C2-A88C-23554C6F3861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f540bdffe0095e9baf1939e013afb8201a07ec5a","datavalue":{"value":{"entity-type":"item","numeric-id":5292628,"id":"Q5292628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4150bc098821cc71780e67ff6e6664288aff0428","datavalue":{"value":{"amount":"+0.91476727","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$E956BD1F-710B-4949-9DFD-BF1798A91D32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"03128b5c62f13ad2ed2c9942145e1ddaf17093bc","datavalue":{"value":{"entity-type":"item","numeric-id":1095904,"id":"Q1095904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c25810d6eb93659897dd3c27bb6ccb08596c536f","datavalue":{"value":{"amount":"+0.90847826","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2144620$F178F87C-1613-4D67-B816-1DA536BD8247","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2144620$AEBC0154-1030-45E5-BB08-107380CCB278","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2144620","badges":[]}}}}}