{"entities":{"Q2274133":{"pageid":2284876,"ns":120,"title":"Item:Q2274133","lastrevid":57823710,"modified":"2026-04-02T16:44:56Z","type":"item","id":"Q2274133","labels":{"en":{"language":"en","value":"Using Ramsey's theorem once"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7107332"}},"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":"Q2274133$3ED90EEE-A5EB-472A-99F9-AC2C31C51A91","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c21423dfb5f451f1b3f8c65dd95505900b3bf947","datavalue":{"value":{"text":"Using Ramsey's theorem once","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2274133$980DAA9E-1083-4BD6-97A4-DD2491ABF180","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6dda2555c9f967c651d98dc5acb405dd8a0b8529","datavalue":{"value":"1475.03071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$B8A1C963-DBAC-49D5-9637-73EA9D4410EC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"aa6fe6778469ced17e25612a269bf91190d4e60c","datavalue":{"value":{"entity-type":"item","numeric-id":375888,"id":"Q375888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$7B54865B-FC7C-4449-8A24-1B6480E71AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5122a321cfb515186c4448a4fbfba8604b1bf26","datavalue":{"value":{"entity-type":"item","numeric-id":335001,"id":"Q335001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$E0B9959A-EE27-4064-BA6B-4370E13EC189","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$80255BC9-EC39-48FF-BBAC-33AD4931BE06","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"47982c139c41a713484decefc5a5dde8b3533371","datavalue":{"value":{"time":"+2019-09-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2274133$01ECFD31-508A-43DD-A6A9-95A9B16025AD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f8f975c69cb005272070c609d12e63fa4ed445cb","datavalue":{"value":"https://arxiv.org/abs/1611.03134","type":"string"},"datatype":"url"},"type":"statement","id":"Q2274133$68500DCC-E745-4369-9694-CAEF6D758185","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8448074eee01af32f589414e093645868ef5789e","datavalue":{"value":"The paper studies the question of how many applications of one principle are needed to prove another in the context of higher-order reverse mathematics, and its connections to Weihrauch reducibility. The base theory is taken to be \\(i\\mathsf{RCA}^\\omega_0\\), consisting of Feferman's system \\(\\widehat{\\mathsf{E\\text-HA}}^\\omega_\\restriction\\) of intuitionistic arithmetic of all finite types and the quantifier-free choice schema \\(\\mathsf{QF\\text-AC}^{1,0}\\); the extension of this theory to classical logic is the theory \\(\\mathsf{RCA}^\\omega_0\\) of \\textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)].  Considering problems \\(P\\) of the form \\(\\forall x\\,(p_1(x)\\to\\exists y\\,p_2(x,y))\\), the authors define a natural notion that a theory \\(T\\supseteq i\\mathsf{RCA}^\\omega_0\\) proves a problem \\(Q\\) with ``one typical use'' of \\(P\\). They also consider a formal version \\(T\\vdash Q\\le_WP\\) of Weihrauch reducibility between such problems (which differs from actual Weihrauch reducibility \\(Q\\le_WP\\) in that the reduction functionals are not a priori required to be computable).  The main general results are that under suitable syntactic restrictions on \\(P\\) and \\(Q\\), \\(i\\mathsf{RCA}^\\omega_0\\) proves \\(Q\\) with one typical use of \\(P\\) iff \\(i\\mathsf{RCA}^\\omega_0\\vdash Q\\le_WP\\), and that this implies \\(Q\\le_WP\\).  As an application, the paper looks on dependencies between the Ramsey principles \\(\\mathsf{RT}(n,k)\\), asserting that any \\(k\\)-colouring of \\([\\mathbb N]^n\\) has an infinite monochromatic set. They show that even though \\(i\\mathsf{RCA}^\\omega_0\\vdash\\mathsf{RT}(2,2)\\to\\mathsf{RT}(2,4)\\), \\(i\\mathsf{RCA}^\\omega_0\\) cannot prove \\(\\mathsf{RT}(2,4)\\) with only one typical use of \\(\\mathsf{RT}(2,2)\\), using known results on Weihrauch reducibility between these problems. More generally, for any \\(n\\ge1\\) and \\(k>j\\ge2\\), \\(i\\mathsf{RCA}^\\omega_0\\) does not prove \\(\\mathsf{RT}(n,k)\\) with only one typical use of \\(\\mathsf{RT}(n,j)\\).  Surprisingly, the classical theory \\(\\mathsf{RCA}^\\omega_0\\) \\textit{does} prove \\(\\mathsf{RT}(2,4)\\) with one typical use of \\(\\mathsf{RT}(2,2)\\): the authors show this by a clever use of excluded middle to distinguish whether there exists an infinite bichromatic set or not. More generally, \\(\\mathsf{RCA}^\\omega_0\\) proves \\(\\mathsf{RT}(n,k)\\) with one typical use of \\(\\mathsf{RT}(n,2)\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$D4606479-13E3-43A8-BEFB-CCFB9B46554E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$08EBCB0D-10DB-4F34-8167-ECD3D79258C0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"13841f0b96793f178ce9a7dcac9f232220625aee","datavalue":{"value":"03B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$F3524682-CA5F-4F2E-AF3F-0040B5FE03D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$4220EDCF-F60C-4774-9342-45DD374C5F1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$7E92842F-C702-409B-AA6D-2EF1FFB6A2DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"379be2ae88ac653823960287ba517e23fc9265f4","datavalue":{"value":"03D30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$3878B3F4-F0DA-4600-B624-CD8368E64370","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d3e255ccb65d7c7f2778d3574f468847545a8473","datavalue":{"value":"7107332","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$C1BFA226-3868-41F6-9B19-1736BEAE35F3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"546f982464ca9e4d7b2d83e5ae55c43306696e3a","datavalue":{"value":"Ramsey's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$E9E62826-B9FE-4E29-A9D2-07C629260A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb19bc887fc5c555d3d129dbb5591935a8f26af7","datavalue":{"value":"Weihrauch reducibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$D2E8DDCD-0EFE-4C98-A7B0-B10BB7850ABE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da09a67431e25e2ec02a9e9c71a249567b978ee0","datavalue":{"value":"uniform reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$FA0DFB01-6476-4EB4-823F-383A960076F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf0a0d929b9a02ed4dea0e9db58247a82b31736d","datavalue":{"value":"higher-order reverse mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$3470AF04-8E11-4B30-A412-6AF74B9FB184","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7c23305d5a301c23057fddc53953635a4398a76","datavalue":{"value":"proof mining","type":"string"},"datatype":"string"},"type":"statement","id":"Q2274133$A2711CD1-6C9B-41AA-B8C6-5BA732451959","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":"Q2274133$8F87D096-8582-46B8-BD52-9DEEC793C7FA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"db8c7c25ae750d8089b4e1b2de28c8f0a7094965","datavalue":{"value":"W2963469697","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$199CF50F-DFC7-4AF0-A569-13699E278DDF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1059ccd1a53029f0e8e04e996afb9ac67390f9c5","datavalue":{"value":{"entity-type":"item","numeric-id":3083466,"id":"Q3083466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$065D2B6A-ACB5-4073-AC1D-568BA7A23A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c833b542e9fb8bb3e367cbaa0347635e2d40b13c","datavalue":{"value":{"entity-type":"item","numeric-id":4600456,"id":"Q4600456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$1F565233-96A0-45F3-8442-ED76B836EB60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79d410c9bfc2cb2ec49057149c42c8ee51c20366","datavalue":{"value":{"entity-type":"item","numeric-id":2443117,"id":"Q2443117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$FA8310D1-017D-4489-99DB-AC91EF6DADC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ad30dcf51cc217162bdb5a03b006ed2d9c1e1c0","datavalue":{"value":{"entity-type":"item","numeric-id":2796522,"id":"Q2796522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$39CD0E49-A102-4D33-ACBE-96647A9CC51D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c37ae4ea7122cb7fa2c62942e3cb2b4db3687ccc","datavalue":{"value":{"entity-type":"item","numeric-id":3186057,"id":"Q3186057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$0A17397F-CCAC-4690-9E4C-43CA7A3F1D56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ae890d102328ee8a14a47f99cbedb8b8afc8a34","datavalue":{"value":{"entity-type":"item","numeric-id":540402,"id":"Q540402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$A74B3D68-2106-4411-BEBF-CA8387418C38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$98C9789E-C23B-48B0-8B43-564413EE0334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"372ac7410c3602549aaffbccc69cf9a80d4b9494","datavalue":{"value":{"entity-type":"item","numeric-id":5711891,"id":"Q5711891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$AC6410C6-B700-484E-8139-E0C70B5D6C52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e73cbdc4f532ed72bacdc9e85f4929b162897095","datavalue":{"value":{"entity-type":"item","numeric-id":5450521,"id":"Q5450521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$D861265D-7412-4F7F-B83F-2341F1049A5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1de29eed033479d0e6af0494b3e99f1851f05f2c","datavalue":{"value":{"entity-type":"item","numeric-id":4600462,"id":"Q4600462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$CA15853F-ACF2-4CB3-B9C8-31CC7864FD79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86a2154fb3ad41c80120b50bf3a939097ea843c7","datavalue":{"value":{"entity-type":"item","numeric-id":503277,"id":"Q503277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$04FCA397-8341-4D84-BE01-394F0CD0FBFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0430e4a9fe16a78c945c278746cad2959afea463","datavalue":{"value":{"entity-type":"item","numeric-id":3395521,"id":"Q3395521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$AB8704C7-AAD4-4B10-BC52-7362B024455E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$02F892B6-DD1B-4369-9DF1-E959A4BC13BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec227ec1221c88cb71bf97806a014560adb97452","datavalue":{"value":{"entity-type":"item","numeric-id":5000259,"id":"Q5000259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2274133$3192E02E-1FDB-4C7E-AB8F-581BDF6F1452","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"858d75581c698f36b8e8c749f094c12fc712d690","datavalue":{"value":"Q128344496","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$2B875A01-A8D0-473D-B939-49FF7FCDFB83","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6010fccd503b9e32c7d73fb8f9db08b236a98b6d","datavalue":{"value":"10.1007/S00153-019-00664-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2274133$C76DC546-BB7B-4DA2-9273-E34AED27251E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59f072dcc93454753bc9f43ca36a2eacb0dcd52a","datavalue":{"value":{"entity-type":"item","numeric-id":3353014,"id":"Q3353014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11de618b4a320c2e6dfc67cdd6851adff5e7bc05","datavalue":{"value":{"amount":"+0.7997060418128967","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":"Q2274133$3CB45A0F-BA74-40EF-B6B7-C50B75E70000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0746ab003dd15d8fa557f36c9e19fbcfc9064d59","datavalue":{"value":{"entity-type":"item","numeric-id":5004961,"id":"Q5004961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a6327a950141f3a475a77c5245618037a1079e2","datavalue":{"value":{"amount":"+0.7990016341209412","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":"Q2274133$AD8FFEF7-1D9B-4326-9EAB-F618DF1CE291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da304cc127955d6011df962755fbdb986fa89afd","datavalue":{"value":{"entity-type":"item","numeric-id":1644984,"id":"Q1644984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d8555a82e2349d291321244d9351a9ae894b7ba","datavalue":{"value":{"amount":"+0.7941226363182068","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":"Q2274133$FBEBF5E4-6ECE-4C3A-B00D-9093399A9362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"956b97ae9bd786765e9ca0896991f9818b597f0c","datavalue":{"value":{"entity-type":"item","numeric-id":1913632,"id":"Q1913632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c33552e12efadc5840a79a7094ff6d215515c422","datavalue":{"value":{"amount":"+0.7893096804618835","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":"Q2274133$17B64E22-D4C4-4DC6-A1A7-83D31B9788B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17e334cdd2ba4d78b331e520cfd4cbd8e7c4b72a","datavalue":{"value":{"entity-type":"item","numeric-id":987936,"id":"Q987936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbb0418c5ee688f773b1df3bea241fa6aae4cfab","datavalue":{"value":{"amount":"+0.7752231955528259","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":"Q2274133$7733B5F2-F3E4-4B0B-931F-473DA9E59B15","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2274133","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2274133"}}}}}