{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:11Z","timestamp":1725455651990},"publisher-location":"Berlin\/Heidelberg","reference-count":36,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022549","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:14:45Z","timestamp":1131862485000},"page":"23-40","source":"Crossref","is-referenced-by-count":10,"title":["G\u00f6del's Dialectica interpretation and its two-way stretch"],"prefix":"10.1007","author":[{"given":"Solomon","family":"Feferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","volume-title":"Bounded Arithmetic","author":"S. Buss","year":"1986","unstructured":"S. Buss [1986]. Bounded Arithmetic, Bibliopolis, Naples."},{"key":"3_CR2","unstructured":"S. A. Cook and A. Urquhart [1994]. Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic (to appear)."},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1016\/S0049-237X(08)71126-1","volume-title":"Handbook of Mathematical Logic","author":"S. Feferman","year":"1977","unstructured":"S. Feferman [1977]. Theories of finite type related to mathematical practice, in Handbook of Mathematical Logic (J. Barwise, ed.), North-Holland, Amsterdam, 913\u2013971."},{"key":"3_CR4","first-page":"546","volume":"21","author":"S. Feferman","year":"1984","unstructured":"S. Feferman [1984]. Kurt G\u00f6del: conviction and caution, Philosophia Naturalis 21, 546\u2013562.","journal-title":"Philosophia Naturalis"},{"key":"3_CR5","first-page":"447","volume-title":"Proof theory: a personal report","author":"S. Feferman","year":"1987","unstructured":"S. Feferman [1987]. Proof theory: a personal report, appendix to second edition of Proof Theory by G. Takeuti, North-Holland, Amsterdam, 447\u2013485."},{"key":"3_CR6","doi-asserted-by":"crossref","first-page":"364","DOI":"10.2307\/2274509","volume":"53","author":"S. Feferman","year":"1988","unstructured":"S. Feferman [1988]. Hilbert's program relativized: proof-theoretical and foundational reductions, J. Symbolic Logic 53, 364\u2013384.","journal-title":"J. Symbolic Logic"},{"key":"3_CR7","volume-title":"Milking the Dialectica interpretation","author":"S. Feferman","year":"1990","unstructured":"S. Feferman [1990]. Milking the Dialectica interpretation, unpublished notes for a lecture at the Conference on Proof Theory, Arithmetic and Complexity, U. C. San Diego, June 25\u201327, 1990."},{"key":"3_CR8","unstructured":"S. Feferman [1993]. What rests on what? The proof-theoretic analysis of mathematics, to appear in Proc. 15th International Wittgenstein Symposium, Kirchberg, Austria."},{"key":"3_CR9","doi-asserted-by":"crossref","first-page":"63","DOI":"10.2307\/2273321","volume":"48","author":"S. Feferman","year":"1983","unstructured":"S. Feferman and G. J\u00e4ger [1983]. Choice principles, the bar rule and automomously iterated comprehension schemes in analysis, J. Symbolic Logic 48, 63\u201370.","journal-title":"J. Symbolic Logic"},{"key":"3_CR10","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/BFb0091896","volume":"879","author":"S. Feferman","year":"1981","unstructured":"S. Feferman and W. Sieg [1981]. Proof-theoretic equivalences between classical and constructive theories for analysis, Lecture Notes in Mathematics 879, 78\u2013142.","journal-title":"Lecture Notes in Mathematics"},{"key":"3_CR11","volume-title":"Ph. D. Thesis","author":"F. Ferreira","year":"1988","unstructured":"F. Ferreira [1988]. Polynomial Time Computable Arithmetic and Conservative Extensions, Ph. D. Thesis, Pennsylvania State University, University Park, PA."},{"key":"3_CR12","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"G. Gentzen [1936]. Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematischen Annalen 112, 493\u2013565.","journal-title":"Mathematischen Annalen"},{"key":"3_CR13","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"K. G\u00f6del [1933]. Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums 4, 34\u201338 (reproduced, with English translation, in [G\u00f6del 1986], 286\u2013295).","journal-title":"Ergebnisse eines Mathematischen Kolloquiums"},{"key":"3_CR14","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"K. G\u00f6del [1958]. \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes, Dialectica 12, 280\u2013287 (reproduced with English translation, in [G\u00f6del 1990], 240\u2013251.","journal-title":"Dialectica"},{"key":"3_CR15","first-page":"271","volume-title":"On an extension of finitary mathematics which has not yet been used","author":"K. G\u00f6del","year":"1972","unstructured":"K. G\u00f6del [1972]. On an extension of finitary mathematics which has not yet been used, in[G\u00f6del 1990], 271\u2013280."},{"key":"3_CR16","volume-title":"Collected Works, Vol. I: Publications 1929\u20131936","author":"K. G\u00f6del","year":"1986","unstructured":"K. G\u00f6del [1986]. Collected Works, Vol. I: Publications 1929\u20131936 (S. Feferman et al., eds.), Oxford University Press, New York."},{"key":"3_CR17","volume-title":"Collected Works, Vol. II: Publications 1937\u20131974","author":"K. G\u00f6del","year":"1990","unstructured":"K. G\u00f6del [1990]. Collected Works, Vol. II: Publications 1937\u20131974 (S. Feferman et al., eds.), Oxford University Press, New York."},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"453","DOI":"10.2307\/2273043","volume":"38","author":"N. D. Goodman","year":"1970","unstructured":"N. D. Goodman [1970]. The faithfulness of the interpretation of arithmetic in the theory of constructions, J. Symbolic Logic 38, 453\u2013459.","journal-title":"J. Symbolic Logic"},{"key":"3_CR19","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF01206605","volume":"95","author":"D. Hilbert","year":"1926","unstructured":"D. Hilbert [1926]. \u00dcber das Unendliche, Mathematische Annalen 95, 161\u2013190.","journal-title":"Mathematische Annalen"},{"key":"3_CR20","first-page":"107","volume":"20","author":"W. Howard","year":"1968","unstructured":"W. Howard [1968]. Functional interpretation of bar induction by bar recursion, Compositio Mathematica 20, 107\u2013124.","journal-title":"Compositio Mathematica"},{"key":"3_CR21","unstructured":"W. Howard [1973], Hereditarily majorizable functionals of finite type, Appendix to [Troelstra 1973], 454\u2013461."},{"key":"3_CR22","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"S. C. Kleene [1952]. Introduction to Metamathematics, North-Holland, Amsterdam."},{"key":"3_CR23","first-page":"81","volume-title":"Constructivity in Mathematics","author":"S. C. Kleene","year":"1959","unstructured":"S. C. Kleene [1959]. Countable functionals, in Constructivity in Mathematics (A. Heyting, ed.), North-Holland, Amsterdam, 81\u2013100."},{"key":"3_CR24","first-page":"241","volume":"16","author":"G. Kreisel","year":"1951","unstructured":"G. Kreisel [1951]. On the interpretation of non-finitist proofs \u2014 Part I. J. Symbolic Logic 16, 241\u2013267.","journal-title":"J. Symbolic Logic"},{"key":"3_CR25","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2307\/2267457","volume":"17","author":"G. Kreisel","year":"1952","unstructured":"G. Kreisel [1952]. On the interpretation of non-finitist proofs \u2014 Part II. Interpretation of number theory. Applications. J. Symbolic Logic 17, 43\u201358.","journal-title":"J. Symbolic Logic"},{"key":"3_CR26","volume-title":"Summaries of talks, Summer Institute for Symbolic Logic, Cornell University 1957","author":"G. Kreisel","year":"1957","unstructured":"G. Kreisel [1957]. G\u00f6del's interpretation of Heyting's arithmetic, Summaries of talks, Summer Institute for Symbolic Logic, Cornell University 1957 (2nd edn. 1960), Inst. for Defense Analyses, Princeton.","edition":"2nd edn."},{"key":"3_CR27","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"G. Kreisel [1959]. Interpretation of analysis by means of constructive functionals of finite types, in Constructivity in Mathematics (A. Heyting, ed.), North-Holland, Amsterdam, 101\u2013128."},{"key":"3_CR28","volume-title":"Logic, Methodology and Philosophy of Science","author":"G. Kreisel","year":"1962","unstructured":"G. Kreisel [1962]. Foundations of intuitionistic logic, in Logic, Methodology and Philosophy of Science (E. Nagel et al., eds.) Stanford University Press, Stanford."},{"volume-title":"Reports of Seminar on the Foundations of Analysis, Stanford, Summer 1963","year":"1963","key":"3_CR29","unstructured":"G. Kreisel (ed.) [1963]. Reports of Seminar on the Foundations of Analysis, Stanford, Summer 1963. Stanford University, Stanford."},{"key":"3_CR30","first-page":"65","volume-title":"G\u00f6del Remembered","author":"G. Kreisel","year":"1987","unstructured":"G. Kreisel [1987]. G\u00f6del's excursions into intuitionistic logic, in G\u00f6del Remembered (P. Weingartner and L. Schmetterer, eds.), Bibliopolis, Naples, 65\u2013186."},{"key":"3_CR31","volume-title":"Mathematical Logic","author":"J. R. Shoenfield","year":"1967","unstructured":"J. R. Shoenfield [1967]. Mathematical Logic, Addison-Wesley, Reading MA."},{"key":"3_CR32","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0168-0072(85)90030-2","volume":"28","author":"W. Sieg","year":"1985","unstructured":"W. Sieg [1985]. Fragments of arithmetic, Annals of Pure and Applied Logic 28, 33\u201372.","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR33","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF01621477","volume":"30","author":"W. Sieg","year":"1991","unstructured":"W. Sieg [1991]. Herbrand analyses, Archive for Mathematical Logic 30, 409\u2013441.","journal-title":"Archive for Mathematical Logic"},{"key":"3_CR34","first-page":"1","volume-title":"Recursive Function Theory","author":"C. Spector","year":"1962","unstructured":"C. Spector [1962]. Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, in Recursive Function Theory (J. C. E. Dekker, ed.), Proc. Symposia in Pure Mathematics 5, American Math. Society, Providence, 1\u201327."},{"volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344","year":"1973","key":"3_CR35","unstructured":"A. S. Troelstra (ed.) [1973]. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344, Springer-Verlag, Berlin."},{"key":"3_CR36","first-page":"217","volume-title":"Introductory note to 1958 and 1972","author":"A. S. Troelstra","year":"1990","unstructured":"A. S. Troelstra [1990]. Introductory note to 1958 and 1972, in[G\u00f6del 1990], 217\u2013241."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022549.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T10:56:30Z","timestamp":1683284190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022549"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/bfb0022549","relation":{},"subject":[]}}