{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:23:21Z","timestamp":1742912601666,"version":"3.40.3"},"publisher-location":"Cham","reference-count":122,"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_1","type":"book-chapter","created":{"date-parts":[[2015,11,2]],"date-time":"2015-11-02T11:51:24Z","timestamp":1446465084000},"page":"3-24","source":"Crossref","is-referenced-by-count":5,"title":["Gentzen\u2019s Consistency Proof in Context"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Kahle","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"W. Ackermann, Letter to David Hilbert, August 23rd, 1933, Nieders\u00e4chsische Staats- und Universit\u00e4tsbibliothek G\u00f6ttingen, Cod. Ms. D. Hilbert\u00a01."},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BF01450016","volume":"117","author":"W. Ackermann","year":"1940","unstructured":"W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie. Math. Ann. 117, 162\u2013194 (1940)","journal-title":"Zur Widerspruchsfreiheit der Zahlentheorie. Math. Ann."},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0049-237X(08)71252-7","volume-title":"The Kleene Symposium","author":"P. Aczel","year":"1980","unstructured":"P. Aczel, Frege structures and the notion of proposition, truth and set, in The Kleene Symposium, ed. by J. Barwise, H. Keisler, K. Kunen (North-Holland, Amsterdam, 1980), pp. 31\u201359"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/S0168-0072(02)00112-4","volume":"121","author":"T. Arai","year":"2003","unstructured":"T. Arai, Epsilon substitution method for \n$$\\text{ID}_{1}(\\Pi _{1}^{0} \\vee \\Sigma _{1}^{0})$$\n. Ann. Pure Appl. Log. 121, 163\u2013208 (2003)","journal-title":"Ann. Pure Appl. Log."},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0168-0072(03)00020-4","volume":"122","author":"T. Arai","year":"2003","unstructured":"T. Arai, Proof theory for theories of ordinals I: recursively Mahlo ordinals. Ann. Pure Appl. Log. 122, 1\u201385 (2003)","journal-title":"Ann. Pure Appl. Log."},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.apal.2004.01.001","volume":"129","author":"T. Arai","year":"2004","unstructured":"T. Arai, Proof theory for theories of ordinals II:\n$$\\Pi _{3}$$\n-reflection. Ann. Pure Appl. Log. 129, 39\u201392 (2004)","journal-title":"Ann. Pure Appl. Log."},{"key":"1_CR7","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"T. Arai","year":"2015","unstructured":"T. Arai, Proof theory for theories of ordinals III: \n$$\\Pi _{N}$$\n-reflection, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0049-237X(98)80020-7","volume-title":"Handbook of Proof Theory","author":"J. Avigad","year":"1998","unstructured":"J. Avigad, S. Feferman, G\u00f6del\u2019s functional (\u201cDialectica\u201d) interpretation, in Handbook of Proof Theory, ed. by S.R. Buss (North-Holland, Amsterdam, 1998), pp. 337\u2013405"},{"key":"1_CR9","unstructured":"P. Benacerraf, H. Putnam (eds.), Philosophy of Mathematics. Selected Readings (Prentice Hall, Englewood Cliffs, 1964) (2nd edn., Cambridge University Press, Cambridge, 1983)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"P. Bernays, Hilberts Untersuchungen \u00fcber die Grundlagen der Arithmetik, in David Hilbert: Gesammelte Abhandlungen, vol. 3, [51] (Springer, Berlin, 1935), pp. 196\u2013216","DOI":"10.1007\/978-3-662-38452-7_14"},{"key":"1_CR11","first-page":"496","volume-title":"Encyclopedia of Philosophy, vol. 3","author":"P. Bernays","year":"1967","unstructured":"P. Bernays, Hilbert, David, in Encyclopedia of Philosophy, vol. 3, ed. by P. Edwards (Macmillan, New York, 1967), pp. 496\u2013504"},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2268971","volume":"14","author":"N. Bourbaki","year":"1949","unstructured":"N. Bourbaki, Foundations of mathematics for the working mathematician. J. Symb. Log. 14(1), 1\u20138 (1949)","journal-title":"J. Symb. Log."},{"key":"1_CR13","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"W. Buchholz","year":"2015","unstructured":"W. Buchholz, On Gentzen\u2019s first consistency proof for arithmetic, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"W. Buchholz, S. Feferman, W. Pohlers, W. Sieg, Iterated Inductive Definitions and Subsystems of Analysis. Lecture Notes in Mathematics, vol. 897 (Springer, Berlin, 1981)","DOI":"10.1007\/BFb0091894"},{"key":"1_CR15","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"S. Buss","year":"2015","unstructured":"S. Buss, Cut elimination In Situ, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"G. Cantor, Gesammelte Abhandlungen mathematischen und philosophischen Inhalts, ed. by E. Zermelo (Springer, Berlin, 1932)","DOI":"10.1007\/978-3-662-00274-2"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"G. Cantor, Briefe, ed. by H. Meschkowski, W. Nilson (Springer, Berlin, 1991)","DOI":"10.1007\/978-3-642-74344-3"},{"key":"1_CR18","first-page":"74","volume-title":"G\u00f6del\u2019s Theorem in Focus","author":"J.W. Dawson Jr","year":"1988","unstructured":"J.W. Dawson Jr., The reception of G\u00f6del\u2019s incompleteness theorems, in G\u00f6del\u2019s Theorem in Focus, ed. by S.G. Shanker (Routledge, London, 1988), pp. 74\u201395"},{"key":"1_CR19","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"M. Detlefsen","year":"2015","unstructured":"M. Detlefsen, Gentzen\u2019s anti-formalist views, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"H.-D. Ebbinghaus et al., Numbers. Graduate Texts in Mathematics (Springer, Berlin, 1991)","DOI":"10.1007\/978-1-4612-1005-4"},{"key":"1_CR21","unstructured":"L. Euler, Vollst\u00e4ndige Anleitung zur Algebra. (Akademie der Wissenschaften, St. Petersburg, 1770). Two volumes."},{"key":"1_CR22","unstructured":"W.B. Ewald (ed.), From Kant to Hilbert. (Oxford University Press, Oxford, 1996). Two volumes."},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1005622403850","volume":"53","author":"S. Feferman","year":"2000","unstructured":"S. Feferman, Does reductive proof theory have a viable rationale? Erkenntnis 53, 63\u201396 (2000)","journal-title":"Erkenntnis"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1017\/CBO9780511974236.009","volume-title":"Kurt G\u00f6del and the Foundations of Mathematics","author":"S. Feferman","year":"2011","unstructured":"S. Feferman, Lieber Herr Bernays! Lieber Herr G\u00f6del! G\u00f6del on finitism, constructivity, and Hilbert\u2019s program, in Kurt G\u00f6del and the Foundations of Mathematics, ed. by M. Baaz et al. (Cambridge University Press, Cambridge, 2011), pp. 111\u2013133"},{"issue":"4","key":"1_CR25","doi-asserted-by":"publisher","first-page":"401","DOI":"10.2307\/420965","volume":"6","author":"S. Feferman","year":"2000","unstructured":"S. Feferman, H.M. Friedman, P. Maddy, J.R. Steel, Does mathematics need new axioms? Bull. Symb. Log. 6(4), 401\u2013446 (2000)","journal-title":"Bull. Symb. Log."},{"key":"1_CR26","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"F. Ferreira","year":"2015","unstructured":"F. Ferreira, Spector\u2019s proof of the consistency of analysis, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"issue":"1","key":"1_CR27","doi-asserted-by":"publisher","first-page":"329","DOI":"10.2178\/jsl\/1140641178","volume":"71","author":"F. Ferreira","year":"2006","unstructured":"F. Ferreira, A. Nunes, Bounded modified realizability. J. Symb. Log. 71(1), 329\u2013346 (2006)","journal-title":"J. Symb. Log."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"A. Fraenkel, Zehn Vorlesungen \u00fcber die Grundlegung der Mengenlehre. Wissenschaft und Hypothese, vol. XXXI (Teubner, Leipzig, 1927). Reprint (Wissenschaftliche Buchgesellschaft, Darmstadt, 1972)","DOI":"10.1007\/978-3-663-15741-0"},{"key":"1_CR29","unstructured":"G. Frege, Grundgesetze der Arithmetik, vol. 1 (Hermann Pohle, Jena, 1893). Reprinted, together with vol. 2 (Olms, Hildesheim 1966)"},{"key":"1_CR30","unstructured":"G. Frege, Grundgesetze der Arithmetik, vol. 2 (Hermann Pohle, Jena, 1903). Reprinted, together with vol. 1 (Olms, Hildesheim 1966)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112, 493\u2013565 (1936). English translation in [102, #4]","DOI":"10.1007\/BF01565428"},{"key":"#cr-split#-1_CR32.1","unstructured":"G. Gentzen, Die gegenw\u00e4rtige Lage in der mathematischen Grundlagenforschung. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Neue Folge 4, 5-18 (1938)"},{"key":"#cr-split#-1_CR32.2","unstructured":"also in Dtsch. Math. 3, 255-268 (1939). English translation in [102, #7]"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"G. Gentzen, \u00dcber das Verh\u00e4ltnis zwischen intuitionistischer und klassischer Arithmetik. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 16, 119\u2013132 (1974). Written in 1933, but withdrawn from publication after the appearence of [37]. English translation in [102, #2]","DOI":"10.1007\/BF02015371"},{"key":"1_CR34","unstructured":"J.-Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur, PhD thesis, Universit\u00e9 Paris 7, 1972"},{"key":"1_CR35","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-0348-8968-1_17","volume-title":"Development of Mathematics, 1950\u20132000","author":"J.-Y. Girard","year":"2000","unstructured":"J.-Y. Girard, Du pourquoi au comment: la th\u00e9orie de la d\u00e9monstration de 1950 \u00e0 nos jours, in Development of Mathematics, 1950\u20132000, ed. by J.-P. Pier (Birkh\u00e4user, Basel, 2000),pp. 515\u2013545"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard, The Blind Spot. (European Mathematical Society, Z\u00fcrich, 2011)","DOI":"10.4171\/088"},{"key":"1_CR37","unstructured":"K. G\u00f6del, Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums 4, 34\u201338 (1933). Translated as On intuitionistic arithmetic and number theory in [113], reprinted in [40] (1933e), pp. 287\u2013295"},{"key":"1_CR38","unstructured":"K. G\u00f6del, Vortrag bei Zilsel\/Lecture at Zilsel\u2019s, 1938. Published in [42] (*1938a), pp. 86\u2013113"},{"key":"1_CR39","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 English translation in [41], pp. 241\u2013251","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"1_CR40","unstructured":"K. G\u00f6del, Collected Works, vol. I, ed. by S. Feferman et al. (Oxford University Press, Oxford, 1986)"},{"key":"1_CR41","unstructured":"K. G\u00f6del, Collected Works, vol. II, ed. by S. Feferman et al. (Oxford University Press, Oxford, 1990)"},{"key":"1_CR42","unstructured":"K. G\u00f6del, Collected Works: Unpublished Essays and Lectures, vol. III, ed. by S. Feferman et al. (Oxford University Press, Oxford, 1995)"},{"key":"1_CR43","volume-title":"Henri Poincar\u00e9","author":"J. Gray","year":"2013","unstructured":"J. Gray, Henri Poincar\u00e9 (Princeton University Press, Princeton, 2013)"},{"key":"1_CR44","unstructured":"M. Hallett. Cantorian Set Theory and Limitation of Size. Oxford Logic Guides, vol. 10 (Oxford University Press, Oxford, 1984)"},{"key":"1_CR45","unstructured":"D. Hilbert, Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongre\u00df zu Paris 1900. Nachrichten von der k\u00f6nigl. Gesellschaft der Wissenschaften zu G\u00f6ttingen. Mathematisch-physikalische Klasse, pages 53\u2013297, 1900. English translation: [46]"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"D. Hilbert, Mathematical Problems. Lecture Delivered Before the International Congress of Mathematicians at Paris in 1900. Bull. Am. Math. Soc. 8, 437\u2013479 (1902). English translation of [45]","DOI":"10.1090\/S0002-9904-1902-00923-3"},{"key":"1_CR47","first-page":"174","volume-title":"Verhandlungen des Dritten Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904","author":"D. Hilbert","year":"1905","unstructured":"D. Hilbert, \u00dcber die Grundlagen der Logik und der Arithmetik, in Verhandlungen des Dritten Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904, ed. by A. Krazer (Teubner, Leipzig, 1905), pp. 174\u2013185"},{"key":"1_CR48","unstructured":"D. Hilbert, Mengenlehre. Lecture Notes Summer term 1917, (Library of the Mathematical Institute, University of G\u00f6ttingen), 1917"},{"key":"1_CR49","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BF02940589","volume":"1","author":"D. Hilbert","year":"1922","unstructured":"D. Hilbert, Neubegr\u00fcndung der Mathematik: Erste Mitteilung. Abhandlungen aus dem Seminar der Hamburgischen Universit\u00e4t 1, 157\u2013177 (1922)","journal-title":"Abhandlungen aus dem Seminar der Hamburgischen Universit\u00e4t"},{"issue":"1\/2","key":"1_CR50","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF02940602","volume":"6","author":"D. Hilbert","year":"1928","unstructured":"D. Hilbert, Die Grundlagen der Mathematik. Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universit\u00e4t 6(1\/2), 65\u201385 (1928)","journal-title":"Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universit\u00e4t"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"D. Hilbert, Gesammelte Abhandlungen. Analysis, Grundlagen der Mathematik, Physik, Verschiedenes, Lebensgeschichte, vol. III (Springer, Berlin, 1935). 2nd edition 1970","DOI":"10.1007\/978-3-662-38452-7"},{"key":"1_CR52","unstructured":"D. Hilbert, P. Bernays, Grundlagen der Mathematik I. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen, vol. 40 (Springer, Berlin, 1934). 2nd edn. 1968. Partly translated into English in the bilingual edition [55]"},{"key":"1_CR53","unstructured":"D. Hilbert, P. Bernays, Grundlagen der Mathematik II. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen, vol. 50 (Springer, Berlin, 1939). 2nd edition [54]"},{"key":"1_CR54","unstructured":"D. Hilbert, P. Bernays, Grundlagen der Mathematik II. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen, vol. 50, 2nd edn. (Springer, Berlin, 1970). 1st edition [53]."},{"key":"1_CR55","unstructured":"D. Hilbert, P. Bernays, Grundlagen der Mathematik I (Foundations of Mathematics I). (College Publications, London, 2011). Bilingual edition of Prefaces and \u00a7\u00a71\u20132 of [52]"},{"key":"1_CR56","unstructured":"G. J\u00e4ger, Theories for Admissible Sets: A Unifying Approach to Proof Theory. (Bibliopolis, Naples, 1986)"},{"key":"1_CR57","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"G. J\u00e4ger","year":"2015","unstructured":"G. J\u00e4ger, D. Probst, A proof-theoretic analysis of theories for stratified inductive definitions, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR58","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"H. Jervell","year":"2015","unstructured":"H. Jervell, Climbing mount \n$$\\varepsilon _{0}$$\n, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR59","unstructured":"R. Kahle, David Hilbert \u00fcber Paradoxien. Departamento de Matem\u00e1tica, Universidade de Coimbra. Preprint Number 06-17(2006)"},{"key":"1_CR60","unstructured":"R. Kahle, The universal set\u2014A (never fought) battle between philosophy and mathematics, in L\u00f3gica e Filosofia da Ci\u00eancia, ed. by O. Pombo, \u00c1. Nepomuceno. Colec\u00e7\u00e3o Documenta, vol. 2 (Centro de Filosofia das Ci\u00eancias da Universidade de Lisboa, Lisboa, 2009), pp. 53\u201365"},{"key":"1_CR61","unstructured":"R. Kahle, Hilbert and Poincar\u00e9 and the paradoxes, in Poincar\u00e9\u2019s Philosophy of Mathematics: Intuition, Experience, Creativity, ed. by H. Tahiri. Cadernos de Filosofia das Ci\u00eancias, vol. 11 (Centro de Filosofia das Ci\u00eancias da Universidade de Lisboa, Lisboa, 2011), pages 79\u201393"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"R. Kahle, Poincar\u00e9 in G\u00f6ttingen, in Poincar\u00e9: Philosopher of Science, Problems and Perspectives, ed. by M. de Paz, R. DiSalle. The Western Ontario Series in the Philosophy of Science, vol. 79 (Springer, Berlin, 2014), pp. 83\u201399","DOI":"10.1007\/978-94-017-8780-2_5"},{"key":"1_CR63","unstructured":"A. Kanamori, The Higher Infinite, 2nd edn. (Springer, Berlin, 2003). 1st edition 1994"},{"key":"1_CR64","unstructured":"U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. (Springer, Berlin, 2008)"},{"key":"1_CR65","unstructured":"A.N. Kolmogorov, O principe tertium non datur. Matematicheskij Sbornik 32, 646\u2013667 (1925). Reprinted in English translation as On the principle of the excluded middle in [113, p. 414\u2013447]"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"G. Kreisel, Hilbert\u2019s programme. Dialectica 12, 346\u2013372 (1958). Reprinted in [9, pp. 207\u2013238 of the second edition]","DOI":"10.1111\/j.1746-8361.1958.tb01469.x"},{"issue":"3","key":"1_CR67","doi-asserted-by":"publisher","first-page":"321","DOI":"10.2307\/2270324","volume":"33","author":"G. Kreisel","year":"1968","unstructured":"G. Kreisel, A survey of proof theory. J. Symb. Log. 33(3), 321\u2013388 (1968)","journal-title":"J. Symb. Log."},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"G. Kreisel, Formal rules and questions of justifying mathematical practice, in Konstruktionen versus Positionen, ed, by K. Lorenz. vol. 1: Spezielle Wissenschaftslehre (de Gruyter, Berlin, 1979), pp. 99\u2013130","DOI":"10.1515\/9783110875560-010"},{"key":"1_CR69","volume-title":"Reports of Seminar on the Foundations of Analysis (\u201cStanford report\u201d)","author":"G. Kreisel","year":"1963","unstructured":"G. Kreisel et al., Reports of Seminar on the Foundations of Analysis (\u201cStanford report\u201d). Technical report, Stanford University, Summer 1963"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"P. Lorenzen, Logik und Agon, in Atti del XII Congresso Internazionale di Filosofia, vol. 4 (Sansoni, Firenze, 1960), pp. 187\u2013194. Reprinted in [71]","DOI":"10.5840\/wcp1219604110"},{"key":"1_CR71","volume-title":"Dialogische Logik","author":"P. Lorenzen","year":"1978","unstructured":"P. Lorenzen, K. Lorenz, Dialogische Logik (Wissenschaftliche Buchgesellschaft, Darmstadt, 1978)"},{"key":"1_CR72","doi-asserted-by":"publisher","first-page":"2419","DOI":"10.1098\/rsta.2005.1656","volume":"363","author":"A. Macintyre","year":"2005","unstructured":"A. Macintyre, The mathematical significance of proof theory. Philos. Trans. R. Soc. A 363, 2419\u20132435 (2005)","journal-title":"Philos. Trans. R. Soc. A"},{"key":"1_CR73","volume-title":"Naturalism in Mathematics","author":"P. Maddy","year":"1997","unstructured":"P. Maddy, Naturalism in Mathematics (Clarendon Press, Oxford, 1997)"},{"issue":"3","key":"1_CR74","doi-asserted-by":"publisher","first-page":"359","DOI":"10.2178\/bsl\/1286284558","volume":"16","author":"C. McLarty","year":"2010","unstructured":"C. McLarty, What does it take to prove Fermat\u2019s last theorem? Grothendieck and the logic of number theory. Bull. Symb. Log. 16(3), 359\u2013377 (2010)","journal-title":"Grothendieck and the logic of number theory. Bull. Symb. Log."},{"key":"1_CR75","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"F. Meskens","year":"2015","unstructured":"F. Meskens, A. Weiermann, Classifying phase transition thresholds for Goodstein sequences and Hydra games, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR76","first-page":"91","volume-title":"Logic, Methodology, and Philosophy of Science IX","author":"G. Mints","year":"1994","unstructured":"G. Mints, Gentzen-type systems and Hilbert\u2019s epsilon substitution method. I, in Logic, Methodology, and Philosophy of Science IX, ed. by D. Prawitz, B. Skyrms, D. Westerstahl (Elsevier, Amsterdam, 1994), pp. 91\u2013122"},{"key":"1_CR77","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"G. Mints","year":"2015","unstructured":"G. Mints, Non-deterministic epsilon substitution method for PA and ID1, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR78","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BF01273688","volume":"35","author":"G. Mints","year":"1996","unstructured":"G. Mints, S. Tupailo, W. Buchholz, Epsilon substitution method for elementary analysis. Arch. Math. Log. 35, 103\u2013130 (1996)","journal-title":"Arch. Math. Log."},{"key":"1_CR79","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S. Negri","year":"2001","unstructured":"S. Negri, J. von Plato, Structural Proof Theory (Cambridge University Press, Cambridge, 2001)"},{"key":"1_CR80","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"P. Oliva","year":"2015","unstructured":"P. Oliva, T. Powell, A game-theoretic computational interpretation of proofs in classical analysis, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR81","doi-asserted-by":"crossref","unstructured":"W. Pohlers, Subsystems of set theory and second order number theory, in Handbook of Proof Theory, ed. by S.R. Buss. Studies in Logic and Foundations of Mathematics, vol. 137 (Elsevier, Amsterdam, 1998), pp. 209\u2013335","DOI":"10.1016\/S0049-237X(98)80019-0"},{"key":"1_CR82","volume-title":"Proof Theory","author":"W. Pohlers","year":"2009","unstructured":"W. Pohlers, Proof Theory. Universitext (Springer, Berlin, 2009)"},{"key":"1_CR83","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"W. Pohlers","year":"2015","unstructured":"W. Pohlers, Semi-formal calculi and their applications, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR84","unstructured":"H. Poincar\u00e9, Les math\u00e9matiques et la logique. Revue de m\u00e9taphysique et de morale 14, 294\u2013317 (1906). Translated in [22, vol. 2, pp. 1052\u20131071]"},{"key":"1_CR85","volume-title":"Sechs Vortr\u00e4ge \u00fcber ausgew\u00e4hlte Gegenst\u00e4nde aus der reinen Mathematik und mathematischen Physik","author":"H. Poincar\u00e9","year":"1910","unstructured":"H. Poincar\u00e9, Sechs Vortr\u00e4ge \u00fcber ausgew\u00e4hlte Gegenst\u00e4nde aus der reinen Mathematik und mathematischen Physik (Teubner, Leipzig, 1910)"},{"key":"1_CR86","doi-asserted-by":"publisher","first-page":"452","DOI":"10.2307\/2270331","volume":"33","author":"D. Prawitz","year":"1968","unstructured":"D. Prawitz, Hauptsatz for higher order logic. J. Symb. Log. 33, 452\u2013457 (1968)","journal-title":"J. Symb. Log."},{"key":"1_CR87","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"D. Prawitz","year":"2015","unstructured":"D. Prawitz, Extending Gentzen\u2019s 2nd consistency proof to normalization of natural deductions in 1st order arithmetic, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"issue":"3","key":"1_CR88","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s00153-004-0232-4","volume":"44","author":"M. Rathjen","year":"2005","unstructured":"M. Rathjen, Ordinal analysis of parameter free \n$$\\Pi _{2}^{1}$$\n-comprehension. Arch. Math. Log. 44(3), 263\u2013362 (2005)","journal-title":"Arch. Math. Log."},{"issue":"1","key":"1_CR89","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00153-004-0226-2","volume":"44","author":"M. Rathjen","year":"2005","unstructured":"M. Rathjen, An ordinal analysis of stability. Arch. Math. Log. 44(1), 1\u201362 (2005)","journal-title":"Arch. Math. Log."},{"key":"1_CR90","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"M. Rathjen","year":"2015","unstructured":"M. Rathjen, Goodstein\u2019s theorem revisited, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR91","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"M. Rathjen","year":"2015","unstructured":"M. Rathjen, P.F.V. Vizca\u00edno, Well ordering principles and bar induction, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-28615-9","volume-title":"Hilbert","author":"C. Reid","year":"1970","unstructured":"C. Reid, Hilbert (Springer, Berlin, 1970)"},{"key":"1_CR93","first-page":"303","volume":"25","author":"K. Sch\u00fctte","year":"1960","unstructured":"K. Sch\u00fctte, Syntactical and semantical properties of simple type theory. J. Symb. Log. 25, 303\u2013326 (1960)","journal-title":"J. Symb. Log."},{"key":"1_CR94","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"K. Sch\u00fctte, Proof Theory (Springer, Berlin, 1977)"},{"key":"1_CR95","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"A. Setzer","year":"2015","unstructured":"A. Setzer, The use of trustworthy principles in a revised Hilbert\u2019s program, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR96","unstructured":"J.R. Shoenfield, Mathematical Logic. (Addison-Wesley, Reading, 1967). Reprinted Association for Symbolic Logic and AK Peters, 2001"},{"key":"1_CR97","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"A. Siders","year":"2015","unstructured":"A. Siders, A direct Gentzen-style consistency proof for Heyting arithmetic, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"issue":"1","key":"1_CR98","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/421139","volume":"5","author":"W. Sieg","year":"1999","unstructured":"W. Sieg, Hilbert\u2019s programs: 1917\u20131922. Bull. Symb. Log. 5(1), 1\u201344 (1999)","journal-title":"Bull. Symb. Log."},{"key":"1_CR99","unstructured":"S.G. Simpson, Subsystems of Second Order Arithmetic, 2nd edn. Perspectives in Logic (Association for Symbolic Logic and Cambridge University Press, New York, 2009)"},{"key":"1_CR100","doi-asserted-by":"crossref","unstructured":"R. Smullyan, G\u00f6del\u2019s Incompleteness Theorems. Oxford Logic Guides, vol. 19. (Oxford University Press, New York, 1992)","DOI":"10.1093\/oso\/9780195046724.001.0001"},{"key":"1_CR101","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, ed. by F.D.E. Dekker. Proceedings of Symposia in Pure Mathematics, vol. 5 (American Mathematical Society, Providence, 1962), pp. 1\u201327","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"1_CR102","unstructured":"M.E. Szabo, The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics (North-Holland, Amsterdam, 1969)"},{"key":"1_CR103","doi-asserted-by":"publisher","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","volume":"72","author":"W.W. Tait","year":"1966","unstructured":"W.W. Tait, A non constructive proof of Gentzen\u2019s Hauptsatz for second order predicate logic. Bull. Am. Math. Soc. 72, 980\u2013983 (1966)","journal-title":"Bull. Am. Math. Soc."},{"key":"1_CR104","doi-asserted-by":"publisher","first-page":"524","DOI":"10.2307\/2026089","volume":"78","author":"W.W. Tait","year":"1981","unstructured":"W.W. Tait, Finitism. J. Philos. 78, 524\u2013546 (1981)","journal-title":"Finitism. J. Philos."},{"key":"1_CR105","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"W.W. Tait","year":"2015","unstructured":"W.W. Tait, Gentzen\u2019s original consistency proof and the bar theorem, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR106","doi-asserted-by":"publisher","first-page":"399","DOI":"10.2969\/jmsj\/01940399","volume":"19","author":"M. Takahashi","year":"1967","unstructured":"M. Takahashi, A proof of cut-elimination in simple type theory. J. Math. Soc. Jpn. 19, 399\u2013410 (1967)","journal-title":"J. Math. Soc. Jpn."},{"key":"1_CR107","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","volume":"23","author":"G. Takeuti","year":"1953","unstructured":"G. Takeuti, On a generalized logic calculus. Jpn. J. Math. 23, 39\u201396 (1953)","journal-title":"Jpn. J. Math."},{"key":"1_CR108","volume-title":"Proof Theory","author":"G. Takeuti","year":"1987","unstructured":"G. Takeuti, Proof Theory, 2nd edn. (North-Holland, Amsterdam, 1987)","edition":"2"},{"key":"1_CR109","unstructured":"A. Tarski, Contribution to the discussion of P. Bernays \u2018Zur Beurteilung der Situation in der beweistheoretischen Forschung\u2019. Revue internationale de philosophie 8, 16\u201320 (1954). Reprinted in [110, pp. 711\u2013714]"},{"key":"1_CR110","volume-title":"Collected Papers","author":"A. Tarski","year":"1986","unstructured":"A. Tarski, Collected Papers, vol. IV (Birkh\u00e4user, Basel, 1986)"},{"key":"1_CR111","unstructured":"A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43, 2nd edn. (Cambridge University Press, Cambridge, 2000)"},{"issue":"3","key":"1_CR112","doi-asserted-by":"publisher","first-page":"284","DOI":"10.2307\/421057","volume":"6","author":"D. van Dalen","year":"2000","unstructured":"D. van Dalen, Brouwer and Fraenkel on intuitionism. Bull. Symb. Log. 6(3), 284\u2013310 (2000)","journal-title":"Bull. Symb. Log."},{"volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","year":"1967","key":"1_CR113","unstructured":"J. van Heijenoort (ed.) From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931. (Harvard University Press, Cambridge, 1967)"},{"key":"1_CR114","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"J. von Plato","year":"2015","unstructured":"J. von Plato, From Hauptsatz to Hilfssatz, in Gentzen\u2019s Centenary: The Quest for Consistency, ed. by R. Kahle, M. Rathjen (Springer, Heidelberg, 2015)"},{"key":"1_CR115","unstructured":"J. von Plato (ed.)Saved from the Cellar. Gerhard Gentzen\u2019s Shorthand Notes on Logic and Foundations of Mathematics. to appear, 201x"},{"issue":"3","key":"1_CR116","doi-asserted-by":"publisher","first-page":"653","DOI":"10.2307\/2273764","volume":"46","author":"H. Wang","year":"1981","unstructured":"H. Wang, Some facts about Kurt G\u00f6del. J. Symb. Log. 46(3), 653\u2013659 (1981)","journal-title":"J. Symb. Log."},{"key":"1_CR117","doi-asserted-by":"crossref","unstructured":"H. Weyl, Das Kontinuum. (Veit, Leipzig, 1918). English translation: [118]","DOI":"10.1515\/9783112451144"},{"key":"1_CR118","unstructured":"H. Weyl, The Continuum: A Critical Examination of the Foundation of Analysis. (Thomas Jefferson University Press, 1987), (Corrected re-publication, Dover 1994). English translation of [117]."},{"key":"1_CR119","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1017\/CBO9780511974236.023","volume-title":"Kurt G\u00f6del and the Foundations of Mathematics","author":"W.H. Woodin","year":"2011","unstructured":"W.H. Woodin, The transfinite universe, in Kurt G\u00f6del and the Foundations of Mathematics, ed. by M. Baaz et al. (Cambridge University Press, New York, 2011), pp. 449\u2013471"},{"key":"1_CR120","doi-asserted-by":"crossref","unstructured":"M. Yasugi, N. Passell (eds.) Memoirs of a Proof Theorist (World Scientific, Singapore, 2003). English translation of a collection of essays written by Gaisi Takeuti","DOI":"10.1142\/5202"},{"key":"1_CR121","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF01449999","volume":"65","author":"E. Zermelo","year":"1908","unstructured":"E. Zermelo, Untersuchungen \u00fcber die Grundlagen der Mengenlehre I. Math. Ann. 65, 261\u2013281 (1908)","journal-title":"Math. Ann."}],"container-title":["Gentzen's Centenary"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10103-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T17:37:52Z","timestamp":1676482672000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10103-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319101026","9783319101033"],"references-count":122,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10103-3_1","relation":{},"subject":[],"published":{"date-parts":[[2015]]}}}