{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:48:45Z","timestamp":1743022125435,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319101026"},{"type":"electronic","value":"9783319101033"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-10103-3_11","type":"book-chapter","created":{"date-parts":[[2015,11,2]],"date-time":"2015-11-02T11:51:24Z","timestamp":1446465084000},"page":"279-300","source":"Crossref","is-referenced-by-count":3,"title":["Spector\u2019s Proof of the Consistency of Analysis"],"prefix":"10.1007","author":[{"given":"Fernando","family":"Ferreira","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"J. Avigad, S. Feferman, G\u00f6del\u2019s functional (\u201cDialectica\u201d) interpretation, in Handbook of Proof Theory, ed. by S.R. Buss. Studies in Logic and the Foundations of Mathematics, vol. 137 (North Holland, Amsterdam, 1998), pp. 337\u2013405","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"652","DOI":"10.2307\/2274319","volume":"50","author":"M. Bezem","year":"1985","unstructured":"M. Bezem, Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. J. Symb. Log. 50, 652\u2013660 (1985)","journal-title":"J. Symb. Log."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"L.E.J. Brouwer, \u00dcber Definitionsbereiche von Funktionen. Math. Ann. 93, 60\u201375 (1927). English translation in [43], 457\u2013463","DOI":"10.1007\/BF01447860"},{"issue":"9","key":"11_CR4","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.1016\/j.apal.2011.11.008","volume":"163","author":"P. Engr\u00e1cia","year":"2012","unstructured":"P. Engr\u00e1cia, The bounded functional interpretation of bar induction. Ann. Pure Appl. Log. 163(9), 1183\u20131195 (2012)","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"759","DOI":"10.2178\/jsl\/1268917503","volume":"75","author":"P. Engr\u00e1cia","year":"2010","unstructured":"P. Engr\u00e1cia, F. Ferreira, The bounded functional interpretation of the double negation shift. J. Symb. Log. 75, 759\u2013773 (2010)","journal-title":"J. Symb. Log."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"F. Ferreira, A most artistic package of a jumble of ideas. Dialectica 62, 205\u2013222 (2008). Special Issue: G\u00f6del\u2019s dialectica Interpretation. Guest editor: Thomas Strahm","DOI":"10.1111\/j.1746-8361.2008.01134.x"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"F. Ferreira, A short note on Spector\u2019s proof of consistency of analysis, in How the World Computes, ed. by B. Cooper, A. Dawar, B. L\u00f6we Lecture Notes in Computer Science, vol. 7318 (Springer, New York, 2012) pp. 222\u2013227","DOI":"10.1007\/978-3-642-30870-3_22"},{"key":"11_CR8","unstructured":"F. Ferreira, U. Kohlenbach, (2015, in preparation)"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.apal.2004.11.001","volume":"135","author":"F. Ferreira","year":"2005","unstructured":"F. Ferreira, P. Oliva, Bounded functional interpretation. Ann. Pure Appl. Log. 135, 73\u2013112 (2005)","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"2615","DOI":"10.1090\/S0002-9947-07-04429-7","volume":"360","author":"P. Gerhardy","year":"2008","unstructured":"P. Gerhardy, U. Kohlenbach, General logical metatheorems for functional analysis. Trans. Am. Math. Soc. 360, 2615\u20132660 (2008)","journal-title":"Trans. Am. Math. Soc."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"K. G\u00f6del, \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. Dialectica 12, 280\u2013287 (1958). Reprinted with an English translation in [13], pp. 240\u2013251","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"11_CR12","unstructured":"K. G\u00f6del, On an extension of finitary mathematics which has not yet been used (1972). Published in [13], pages 271\u2013280. Revised version of [11]."},{"key":"11_CR13","unstructured":"K. G\u00f6del, Collected Works, Vol. II. ed. by S. Feferman et al. (Oxford University Press, Oxford, 1990)"},{"key":"11_CR14","first-page":"107","volume":"20","author":"W.A. Howard","year":"1968","unstructured":"W.A. Howard, Functional interpretation of bar induction by bar recursion. Compos. Math. 20, 107\u2013124 (1968)","journal-title":"Compos. Math."},{"key":"11_CR15","unstructured":"W.A. Howard, Hereditarily majorizable functionals of finite type, 1973. Published in [42], pages 454\u2013461"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"17","DOI":"10.2307\/2273252","volume":"46","author":"W.A. Howard","year":"1980","unstructured":"W.A. Howard, Ordinal analysis of simple cases of bar recursion. J. Symb. Log. 46, 17\u201330 (1980)","journal-title":"J. Symb. Log."},{"key":"11_CR17","first-page":"105","volume":"42","author":"W.A. Howard","year":"1981","unstructured":"W.A. Howard, Ordinal analysis of bar recursion of type zero. Compos. Math. 42, 105\u2013119 (1981)","journal-title":"Compos. Math."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"W.A. Howard, G.Kreisel. Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Log. 31, 325\u2013358 (1966)","DOI":"10.2307\/2270450"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0003-4843(79)90006-8","volume":"16","author":"M. Hyland","year":"1979","unstructured":"M. Hyland, Filter spaces and continuous functionals. Ann. Math. Log. 16, 101\u2013143 (1979)","journal-title":"Ann. Math. Log."},{"key":"11_CR20","unstructured":"S. Kleene, Recursive functions and intuitionistic mathematics, in Proceedings of the International Congress of Mathematicians, Cambridge 1950, vol. 1 (American Mathematics Society, 1952), pp. 679\u2013685"},{"key":"11_CR21","volume-title":"The Foundations of Intuitionistic Mathematics","author":"S. Kleene","year":"1965","unstructured":"S. Kleene, R. Vesley, The Foundations of Intuitionistic Mathematics (Amsterdam, North Holland, 1965)"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"1239","DOI":"10.2307\/2275367","volume":"57","author":"U. Kohlenbach","year":"1992","unstructured":"U. Kohlenbach, Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symb. Log. 57, 1239\u20131273 (1992)","journal-title":"J. Symb. Log."},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.2307\/2586791","volume":"64","author":"U. Kohlenbach","year":"1999","unstructured":"U. Kohlenbach, On the no-counterexample interpretation. J. Symb. Log. 64, 1491\u20131511 (1999)","journal-title":"J. Symb. Log."},{"key":"11_CR24","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1090\/S0002-9947-04-03515-9","volume":"357","author":"U. Kohlenbach","year":"2005","unstructured":"U. Kohlenbach, Some logical metatheorems with applications in functional analysis. Trans. Am. Math. Soc. 357, 89\u2013128 (2005)","journal-title":"Trans. Am. Math. Soc."},{"key":"11_CR25","unstructured":"U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics (Springer, Berlin, 2008)"},{"key":"11_CR26","unstructured":"G. Kreisel, Interpretation of analysis by means of constructive functionals of finite types, in Constructivity in Mathematics ed. by A. Heyting (Amsterdam, North Holland, 1959), pp. 101\u2013128"},{"key":"11_CR27","unstructured":"G. Kreisel, Reports of the seminar on the foundations of analysis. Technical report, Stanford University, 1963. Mimeographed report in two parts"},{"key":"11_CR28","doi-asserted-by":"publisher","first-page":"321","DOI":"10.2307\/2270324","volume":"3","author":"G. Kreisel","year":"1968","unstructured":"G. Kreisel, A survey of proof theory. J. Symb. Log. 3, 321\u2013388 (1968)","journal-title":"J. Symb. Log."},{"key":"11_CR29","first-page":"65","volume-title":"G\u00f6del\u2019s excursions into intuitionistic logic, in G\u00f6del Remembered","author":"G. Kreisel","year":"1987","unstructured":"G. Kreisel, G\u00f6del\u2019s excursions into intuitionistic logic, in G\u00f6del Remembered (Bibliopolis, Napoli, 1987), pp. 65\u2013186"},{"key":"11_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0060871","volume-title":"Extensional G\u00f6del Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics","author":"H. Luckhardt","year":"1973","unstructured":"H. Luckhardt, Extensional G\u00f6del Functional Interpretation: A Consistency Proof of Classical Analysis, Lecture Notes in Mathematics, vol. 306 (Springer, Berlin, 1973)"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"P. Oliva, Understanding and using Spector\u2019s bar recursive interpretation of classical analysis, in Logical Approaches to Computational Barriers \u2013 Proceedings of Computability in Europe 2006, ed. by B. L\u00f6we A. Beckmann, U. Berger, J. Tucker. Lecture Notes in Computer Science, vol. 3988 (Springer, New York, 2006) pp. 423\u2013434","DOI":"10.1007\/11780342_44"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"M. Rathjen, The realm of ordinal analysis, in Sets and Proofs, ed by S.B. Cooper, J.K. Truss London Mathematical Society Lecture Notes Series, vol. 258 (Cambridge University Press, Cambridge, 1999), pp. 219\u2013280","DOI":"10.1017\/CBO9781107325944.011"},{"key":"11_CR33","first-page":"123","volume":"23","author":"B. Scarpellini","year":"1971","unstructured":"B. Scarpellini, A model for bar recursion of higher types. Compos. Math. 23, 123\u2013153 (1971)","journal-title":"Compos. Math."},{"key":"11_CR34","unstructured":"J.R. Shoenfield, Mathematical Logic. (Addison-Wesley Publishing Company, Wokingham, 1967). Republished in 2001 by AK Peters."},{"key":"11_CR35","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/0168-0072(85)90030-2","volume":"28","author":"W. Sieg","year":"1985","unstructured":"W. Sieg, Fragments of arithmetic. Ann. Pure Appl. Log. 28, 33\u201371 (1985)","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics, in Recursive Function Theory: Proceedings of Symposia in Pure Mathematics vol 5, ed. by F.D.E. Dekker (American Mathematical Society, Providence, Rhode Island 1962), pp. 1\u201327","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"G. Sundholm, M. van Atten, The proper explanation of intuitionistic logic: on Brouwer\u2019s demonstration of the Bar Theorem, in One Hundred Years of Intuitionism (1907\u20132007), ed. by M. van Atten, P. Boldini, M. Bourdeau, G. Heinzmann. Publications des Archives Henri Poincar\u00e9 \/ Publications of the Henri Poincar\u00e9 Archives (Birkh\u00e4user Basel, 2008), pp. 60\u201377","DOI":"10.1007\/978-3-7643-8653-5_5"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"W. Tait, Normal form theorem for bar recursive functions of finite type, in Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics (Elsevier, Amsterdam, 1971), pp. 353\u2013367","DOI":"10.1016\/S0049-237X(08)70853-X"},{"key":"11_CR39","doi-asserted-by":"publisher","first-page":"524","DOI":"10.2307\/2026089","volume":"78","author":"W. Tait","year":"1981","unstructured":"W. Tait, Finitism. J. Philos. 78, 524\u2013546 (1981)","journal-title":"Finitism. J. Philos."},{"key":"11_CR40","unstructured":"A.S. Troelstra, Introductory note to [11] and [12] (1990). Published in [13], pages 214\u2013241"},{"key":"11_CR41","unstructured":"A.S. Troelstra, D. van Dalen, Constructivism in Mathematics. An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics (Amsterdam, North Holland, 1988)"},{"volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics","year":"1973","key":"11_CR42","unstructured":"A.S. Troelstra (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344 (Springer, Berlin, 1973)"},{"volume-title":"From Frege to G\u00f6del","year":"1967","key":"11_CR43","unstructured":"J. van Heijenoort (ed.), From Frege to G\u00f6del (Harvard University Press, Cambridge, 1967)"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"H. Vogel, \u00dcber die mit dem Bar-Rekursor vom Typ 0 definierbaren Ordinalzahlen. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 19, 165\u2013173 (1978\/1979)","DOI":"10.1007\/BF02011877"}],"container-title":["Gentzen's Centenary"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10103-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T19:41:33Z","timestamp":1675280493000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10103-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319101026","9783319101033"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10103-3_11","relation":{},"subject":[],"published":{"date-parts":[[2015]]}}}