{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T14:30:23Z","timestamp":1693837823349},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2014,11,13]],"date-time":"2014-11-13T00:00:00Z","timestamp":1415836800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,12]]},"abstract":"<jats:p>We use G\u00f6del's dialectica interpretation to produce a computational version of the well-known proof of Ramsey's theorem by Erd\u0151s and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.<\/jats:p>","DOI":"10.1017\/s0960129513000340","type":"journal-article","created":{"date-parts":[[2014,11,13]],"date-time":"2014-11-13T23:39:33Z","timestamp":1415921973000},"page":"1755-1778","source":"Crossref","is-referenced-by-count":6,"title":["A constructive interpretation of Ramsey's theorem via the product of selection functions"],"prefix":"10.1017","volume":"25","author":[{"given":"PAULO","family":"OLIVA","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"THOMAS","family":"POWELL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,13]]},"reference":[{"key":"S0960129513000340_ref10","unstructured":"Escard\u00f3 M. H. and Oliva P. (2012) Computing Nash equilibria of unbounded games. In: Proceedings of the Turing 100 Conference. Turing 100, Manchester."},{"key":"S0960129513000340_ref18","unstructured":"Oliva P. and Powell T. (2012) A game-theoretic computational interpretation of proofs in classical analysis. (Preprint available at arxiv.org\/abs\/1204.5244.)"},{"key":"S0960129513000340_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13962-8_16"},{"key":"S0960129513000340_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59971-2"},{"key":"S0960129513000340_ref3","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/106\/1057813"},{"key":"S0960129513000340_ref11","first-page":"233","article-title":"System T and the product of selection functions","volume":"12","author":"Escard\u00f3","year":"2011","journal-title":"Leibniz International Proceedings in Informatics"},{"key":"S0960129513000340_ref4","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1034"},{"key":"S0960129513000340_ref19","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"S0960129513000340_ref9","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2010.0471"},{"key":"S0960129513000340_ref23","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/s2-47.2.193"},{"key":"S0960129513000340_ref14","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1215\/00294527-2009-019","article-title":"Ramsey's theorem for pairs and provably recursive functions","volume":"50","author":"Kohlenbach","year":"2009","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S0960129513000340_ref12","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0960129513000340_ref15","first-page":"241","article-title":"On the interpretation of non-finitist proofs, part I","volume":"16","author":"Kreisel","year":"1951","journal-title":"Journal of Symbolic Logic"},{"key":"S0960129513000340_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"S0960129513000340_ref5","unstructured":"Coquand T. (1994b) A direct proof of Ramsey's theorem. Available at http:\/\/www.cse.chalmers.se\/~coquand\/ramsey2.pdf."},{"key":"S0960129513000340_ref17","unstructured":"Kreuzer A. (2009) Der Satz von Ramsey f\u00fcr Paare und beweisbar rekursive Funktionen, Diploma thesis, Technische Universit\u00e4t Darmstadt."},{"key":"S0960129513000340_ref6","volume-title":"Combinatorial Set Theory: Partition Relations for Cardinals","author":"Erd\u0151s","year":"1984"},{"key":"S0960129513000340_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.09.001"},{"key":"S0960129513000340_ref22","doi-asserted-by":"publisher","DOI":"10.1090\/mbk\/059"},{"key":"S0960129513000340_ref21","first-page":"1","volume-title":"Recursive Function Theory: Proceedings Symposia in Pure Mathematics","author":"Spector","year":"1962"},{"key":"S0960129513000340_ref13","volume-title":"Applied Proof Theory: Proof Interpretations and their Use in Mathematics","author":"Kohlenbach","year":"2008"},{"key":"S0960129513000340_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990351"},{"key":"S0960129513000340_ref16","doi-asserted-by":"publisher","DOI":"10.2307\/2267457"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T21:07:26Z","timestamp":1555708046000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000340\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,13]]},"references-count":23,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["S0960129513000340"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000340","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,13]]}}}