{"entities":{"Q5903941":{"pageid":8014790,"ns":120,"title":"Item:Q5903941","lastrevid":39852137,"modified":"2025-01-27T18:57:46Z","type":"item","id":"Q5903941","labels":{"en":{"language":"en","value":"Solution to a problem of Ono and Komori"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4097367"}},"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":"Q5903941$AC96D7C4-2092-4F09-B282-790236919483","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5f7e73facbc105c7d35f338b8d3b115f9704ce3a","datavalue":{"value":{"text":"Solution to a problem of Ono and Komori","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5903941$386DBCB7-9EA1-4DA5-BBFD-C634DD95E86C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7260be91d32ab1ca2b88325ebf2a3c2047376a84","datavalue":{"value":"0671.03036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5903941$64881555-6E35-4B13-B377-62C45839BF84","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9efa9bd05efef2b36683a66c9725534a75880c74","datavalue":{"value":"10.1007/BF00296176","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5903941$19E44565-8E52-44CE-B6CD-7E8A0164BEF7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1bcf20fbd6e518d6ec705e75c1250ec189c8029f","datavalue":{"value":{"entity-type":"item","numeric-id":689215,"id":"Q689215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5903941$1489EFC0-3DE5-4248-8649-97C4C768AEED","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":"Q5903941$5DC4D2C3-11AB-4F90-8A84-18AA2D61094B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q5903941$D9634315-0F59-4DA5-87ED-389E283CE1F5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"61a0c036cc96135af8c8db832d1234a6af27e979","datavalue":{"value":"\\textit{H. Ono} and \\textit{Y. Komori} [J. Symb. Logic 50, 169-201 (1985; Zbl 0583.03018)] posed several open problems concerning some systems of contraction-free logics. This paper gives the solution to Open Problem {\\#}6: Give a Gentzen-type formulation for the distributive logic \\(L_{DBCC}\\) [equivalently, \\(H_{DBCC}]\\) or \\(L_{DBCK}\\) [equivalently, \\(H_{DBCK}]\\), for which a cut elimination theorem holds. The axiomatisation of the former is very much like that for the contractionless relevant logic \\(RW+\\) with fusion (intensional conjunction) and a false constant, F. Simply drop Permutation and an explicit Identity axiom in favor of \\(A\\to.B\\to A\\) and the rule: From \\(A\\to.B\\to C\\) and B to conclude \\(A\\to C\\). For the latter, keep the Permutation axiom, add the axiom just given, and Replace the normal \\(\\vee\\)-Composition axiom with the stronger \\(A\\to C\\to.B\\to C\\to.A\\vee B\\to C.\\)    The Gentzen systems of this paper \\((LL_{DBCC}\\), \\(LL_{DBCK}\\), respectively) are singular on the right and utilise two kinds of sequences or methods of combining formulae on the left, as is now common in dealing with relevant logics. See \\textit{J. M. Dunn} [in: \\textit{A. R. Anderson} and \\textit{N. D. Belnap jun.}, Entailment, Vol. 1 (1975; Zbl 0323.02030), pp. 381-391], for example. Once this technique is employed, the choice of appropriate structural and logical rules becomes relatively straightforward: Add a rule of intensional weakening and the axiom F:A to \\(LRW+\\) (without the rule of intensional permutation or exchange for the former). See the reviewer [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)], for instance.    However, the proof of an appropriate cut theorem becomes correspondingly complicated. The author chooses the form:  \\[  \\frac{X1:A1,...,Xn:An\\quad y(A1...An):B}{Y(X1...Xn):B}  \\]  which is proven by triple induction on rank, degree and the number of contractions (applications of extensional contraction) above the major premise.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$5400858E-671E-4007-A435-C9BA00DF2367","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0aa64c621a2feafe101247ed541c38a7affa2b8e","datavalue":{"value":{"entity-type":"item","numeric-id":579233,"id":"Q579233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5903941$EB29D580-53D6-4008-828A-2F3C105F9F9E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5903941$E005490A-47AC-4D75-99DF-AF136120E73F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bd857b4d539debc924b23d4d2c029b3554136b84","datavalue":{"value":"03B99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5903941$10F5CDF4-A0FB-46E7-9ABB-F6C0F220AB29","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"65470f5e69f3d364b3e339f1dd30466a5c96ecab","datavalue":{"value":"4097367","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5903941$A9D93B04-0D60-4885-AD03-589920212CA4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"007178e48802a62bc4654c927dc92fdb00a13725","datavalue":{"value":"BCK logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$CD347503-049E-4A82-ABA8-3BAD1125DC7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4023a236734655c68f1f37fb4aadf1f34993f4a5","datavalue":{"value":"BCC logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$4B5394C3-9437-4CB2-AF54-A3D8F81C2E32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e72398f9a28f182ef9fd00964c3b0378b770645a","datavalue":{"value":"contractionless logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$79F1E2E5-E2F0-48F9-9747-60B1880DB838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a9f1655a23f7bb198567245ef1b3fe5ba894ec8","datavalue":{"value":"RW","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$2911DFD4-FABF-47A2-A53D-06578993B506","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"093bda0fe2ce6b9c31255c3a2d81074b995cb83e","datavalue":{"value":"contraction-free logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$BF40942C-6DE2-4F60-9520-3EEF74D78811","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e99e69567f640b1f327b140fce369b10bed2644b","datavalue":{"value":"distributive logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$7C82A388-DF0F-4E27-9620-711498BE8051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$5E3DE247-F505-4EDB-A59B-F047558ED218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4908130fad200c533896629f09c6eb4da5e3c07","datavalue":{"value":"Gentzen systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5903941$28810292-1CFB-455E-A811-2D05B70D594F","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":"Q5903941$F79D47D6-F32B-4421-B6FC-C8445B206B44","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b70c7b3f003527069c2310fc828f8afaad5df5d6","datavalue":{"value":{"entity-type":"item","numeric-id":1838471,"id":"Q1838471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5903941$2239894B-1B9D-4B9A-9A3C-6AE66A44D4C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb5cbc6e4207291864084d3942a2b63091f8bab1","datavalue":{"value":{"entity-type":"item","numeric-id":1072541,"id":"Q1072541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5903941$2C761A97-00F8-4321-A7D6-B0DC3AC6A53B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc09538a5c77707bd740c1af4339f9cfde82b8b","datavalue":{"value":{"entity-type":"item","numeric-id":3707997,"id":"Q3707997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5903941$59A9108C-16C8-4B0A-A7CF-12CE11580B83","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6c748c2803a6d118df430975b3ef423365586b7","datavalue":{"value":{"entity-type":"item","numeric-id":5966494,"id":"Q5966494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7511143d2814db88ab4154477ad21aadb3992f7","datavalue":{"value":{"amount":"+0.95024455","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":"Q5903941$5CDB4DE0-4D81-47C4-BE73-A3A1DFF0222D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d47b2cd59f4f35f3874d1a5c98b606bb7502c5f3","datavalue":{"value":{"entity-type":"item","numeric-id":4856945,"id":"Q4856945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66e6b189cd270cf2b8f1f367bd28d8f200031f24","datavalue":{"value":{"amount":"+0.81539214","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":"Q5903941$8AA16DF8-C3A6-4208-950F-BE7EAC0BA91A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d885227f885cbf4619d0b2a0a4268af7c45e49e0","datavalue":{"value":{"entity-type":"item","numeric-id":5279185,"id":"Q5279185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ec37bdd9629a28167961658af6028f0b24d1342","datavalue":{"value":{"amount":"+0.8064137","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":"Q5903941$3BBD7D02-F0E2-487C-85AD-3F6A796D4004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f63d84f24d8bd1e2bb35c8f6cfd21559ed6f4edc","datavalue":{"value":{"entity-type":"item","numeric-id":2277247,"id":"Q2277247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eaec8de488f0c284dd1a9051ebe4ceb08f9af091","datavalue":{"value":{"amount":"+0.7776175","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":"Q5903941$E35BF2B0-1364-46A3-9591-36C0804C51E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a0ac52ea3df78e57e6044738608477c9dcdc5be","datavalue":{"value":{"entity-type":"item","numeric-id":5020358,"id":"Q5020358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4574323708a27604051d93f242c5a478d2bd766","datavalue":{"value":{"amount":"+0.76374996","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":"Q5903941$08DEA57E-5F63-4E71-A69B-5C5EC1080A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a19f255d39c65b5b7fd3a86a166cc34f7825b115","datavalue":{"value":{"entity-type":"item","numeric-id":1104918,"id":"Q1104918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9a65d249f6c87738198a38b59a7fe93d6e387eb","datavalue":{"value":{"amount":"+0.7634296","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":"Q5903941$D8BEF98C-1C8E-4D6F-8D8B-C7F06ED45651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12e9b46da072a9a280b667bf2be41b3e5d24ecc5","datavalue":{"value":{"entity-type":"item","numeric-id":3128476,"id":"Q3128476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecbc5d2cadd8786078ecdf421079527492c1b56d","datavalue":{"value":{"amount":"+0.73312914","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":"Q5903941$272FF7DA-B3E0-4A15-83BD-A98C5838D491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5216c12011557aab9968b27125ae5048ba8d2088","datavalue":{"value":{"entity-type":"item","numeric-id":4395550,"id":"Q4395550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40e0e92c9e113cb4195ab1011e5171241264162e","datavalue":{"value":{"amount":"+0.7287292","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":"Q5903941$A41B3246-8650-4FB2-A114-12E94785F781","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d145461fe957f0967e37093d1c4baba0d279c6b9","datavalue":{"value":{"entity-type":"item","numeric-id":4894717,"id":"Q4894717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ee655afbfd5cef1cb5b1404997bb9988b8c5a21","datavalue":{"value":{"amount":"+0.7216988","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":"Q5903941$03BACAB0-8959-4AE5-B45B-8D0696674EF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3206d7c121ced57d7a62b35ef045ac4abc52af06","datavalue":{"value":{"entity-type":"item","numeric-id":5172146,"id":"Q5172146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2c876ac445572301abda1e888ca43575cc1019b","datavalue":{"value":{"amount":"+0.7156246","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":"Q5903941$D4BF582A-3E5D-437C-8297-07A947FFC986","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5903941","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5903941"}}}}}