{"entities":{"Q2367410":{"pageid":2378153,"ns":120,"title":"Item:Q2367410","lastrevid":74092539,"modified":"2026-04-14T18:20:13Z","type":"item","id":"Q2367410","labels":{"en":{"language":"en","value":"Cut elimination for the unified logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 243574"}},"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":"Q2367410$7563613E-396E-43CC-8727-D1A3B1F6F9BF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"89dfd54e9075f969296fb8a26f433b84ce97d641","datavalue":{"value":{"text":"Cut elimination for the unified logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2367410$A5DDA7AC-72AE-4213-945B-219588E082DE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4fd0e91967299f4c2fb48381477368255a989a38","datavalue":{"value":"0786.03041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367410$2881DF69-6E32-4FD9-BFE9-90BFFB3A8763","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a4e48b25a88008497105aaa47d50856f90eaa041","datavalue":{"value":"10.1016/0168-0072(93)90184-F","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367410$BBC3756A-182F-48EC-B4A7-5BBDF4ADECA4","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$77CEDE90-44D6-4B24-AB45-7728687FA0C7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2a03d7e72c2f27d8f30f9a3e566010dcf9193975","datavalue":{"value":{"time":"+1993-08-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2367410$621E1ED0-6248-45F6-8DDC-6A7C3627CC68","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cf7af4db0d7fe488609121301818615ebd5f7a7c","datavalue":{"value":"The Unified Logic, \\(\\text{\\textbf{LU}}\\), is introduced by \\textit{J.-Y. Girard} [ibid. 59, 201-217 (1993; Zbl 0781.03044)]. Its sequent is of the form \\(\\Gamma;\\Gamma'\\lvdash \\Delta';\\Delta\\), where the outer zone \\(\\langle\\Gamma,\\Delta\\rangle\\) has the linear logic maintenance, and the inner \\(\\langle\\Gamma',\\Delta'\\rangle\\) the classical one. Among very many rules of inference, there are those of permeation that connect the two zones. Girard states (p. 215) that ``a cut-elimination theorem for \\(\\text{\\textbf{LU}}\\)'' is ``more or less obvious''. Probably, the emphasis should be on ``less'' here, because there are three rules of cut (one rule for linear cut, and two rules of classical cuts), and, as the author of this paper states, the elimination of a linear cut produces classical ones and vice versa.   She carries out a proof of the cut-elimination theorem by giving new definitions of the degrees of formulas and the heights of proofs that are taylored for the nature of the formulas and proofs involved, like polarities, exponential connectives, and kinds of cuts. In the appendices, the author gives bounds on the growth of heights in the cut- elimination procedure, and another notion of degree. She also hints at the usefulness of the notion of depth in handling non-well-founded formulas.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367410$981803CA-15F4-4830-9500-30CC83A1D46A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367410$6070F773-D353-4949-ABFE-F4707664D590","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d082089e4ce4068bda9bc0961921394dac8cebde","datavalue":{"value":"243574","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367410$1C76CD35-6313-4D7F-B32C-773EEBB72DFB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"91a6cd16682fdee3705d64b127e7d12cf26a3690","datavalue":{"value":"unified logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367410$DAF5F2CD-9597-423A-A3F3-62FB6BEB306A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367410$41E9EDBF-DB91-490C-8AEC-FE5344AD990E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367410$A833CA6D-F40E-40BD-8A3F-284C329F07B2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a88302bb95e1e4db76c4441eafc7b30c336e74eb","datavalue":{"value":{"entity-type":"item","numeric-id":534714,"id":"Q534714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$18AB73E3-84A0-4833-BD01-CA9347C73D79","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":"Q2367410$55D7A5F0-6570-4EBB-A0D1-1E2E7E0D9486","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"42bdbea0160e788f4fb95a24a8a29ffb0eadc069","datavalue":{"value":{"entity-type":"item","numeric-id":4018167,"id":"Q4018167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$37A99F21-9D59-4CA7-B345-2072C8C49CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$4A734624-A280-45FA-9FAB-C698814C6161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$823CB7CC-2749-4984-A0B6-331278FA4128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a2b2a8cf71a298beb3d5742fd0312db85012cf7","datavalue":{"value":{"entity-type":"item","numeric-id":579249,"id":"Q579249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$25872503-8A35-4D77-8104-1F1B1A5C37EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c20b3efd28014f3e3743af53ab793f5500601551","datavalue":{"value":{"entity-type":"item","numeric-id":1193854,"id":"Q1193854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$BB53127A-FCA2-46A5-B03F-A9CB99F9A311","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d66518f09c99314187d256b3e54c7fdc6eb07ce","datavalue":{"value":{"entity-type":"item","numeric-id":4006233,"id":"Q4006233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$C78FAA5B-7BB2-4D40-9700-7FBC054F8E00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14fba5e8ace22a05b3ebef9aa0392420cd4ad549","datavalue":{"value":{"entity-type":"item","numeric-id":685059,"id":"Q685059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$CA7F4F3B-2C7B-4D30-91DF-00C64EA5DF82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d28aff50fe8c186ed6c74cedf85881e09d7ecec4","datavalue":{"value":{"entity-type":"item","numeric-id":1802077,"id":"Q1802077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367410$4AAD7806-D72C-4EBC-8052-51D6E9861375","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"239988fc94c5281744905e6d9821fc9046d6e8f2","datavalue":{"value":"https://doi.org/10.1016/0168-0072(93)90184-f","type":"string"},"datatype":"url"},"type":"statement","id":"Q2367410$4341D1A4-F2C6-4535-B7C7-A9F10EE57F46","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"41e5690f6f63b2ef275419cfaf0d458bf05d6d26","datavalue":{"value":"W1987815301","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367410$3E42F33A-3091-4EB6-8C26-F87208571223","rank":"normal"}],"P1643":[{"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":"da5bb3e1bb0285f161b595e531675291daf3c4b9","datavalue":{"value":{"amount":"+0.7704853","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$B574DFBE-1416-4B1E-87AE-283F48E544AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09158d34a4904eab388c01ecae4796ef896eadf6","datavalue":{"value":{"entity-type":"item","numeric-id":4372906,"id":"Q4372906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a071b4159cf35fe0ff67d49cbd31dbf940b6b4f","datavalue":{"value":{"amount":"+0.7636699","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$FB61648A-15DF-4807-8B74-55A112BC7C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7a1e17eddf55b13c84ff2defa149d71a93296f0","datavalue":{"value":{"entity-type":"item","numeric-id":4530460,"id":"Q4530460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96b85e195fe4b19775cc099065a8fb57bb587d30","datavalue":{"value":{"amount":"+0.76354045","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$1D045AF3-2068-4523-B456-CACEA4EBDC44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"679d9b5649be24e59e1d02b2ed1323f935c2556c","datavalue":{"value":{"entity-type":"item","numeric-id":685059,"id":"Q685059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e38100dd01bc118f1e2d175e002f0f23e1bcc5e","datavalue":{"value":{"amount":"+0.76297134","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$47D30FCB-6C69-43F7-A682-E637869C10E7","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":"1243341cc165426a0182ec7fe7c5602e585ed82e","datavalue":{"value":{"amount":"+0.75416076","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$5F841BAE-6172-40B6-A665-1FE4B415F0D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d2f0364eddd9dde4fbc637777ff49bdd08d80dd","datavalue":{"value":{"entity-type":"item","numeric-id":3586051,"id":"Q3586051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9faf0d3fbb72b878a0180090c5eb87f7bfe4c8d","datavalue":{"value":{"amount":"+0.7485349","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$4C8AD8AE-2E98-4428-B600-4A1ED820A9D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dac20f065715347c44d6430c9e8b0a7e73aa2d2a","datavalue":{"value":{"entity-type":"item","numeric-id":4286216,"id":"Q4286216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59a6f569c2b90f3285e15f12f6fc7dee47d9bd0a","datavalue":{"value":{"amount":"+0.7466072","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$D8F259D9-8FA4-463E-BFAB-5BD774E43CA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"772a5e55fd0c7ea3b650401fc75f9c7ce7dc2129","datavalue":{"value":{"entity-type":"item","numeric-id":4644567,"id":"Q4644567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f48aa0a427aecf3c31cfde11265fdfacb8ccc97","datavalue":{"value":{"amount":"+0.7411789","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$A1BBB332-4626-4F44-8812-20DAC10F42A5","rank":"normal"},{"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":"ff8f5077dcbbb047b341aa9f15c65cd616e8296e","datavalue":{"value":{"amount":"+0.738649","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$C28F90F2-4A21-461B-B3C1-1EE1449582A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da41e92f06b0f33fd3e03e3fdb03e6c775298960","datavalue":{"value":{"entity-type":"item","numeric-id":5387850,"id":"Q5387850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d96723aaf51badab3f624d01930bfc92f6d8bcd1","datavalue":{"value":{"amount":"+0.73794466","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2367410$CD617593-B6D5-4153-844A-51790B55C91F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut elimination for the unified logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut_elimination_for_the_unified_logic"}}}}}