{"entities":{"Q1919985":{"pageid":1930727,"ns":120,"title":"Item:Q1919985","lastrevid":43421523,"modified":"2025-07-25T16:37:12Z","type":"item","id":"Q1919985","labels":{"en":{"language":"en","value":"A reduction rule for Peirce formula"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 910393"}},"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":"Q1919985$8DA4140D-9B56-4AA9-A804-FD6E9AC1A3C9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"305ec3d903c7e83d9520be1299d418a971f3e33d","datavalue":{"value":{"text":"A reduction rule for Peirce formula","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1919985$8B35997D-743A-48A9-97BD-F51E50505896","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a65e0b65f6069e5d91f2e11ec15cab721aa7e1a5","datavalue":{"value":"0857.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1919985$32CEACA9-2531-427A-ABD4-FAD128818B78","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bfc10c21ef85410552f1c97eed16a2229fd0057f","datavalue":{"value":"10.1007/BF00372774","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1919985$F7D9CBEA-E4EF-4391-8905-D9921E9904D6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9126baf050ca2a9061dbf118bb26f3c0708e62a7","datavalue":{"value":{"entity-type":"item","numeric-id":1075051,"id":"Q1075051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$135713DC-0202-4189-91BF-FB6B8DFD947B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"284b349575b4cf80ae5ff7dbd50dcd981e4aa70a","datavalue":{"value":{"entity-type":"item","numeric-id":1089329,"id":"Q1089329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$5526628B-F35F-4EF1-99D6-B0AB2AFF0F5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5cc82f69219366188f484a12a1c2b76f1ba14053","datavalue":{"value":{"entity-type":"item","numeric-id":1852417,"id":"Q1852417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$D0BE8521-8FDA-4B61-B277-6B19973C9D50","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$47EB076E-FF01-403A-987A-C52FAA414DA0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7d08bb9a72a2259fe21464e6025b4a7e58a684cc","datavalue":{"value":{"time":"+1997-03-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1919985$B07FEE22-8FE9-44B9-AFA8-0691ECF08346","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fd692a3e2e74a7e47f79ba3967c5068f044d3cac","datavalue":{"value":"It is well known that, via the Curry-Howard isomorphism, SK-combinators and their types also represent, respectively, proofs and theorems in intuitionistic implicational logic. The reduction rules for the combinators can be motivated by proof reductions. The authors of this paper introduce a new ``combinator'' P, with a type that corresponds to Peirce's Law, so that proofs of classical implicational logic can be represented using SKP-combinators. A reduction rule for P is motivated by a proof reduction in classical implicational logic. The addition of P and its reduction rule to untyped combinatory logic implies the equality of all combinators, so only the addition of typed Ps to typed combinatory logic is proposed. Even so, this system is neither Church-Rosser nor strongly normalizing and, in it, all combinators with the same type (such as the Church numerals) are provably equal. A weak normalization theorem can be proved when an additional reduction rule for P is added. Most of the paper uses lambda calculus notation, which can be translated into combinators. When this is done this new rule becomes particularly complicated.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$916B8109-15B2-4D83-8B58-BDA6C10F0F2A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"376f136d3715d0668145bfef82b652dbeb24818d","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$297F7B02-E709-410B-92E8-362DD2E58D9E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1919985$48532792-CA0B-48C9-869D-2056A260188C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1919985$64052634-2B1F-409D-9AF8-A840DE65AF2B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c3b97f9c45d94d9ae465870c432cfcf9f54fefd8","datavalue":{"value":"910393","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1919985$2B5CDD1C-25AC-43A7-BD58-7DB2C1A5AC02","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"073048bef0819f3997d1457802bd9cc0746d3bd8","datavalue":{"value":"classical combinator","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$FCA72D23-B9A2-4AC5-99C5-A2E15A719A57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f64a23878402d21a7bc9c32da5b44608ab265b60","datavalue":{"value":"Peirce's law","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$CBE83F81-C99D-4514-B86D-870962261D1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2377b88a696371844cdb9dc79202e137415d896f","datavalue":{"value":"Curry-Howard isomorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$05AF14C1-1FA5-4CFD-9401-2C69283C8EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b62da7a56d211a3218610242fbc3081bae81610","datavalue":{"value":"proofs of classical implicational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$28274166-E865-488A-B96D-8D1CDCA922A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff79e803a1c5d08a94972a742953580846010d37","datavalue":{"value":"reduction rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$E2B4DE00-89B4-42C6-BACD-59E64344B898","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fcab9163f53d6e5a171b7b1c65e7d87f375401bc","datavalue":{"value":"proof reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$79509F4B-283A-4679-9CE9-8129DD7A4F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5263ef9f2085aab5a422247e6ec140dd66cbd7d9","datavalue":{"value":"combinatory logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$84C41329-AA0E-479D-ADA9-524FEC6D0251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4cfb8b6ba53ca6517720ca34e0bb33f261210259","datavalue":{"value":"weak normalization theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$4E8A6946-6024-4FFE-80D0-7389215CDCC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1919985$088D8F65-C1D3-4E25-B80A-840A48FB8E13","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":"Q1919985$EA90F5CC-1F67-4909-9B77-74EB18F159C4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$E422A039-78E6-48C6-9986-A78FC5D6C264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85d93ce51131096c8017b69c28438b91e3869e1b","datavalue":{"value":{"entity-type":"item","numeric-id":1919985,"id":"Q1919985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$3CB32FBD-DF7D-4A49-8B54-205DB36CBC61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d82b227295c10b6c3c9289b01dc8016d6c611441","datavalue":{"value":{"entity-type":"item","numeric-id":3727946,"id":"Q3727946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$935BD462-0139-4CD7-8C4B-625A7BC65237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$D41D6A8A-EA39-47CC-A8A2-BF35AA96B02E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ed6186f00d683b4c7cb7f70af7a03fd2b654c87","datavalue":{"value":{"entity-type":"item","numeric-id":5632554,"id":"Q5632554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1919985$4B1CB557-8528-439D-859F-0DF2B42BBDE0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a353884fcbb18bbc91d8b1ffea1bd012a5d5a7b","datavalue":{"value":{"entity-type":"item","numeric-id":2625364,"id":"Q2625364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d78bbc163bddb925f63727103f7b2de5170abab6","datavalue":{"value":{"amount":"+0.83549994","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":"Q1919985$66D4F502-5B63-48E9-9A7D-D7A5B09C8A04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ae6a9a5d1dc214bf54cc314afd3704368b5e51a","datavalue":{"value":{"entity-type":"item","numeric-id":2640975,"id":"Q2640975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d45566c41dd272cbb2ed5f1a445ed227e01c9e3","datavalue":{"value":{"amount":"+0.83438206","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":"Q1919985$2797302E-9EB6-4E68-9A83-4192F47CA9AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad724b2747a6bfa95429cbedb7abb587865ae12c","datavalue":{"value":{"entity-type":"item","numeric-id":2638532,"id":"Q2638532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30b4d99abe976a632ef151ecf8cf06a0ddd293b5","datavalue":{"value":{"amount":"+0.8262773","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":"Q1919985$94996CEC-9482-41C2-8007-55D778F71970","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e6fc6366c0c2b2e621d1db85f37747606df9abb","datavalue":{"value":{"entity-type":"item","numeric-id":3781102,"id":"Q3781102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81cf13b844c4a14e6756f46cf1b9a89a64991eae","datavalue":{"value":{"amount":"+0.8195348","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":"Q1919985$AB883D47-4413-40D9-9287-3B99B48EE275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"82dcd1f2685c178ffd19be00feff637aa5216fc7","datavalue":{"value":{"entity-type":"item","numeric-id":4316254,"id":"Q4316254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea338a4003206ef46518d54b4cbe4c77803bf6e9","datavalue":{"value":{"amount":"+0.8161025","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":"Q1919985$FB3D2678-E88D-4DCE-9ABA-490551A05435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"956eced5124153bfe57828fbdceaeb636c238545","datavalue":{"value":{"entity-type":"item","numeric-id":975276,"id":"Q975276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd1e937c3f9f18e65d72560a4d93274c0633cc9c","datavalue":{"value":{"amount":"+0.812801","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":"Q1919985$F79BC004-F2BA-485D-9B02-30F4E74488EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a93fb29fa5d72d66d91ea6d805e5fa0bc3052982","datavalue":{"value":{"entity-type":"item","numeric-id":5363179,"id":"Q5363179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ea5d3b3faa305c5d546e19f1cddd7681f1c97cd","datavalue":{"value":{"amount":"+0.80852365","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":"Q1919985$028086E3-DD59-45D8-9B4F-EC87E2710EE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72e9f2468e8443cf882d018f09e53bf205886246","datavalue":{"value":{"entity-type":"item","numeric-id":2959884,"id":"Q2959884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2ea2162da89a3417d1396f9b45c9ffcd9a5042e","datavalue":{"value":{"amount":"+0.80653936","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":"Q1919985$53AA9370-99A2-4071-BBB8-7A406BC2085B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"402c615b4a0ee861adc739e716a54ef1fac09f65","datavalue":{"value":{"entity-type":"item","numeric-id":2426436,"id":"Q2426436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"158287cddcb48f1fb8fcf729b436a87dd02bf6c5","datavalue":{"value":{"amount":"+0.8045908","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":"Q1919985$DFD190D8-42D0-4C2A-B56C-3AD16D7D45A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25788e26770ef016fadb0bd53f68d1baf687212a","datavalue":{"value":{"entity-type":"item","numeric-id":534185,"id":"Q534185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"445de4eda8f92f3da47f66fe016123ce5f2fbced","datavalue":{"value":{"amount":"+0.8022998","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":"Q1919985$88B57FC2-C5CC-48BF-A674-8B6623615BCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1919985","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1919985"}}}}}