{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T12:27:39Z","timestamp":1693398459072},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":17816,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1965,6]]},"abstract":"<jats:p>This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in \u00a72. The additional rules have the form of definition by transfinite recursion up to some ordinal \u03be (where \u03be is represented by a primitive recursive (p.r.) ordering). In \u00a73 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to \u03be. Let <jats:italic>R<\/jats:italic><jats:sub>\u03be<\/jats:sub> denote (temporarily) the system with recursion up to \u03be. The main results of this paper are of two sorts:<\/jats:p><jats:p>Sections 5\u20137 are concerned with less elementary closure properties of the systems <jats:italic>R<\/jats:italic><jats:sub>\u03be<\/jats:sub>. Namely, we show that certain classes of functional equations in <jats:italic>R<\/jats:italic><jats:sub>\u03b7<\/jats:sub> can be solved in <jats:italic>R<\/jats:italic><jats:sub>\u03b7<\/jats:sub> for some explicitly determined \u03b7 &lt; \u03b5(\u03b7) (the least \u03b5-number &gt; \u03be). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional <jats:italic>F<\/jats:italic>, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.<\/jats:p>","DOI":"10.2307\/2270132","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T16:28:25Z","timestamp":1146932905000},"page":"155-174","source":"Crossref","is-referenced-by-count":25,"title":["Functionals defined by transfinite recursion"],"prefix":"10.1017","volume":"30","author":[{"given":"W. W.","family":"Tait","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200056607_ref005","first-page":"385","volume":"25","author":"Kreisel","year":"1960","journal-title":"Induction and recursion"},{"key":"S0022481200056607_ref006","first-page":"412","article-title":"Some generalizations of the notion of well-ordering","volume":"9","author":"Parikh","year":"1962","journal-title":"Notices of the American Mathematical Society"},{"key":"S0022481200056607_ref004","first-page":"322","volume":"24","author":"Kreisel","year":"1959","journal-title":"Proof by transfinite induction and definition by transfinite recursion in quantifier-free systems"},{"key":"S0022481200056607_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF01342980"},{"key":"S0022481200056607_ref010","volume-title":"Grundlagen der Mathematik","volume":"II","author":"Hilbert","year":"1939"},{"key":"S0022481200056607_ref003","first-page":"1","article-title":"Recursive functionals and quantifiers of finite types I","volume":"91","author":"Kleene","year":"1959","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0022481200056607_ref001","volume-title":"Recursive number theory","author":"Goodstein","year":"1957"},{"key":"S0022481200056607_ref002","first-page":"339","article-title":"Hierarchies of recursive arithmetics","volume":"9","author":"Guard","year":"1962","journal-title":"Notices of the American Mathematical Society"},{"key":"S0022481200056607_ref008","first-page":"175","volume":"30","author":"Tait","year":"1965","journal-title":"The substitution method"},{"key":"S0022481200056607_ref009","unstructured":"Tait W. W. , The no-counterexample interpretation. To appear."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200056607","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T15:41:07Z","timestamp":1559576467000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200056607\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1965,6]]},"references-count":10,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1965,6]]}},"alternative-id":["S0022481200056607"],"URL":"https:\/\/doi.org\/10.2307\/2270132","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1965,6]]}}}