{"entities":{"Q1210141":{"pageid":1220890,"ns":120,"title":"Item:Q1210141","lastrevid":69904152,"modified":"2026-04-13T11:06:50Z","type":"item","id":"Q1210141","labels":{"en":{"language":"en","value":"Linearizing intuitionistic implication"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 169667"}},"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":"Q1210141$D0AF45C3-716B-42F5-AA34-92C5B6A5E550","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5aa215ffcfb4398d88dfc875c8d3e055bad265fc","datavalue":{"value":{"text":"Linearizing intuitionistic implication","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1210141$A89C4A62-9162-4704-996C-BFDDBB3B2C28","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8aab59f6504462bf570dd643a414ec27d9fea143","datavalue":{"value":"0767.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1210141$8A4789FF-227D-4A4A-B56F-828A54768B2B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4847352a657a1548e19c367e0c39a1c0adf60553","datavalue":{"value":"10.1016/0168-0072(93)90041-B","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1210141$087C02DA-0DE1-4D04-A077-C53525B2F8AB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$54FD982A-CB98-4EAF-8983-FC5A6D2FFB61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6d0bbdada3c9be42b370691f727810aaafa99222","datavalue":{"value":{"entity-type":"item","numeric-id":1575866,"id":"Q1575866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$FBFB7F31-5A4F-494C-A070-3F352AE4A153","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"183df695ae89db8e2a7647ddbe2de62ff0deb022","datavalue":{"value":{"entity-type":"item","numeric-id":1052316,"id":"Q1052316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$6146B6D6-FA6F-4AFB-BC30-41F5368B6B13","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":"Q1210141$ACC22C51-4DDC-492E-8DE4-456219EAAC90","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1772b6c81a5108c06854e0de4518fb90e5a6ebdc","datavalue":{"value":{"time":"+1993-05-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1210141$662E628C-9BCC-4BB0-BCD1-546D36A30B01","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e4003ef393a4859a3d0447685f82f8a91d485568","datavalue":{"value":"In the introduction the authors give a nice description of how linear logic is obtained from classical and intuitionistic logic by a modification in three steps. IIL denotes Implicational propositional Intuitionistic Logic. And IMALL is the Intuitionistic fragment of Multiplicative-Additive Linear Logic. Contrary to IIL, IMALL has neither contraction nor weakening and expressly forbids the copying of the principal formula of any rule into a premise. IIL* results from IIL by modifying one of its rules and by discarding the cut and contraction rules. The advantage of IIL* is that there is no copying of principal formulas.   Lemmas 3.2 and 3.4 state that given a proof of \\(\\Gamma\\vdash C\\) in IIL, a proof of \\(\\Gamma\\vdash C\\) can be constructed in ILL*, and, conversely, given a proof of \\(\\Gamma\\vdash C\\) in IIL*, a proof of \\(\\Gamma\\vdash C\\) can be constructed in IIL. The lack of contraction in IIL* makes the formulation of the sequent rules for implicational intuitionistic propositional logic amenable to encoding into IMALL.   For any IIL* sequent \\(\\Gamma\\vdash C\\) let \\(\\theta(\\Gamma\\vdash C)\\) be its translation into IMALL. The authors show in section 5 that there exists a cut-free proof of \\(\\Gamma\\vdash C\\) in IIL* if and only if there is a cut- free proof of \\(\\theta(\\Gamma\\vdash C)\\) in IMALL. This establishes their Theorem 1.1: IIL can be embedded into IMALL. The embedding preserves the structure of cut-free proofs in IIL*.   In section 6 the authors show that the embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1210141$99FA7AB0-2CDC-43C2-88AB-2B5CD5B9C597","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1210141$8AB51E59-861F-465D-A9DA-DCC225A7B180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1210141$E0F55DA2-AF64-4753-87D7-B1AAE5191EDE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"503cbde434ec114c2503ed2b196a13785a06391f","datavalue":{"value":"169667","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1210141$99BC9D5D-1E8B-4BBD-A4DF-6DFDA62FB1B4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1210141$24B71B95-BD6E-45E3-A79A-D1EB89DFB808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1210141$A1886A53-1ED5-46F7-B7FB-7AEF6E0741BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9bde502d875fa8eeedd7c6109a48a0c26939dc22","datavalue":{"value":"cut-free proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1210141$451E1B0D-155F-48BA-8476-045B323EA4FE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9bea83566ad047ec39e22bd8867e363c00af7d87","datavalue":{"value":{"entity-type":"item","numeric-id":5975143,"id":"Q5975143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$5F53122A-57BE-42F1-9566-2666FE282FC4","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":"Q1210141$01C69834-6ADD-40D6-93F5-C0B43F9A9284","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1945271fe13c6999422e12998474c5a1f95a82e8","datavalue":{"value":{"entity-type":"item","numeric-id":685430,"id":"Q685430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$79123611-2E51-4D76-8C05-FF77419BB305","rank":"normal"},{"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":"Q1210141$F7501DED-4531-404A-B71C-CA940154CB30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccaa3f7e97d228d907b8c697808a7482aef33deb","datavalue":{"value":{"entity-type":"item","numeric-id":3357521,"id":"Q3357521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$84FB956B-A928-4EB5-809B-658D591F3D4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2044dd1c7b02d485789fb5cbe805612ad49ec0e3","datavalue":{"value":{"entity-type":"item","numeric-id":2639952,"id":"Q2639952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$C78FDD4D-CC79-46C5-9BF7-1785DE568ADE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40e1d2fad2b3369089cffb0934f8fbe434f4fba5","datavalue":{"value":{"entity-type":"item","numeric-id":1192350,"id":"Q1192350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$1820844A-0F18-495C-A35E-9CB72F7D1B3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15ffb46be9e49b237f6fde18c89e459513c877e1","datavalue":{"value":{"entity-type":"item","numeric-id":5547552,"id":"Q5547552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$DAF48185-AD4E-46DE-87B6-17C99910E06B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe4c1ea89bc5854f421d3a6b161146d5aecefa12","datavalue":{"value":{"entity-type":"item","numeric-id":4032862,"id":"Q4032862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$79B3872C-FF6D-4F52-95B2-5232C8272AF7","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":"Q1210141$18B505F8-F4FC-4468-A113-3EB06520B482","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90f212fb967f9a9d9854f9848f7aff4d399d7a98","datavalue":{"value":{"entity-type":"item","numeric-id":4204146,"id":"Q4204146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$BC2A2599-AED9-4452-A01E-F7AF30FB1D45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54351e142ba78301c80d7c3516f9734aa8ddee58","datavalue":{"value":{"entity-type":"item","numeric-id":3791120,"id":"Q3791120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$0779AE0C-9045-45D9-85AF-FC334F2BA5F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$59042035-7D85-4085-AD37-0E64CC4CF20C","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":"Q1210141$911E21B3-16ED-4DD6-BBDC-EDC83F0E75E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$5EAACCF8-8725-4BF8-8504-E97E607ADD33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb0cef3710adbd86fd4521d1c8531cd34e84dd13","datavalue":{"value":{"entity-type":"item","numeric-id":1105351,"id":"Q1105351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$B1B1CA73-3695-4936-967F-7C886EA97E62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"074134d8b33bdd9cca293a6e8f5f8ee888ec9918","datavalue":{"value":{"entity-type":"item","numeric-id":1192352,"id":"Q1192352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$DE856B61-065F-4B9F-B153-C5A34390C260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29ef20d70ae4a35d8a1f0191877c0c62d6346fe8","datavalue":{"value":{"entity-type":"item","numeric-id":3997125,"id":"Q3997125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$E4E08DEF-0EE7-4552-B368-52CB6CE8D3ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aebd32d099ee8c91552756addce4fb86715ed2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2640596,"id":"Q2640596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$D2543EC7-BEAA-4ADE-BD21-69B9B6DA6E62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"164d5958e5083b10f8e82ed42140727a0ef780a4","datavalue":{"value":{"entity-type":"item","numeric-id":3972527,"id":"Q3972527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$2010A6AC-0476-46DF-B03B-9A2E955D7F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"557c38065713b3b61905416b8b78d9d7e988c69a","datavalue":{"value":{"entity-type":"item","numeric-id":5519124,"id":"Q5519124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$96E4FA46-3E7F-4DA0-9B27-34B107A567DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cea085d8c059c5f81ccc8c6d0a2a9f9fb30e1313","datavalue":{"value":{"entity-type":"item","numeric-id":1259589,"id":"Q1259589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$19935AB6-8A0A-47C1-91DC-BBF028364FD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e09b13f4aec757d843096e32ee6e69eaf715a00","datavalue":{"value":{"entity-type":"item","numeric-id":3259711,"id":"Q3259711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$2257415D-0476-475C-82B5-D74577DFB03E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5ea676d7dea028bdc934c4cff4737ce3b2e6c3b","datavalue":{"value":{"entity-type":"item","numeric-id":5771193,"id":"Q5771193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1210141$44424444-1D39-4B0C-BCEE-E983B0EFF5E2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72f4eaeb4480d971e949b0a2fbd8d8001d316a66","datavalue":{"value":{"entity-type":"item","numeric-id":4882488,"id":"Q4882488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d949c26195687f1b2aba0f0e1442f330b596c0d7","datavalue":{"value":{"amount":"+0.7728146910667419","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":"Q1210141$7BB156ED-1E69-4A1B-8C52-89D8E27BDE65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4c2f2f39a0c695dbffa7d725e1703c49ea94757","datavalue":{"value":{"entity-type":"item","numeric-id":1891252,"id":"Q1891252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43ffcc831db55ab206e1ab14d88bf06e345f4f32","datavalue":{"value":{"amount":"+0.7713231444358826","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":"Q1210141$71DFC73F-AE79-4A0A-A906-6F9D4B027722","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba40d8089a89a43c7e46fbbf0e9bad331273fd66","datavalue":{"value":{"entity-type":"item","numeric-id":1344853,"id":"Q1344853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5e5790122d3e0370bc6557dda688f975c8e5af4","datavalue":{"value":{"amount":"+0.7676277160644531","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":"Q1210141$7DCA336D-C6A9-4FC6-AB41-705EE7DDC1B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9717f47c582a39eeb1829ae6667f765c31439ac7","datavalue":{"value":{"entity-type":"item","numeric-id":5902221,"id":"Q5902221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bf7dbc681700638706faa7abb4b934c9d220007","datavalue":{"value":{"amount":"+0.76513671875","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":"Q1210141$5C62783A-A776-4882-AE87-4A3E2721B892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24e7ec0eb5e8f017d8c636db8b23b6051c947ab3","datavalue":{"value":{"entity-type":"item","numeric-id":5145339,"id":"Q5145339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b39f9e27f366360feb76347ae0b6a8133be0695","datavalue":{"value":{"amount":"+0.7597836852073669","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":"Q1210141$6F1A8344-84A7-41FF-9070-9B45ECC11582","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Linearizing intuitionistic implication","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Linearizing_intuitionistic_implication"}}}}}