{"entities":{"Q987936":{"pageid":989784,"ns":120,"title":"Item:Q987936","lastrevid":65817696,"modified":"2026-04-12T05:34:56Z","type":"item","id":"Q987936","labels":{"en":{"language":"en","value":"Ramsey's theorem for pairs and provably recursive functions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5778809"}},"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":"Q987936$CDB622BF-19EF-4D6D-8968-110A086E0C2E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8ee281c0e168ad405b8d5c650508510b5817d4ed","datavalue":{"value":{"text":"Ramsey's theorem for pairs and provably recursive functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q987936$B7E4A1AC-BDF2-4A63-BBB2-15C089836FF2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"993a0e4ce3557988c2a14f6d6f3164d4b7e87857","datavalue":{"value":"1221.03059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$A9E93065-FE43-4FB2-9C11-C64CD0417B5D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ff191a668f19f87355ea36e094b2f4104c83684c","datavalue":{"value":"10.1215/00294527-2009-019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$5928F149-4CE2-48F9-A218-128376D305D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3757c450e8ea3891f056e58fdb032b2670ff909f","datavalue":{"value":{"entity-type":"item","numeric-id":175049,"id":"Q175049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q987936$6375955F-8C94-43E6-B970-C4353F011750","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"71b151c9da44809f650995a7f88ca4d5f5807da4","datavalue":{"value":{"entity-type":"item","numeric-id":365681,"id":"Q365681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q987936$0404C238-7493-4951-B9D3-FC493040638A","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":"Q987936$9D012C5F-1CDB-436F-A40E-4EB5BEE352B4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d9c8db179f9c66121cffb2b883a8a32d7415ee58","datavalue":{"value":{"time":"+2010-09-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q987936$A0315C67-C7C6-4A7B-B640-FAB400B6640C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d7c555c6093954eb7bc72c496d2024b560cb7935","datavalue":{"value":"The paper under review adresses the strength of \\textit{F. P. Ramsey}'s theorem for pairs [Proc. Lond. Math. Soc. (2) 30, 264--286 (1929; JFM 55.0032.04)] over a weak base theory applying methods of `proof mining'.   The authors work in a weak base theory \\({\\mathcal T}\\), based on fragments E-G\\(_n\\)A\\(^\\omega\\) of extensional arithmetic in the language of functionals of all finite types, introduced by the second author [Arch. Math. Logic 36, No.~1, 31--71 (1996; Zbl 0882.03050)]. Thus, \\({\\mathcal T}\\) is obtained by considering the union E-G\\(_\\infty\\)A\\(^\\omega\\) of these systems and adding QF-AC (quantifier-free axiom of choice from functions to numbers and from numbers to functions) as well as WKL (weak K\u00f6nig's Lemma).  For \\(n\\geq 1\\), let RT\\(_n^2\\) denote Ramsey's theorem for \\(n\\)-colorings of \\([{\\mathbb N}]^2\\) and, given an \\(n\\)-coloring \\(c:[{\\mathbb N}]^2\\to \\{0,1,\\ldots,n-1\\}\\), let RT\\(_n^2(c)\\) be the statement expressing the fact that Ramsey's theorem holds for \\(c\\).  The main technical result of the paper establishes that over \\({\\mathcal T}\\) one can prove RT\\(_n^2(c)\\) from a suitable instance \\(\\Pi_0^1\\text{-CA}(\\tilde{\\varphi}(c))\\) of \\(\\Pi_0^1\\)-comprehension. The authors obtain this result by a logical analysis of the proof of Ramsey's theorem for pairs due to Erd\u0151s and Rado.  Combining this with previous results of \\textit{U. Kohlenbach} [Ann. Pure Appl. Logic 95, No. 1--3, 257--285 (1998; Zbl 0945.03088)] on the arithmetical content of restricted forms of comprehension and choice, the authors obtain the second main result of the paper:  If  \\[ {\\mathcal T}\\vdash \\forall f\\in{\\mathbb N}^{\\mathbb N} (\\Pi_0^1\\text{-CA}(\\varphi(f))\\wedge \\forall k\\in{\\mathbb N} (\\text{RT}_2^2(\\psi(f,k)))\\to \\exists n\\in{\\mathbb N} A_{qf}(f,n)), \\]  where \\(\\varphi\\), \\(\\psi\\) are closed terms of \\({\\mathcal T}\\) of suitable types, then there exists a primitive recursive (in the sense of Kleene) functional \\(\\Phi\\) such that  \\[ \\widehat{\\text{E-PA}}^\\omega\\!\\!\\!\\upharpoonright \\,\\,\\vdash \\,\\, \\forall f\\in{\\mathbb N}^{\\mathbb N} A_{qf}(f,\\Phi(f)). \\]  Moreover, the proof-theoretic method provides an extraction algorithm for \\(\\Phi\\) from a given proof.","type":"string"},"datatype":"string"},"type":"statement","id":"Q987936$B28EBDC5-D0A9-4FFA-9837-16722BEFD7F7","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"62b70b9796d45b1d2ff767f1b609c223d300570a","datavalue":{"value":{"entity-type":"item","numeric-id":590977,"id":"Q590977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q987936$5AF0A603-1C39-4990-877A-878B0ACD0251","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$25F68F60-4784-4791-BFF0-007755DC8FEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$09AD1A2B-63B7-406F-A9E8-9F22E4EA0900","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b4b251e34f965e85a4a30c5d646e0bae1192967","datavalue":{"value":"05D10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$FF7C6654-13CF-464E-85C3-E2E4D97E9AA0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c477e0af81debbebf48186ebf2e18c45d8eb6638","datavalue":{"value":"5778809","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$0DB57727-C1FF-408B-A434-C72C41815593","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21fed8963868ebc415fe6777e2aeb4de8e8a0e26","datavalue":{"value":"Ramsey's theorem for pairs","type":"string"},"datatype":"string"},"type":"statement","id":"Q987936$AB30E422-29E3-472C-BEF6-39785EB49BD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"425e268df6c5cb5624c84c71ce4739194b7f0d90","datavalue":{"value":"provably recursive functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q987936$97FE85A4-3025-4889-952E-553306D8CF9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7c23305d5a301c23057fddc53953635a4398a76","datavalue":{"value":"proof mining","type":"string"},"datatype":"string"},"type":"statement","id":"Q987936$E809ED25-F8AC-410A-B3C1-96030C357575","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":"Q987936$0DE85DA0-2863-4187-8251-91EE3E101CEE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"788840776b81df11cd10f7cb2ae7a6eb6d99d13b","datavalue":{"value":"https://doi.org/10.1215/00294527-2009-019","type":"string"},"datatype":"url"},"type":"statement","id":"Q987936$5BCC6D3F-39A3-4987-9D46-057F7A704E54","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e196f79e0725709fbf073b19c4ea891fd245366b","datavalue":{"value":"W2130233653","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q987936$44A7A92F-9301-4B91-95F8-A9AFC46E2FBA","rank":"normal"}],"P1643":[{"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":"5ae757f03375232c78be76df2772510d39e2a3a8","datavalue":{"value":{"amount":"+0.7562475","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$E380D41B-9D48-4B2D-AB51-167741B16044","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb4cad0292f73c50bff1f9a51494a0119ad7eaf1","datavalue":{"value":{"entity-type":"item","numeric-id":2898881,"id":"Q2898881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee42084d0ae1bc83d6e7e35f975f95bdaa7e756a","datavalue":{"value":{"amount":"+0.7301227","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$1FECEE25-B9FA-47CC-A1C1-35B3AF9FE9FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6c7b588e9e63c7de65c54b22daee5fd4cbd1d18","datavalue":{"value":{"entity-type":"item","numeric-id":507201,"id":"Q507201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64873fd019ddc4bb1c9374bc82c980a4e80614a7","datavalue":{"value":{"amount":"+0.698944","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$2CA120E0-2744-40F5-86E5-8236431B0FDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa0ea4e0b221e05043dda4c7acf0f9b659539b91","datavalue":{"value":{"entity-type":"item","numeric-id":3190948,"id":"Q3190948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fa98a72ca27f20e21cae294144cb3759e0dd269","datavalue":{"value":{"amount":"+0.6952672","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$B1B8656F-281C-42D8-89F7-61C681BEA2DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea210ee7c00a41c9154bb273eff1706ba0fc2d1f","datavalue":{"value":{"entity-type":"item","numeric-id":4915224,"id":"Q4915224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dbd5c08c841b3d5d96f37e81576fd60ef9c28a7","datavalue":{"value":{"amount":"+0.69343567","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$4530F072-287C-47CF-9E5B-A487EA25772D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12cd2d9b2abd0686998793010b04c658af22212b","datavalue":{"value":{"entity-type":"item","numeric-id":4977228,"id":"Q4977228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40b923184f3cacd20fc0e9e148c2c6b13dc9b876","datavalue":{"value":{"amount":"+0.6907838","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$3EA7B32D-5DF2-43F3-9F2C-74BA8295B360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ef81f647cf3e81eb4ac7f88c43eef7f20ee866f","datavalue":{"value":{"entity-type":"item","numeric-id":2968410,"id":"Q2968410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70dec4e53320575d8f704ca5caf14c2fa89aa54f","datavalue":{"value":{"amount":"+0.6836526","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$CCBD4293-01DA-4D52-AB7B-662F69C3EB8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28468bc65ee7ad3c62c861af26915cd2ef7b90b7","datavalue":{"value":{"entity-type":"item","numeric-id":2401697,"id":"Q2401697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"576b13f2481a89dad4f891e37189e473cd04bbdf","datavalue":{"value":{"amount":"+0.6754662","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$259FBA4C-C775-443C-B4B7-78E323AF2B56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39b73d3d0ca97dd10dce841825c231f7475b8844","datavalue":{"value":{"entity-type":"item","numeric-id":2732267,"id":"Q2732267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"edd36397a0c9c9a74c277c87d86921fcffa3c3f8","datavalue":{"value":{"amount":"+0.67502016","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$5218562A-201E-487C-A53F-C024EF6F6EB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f1aa137ed58605d23c57ae58f6c2b1771bc3fa6","datavalue":{"value":{"entity-type":"item","numeric-id":2915896,"id":"Q2915896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a75445b88a84a432bfb165639cac6faa1b2364e0","datavalue":{"value":{"amount":"+0.6715585","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q987936$ACCE5FB6-23B9-4B52-AB18-567A876E8BBD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Ramsey's theorem for pairs and provably recursive functions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Ramsey%27s_theorem_for_pairs_and_provably_recursive_functions"}}}}}