{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:53:28Z","timestamp":1712372008298},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T00:00:00Z","timestamp":1518393600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2018,3]]},"abstract":"Abstract<\/jats:title>In [12], Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector\u2019s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y<\/jats:italic> which controls the stopping condition of Spector\u2019s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg\u2019s original proof, however, relies on a detour through Tait\u2019s infinitary terms and the correspondence between ordinal recursion for $\\alpha < {\\varepsilon _0}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg\u2019s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y<\/jats:italic> is in the fragment Ti<\/jats:italic><\/jats:sub> then terms built from $BR^{\\mathbb{N},\\sigma } $<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> for this particular Y<\/jats:italic> are definable in the fragment ${T_{i + {\\rm{max}}\\left\\{ {1,{\\rm{level}}\\left( \\sigma \\right)} \\right\\} + 2}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1017\/jsl.2017.33","type":"journal-article","created":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T00:26:45Z","timestamp":1518395205000},"page":"70-83","source":"Crossref","is-referenced-by-count":5,"title":["A DIRECT PROOF OF SCHWICHTENBERG\u2019S BAR RECURSION CLOSURE THEOREM"],"prefix":"10.1017","volume":"83","author":[{"given":"PAULO","family":"OLIVA","sequence":"first","affiliation":[]},{"given":"SILVIA","family":"STEILA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,2,12]]},"reference":[{"key":"S0022481217000330_ref5","first-page":"105","article-title":"Ordinal analysis of bar recursion of type zero","volume":"42","author":"Howard","year":"1980","journal-title":"Compositio Mathematica"},{"key":"S0022481217000330_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71689-6"},{"key":"S0022481217000330_ref12","unstructured":"[12] Schwichtenberg H. , On bar recursion of types 0 and 1, this Journal, vol. 44 (1979), no. 3, pp. 325\u2013329."},{"key":"S0022481217000330_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"S0022481217000330_ref3","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0022481217000330_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exv058"},{"key":"S0022481217000330_ref7","unstructured":"[7] Kohlenbach U. , On the no-counterexample interpretation, this Journal, vol. 64 (1999), no. 4, pp. 1491\u20131511."},{"key":"S0022481217000330_ref8","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-1715716"},{"key":"S0022481217000330_ref10","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"S0022481217000330_ref4","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard","year":"1968","journal-title":"Compositio Mathematica"},{"key":"S0022481217000330_ref13","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"S0022481217000330_ref11","first-page":"279","volume-title":"Proceedings of the Logic Colloquium\u201973","volume":"80","author":"Schwichtenberg","year":"1975"},{"key":"S0022481217000330_ref2","volume-title":"Zur Theorie rekursiver Funktionale h\u00f6herer Typen","author":"Diller","year":"1968"},{"key":"S0022481217000330_ref6","unstructured":"[6] Howard W. A. , Ordinal analysis of simple cases of bar recursion, this Journal, vol. 46 (1981), no. 1, pp. 17\u201330."}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481217000330","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,15]],"date-time":"2019-04-15T18:56:59Z","timestamp":1555354619000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481217000330\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,12]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["S0022481217000330"],"URL":"https:\/\/doi.org\/10.1017\/jsl.2017.33","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,12]]}}}