{"entities":{"Q4489072":{"pageid":6518671,"ns":120,"title":"Item:Q4489072","lastrevid":108606137,"modified":"2026-11-07T04:23:28Z","type":"item","id":"Q4489072","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1471988"}},"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":"Q4489072$C7FB9B79-B80F-4893-A5A7-3C490690227B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f0351166cd12428bee0f5d1bfce5f914073e5ba5","datavalue":{"value":"0963.03002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4489072$D145E483-8529-4B25-85BE-25F775943B75","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d07da6141e61d14f40fca64574461dd10f1172df","datavalue":{"value":{"entity-type":"item","numeric-id":1327481,"id":"Q1327481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4489072$34B5237C-ED90-4754-94FA-4CAF31CA9055","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7d0e28e6bdfdb3b39ab02d4e8ca0727f8eac2c75","datavalue":{"value":{"time":"+2001-06-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4489072$A6C72190-2E6C-4FCD-898B-27A17467F66B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4489072$E6BFD8B5-46BA-4ABD-A93E-1DC422D96EEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4489072$E849CA73-F184-4195-AEC9-FDA94F96216B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4489072$5A065484-D2C9-4612-9486-91672ADFF819","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f202359503252d350023d20c14d464e368bdec5","datavalue":{"value":"1471988","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4489072$F29DEA38-6A9E-4556-BC8D-C74400F2F975","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":"Q4489072$FC1805AA-19E1-41F1-B107-3D04289F719E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b3ca5d7bb5b727be1de5d72845cf8d93eed70a8","datavalue":{"value":{"entity-type":"item","numeric-id":4985610,"id":"Q4985610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf28774a7a1696db29af08d0f6a4bccc6a61d137","datavalue":{"value":{"amount":"+0.7427000403404236","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":"Q4489072$448AC112-1DBF-4F61-BFE9-8279A4360EA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa8b1b4f2a849203410afaf6111715780790c37c","datavalue":{"value":{"entity-type":"item","numeric-id":2710612,"id":"Q2710612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"521fb1df5472da0b060514500416205a88025343","datavalue":{"value":{"amount":"+0.7354893088340759","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":"Q4489072$6A616471-EE50-4D0A-A3B8-7614175DED2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b692ce3de9122d8fcb53989f11735e3ac2ddea6","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"521fb1df5472da0b060514500416205a88025343","datavalue":{"value":{"amount":"+0.7354893088340759","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":"Q4489072$7AA922C5-8014-4E2D-9D31-C3FA2A60A46C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b419f24277f2c2c36c621175f439653d84f33ae8","datavalue":{"value":{"entity-type":"item","numeric-id":3655015,"id":"Q3655015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"217f2a3c903bb82c4cf735a1255bd6340b0889e9","datavalue":{"value":{"amount":"+0.7336334586143494","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":"Q4489072$6422AD14-0D84-4E5B-A4A6-076F88DCFB91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b78357d02d79ebca3a6ccfce57a4024be7b3963f","datavalue":{"value":{"entity-type":"item","numeric-id":1337604,"id":"Q1337604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11aa466225a2aa64e6afd603b109400e563b68f0","datavalue":{"value":{"amount":"+0.7113792300224304","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":"Q4489072$5D00E236-575E-4235-BAC8-A440B8EB179F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"84741b767dfa9b65275df53f0f2f1337debc0cae","datavalue":{"value":"The normalization theorem, the main theorem of this paper, shows, for the logical system P-W (or BB'I) formulated in sequent calculus style, that a refinement of the cut-elimination theorem holds: That is, any provable formula in the system P-W can be deduced via a cut-free proof in a special form. This theorem is used in results mentioned below, and was a fundamental discovery which led us to solve syntactically the so-called P-W problem. The first solution to the P-W problem by means of cut-elimination was given by Nagayama, the author of the present paper. However, this solution was never published. Thus the reviewer intends throughthis review to verify this fact and to give her the credit she deserves. The reviewer's paper [Stud. Log. 54, 397--416 (1993; Zbl 0813.03015)] was originally written to fill a small gap found in Nagayama's first proof concerning the P-W problem. Nagayma's original solution only uses the system BB'I, whereas the reviewer's solution initially investigates the relationship between two logical systems, BB'I and BB', and then solves the problem. Since Nagayama liked her own approach better and considered the reviewer's approach completely different, she had no intention to become a co-author which might have been more appropriate. After all, her original proof was very complicated: Furthermore, since the reviewer's paper was published prior to her completion of her own proof, she finally gave up writing it. Nagayama also obtained a version of the normalization theorem for the logical system BCK, and proved the theorem that the BCK-algebras do not form a variety. Although this result was published [Stud. Log. 53, 227--234 (1994; Zbl 0799.06032)], the proof, simplified later, does not use the version of the normalization theorem for BCK. The reviewer still regrets the fact that the original proof to the P-W problem was never published. But now he feels better, since the paper under review at least reveals the universal fact in several logical systems which encouraged and led us to solve hard problems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q4489072$64B2FDC4-FA2D-4271-A856-A77B06787F10","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4489072","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4489072"}}}}}