{"entities":{"Q676308":{"pageid":678157,"ns":120,"title":"Item:Q676308","lastrevid":63645699,"modified":"2026-04-11T14:34:58Z","type":"item","id":"Q676308","labels":{"en":{"language":"en","value":"Contraction-elimination for implicational logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 992109"}},"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":"Q676308$7368C5AB-F469-4D3B-A1B5-3CA4A9E012AA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"db693709c92f0813fff23ac9ffe7513350fc2f12","datavalue":{"value":{"text":"Contraction-elimination for implicational logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q676308$0A79DDD2-B93B-4124-A40C-110586E3F44F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9ff53427a12929e2318fd6e312eb7f7b69b6b460","datavalue":{"value":"0872.03037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$19ED663F-97A4-4731-8BE0-08414FFB7A04","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"db8ca8d546e0f182af923cee5ecbf80e17fa03e4","datavalue":{"value":"10.1016/S0168-0072(97)81394-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$A220CAD6-BE36-43EB-B93F-5B61CDD7E142","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5204fccf6931ba93979bc107c2fe66e59a9ff1f6","datavalue":{"value":{"entity-type":"item","numeric-id":676307,"id":"Q676307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q676308$2A05148D-9074-41E7-A0CA-146FA18855B4","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":"Q676308$2F17C3BB-90F9-435D-8121-ECBEC44E606F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"53ca32303030cbcdd57a20141335cf713f9048cc","datavalue":{"value":{"time":"+1997-10-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q676308$79457579-D99D-44B0-B5F2-53D91936B8D9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"15a68408498ce68a2c4decb79b918bbbfe09fbf3","datavalue":{"value":"The author considers the implicational fragments of the classical and intuitionistic logics and obtains a quite interesting syntactical result regarding the role of contraction rules in the corresponding Gentzen-type formulations of these fragments.   A propositional letter \\(p\\) is said to be PNN (respectively PPN) in a sequent \\(\\Gamma\\lvdash A\\) if \\(p\\) occurs at least once (resp. twice) positively and at least twice (resp. once) negatively in \\(\\Gamma\\lvdash A\\). The following ``contraction-elimination theorem'' is proved: if a sequent \\(\\Gamma\\lvdash A\\) is provable in the implicational fragment of \\({\\mathbf L}{\\mathbf K}\\) (resp. \\({\\mathbf L}{\\mathbf J}\\)) and if no propositional letter is PNN (resp. PPN) in \\(\\Gamma\\lvdash A\\), then \\(\\Gamma\\lvdash A\\) is provable without the right (resp. left) contraction rule. An immediate consequence of this theorem is the following one: if an implicational formula \\(A\\) is a theorem of classical logic (resp. of intuitionistic logic) and is not a theorem of intuitionistic logic (resp. BCK-logic), then there is a propositional letter which is PNN (resp. PPN) in \\(A\\).   The methods used in proofs are purely syntactical.","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$4B675FC8-9E00-4FB6-9CEB-CD1C188E6E2F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$B59EA501-EB05-40EB-BFFD-F54AC12592AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$2C55E701-ACA7-412A-8D9A-3B2747B94DC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"89a6721807d2106ad3a18783b4fcbc004e6a56c5","datavalue":{"value":"03B60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$1E882C87-F125-4914-A760-1DF0A1E1004B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6fd48a4f2d1323cc916553cf0cf7258d2ddf8222","datavalue":{"value":"992109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$A1BCCABD-9BC9-4EC1-A1D0-02EF10AF7CF6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"637cab94c87a5b556b1043f03f56b4600824940f","datavalue":{"value":"implicational fragments","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$90B36B3B-EE5B-400E-869D-92DB54081F29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05352066a1e3f1ee80c5805bf4e7ac2fb1fb2fff","datavalue":{"value":"contraction rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$0D875B25-18FD-48C7-A564-6EA50A724167","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f562a1de1430bfc0aa42cc4e06a317f5260ed47c","datavalue":{"value":"Gentzen-type formulations","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$2E05E0B6-439F-4319-9FFF-9B0801BB708C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ffd3928aa1fd818bc1a8806528172e266ac8bcc","datavalue":{"value":"classical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$18EAB660-F8C9-40BE-92FD-33B12FF24DAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$66E0836B-881A-41A6-BB2D-C676724E0C34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70e6230853178ae07c963996ccc88c435cbb674e","datavalue":{"value":"BCK-logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q676308$291A3960-C249-40AD-B2E1-10D4EFA971B4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q676308$FF13D130-D137-4678-A76B-DCB1EDF49098","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":"Q676308$BB20B733-D48F-4604-9C86-9C2EB4D4DDCC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"25313d367058edb8143ccf81859fe214d888d1ea","datavalue":{"value":{"entity-type":"item","numeric-id":5723175,"id":"Q5723175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q676308$747314D5-1DE8-48CF-A018-111CC9146BD2","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":"Q676308$64B6D40E-4E79-41D3-A925-31A792D5B716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q676308$757F382E-03F4-4D86-BC02-E5A30951316B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ada9be77a9c1e99df1ef74deac15f29dcbb5279e","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(97)81394-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q676308$710A889B-4C02-4DF8-9485-C0B24BBFA331","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c100992172df053a547b69d08df698efe3b13b9d","datavalue":{"value":"W2071338206","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q676308$51F26E97-8624-4019-8B40-1E1DDDCE9EAA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc025492c3f688012f1576558ed7c64211309902","datavalue":{"value":{"entity-type":"item","numeric-id":4032862,"id":"Q4032862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ffd2197e86fa006a1083c7b888330bc389622331","datavalue":{"value":{"amount":"+0.8969599","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":"Q676308$15399620-6A77-467D-89EE-AC3C81807561","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":"825054e286bc500c9eeffd5e12085646063a3ef4","datavalue":{"value":{"amount":"+0.8959123","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":"Q676308$B1C04613-9D4D-4C71-9398-7EAB2170BDD0","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":"de31ec07f350851ba19d61405109d3b72ea6c72b","datavalue":{"value":{"amount":"+0.8922414","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":"Q676308$72603379-9628-42A1-B376-14A82CCEA9B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8247e0036be779cdf732b2573b66754ba24433a6","datavalue":{"value":{"entity-type":"item","numeric-id":3451176,"id":"Q3451176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1df156ce7fe72f3ff510192ff54945cb7e71e383","datavalue":{"value":{"amount":"+0.8920479","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":"Q676308$3C0A27B8-A72F-4F73-846E-5E166584E80A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f1ad3ec1d37c549f5912310543255803e5651ef","datavalue":{"value":{"entity-type":"item","numeric-id":2374542,"id":"Q2374542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1df156ce7fe72f3ff510192ff54945cb7e71e383","datavalue":{"value":{"amount":"+0.8920479","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":"Q676308$9D7DBF58-DF74-4CFB-BDEC-8306EF5D70B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0eb7e3496eaeebf49c85ec917e73c30283d0c57d","datavalue":{"value":{"entity-type":"item","numeric-id":2888635,"id":"Q2888635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"615139b4aca7372b3536ab9781f314a563f4dd77","datavalue":{"value":{"amount":"+0.8808316","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":"Q676308$EDDA2F59-3825-4525-B188-7AE2C374219E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5405a0c543ae60f2a5551ae64f4a7919cb6a3a1","datavalue":{"value":{"entity-type":"item","numeric-id":791512,"id":"Q791512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f92aa235513077cc4d2f340fd69c87c63f99f29f","datavalue":{"value":{"amount":"+0.879668","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":"Q676308$DC696A71-074B-43BF-9539-9DB7322F5EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66dbc1c7946709f0da84bc648ed0c6a2db12ab65","datavalue":{"value":{"entity-type":"item","numeric-id":1181491,"id":"Q1181491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"356209d222cd29631e1881b668901b226bad7662","datavalue":{"value":{"amount":"+0.8794439","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":"Q676308$09F38084-CB0F-4B1F-8A8B-93AEC38B41BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bec22ff490172df0fc4deb3bf2206207f1361fb","datavalue":{"value":{"entity-type":"item","numeric-id":1576374,"id":"Q1576374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8674a90178f7c093b860568d2e260ba2ef3544bd","datavalue":{"value":{"amount":"+0.8794117","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":"Q676308$140BD780-A41B-438B-90AD-B7CA7BDDA6D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8f77f41b3686091707996de9dae1076e0fa3e63","datavalue":{"value":{"entity-type":"item","numeric-id":1580655,"id":"Q1580655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"553f8bf48d0bc501eed2c14eeb28adc4eeeb9078","datavalue":{"value":{"amount":"+0.8793157","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":"Q676308$039E1CE6-03D2-44E3-9E1F-A2C031BE1551","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Contraction-elimination for implicational logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Contraction-elimination_for_implicational_logics"}}}}}