{"entities":{"Q2452677":{"pageid":2463420,"ns":120,"title":"Item:Q2452677","lastrevid":78693623,"modified":"2026-05-06T12:12:57Z","type":"item","id":"Q2452677","labels":{"en":{"language":"en","value":"BCK is not structurally complete"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6300871"}},"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":"Q2452677$22D24279-8AAC-46A7-AC9C-2418E3EC0A46","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1b85c4c833d59e176f6cd164053e5a8bdb7d04c9","datavalue":{"value":{"text":"BCK is not structurally complete","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2452677$4CA47890-4A1E-436E-8624-A9C5554972EF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a723bc3f7a8cd33f8c5b29f0b58c78f3ac22f772","datavalue":{"value":"1327.03017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$C406006A-C049-4DC6-BA66-3FA7A85A0C13","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c848489c2104e24e1ab1bc357361dfeef3fe6b54","datavalue":{"value":"10.1215/00294527-2420642","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$FA462175-8E45-4AB0-873D-4D8A2AA2BCD6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"241d91eac26be9dafce27577b0d1f937fbd531b1","datavalue":{"value":{"entity-type":"item","numeric-id":353354,"id":"Q353354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$B49E6DE7-C0A8-4E11-B2A9-6F33E7E89AAB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$1AFDD515-7898-4181-886A-1F67FA7F7C96","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0fddd97b3c6b0df70ec750ef42d1239f50e1e71b","datavalue":{"value":{"time":"+2014-06-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2452677$636AAC57-4620-495E-AE1F-E16E525E9C18","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ebe8e3eac52a2915f66433554c9cfea5b5e3afbc","datavalue":{"value":"https://projecteuclid.org/euclid.ndjfl/1398345780","type":"string"},"datatype":"url"},"type":"statement","id":"Q2452677$FDD05117-04B4-4A92-BB78-18795B9D4C02","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"32ac8af481ba154891974cc35030adabb5e302f4","datavalue":{"value":"A logic is a set of formulae closed under a consequence operation given by some axioms and structural inference rules. An inference rule \\(\\alpha _{1},...,\\alpha _{n}/\\beta \\) is \\textit{derivable} in a logic \\(L\\) if \\(\\beta \\in C(\\{\\alpha _{1},...,\\alpha _{n}\\})\\) where \\(C\\) is the consequence operation of \\(L\\). And it is \\textit{admissible} if \\(\\sigma (\\alpha _{1}),...,\\sigma (\\alpha _{n})\\in L\\) implies \\(\\sigma (\\beta )\\in L\\) for every substitution \\(\\sigma \\). A logic is \\textit{structurally complete} if \\ every rule admissible in \\(L\\) is also derivable in \\(L\\).  The logic BCK is the pure implicational logic axiomatized (together with \\textit{modus ponens}) with the following axioms:   (B) \\((\\varphi \\rightarrow \\psi )\\rightarrow [ (\\chi \\rightarrow \\varphi )\\rightarrow (\\chi \\rightarrow \\psi )]\\);   (C) \\([\\varphi \\rightarrow (\\psi \\rightarrow \\chi )]\\rightarrow [ \\psi \\rightarrow (\\varphi \\rightarrow \\chi )]\\);   (K) \\( \\varphi \\rightarrow (\\psi \\rightarrow \\varphi ).\\)  The author proves that BCK is not structurally complete by showing that the rule (let us call it \\(\\rho \\) here) \\((\\alpha \\rightarrow \\beta )\\rightarrow \\beta /(\\beta \\rightarrow \\alpha )\\rightarrow \\alpha \\) is admissible but not derivable in BCK. The admissibility of \\(\\rho \\) is proved by using a Gentzen-style sequent calculus version of BCK. This Gentzen calculus makes an essential use of \\textit{split terms}, a notion introduced by the author (``split terms can be thought of as encoding cut-free proofs of provable sequents in which they occur'', p. 199). The non-derivability of \\(\\rho \\) is proved by showing its failure in the \\( \\{\\rightarrow ,1\\}\\)-reduct of the totally ordered 3-element Heyting algebra. In the last section of the paper, the author notes: ``admissible but non derivable rules describe certain properties of the free BCK-algebra that are not shared by all BCK-algebras'' (p. 203). Then, he proceeds to prove one of these special properties.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2452677$1CE7AFCA-E660-46EE-9760-F89715EE170B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"1337cba793ece012dc87025b12e0025a65ffdc83","datavalue":{"value":{"entity-type":"item","numeric-id":590824,"id":"Q590824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$FE4229ED-BBD1-4F4D-8051-DE4A8ACBE42D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$C29367FD-3D8A-4C5B-9205-4E8FA0BAAAD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$BA086C03-B8EE-404A-B0C8-CFD1BF52BD13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a1f7150f9a39f853b63ad46f37d78a6cea4d967e","datavalue":{"value":"06F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$1C76DC92-0CA2-494E-A17D-8D5B93AB4438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$0F52E26A-D5A1-463E-86BE-D9F0EE7A29E6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7278a7af5156f11b7d70501407a7916d0822bba0","datavalue":{"value":"6300871","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$D113FE4E-C8E7-4B17-9C44-45CD8BC419ED","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"007178e48802a62bc4654c927dc92fdb00a13725","datavalue":{"value":"BCK logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2452677$8444B9FA-A845-4DAF-BEBB-7CD614788B62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"548bc79ce362c691471fdce748b63aafcb850b45","datavalue":{"value":"structural completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q2452677$D0B1D46E-68B0-4B06-B4F6-D00A0773E4D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"203383f5640e2b7ae9ac255db7b9410f9f3dc7ba","datavalue":{"value":"admissible rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q2452677$F76E34C0-A413-48B3-8F9D-AF6E23A8E363","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":"Q2452677$3C0829EB-E86C-4C26-986B-3CA58FA9B482","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7293598495bb23b4159df723783fe1c2f2287e77","datavalue":{"value":"W2071182863","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2452677$785C3E58-FA71-47FE-9F4F-1FC0336BF619","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf9f35305cec81383dab47d3302a015808f01f7","datavalue":{"value":{"entity-type":"item","numeric-id":1038654,"id":"Q1038654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$6D8A941B-1DB3-4969-B739-23E33EC26352","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8d037473ac64fb3b587cff76b7f68eeb417fc42","datavalue":{"value":{"entity-type":"item","numeric-id":5607967,"id":"Q5607967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$CC4E1B7C-E128-4685-8F97-FB71647314D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11a17c0e2b84bbe65ca76d56341f4b62b65e88e8","datavalue":{"value":{"entity-type":"item","numeric-id":948761,"id":"Q948761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$27D479BD-F80A-457E-A9DD-51EB5225932B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"caef83d8c323369d390f06220cb4f544d73185f7","datavalue":{"value":{"entity-type":"item","numeric-id":3544316,"id":"Q3544316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$A1152EE9-D1B5-43FC-AEAC-45723602D20B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be9ad6b6e321a7e2337813c8f50d9008365af515","datavalue":{"value":{"entity-type":"item","numeric-id":5616120,"id":"Q5616120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2452677$E92611A6-EA53-40FC-BC25-9EAC716151AA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4204f808519bc56b4b155cc0d66be7c49cec5f79","datavalue":{"value":{"entity-type":"item","numeric-id":3342540,"id":"Q3342540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"814fc0e2889f1b2c647f0abf81a3d66982a9e283","datavalue":{"value":{"amount":"+0.7909603714942932","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":"Q2452677$F3549BBF-2CB4-48A6-AD88-20D99801C644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77dda455f2ff103a2dfe2af72f5a7a96f73ebf56","datavalue":{"value":{"entity-type":"item","numeric-id":4836055,"id":"Q4836055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48b85159285bb7f98280b46a2ef152ae1ac77b78","datavalue":{"value":{"amount":"+0.7830356359481812","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":"Q2452677$7F40562A-AEAD-4EAC-B953-0FA1B9AC0392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df7715d37aa83c72d0cc85449b40f0f2827adb54","datavalue":{"value":{"entity-type":"item","numeric-id":3352995,"id":"Q3352995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48b85159285bb7f98280b46a2ef152ae1ac77b78","datavalue":{"value":{"amount":"+0.7830356359481812","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":"Q2452677$DF106414-FAA0-4073-B000-984DBB8B978D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"234b137cab501657b58cc80a0605388121ef3d50","datavalue":{"value":{"entity-type":"item","numeric-id":4815865,"id":"Q4815865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c71aea945458ebde113a471cda7e1d791b7c6974","datavalue":{"value":{"amount":"+0.7767053842544556","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":"Q2452677$9D34807A-3B3E-4627-81D9-CAA64446E7FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f84dca0cf31f2217dbbfcd694741277df07b676","datavalue":{"value":{"entity-type":"item","numeric-id":3351349,"id":"Q3351349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4bcc11117e46289e3fa9768976d8609f4e611d1","datavalue":{"value":{"amount":"+0.7743524312973022","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":"Q2452677$0ECE7341-5235-4CF3-86BE-BDD685FDF8E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"BCK is not structurally complete","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/BCK_is_not_structurally_complete"}}}}}