{"entities":{"Q2751819":{"pageid":2762558,"ns":120,"title":"Item:Q2751819","lastrevid":79199669,"modified":"2026-05-06T13:22:14Z","type":"item","id":"Q2751819","labels":{"en":{"language":"en","value":"Classical multiplicative linear logic \\(\\simeq\\) intuitionistic MLL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1665184"}},"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":"Q2751819$25BEB97B-A370-4CB3-A918-5FA668862486","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d0e5eca1cc6f06a9c9839d113b4e243f5655a528","datavalue":{"value":"0990.03050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751819$51A2A09E-EC90-4CC6-B325-03D6F149B553","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c08f14a616a88a4c5909efb80b5d497ec301efdd","datavalue":{"value":{"time":"+2002-03-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2751819$8B76C3E6-2A47-4895-B041-7F42110CABBA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751819$4689C7CE-F40D-4F3C-B71C-B4187EE34686","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7d4a60cda4eb40a5e138c73a670fdc47b263edee","datavalue":{"value":"1665184","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2751819$C4677BCB-ED45-463E-8137-D15A5D389629","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7911f0401d5e333d60e9f3fb2e80cae638c566cf","datavalue":{"value":"classical multiplicative linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751819$71AB330A-F02B-449A-9703-C0F1D057DF6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6fdf9181d54243407b71bf422d76d629432c6f9","datavalue":{"value":"natural translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751819$E341052D-675D-4FFF-8DF5-489AF04CF784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b8455f6b14475445dd3c8abdc10ff392d2d4624","datavalue":{"value":"multiplicative connectives","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751819$BEEABCAF-1370-4E88-8549-D37A55D46FE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751819$BE2A8441-8D9E-480C-B5A2-A3DAF5E6F472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9b243572f25465f3ae7a32f2d3b06ae2073b8520","datavalue":{"value":{"entity-type":"item","numeric-id":590478,"id":"Q590478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2751819$658E8B5B-1B5C-4E27-A70B-29A6A2F6B8E0","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":"Q2751819$51C4CE06-3597-448D-AA69-D17FD41E2043","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e7d45500be55ac5ba460611a0d503ccff8a94b67","datavalue":{"value":{"text":"Classical multiplicative linear logic \\(\\simeq\\) intuitionistic MLL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2751819$7D1E8DD4-8C7B-4737-89CF-B0BCEC5A1576","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f1cbe77a823c41740fa7f13d0b4ec9f7c92fea56","datavalue":{"value":"The authors show that a deduction in CMLL (Classical Multiplicative Linear Logic) can be regarded as the result of the natural translation, *, of an intuitionistic one, IMLL. This is as expected, because rules for multiplicative connectives are so set up that any recurrence of a formula can be traced unambiguously through a deduction. The authors allow the constant \\(I\\) (truth), and avoid proof nets so the translation is among sequents. On the CMLL side, symbols used are: \\(I\\), propositional variables and their negations. Formulas are built by means of \\(\\otimes\\) (and), \\({\\mathfrak p}\\) (or), and a sequent is a multi-set. On the IMLL side, the negation is not used, the connectives are \\(\\otimes\\) and \\(\\circ\\diagrbar\\;\\) (implies), and a sequent is of the form \\(\\Gamma\\to A\\). The theorem reads roughly: If \\(d\\) is a CMLL derivation of \\(\\Gamma,A\\), and there are IMLL \\(e\\) and \\(\\Gamma_1\\to A_1\\) such that \\(d\\) is \\(e^*\\), and so \\(\\Gamma,A\\) is \\((\\Gamma_1\\to A_1)^*\\). E.g. the axiom \\(\\overline{p},p\\) is obtained as \\((p\\to p)^*\\). \\{The actual theorem is more complicated mainly due to \\(I\\)\\}. NEWLINENEWLINENEWLINEIn definition of *, the negation sign is missing here and there.NEWLINENEWLINEFor the entire collection see [Zbl 0960.00036].","type":"string"},"datatype":"string"},"type":"statement","id":"Q2751819$65FCBFB2-8BCE-4A32-8BCB-991BBB2C6CDA","rank":"normal"}],"P1643":[{"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":"31698140d5265a39a03cd845585679a75508ebc8","datavalue":{"value":{"amount":"+0.750686526298523","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":"Q2751819$BC1CD367-397B-473E-AAA3-3ED4409A3BA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ea70ba171b852e8efc26bea54c918fc8c8372fe","datavalue":{"value":{"entity-type":"item","numeric-id":1210141,"id":"Q1210141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d8c816d3e723a0f4e2560fa85335f6465749641","datavalue":{"value":{"amount":"+0.7366510629653931","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":"Q2751819$55A7F04D-5182-49BF-AEF9-5B6760C4822A","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":"7cf4cecfa95201652d241c03f13457c27c14ef2a","datavalue":{"value":{"amount":"+0.7360374331474304","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":"Q2751819$E440910E-B728-4A65-BF18-C77667B1063C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"552994d5ec99f6724e93968a7ea6470db96a1add","datavalue":{"value":{"entity-type":"item","numeric-id":3126403,"id":"Q3126403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30b0047c586e741e20667622bf3c7f16a95bca31","datavalue":{"value":{"amount":"+0.7146264910697937","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":"Q2751819$E10F6599-02E6-4257-BC89-F59782F45048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d110f87b773c3c5f12c078339b2d1360fb9ffdde","datavalue":{"value":{"entity-type":"item","numeric-id":4006233,"id":"Q4006233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f2f98a0a8470dff99c6fad549680fe0f0a202b1d","datavalue":{"value":{"amount":"+0.7092752456665039","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":"Q2751819$E83D3034-8660-4C12-8F14-5E86F55A7F65","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Classical multiplicative linear logic \\(\\simeq\\) intuitionistic MLL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Classical_multiplicative_linear_logic_%5C(%5Csimeq%5C)_intuitionistic_MLL"}}}}}