{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:55:27Z","timestamp":1759146927069},"reference-count":12,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":12611,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1979,9]]},"abstract":"<jats:p>For general information on bar recursion the reader should consult the papers of Spector [8], where it was introduced, Howard [2] and Tait [11]. In this note we shall prove that the terms of G\u00f6del's theory <jats:italic>T<\/jats:italic>(in its extensional version of Spector [8]) are closed under the rule BR<jats:sub>0,1<\/jats:sub> of bar recursion of types 0 and 1. Our method of proof is based on the notion of an infinite term introduced by Tait [9]. The main tools of the proof are (i) the normalization theorem for (notations for) infinite terms and (ii) valuation functionals. Both are elaborated in [6]; for brevity some familiarity with this paper is assumed here. Using (i) and (ii) we reduce BR<jats:sub>0,1<\/jats:sub> to \u03be-recursion with \u03be &lt; \u03b5<jats:sub>0<\/jats:sub>. From this the result follows by work of Tait [10], who gave a reduction of 2<jats:sup>\u03be<\/jats:sup>-recursion to \u03be-recursion at a higher type. At the end of the paper we discuss a perhaps more natural variant of bar recursion introduced by Kreisel in [4].<\/jats:p><jats:p>Related results are due to Kreisel (in his appendix to [8]), who obtains results which imply, using the reduction given by Howard [2] of the constant of bar recursion of type \u03c4 to the rule of bar recursion of type (0 \u2192 \u03c4) \u2192 \u03c4, that <jats:italic>T<\/jats:italic> is not closed under the rule of bar recursion of a type of level \u2265 2, to Diller [1], who gave a reduction of BR<jats:sub>0,1<\/jats:sub> to \u03be-recursion with \u03be bounded by the least \u03c9-critical number, and to Howard [3], who gave an ordinal analysis of the constant of bar recursion of type 0. I am grateful to H. Barendregt, W. Howard and G. Kreisel for many useful comments and discussions.<\/jats:p>","DOI":"10.2307\/2273126","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:50:56Z","timestamp":1146952256000},"page":"325-329","source":"Crossref","is-referenced-by-count":11,"title":["On bar recursion of types 0 and 1"],"prefix":"10.1017","volume":"44","author":[{"given":"Helmut","family":"Schwichtenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200048258_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71689-6"},{"key":"S0022481200048258_ref004","article-title":"The model G of the theory BR","volume":"312","author":"Kreisel","year":"1976","journal-title":"Zentralblatt f\u00fcr Mathematik und ihre Grenzgebiete"},{"key":"S0022481200048258_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0022481200048258_ref003","unstructured":"Howard W. A. , Ordinal analysis of bar recursion of type zero, 1970 (unpublished)."},{"key":"S0022481200048258_ref005","volume-title":"Einige Anwendungen von unendlichen Termen und Werifunktionalen","author":"Schwichtenberg","year":"1973"},{"key":"S0022481200048258_ref006","first-page":"279","volume-title":"Logic Colloquium '73","author":"Schwichtenberg","year":"1975"},{"key":"S0022481200048258_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"S0022481200048258_ref008","first-page":"1","volume-title":"Recursive function theory","author":"Spector","year":"1962"},{"key":"S0022481200048258_ref010","first-page":"185","volume-title":"Logic, methodology and the philosophy of science. III","author":"Tait","year":"1976"},{"key":"S0022481200048258_ref011","first-page":"352","volume-title":"Proceeding of the Second Scandinavian Logic Symposium","author":"Tait","year":"1971"},{"key":"S0022481200048258_ref001","volume-title":"Zur Theorie rekursiver Funktionale h\u00f6herer Typen","author":"Diller","year":"1968"},{"key":"S0022481200048258_ref002","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard","year":"1968","journal-title":"Compositio Mathematica"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200048258","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T20:52:37Z","timestamp":1558903957000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200048258\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,9]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1979,9]]}},"alternative-id":["S0022481200048258"],"URL":"https:\/\/doi.org\/10.2307\/2273126","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1979,9]]}}}