{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T08:40:30Z","timestamp":1693557630923},"reference-count":16,"publisher":"Wiley","issue":"4-5","license":[{"start":{"date-parts":[[2012,7,18]],"date-time":"2012-07-18T00:00:00Z","timestamp":1342569600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that Spector's \u201crestricted\u201d form of bar recursion is sufficient (over system <jats:italic>T<\/jats:italic>) to define Spector's search functional. This new result is then used to show that Spector's restricted form of bar recursion is in fact as general as the supposedly more general form of bar recursion. Given that these two forms of bar recursion correspond to the (explicitly controlled) iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is <jats:italic>T<\/jats:italic>\u2010equivalent to the corresponding iterated product of quantifiers.<\/jats:p>","DOI":"10.1002\/malq.201100106","type":"journal-article","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T05:31:42Z","timestamp":1342675902000},"page":"356-265","source":"Crossref","is-referenced-by-count":10,"title":["On Spector's bar recursion"],"prefix":"10.1002","volume":"58","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":"311","published-online":{"date-parts":[[2012,7,18]]},"reference":[{"key":"e_1_2_9_2_1","first-page":"337","volume-title":"Studies in Logic and the Foundations of Mathematics Vol. 137","author":"Avigad J.","year":"1998"},{"key":"e_1_2_9_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274319"},{"key":"e_1_2_9_4_1","unstructured":"M. H.Escard\u00f3andP.Oliva Computational interpretations of analysis via products of selection functions in: Programs Proofs Processes 6th Conference on Computability in Europe CiE 2010 Ponta Delgada Azores Portugal June 30\u2013July 4 2010 Proceedings edited by F. Ferreira B. L\u00f6we E. Mayordomo and L. M. Gomes Lecture Notes in Computer Science Vol. 6158 (Springer 2010) pp.141\u2013150."},{"key":"e_1_2_9_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990351"},{"key":"e_1_2_9_6_1","doi-asserted-by":"crossref","unstructured":"M. H.Escard\u00f3andP.Oliva Computational interpretations of analysis via products of selection functions submitted for publication(2011).","DOI":"10.1007\/978-3-642-13962-8_16"},{"key":"e_1_2_9_7_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2010.0471"},{"key":"e_1_2_9_8_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"e_1_2_9_9_1","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard W. A.","year":"1968","journal-title":"Compositio Math."},{"key":"e_1_2_9_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273252"},{"key":"e_1_2_9_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586791"},{"key":"e_1_2_9_12_1","volume-title":"Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Monographs in Mathematics","author":"Kohlenbach U.","year":"2008"},{"key":"e_1_2_9_13_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0060871","volume-title":"Extensional G\u00f6del Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics Vol. 306","author":"Luckhardt H.","year":"1973"},{"key":"e_1_2_9_14_1","first-page":"123","article-title":"A model for bar recursion of higher types","volume":"23","author":"Scarpellini B.","year":"1971","journal-title":"Compos. Math."},{"key":"e_1_2_9_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273126"},{"key":"e_1_2_9_16_1","doi-asserted-by":"crossref","unstructured":"C.Spector Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics in: Recursive function theory Proceedings of the Fifth Symposium in Pure Mathematics of the American Mathematical Society held in New York April 6\u20137 1961 edited by F. D. E. Dekker Proceedings of Symposia in Pure Mathematics Vol. 5 (American Mathematical Society Providence R.I.) pp.1\u201327","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"e_1_2_9_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.201100106","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.201100106","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.201100106","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T03:39:09Z","timestamp":1693453149000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.201100106"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,18]]},"references-count":16,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1002\/malq.201100106"],"URL":"https:\/\/doi.org\/10.1002\/malq.201100106","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,18]]}}}