{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:26Z","timestamp":1759147106437},"reference-count":36,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1562,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2009,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Extending G\u00f6del's <jats:italic>Dialectica<\/jats:italic> interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.<\/jats:p>","DOI":"10.2178\/jsl\/1254748682","type":"journal-article","created":{"date-parts":[[2009,10,5]],"date-time":"2009-10-05T13:05:40Z","timestamp":1254747940000},"page":"1100-1120","source":"Crossref","is-referenced-by-count":6,"title":["Functional interpretation and inductive definitions"],"prefix":"10.1017","volume":"74","author":[{"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henry","family":"Towsner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200003066_ref035","unstructured":"Troelstra A. S. , Introductory note to 1958 and 1972, In Feferman et al. [16], pp. 217\u2013241."},{"key":"S0022481200003066_ref036","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066745"},{"key":"S0022481200003066_ref028","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"S0022481200003066_ref033","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610038"},{"key":"S0022481200003066_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"},{"key":"S0022481200003066_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050167"},{"key":"S0022481200003066_ref007","doi-asserted-by":"crossref","unstructured":"Buchholz Wilfried , The \u03a9\u03bc+1-rule, In Buchholz et al. [9], pp. 188\u2013233.","DOI":"10.1007\/BFb0091898"},{"key":"S0022481200003066_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"S0022481200003066_ref005","first-page":"1785","volume":"65","author":"Avigad","year":"2000","journal-title":"Interpreting classical theories in constructive ones"},{"key":"S0022481200003066_ref017","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard","year":"1968","journal-title":"Compositio Mathematica"},{"key":"S0022481200003066_ref016","volume-title":"Collected works","volume":"II","author":"G\u00f6del","year":"1990"},{"key":"S0022481200003066_ref015","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0022481200003066_ref025","unstructured":"Kreisel Georg , Generalized inductive definitions, Stanford Report on the Foundations of Analysis (mimeographed), 1963."},{"key":"S0022481200003066_ref008","doi-asserted-by":"crossref","unstructured":"Buchholz Wilfried , Ordinal analysis of ID\u03bd , In Buchholz et al. [9], pp. 234\u2013260.","DOI":"10.1007\/BFb0091899"},{"key":"S0022481200003066_ref019","volume-title":"Theories for admissible sets: A unifying approach to proof theory","author":"J\u00e4ger","year":"1986"},{"key":"S0022481200003066_ref003","volume-title":"A variant of the double-negation translation","author":"Avigad"},{"key":"S0022481200003066_ref027","doi-asserted-by":"crossref","unstructured":"Pohlers Wolfram , Proof theoretical analysis of ID\u03bd by the method of local predicativity, In Buchholz et al. [9], pp. 261\u2013357.","DOI":"10.1007\/BFb0091900"},{"key":"S0022481200003066_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF02025118"},{"key":"S0022481200003066_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"S0022481200003066_ref021","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1955-09896-3"},{"key":"S0022481200003066_ref022","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-04-03515-9"},{"key":"S0022481200003066_ref018","first-page":"355","volume":"37","author":"Howard","year":"1972","journal-title":"A system of abstract constructive ordinals"},{"key":"S0022481200003066_ref002","unstructured":"Aehlig Klaus , On fragments of analysis with strengths of finitely iterated inductive definitions, Ph.D. thesis, University of Munich, 2003."},{"key":"S0022481200003066_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(97)00045-6"},{"key":"S0022481200003066_ref024","first-page":"147","article-title":"Proof mining: a systematic way of analyzing proofs in mathematics","volume":"242","author":"Kohlenbach","year":"2003","journal-title":"Trudy Matematicheskogo Instituia Imeni V. A. Steklova"},{"key":"S0022481200003066_ref020","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1955-0070594-4"},{"key":"S0022481200003066_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.11.001"},{"key":"S0022481200003066_ref029","volume-title":"Mathematical logic","author":"Shoenfield","year":"2001"},{"key":"S0022481200003066_ref023","volume-title":"Applied proof theory: Proof interpretations and their use in mathematics","author":"Kohlenbach"},{"key":"S0022481200003066_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0079558"},{"key":"S0022481200003066_ref012","unstructured":"Feferman Solomon , Ordinals associated with theories for one inductively defined set, unpublished paper, 1968."},{"key":"S0022481200003066_ref032","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011878"},{"key":"S0022481200003066_ref034","first-page":"475","volume-title":"Intuition and proof theory","author":"Tait","year":"1970"},{"key":"S0022481200003066_ref030","unstructured":"Sieg Wilfried , Trees in metamathematics: theories of inductive definitions and subsystems of analysis, Ph.D. thesis, Stanford University."},{"key":"S0022481200003066_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0091894"},{"key":"S0022481200003066_ref031","doi-asserted-by":"crossref","unstructured":"Sieg Wilfried , Inductive definitions, constructive ordinals, and normal derivations, In Buchholz et al. [9], pp. 143\u2013187.","DOI":"10.1007\/BFb0091897"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200003066","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T18:35:55Z","timestamp":1556562955000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200003066\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["S0022481200003066"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1254748682","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12]]}}}