Linked bibliography for the SEP article "Proof Theory" by Michael Rathjen and Wilfried Sieg

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

The translations in this paper are ours, unless we explicitly refer to an English edition.

  • Ackermann, Wilhelm, 1925, “Begründung des ‘tertium non datur’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit”, Mathematische Annalen, 93: 1–36. doi:10.1007/bf01449946 (Scholar)
  • Aczel, Peter, 1978, “The Type Theoretic Interpretation of Constructive Set Theory”, in A. MacIntyre, L. Pacholski, and J. Paris (eds.), Studies in Logic and the Foundations of Mathematics, 96, Amsterdam: North-Holland, pp. 55–66. doi:10.1016/s0049-237x(08)71989-x (Scholar)
  • Arai, Toshiyasu, 2003, “Proof theory for theories of ordinals I: recursively Mahlo ordinals”, Annals of Pure and Applied Logic, 122(1–3): 1–85. doi:10.1016/s0168-0072(03)00020-4 (Scholar)
  • –––, 2004, “Proof theory for theories of ordinals II: \(\Pi_3\)-Reflection”, Annals of Pure and Applied Logic, 129(1–3): 39–92. doi:10.1016/j.apal.2004.01.001 (Scholar)
  • Avigad, Jeremy and Richard Zach, 2007, “The Epsilon Calculus”, Stanford Encyclopedia of Philosophy (Fall 2007), Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/fall2007/entries/epsilon-calculus/> (Scholar)
  • Awodey, Steve, 2012, “Homotopy Type Theory and Univalent Foundations”, Slides from a talk at Carnegie Mellon, March 2012. [ Awodey 2012 available online] (Scholar)
  • Bachmann, Heinz, 1950, “Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordinalzahlen”, Vierteljahrsschrift der Naturforschenden Gesellschaft Zürich, 95(2): 115–147. [Bachmann 1950 available online] (Scholar)
  • Barwise, Jon, 1975, Admissible Sets and Structures: An Approach to Definability Theory, (Perspectives in Mathematical Logic, 7), Berlin: Springer. (Scholar)
  • ––– (ed.), 1977, Handbook of Mathematical Logic, ( Studies in Logic and the Foundations of Mathematics, 90), Amsterdam: North Holland. (Scholar)
  • Bernays, Paul, 1918, Beiträge zur axiomatischen Behandlung des Logik-Kalküls, Habilitationsschrift, Göttingen, reprinted in Ewald and Sieg 2013: 222–272. (Scholar)
  • –––, 1921, “Disposition for Hilbert’s Seminar: MI”, published in Sieg 2013: 123–124. (Scholar)
  • –––, 1922 [1998], “Über Hilberts Gedanken zur Grundlegung der Mathematik”, Jahresberichte der Deutschen Mathematiker-Vereinigung, 31: 10–19. Translated in Mancosu 1998: 215–222. (Scholar)
  • –––, 1927, “Probleme der theoretischen Logik”, Unterrichtsblätter für Mathematik und Naturwissenschaften, 33: 369–377. (Scholar)
  • –––, 1935, “Hilberts Untersuchungen über die Grundlagen der Arithmetik”, in Hilbert 1935: 196–216. doi:10.1007/978-3-662-38452-7_14">10.1007/978-3-662-38452-7_14 (Scholar)
  • –––, 1965, “Betrachtungen zum Sequenzenkalkül”, in Anna-Teresa Tymieniecka and C. Parsons (eds.), Contributions to Logic and Methodology, in honor of J. M. Bochenski, Amsterdam: North-Holland, 1–44. doi:10.1016/b978-1-4832-3159-4.50007-1 (Scholar)
  • –––, 1976, Abhandlungen zur Philosophie der Mathematik, Darmstadt: Wissenschaftliche Buchgesellschaft. (Scholar)
  • Bernstein, Felix, 1919, “Die Mengenlehre Georg Cantors und der Finitismus”, Jahresberichte der Deutschen Mathematiker-Vereinigung, 28: 63–78. (Scholar)
  • Bishop, Errett, 1967, Foundations of Constructive Analysis, New York: McGraw-Hill. (Scholar)
  • Brouwer, Luitzen Egbertus Jan, 1927, “Über Definitionsbereiche von Funktionen”, Mathematische Annalen, 97: 60–75. doi:10.1007/bf01447860 English translation in van Heijenoort 1967: 446–463. (Scholar)
  • –––, 1928 [1967], “Intuitionistische Betrachtungen über den Formalismus”, Koninklijke Akademie van wetenschappen te Amsterdam, Proceedings of the section of sciences, 31: 374–379. English translation in van Heijenoort 1967: 490–492. (Scholar)
  • Buchholz, Wilfried, 1977a, Eine Erweiterung der Schnitteliminationsmethode, Habilitationsschrift, München. (Scholar)
  • –––, 1977b, “A New System of Proof-Theoretic Ordinal Functions”, Annals of Pure and Applied Logic, 32: 195–207. doi:10.1016/0168-0072(86)90052-7 (Scholar)
  • –––, 1987, “An independence result for \((\Pi^1_1\)-CA+BI)”, Annals of Pure and Applied Logic, 33: 131–155. doi:10.1016/0168-0072(87)90078-9 (Scholar)
  • –––, 1993, “A Simplified Version of Local Predicativity”, in Peter Aczel, Harold Simmons, and Stanley S. Wainer (eds.), Proof Theory: A selection of papers from the Leeds Proof Theory Programme 1990, Cambridge: Cambridge University Press, 115–147. doi:10.1017/cbo9780511896262.006 (Scholar)
  • –––, 1997, “Explaining Gentzen’s Consistency Proof Within Infinitary Proof Theory”, in Georg Gottlob, Alexander Leitsch, and Daniele Mundici (eds.), KGC ’97 Proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory, , Lecture Notes in Computer Science 1289, Berlin: Springer-Verlag, pp. 4–17. doi:10.1007/3-540-63385-5_29 (Scholar)
  • –––, 2015, “On Gentzen’s First Consistency Proof for Arithmetic” in Kahle and Rathjen 2015: 63–87. doi:10.1007/978-3-319-10103-3_4">10.1007/978-3-319-10103-3_4 (Scholar)
  • Buchholz, Wilfried, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, 1981, Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, (Lecture Notes in Mathematics, 897), Berlin: Springer. doi:10.1007/bfb0091894 (Scholar)
  • Buchholz, Wilfried and Kurt Schütte, 1988, Proof Theory of Impredicative Subsystems of Analysis, Naples: Bibliopolis. (Scholar)
  • Buchholz, Wilfried and Wilfried Sieg, 1990, “A Note on Polynomial Time Computable Arithmetic”, in Sieg 1990: 51–56. doi:10.1090/conm/106/1057815">10.1090/conm/106/1057815 (Scholar)
  • Buchholz, Wilfried and Stan Wainer, 1987, “Provable Computable Functions and the Fast Growing Hierarchy”, in Simpson 1987: 179–198. doi:10.1090/conm/065/891248">10.1090/conm/065/891248 (Scholar)
  • Burr, Wolfgang, 2000, “Functional Interpretation of Aczel’s Constructive Set Theory”, Annals of Pure and Applied Logic, 104: 31–73. doi:10.1016/s0168-0072(00)00007-5 (Scholar)
  • Buss, Samuel R., 1986, Bounded Arithmetic, Napoli: Bibliopolis. [Buss 1986 draft available online] (Scholar)
  • Cantor, Georg, 1872, “Ueber die Ausdehnung eines Satzes aus der Theorie der trigonometrischen Reihen”, Mathematische Annalen, 5: 123–132. [Cantor 1872 available online] (Scholar)
  • –––, 1897, “Beiträge zur Begründung der transfiniten Mengenlehre II”, Mathematische Annalen, 49(2): 207–246. doi:10.1007/BF01444205 (Scholar)
  • Carnap, Rudolf, 1934, Logische Syntax der Sprache, Wien: Springer. doi:10.1007/978-3-662-25376-2 (Scholar)
  • Church, Alonzo, 1936, “An Unsolvable Problem of Elementary Number Theory”, American Journal of Mathematics, 58(2): 345–363. doi:10.2307/2371045 (Scholar)
  • Church, Alonzo and S.C. Kleene, 1936, “Formal Definitions in the Theory of Ordinal Numbers”, Fundamenta Mathematicae, 28(1): 11–21. [Church and Kleene 1936 available online] (Scholar)
  • Cichon, E.A., 1983, “A Short Proof of Two Recently Discovered Independence Results Using Recursion Theoretic Methods”, Proceedings of the American Mathematical Society, 87(4): 704–706. doi:10.1090/s0002-9939-1983-0687646-0 (Scholar)
  • Curry, Haskell B., 1930 “Grundlagen der Kombinatorischen Logik”, American Journal of Mathematics, 52(3): 509–536, 52(4): 789–834. doi:10.2307/2370619 (part 1) doi:10.2307/2370716 (part 2) (Scholar)
  • Dawson, John W., 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, Wellesley, MA: A.K. Peters. (Scholar)
  • Dedekind, Richard, 1872, Stetigkeit und irrationale Zahlen, Braunschweig: Vieweg. Translated by Wooster Woodruff Beman as “Continuity and Irrational Numbers”, in Essays on the Theory of Numbers , Chicago: Open Court, 1901; reprinted with corrections by William Ewald in Ewald 1996: 765–779 (vol. 2). (Scholar)
  • –––, 1888, Was sind und was sollen die Zahlen, Braunschweig: Vieweg. Translated by Wooster Woodruff Beman as “The Nature and Meaning of Numbers”, in Essays on the Theory of Numbers , Chicago: Open Court, 1901; reprinted with corrections by William Ewald in Ewald 1996: 787–833 (vol. 2). (Scholar)
  • –––, 1890 [1967], “Letter to H. Keferstein”, Cod. Ms. Dedekind III, I, IV (1890). Printed in Sinaceur 1974: 270–278. Translated in van Heijenoort 1967: 98–103. (Scholar)
  • –––, 1932, Gesammelte mathematische Werke, Volume 3, Robert Fricke, Emmy Noether, and Öystein Ore (eds), Braunschweig: Vieweg. [Dedekind 1932 available online] (Scholar)
  • Diestel, Reinhard, 1997 Graph Theory, New York, Berlin, Heidelberg: Springer. doi:10.1007/978-3-662-53622-3 (doi is for the fifth edition but page numbers are from the first edition). (Scholar)
  • Diller, Justus, 2008, “Functional Interpretations of Constructive Set Theory in All Finite Types”, Dialectica, 62(2): 149–177. doi:10.1111/j.1746-8361.2008.01133.x (Scholar)
  • Diller, Justus and Gert H. Müller (eds), 1975, \(\models\) ISILCProof Theory Symposium: Proceedings of the International Summer Institute and Logic Colloquium, Kiel 1974, (Lecture Notes in Mathematics, 500), Berlin: Springer. (Scholar)
  • Dugac, Pierre, 1976, Richard Dedekind et les fondements des mathématiques, Paris: VRIN. (Scholar)
  • Ewald, William (ed.), 1996, From Kant to Hilbert: A Source Book in the Foundations of Mathematics, Oxford: Oxford University Press, two volumes. (Scholar)
  • Ewald, William and Wilfried Sieg (eds.), 2013, David Hilbert’s Lectures on the Foundations of Arithmetic and Logic 1917–1933, Heidelberg: Springer. doi:10.1007/978-3-540-69444-1 (Scholar)
  • Feferman, Solomon, 1962, “Transfinite Recursive Progressions of Axiomatic Theories”, Journal of Symbolic Logic, 27(3): 259–316. doi:10.2307/2964649 (Scholar)
  • –––, 1964, “Systems of Predicative Analysis”, Journal of Symbolic Logic, 29(1): 1–30. doi:10.2307/2269764 (Scholar)
  • –––, 1968, “Autonomous Transfinite Progressions and the Extent of Predicative Mathematics”, in Logic, Methodology, and Philosophy of Science III, Proceedings of the Third International Congress, Amsterdam, 1967, (Studies in Logic and the Foundations of Mathematics, Volume 52), Amsterdam: North-Holland, 121–135. doi:10.1016/s0049-237x(08)71190-x (Scholar)
  • –––, 1970a, “Hereditarily Replete Functionals Over the Ordinals”, in Kino, Myhill, and Vesley 1970: 289–301. doi:10.1016/s0049-237x(08)70760-2 (Scholar)
  • –––, 1970b, “Formal Theories for Transfinite Inductive Definitions and Some Subsystems of Analysis”, in Kino, Myhill, and Vesley 1970: 303–326. doi:10.1016/s0049-237x(08)70761-4 (Scholar)
  • –––, 1975, “A Language and Axioms for Explicit Mathematics”, in Algebra and Logic Papers from the 1974 Summer Research Institute of the Australian Mathematical Society, Monash University, Australia , (Lecture Notes in Mathematics, 450), John Newsome Crossley (ed.), Berlin: Springer, 87–139. doi:10.1007/bfb0062852 (Scholar)
  • –––, 1979, “Constructive Theories of Functions and Classes”, in Maurice Boffa, Dirk van Dalen, Kenneth McAloon (eds.), Logic Colloquium ’78: Proceedings of the colloquium held in Mons, 1 August 1978, Amsterdam: North-Holland, 159–224. doi:10.1016/s0049-237x(08)71625-2 (Scholar)
  • –––, 1987, “Proof Theory: A Personal Report”, in Takeuti 1987: 445–485. (Scholar)
  • –––, 1988, “Hilbert’s Program Relativized: Proof-Theoretical and Foundational Reductions”, Journal of Symbolic Logic, 53(2): 364–384. doi:10.1017/s0022481200028310 (Scholar)
  • –––, 1989, “Remarks for ‘The Trends in Logic’”, in R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo (eds), Logic Colloquium ‘88: Proceedings of the Colloquium held in Padova Italy 22–31 August 1988, (Studies in Logic and the Foundations of Mathematics, 127), Amsterdam: North-Holland, 361–363. doi:10.1016/s0049-237x(08)70276-3 (Scholar)
  • –––, 1998, In the Light of Logic, Oxford: Oxford University Press. (Scholar)
  • –––, 2000, “Does Reductive Proof Theory Have a Viable Rationale?”, Erkenntnis, 53(1–2): 63–96. doi:10.1023/a:1005622403850 (Scholar)
  • Feferman, Solomon and Wilfried Sieg, 1981a, “Inductive Definitions and Subsystems of Analysis”, in Buchholz, Feferman, Pohlers, and Sieg 1981: 16–77. doi:10.1007/bfb0091895 (Scholar)
  • –––, 1981b, “Proof Theoretic Equivalences between Classical and Constructive Theories for Analysis”, in Buchholz, Feferman, Pohlers, and Sieg 1981: 78–142. doi:10.1007/bfb0091896 (Scholar)
  • Feferman, Solomon and Thomas Strahm, 2010, “Unfolding Finitist Arithmetic”, Review of Symbolic Logic, 3(4): 665–689. doi:10.1017/s1755020310000183 (Scholar)
  • Ferreira, Fernando, 1990, “Polynomial Time Computable Arithmetic”, in Sieg 1990: 137–156. doi:10.1090/conm/106/1057819 (Scholar)
  • Ferreirós, José, 2008, Labyrinth of Thought: A History of Set Theory and Its Role in Modern Mathematics, second revised edition, Basel: Birkhäuser. First edition was published in 1999. doi:10.1007/978-3-7643-8350-3 (Scholar)
  • Franks, Curtis, 2009, The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited, Cambridge: Cambridge University Press. doi:10.1017/cbo9780511642098 (Scholar)
  • Franzén, Torkel, 2004a, Inexhaustability. A non-exhaustive treatment, (Lecture Notes in Logic 16), Association for Symbolic Logic, Wellesley, MA: A.K. Peters. (Scholar)
  • –––, 2004b, “Transfinite Progressions: a Second Look at Completeness”, Bulletin of Symbolic Logic, 10(3): 367–389. doi:10.2178/bsl/1102022662 (Scholar)
  • Frege, Gottlob, 1879, Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle: Verlag von Louis Nebert. (Scholar)
  • Friedman, Harvey, 1970, “Iterated Inductive Definitions and \(\Sigma^1_2\)-AC”, in Kino, Myhill, and Vesley 1970: 435–442. doi:10.1016/s0049-237x(08)70769-9 (Scholar)
  • Friedman, Harvey, Neil Robertson, and Paul Seymour, 1987, “The Metamathematics of the Graph Minor Theorem”, in Simpson 1987: 229–261. doi:10.1090/conm/065/891251 (Scholar)
  • Friedman, Harvey and Michael Sheard, 1995, “Elementary Descent Recursion and Proof Theory”, Annals of Pure and Applied Logic, 71(1): 1–45. doi:10.1016/0168-0072(94)00003-l (Scholar)
  • Gabriel, Gottfried, Friedrich Kambartel, and Christian Thiel (eds.), 1980, Gottlob Freges Briefwechsel mit D. Hilbert, E. Husserl, B. Russell, sowie ausgewählte Einzelbriefe Freges, (Philosophische Bibliothek, Band 321), Hamburg: Felix Meiner Verlag. [Gabriel et al. available online] (Scholar)
  • Ganesalingam, Mohan and W. Timothy Gowers, 2017, “A Fully Automatic Theorem Prover with Human-Style Output”, Journal of Automated Reasoning, 58(2): 253–291. doi:10.1007/s10817-016-9377-1 (Scholar)
  • Gentzen, Gerhard, 1932, “Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen”, Mathematische Annalen, 107: 329–350. English translation, “On the Existence of Independent Axiom Systems for Infinite Sentence Systems”, in Gentzen 1969: 29–52. doi:10.1007/bf01448897 (de) doi:10.1016/S0049-237X(08)70820-6 (en) (Scholar)
  • –––, [1933] 1974, “Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik”, Archiv für mathematische Logik und Grundlagenforschung, 16(3–4): 119–132. Written in 1933, but withdrawn from publication after the appearence of Gödel 1933. English translation, “On the Relation Between Intuitionist and Classical Arithmetic”, in Gentzen 1969: 53–67. doi:10.1007/BF02015371 (de) doi:10.1016/S0049-237X(08)70821-8 (en) (Scholar)
  • –––, 1934/35, “Untersuchungen über das logische Schließen I,II”, Mathematische Zeitschrift, 39: 176–210, 405–431. English translation, “Investigations into Logical Deduction”, in Gentzen 1969: 68–131. doi:10.1007/bf01201353 (I, de) doi:10.1007/BF01201363 (II, de) doi:10.1016/S0049-237X(08)70822-X (en) (Scholar)
  • –––, 1936, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen, 112: 493–565. English translation, “The Consistency of Elementary Number Theory”, in Gentzen 1969: 132–213. doi:10.1007/bf01565428 (de) doi:10.1016/S0049-237X(08)70823-1 (en) (Scholar)
  • –––, 1938a, “Die gegenwärtige Lage in der mathematischen Grundlagenforschung”, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Neue Folge 4, Leipzig: Hirzel, 5–18. English translation, “The Present State of Research into the Foundations of Mathematics”, in Gentzen 1969: 234–251. doi:10.1016/s0049-237x(08)70826-7 (en) (Scholar)
  • –––, 1938b, “Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie”, Forschungen zur Logik und zur Grundlegung der exacten Wissenschaften, Neue Folge 4, Leipzig: Hirzel, 19–44. English translation, “New Version of the Consistency Proof for Elementary Number Theory”, in Gentzen 1969: 252–286. doi:10.1016/s0049-237x(08)70827-9 (Scholar)
  • –––, 1943, “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie”, Mathematische Annalen, 119(1): 140–161. English translation, “Provability and Nonprovability of Restricted Transfinite Induction in Elementary Number Theory”, in Gentzen 1969: 287–308. doi:10.1007/bf01564760 (de) doi:10.1016/S0049-237X(08)70828-0 (en) (Scholar)
  • –––, 1945, Stenogramm von G. Gentzen, Transcription by H. Kneser and H. Urban, 13 pages. (Scholar)
  • –––, 1969, The Collected Papers of Gerhard Gentzen, (Studies in Logic and the Foundations of Mathematics, 55), translated and edited by M.E. Szabo, Amsterdam: North-Holland. (Scholar)
  • –––, 1974, “Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie”, Archiv für Mathematische Logik und Grundlagenforschung, 16(3–4): 97–118. doi:10.1007/bf02015370 (Scholar)
  • Girard, Jean-Yves, 1971, Une extension de l’interpretation de Gödel a l’analyse et son application a l’élimination des coupures dans l’analyse et la théorie des types, in J.E. Fenstad (ed.), 1971, Proceedings of the Second Scandinavian Logic Symposium, (Studies in Logic and the Foundations of Mathematics, 63), Amsterdam: North-Holland, 63–92. doi:10.1016/s0049-237x(08)70843-7 (Scholar)
  • –––, 1987, Proof Theory and Logical Complexity, Volume 1, Napoli: Bibliopolis. (Scholar)
  • Gödel, Kurt, 1929 [1986], Über die Vollständigkeit des Logikkalküls, Dissertation, Wien, also in Gödel 1986: 60–101. (Scholar)
  • –––, 1931a, “Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38: 173–198. doi:10.1007/bf01700692 (Scholar)
  • –––, 1931b [1986], “Nachtrag [to the Diskussion zur Grundlegung der Mathematik]”, Erkenntnis, 2: 149–151 (the full Diskussion starts on 135). Reprinted in Gödel 1986: 200–205. doi:10.1007/BF02028146 (de) (Scholar)
  • –––, 1933, “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38, in English translation in Gödel 1986. (Scholar)
  • –––, 1934, “On Undecidable Propositions of Formal Mathematical Systems”, Princeton lecture notes, in Gödel 1986: 346–371. (Scholar)
  • –––, 1938/9, “On Undecidable Diophantine Propositions”, Manuscript for a lecture written 1938 or 1939, in Gödel 1995: 164–175. (Scholar)
  • –––, 1942, “In what sense is intuitionistic logic constructive?”, in Gödel 1995: 189–200. (Scholar)
  • –––, 1958, “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica, 12(3–4): 280–287. doi:10.1111/j.1746-8361.1958.tb01464.x (Scholar)
  • –––, Collected Works, Oxford: Oxford University Press. Includes both the German originals with English translations, Solomon Feferman, Editor-in-Chief.
    • 1986, Volume I: Publications 1929–1936, Solomon Feferman, John W. Dawson, Jr., Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort (eds). (Scholar)
    • 1990, Volume II: Publications 1938–1974, Solomon Feferman, John W. Dawson, Jr., Stephen C. Kleene, Gregory H. Moore, Robertt M. Solovay, and Jean van Heijenoort (eds). (Scholar)
    • 1995, Volume III: Unpublished Essays and Lectures, Solomon Feferman, John W. Dawson, Jr., Warren Goldfarb, Charles Parsons, and Robert M. Solovay (eds).
    • 2003, Volume IV: Correspondence, A–G, Solomon Feferman, John W. Dawson, Warren Goldfarb, Charles Parsons, and Wilfred Sieg (eds).
  • Goodstein, R.L., 1944, “On the Restricted Ordinal Theorem”, Journal of Symbolic Logic, 9(2): 33–41. doi:10.2307/2268019 (Scholar)
  • Gowers, Timothy (with Alexander Diaz-Lopez), 2016, “Interview with Sir Timothy Gowers”, Notices of the American Mathematical Society, 63(9): 1026–1028. doi:10.1090/noti1432 (Scholar)
  • Hallett, Michael, 2013, “Introduction to Hilbert’s 1931 Göttingen Lecture”, in Ewald and Sieg 2013: 983–984. (Scholar)
  • Hallett, Michael and Wilfried Sieg, 2013, “Introduction to the Kneser Mitschriften”, in Ewald and Sieg 2013: 565–576. (Scholar)
  • Hardy, G.H., 1904, “A Theorem Concerning the Infinite Cardinal Numbers”, Quarterly Journal of Mathematics, 35: 87–94. (Scholar)
  • Harrison, John, 2009, Handbook of Practical Logic and Automated Reasoning, Cambridge: Cambridge University Press. doi:10.1017/cbo9780511576430 (Scholar)
  • Herbrand, Jacques, 1930, Recherches sur la théorie de la démonstration, Dissertation, University of Paris. [Herbrand 1930 available online] (Scholar)
  • –––, 1931, “Sur la non-contradiction de l’arithmétique”, Crelles Journal für die reine und angewandte Mathematik, 166: 1–8. doi:10.1515/crll.1932.166.1 (Scholar)
  • Heyting, Arend, 1930, “Die formalen Regeln der intuitionistischen Logik und Mathematik”, (Sitzungsberichte der Preußischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse), Berlin. (Scholar)
  • ––– (ed.), 1959, Constructivity in Mathematics, Proceedings of the Colloquium held at Amsterdam, 1957, (Studies in Logic and the Foundations of Mathematics), Amsterdam: North-Holland Publishing Company. (Scholar)
  • Hilbert, David, 1898/99, Grundlagen der Euklidischen Geometrie, Lecture Notes by H. von Schaper, MI. Printed in Hilbert 2004: 302–395. (Scholar)
  • –––, 1899, “Grundlagen der Geometrie”, in Festschrift zur Feier der Enthüllung des Gauss-Weber Denkmals in Göttingen, Teubner 1899: 1–92. (Scholar)
  • –––, 1900a, “Über den Zahlbegriff”, Jahresberichte der Deutschen Mathematiker-Vereinigung, 8: 180–194. English translation in Ewald 1996: 1089–1095. [Hilbert 1900a available online] (Scholar)
  • –––, 1900b, “Mathematische Probleme”, Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, 253–297, translated in Ewald 1996: 1096–1105. (Scholar)
  • –––, 1904, Zahlbegriff und Quadratur des Kreises, Lecture notes by M. Born. (Scholar)
  • –––, 1905 [1967], “Über die Grundlagen der Logik und der Arithmetik”, in Verhandlungen des Dritten Internationalen Mathematiker-Kongresses, Teubner, 174–185. Translated in van Heijenoort 1967: 129–138. (Scholar)
  • –––, 1917, Mengenlehre, Lecture notes by M. Goeb, MI. (Scholar)
  • –––, 1917–18, Prinzipien der Mathematik, Lecture notes by P. Bernays, MI. Published in Ewald and Sieg 2013: 59–221. (Scholar)
  • –––, 1918, “Axiomatisches Denken”, Mathematische Annalen, 78: 405–415. doi:10.1007/bf01457115 Reprinted in Hilbert 1935: 146–156. (Scholar)
  • –––, 1922, “Neubegründung der Mathematik”, Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, 1: 157–177; translated in Ewald 1996: 1117–1134. (Scholar)
  • –––, 1922–23, Logische Grundlagen der Mathematik, Lecture notes by P. Bernays, SUB 567. (Scholar)
  • –––, 1923, “Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88(1–2): 151–165; translated in Ewald 1996: 1136–1148. doi:10.1007/bf01448445 (de) (Scholar)
  • –––, 1926, “Über das Unendliche”, Mathematische Annalen, 95: 161–190. doi:10.1007/bf01206605 English translation in van Heijenoort 1967: 367–392. (Scholar)
  • –––, 1927 [1967], “Die Grundlagen der Mathematik”, Vortrag gehalten auf Einladung des Mathematischen Seminars im Juli 1927 in Hamburg, published in Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, 6(1/2): 65–85; translated in van Heijenoort 1967: 464–479. doi:10.1007/BF02940602 (de) (Scholar)
  • –––, 1928, “Probleme der Grundlegung der Mathematik”, Mathematische Annalen, 102: 1–9. Reprint, with emendations and additions, of paper with the same title, published in Atti del Congresso internazionale dei matematici, Bologna 1928, 135–141. doi:10.1007/bf01782335 (original) (Scholar)
  • –––, 1931a, “Die Grundlegung der elementaren Zahlenlehre”, Mathematische Annalen, 104: 485–494; translated in Ewald 1996: 1148–1157. doi:10.1007/bf01457953 (de) (Scholar)
  • –––, 1931b, “Beweis des tertium non datur”, Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-physikalische Klasse, 120–125. (Scholar)
  • –––, 1935, Dritter Band: Analysis · Grundlagen der Mathematik · Physik Verschiedenes, of his Gesammelte Abhandlungen, volume 3, Berlin: Springer. doi:10.1007/978-3-662-38452-7 (Scholar)
  • –––, David Hilbert’s Lectures on the Foundations of Mathematics and Physics, 1891–1933, Berlin: Springer.
    • 2004, volume 1, David Hilbert’s Lectures on the Foundations of Geometry, 1891–1902, Michael Hallett and Ulrich Majer (eds). (Scholar)
    • 2009, volume 5, David Hilbert’s Lectures on the Foundations of Physics, 1915–1927, Tilman Sauer and Ulrich Majer (eds). doi:10.1007/b12915 (Scholar)
    • 2013, volume 3, David Hilbert’s Lectures on the Foundations of Arithmetic and Logic, 1917–1933, Ewald and Sieg (eds). (Scholar)
  • Hilbert, David and Wilhelm Ackermann, 1928, Grundzüge der theoretischen Logik, Berlin: Springer. (Scholar)
  • Hilbert, David and Paul Bernays, Grundlagen der Mathematik, Berlin: Springer, with revisions detailed in foreword by Bernays.
    • 1934, Volume 1, second edition, 1968
    • 1939, Volume II, second edition, 1970
  • Howard, W.A., 1968, “Functional Interpreation of Bar Induction by Bar Recursion”, Compositio Mathematica, 20: 107–124. [Howard 1968 available online] (Scholar)
  • –––, 1972, “A System of Abstract Constructive Ordinals”, Journal of Symbolic Logic, 37(2): 355–374. doi:10.2307/2272979 (Scholar)
  • Jäger, Gerhard, 1980, “Beweistheorie von KPN”, Archiv für Mathematische Logik und Grundlagenforschung, 20(1–2): 53–63. doi:10.1007/bf02011138 (Scholar)
  • –––, 1982, “Zur Beweistheorie der Kripke-Platek-Mengenlehre über den natürlichen Zahlen”, Archiv für Mathematische Logik und Grundlagenforschung, 22(3–4): 121–139. doi:10.1007/bf02297652 (Scholar)
  • –––, 1983, “A well-ordering proof for Feferman’s theory \(T_0\)”, Archiv für Mathematische Logik und Grundlagenforschung, 23(1): 65–77. doi:10.1007/bf02023014 (Scholar)
  • –––, 1986, Theories for Admissible Sets: A Unifying Approach to Proof Theory, Napoli: Bibliopolis. (Scholar)
  • Jäger, Gerhard and Wolfram Pohlers, 1982, “Eine beweistheoretische Untersuchung von \(\Delta^1_2\)-CA+BI und verwandter Systeme”, Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch–Naturwissenschaftliche Klasse, 1–28. (Scholar)
  • Jäger, Gerhard and Wilfried Sieg (eds), 2018, Feferman on Foundations: Logic, Mathematics, Philosophy, (Outstanding Contributions to Logic, 13), Cham: Springer. doi:10.1007/978-3-319-63334-3 (Scholar)
  • Kahle, Reinhard and Michael Rathjen (eds), 2015, Gentzen’s Centenary: The Quest for Consistency, Cham: Springer. doi:10.1007/978-3-319-10103-3 (Scholar)
  • Kanamori, A. and M. Magidor, 1978,“The Evolution of Large Cardinal Axioms in Set Theory”, in Gert H. Müller and Dana Scott (eds.), Higher Set Theory, (Lecture Notes in Mathematics, 669), Berlin: Springer, pp. 99–275. doi:10.1007/bfb0103104 (Scholar)
  • Kino, A., J. Myhill, and R. Vesley (eds), 1970, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, (Studies in Logic and the Foundations of Mathematics, 60), Amsterdam: North-Holland. (Scholar)
  • Kirby, Laurie and Jeff Paris, 1982, “Accessible Independence Results for Peano Arithmetic”, Bulletin of the London Mathematical Society, 14: 285–293. doi:10.1112/blms/14.4.285 (Scholar)
  • Kleene, Stephen Cole, 1938, “On Notations for Ordinal Numbers”, Journal of Symbolic Logic, 3(4): 150–155. doi:10.2307/2267778 (Scholar)
  • –––, 1958, “Extension of an Effectively Generated Class of Functions by Enumeration”, Colloquium Mathematicum, 6: 67–78. doi:10.4064/cm-6-1-67-78 (Scholar)
  • –––, 1959, “Countable Functionals”, in Heyting 1959: 81–100. (Scholar)
  • Kleene, Stephen Cole and Richard Eugene Vesley, 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, Amsterdam: North Holland. (Scholar)
  • Kohlenbach, Ulrich, 2007, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Berlin, Heidelberg: Springer. doi:10.1007/978-3-540-77533-1 (Scholar)
  • Kolmogorov, Andrei Nikolaevich, 1925 [1967], “O principe tertium non datur” (Russian), Matematiceskij Sbornik, 32: 646–667. Translated as “On the Principle of the Excluded Middle” in van Heijenoort 1967: 414–437. (Scholar)
  • Kreisel, G., 1952, “On the Interpretation of Non-Finitist Proofs, Part II: Interpretation of Number Theory, Applications”, Journal of Symbolic Logic, 17(1): 43–58. doi:10.2307/2267457 (Scholar)
  • –––, 1958, “Mathematical Significance of Consistency Proofs”, Journal of Symbolic Logic, 23(2): 155–182. doi:10.2307/2964396 (Scholar)
  • –––, 1959, “Interpretation of Analysis by Means of Constructive Functionals of Finite Type”, in Heyting 1959: 101–128. (Scholar)
  • –––, 1960, “Ordinal Logics and the Characterization of Informal Concepts of Proof”, Proceedings of the International Congress of Mathematicians, 14–21 August 1958, Edinburgh, Cambridge: Cambridge University Press, 289–299. [Kreisel 1960 available online] (Scholar)
  • –––, 1963, “Generalized Inductive Definitions”, in Reports of the Seminar on the Foundations of Analysis, Stanford,(mimeographed), Mathematical Sciences Library, Stanford University, 3.1–3.25. (Scholar)
  • –––, 1982, “Finiteness Theorems in Arithmetic: An Application of Herbrand’s Theorem for \(\Sigma_2\)-Formulas”, in J. Stern (ed.), Proceedings of the Herbrand Symposium, (Studies in Logic and the Foundations of Mathematics, 107), North-Holland Publishing Company, 39–55. doi:10.1016/s0049-237x(08)71876-7 (Scholar)
  • Kreisel, G., G.E. Mints, and S.G. Simpson, 1975, “The Use of Abstract Language in Elementary Metamathematics: Some Pedagogic Examples”, in Rohit Parikh (ed.), Logic Colloquium Symposium on Logic Held at Boston, 1972–73, Berlin: Springer, 38–131. doi:10.1007/bfb0064871 (Scholar)
  • Lejeune Dirichlet, Peter Gustav and Richard Dedekind, Vorlesungen über Zahlentheorie (Lectures on Number Theory), Braunschweig, Vieweg.
    • 1863, first edition
    • 1871, second edition
    • 1879, third edition
    • 1894, fourth edition
  • Lipschitz, Rudolf, 1986, Briefwechsel mit Cantor, Dedekind, Helmholtz, Kronecker, Weierstrass und anderen, Winfried Scharlau (ed.), Braunschweig: Vieweg. doi:10.1007/978-3-663-14205-8 (Scholar)
  • López-Escobar, E.G.K., 1976, “On an Extremely Restricted \(\omega\)-rule”, Fundamenta Mathematicae, 90(2): 159–172. [Lópex-Escobar 1976 available online] (Scholar)
  • Luckhardt, H., 1989, “Herbrand-Analysen zweier Beweise des Satzes von Roth: polynomiale Anzahlschranken”, Journal of Symbolic Logic, 54(1): 234–263. doi:10.2307/2275028 (Scholar)
  • Mancosu, Paolo, 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press. (Scholar)
  • –––, 1999a, “Between Russell and Hilbert: Behmann on the Foundations of Mathematics”, Bulletin of Symbolic Logic, 5(3): 303–330. doi:10.2307/421183 (Scholar)
  • –––, 1999b, “Between Vienna and Berlin: The Immediate Reception of Gödel’s Incompleteness Theorems”, History and Philosophy of Logic, 20(1): 33–45. doi:10.1080/014453499298174 (Scholar)
  • Martin-Löf, Per, 1984, Intuitionistic Type Theory, Naples: Bibliopolis. (Scholar)
  • Mints, G.E., 1981, “Closed Categories and the Theory of Proofs”, Journal of Soviet Mathematics, 15(1): 45–62. doi:10.1007/bf01404107 (Scholar)
  • Myhill, John, 1975, “Constructive Set Theory”, Journal of Symbolic Logic, 40(3): 347–382. doi:10.2307/2272159 (Scholar)
  • Noether, Emmy, 1932, “Remark on Dedekind 1872”, in Dedekind 1932: 334. (Scholar)
  • Paris, Jeff and Leo Harrington, 1977, “A Mathematical Incompleteness in Peano Arithmetic”, Barwise 1977: 1133–1142. doi:10.1016/s0049-237x(08)71130-3 (Scholar)
  • Peano, Giuseppe, 1889, Arithmetices principia, nova methodo exposita, Turin. [Peano 1889 available online] (Scholar)
  • Peckhaus, Volker, 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoeck & Ruprecht. (Scholar)
  • Pohlers, Wolfram, 1975, “An Upper Bound for the Provability of Transfinite Induction in Systems with N-Times Iterated Inductive Definitions”, in Diller and Müller 1975: 271–289. doi:10.1007/bfb0079558 (Scholar)
  • –––, 1977, Beweistheorie der iterierten induktiven Definitionen, Habilitationsschrift, München. (Scholar)
  • –––, 1982, “Cut Elimination for Impredicative Infinitary Systems, Part II: Ordinal Analysis for Iterated Inductive Definitions”, Archiv für mathematische Logik und Grundlagenforschung, 22(1–2): 113–129. doi:10.1007/bf02318028 (Scholar)
  • –––, 1991, “Proof Theory and Ordinal Analysis”, Archive for Mathematical Logic, 30(5–6): 311–376. doi:10.1007/bf01621474 (Scholar)
  • –––, 2009, Proof Theory: The First Step into Impredicativity, Berlin: Springer. doi:10.1007/978-3-540-69319-2 (Scholar)
  • Poincaré, Henri, 1905 [1996], “Les mathématiques et la logique”, Revue de Métaphysique et de Morale, 13(6): 815–835; translated in Ewald 1996: 1021–1038). (Scholar)
  • Prawitz, Dag, 1965, Natural Deduction: A Proof-Theoretical Study, Stockholm: Almqvist & Wiksell.. (Scholar)
  • –––, 1968, “Hauptsatz for Higher Order Logic”, Journal of Symbolic Logic, 33(3): 452–457. doi:10.2307/2270331 (Scholar)
  • Rathjen, Michael, 1988, Untersuchungen zu Teilsystemen der Zahlentheorie zweiter Stufe und der Mengenlehre mit einer zwischen \(\Delta^1_2\)-CA und \(\Delta^1_2\)-CA+BI liegenden Beweisstärke, Ph.D. thesis, University of Münster, Münster. (Scholar)
  • –––, 1990, “Ordinal Notations Based on a Weakly Mahlo Cardinal”, Archive for Mathematical Logic, 29(4): 249–263. doi:10.1007/bf01651328 (Scholar)
  • –––, 1991, “Proof-Theoretic Analysis of KPM”, Archive for Mathematical Logic, 30(5–6): 377–403. doi:10.1007/bf01621475 (Scholar)
  • –––, 1993a, “How to Develop Proof-Theoretic Ordinal Functions on the Basis of Admissible Sets”, Mathematical Logic Quarterly, 39(1): 47–54. doi:10.1002/malq.19930390107 (Scholar)
  • –––, 1994a, “Collapsing Functions Based on Recursively Large Ordinals: A Well-Ordering Proof for KPM”, Archive for Mathematical Logic, 33(1): 35–55. doi:10.1007/bf01275469 (Scholar)
  • –––, 1994b, “Proof Theory of Reflection”, Annals of Pure and Applied Logic, 68(2): 181–224. doi:10.1016/0168-0072(94)90074-4 (Scholar)
  • –––, 1995, “Recent Advances in Ordinal Analysis: \(\Pi^1_2\)-CA and Related Systems”, Bulletin of Symbolic Logic, 1(4): 468–485. doi:10.2307/421132 (Scholar)
  • –––, 1998, “Explicit Mathematics with the Monotone Fixed Point Principle”, Journal of Symbolic Logic, 63(2): 509–542. doi:10.2307/2586846 (Scholar)
  • –––, 1999a, “The Realm of Ordinal Analysis”, in S. Barry Cooper and John K. Truss (eds.), Sets and Proofs, Cambridge: Cambridge University Press, 219–279. doi:10.1017/cbo9781107325944.011 (Scholar)
  • –––, 1999b, “Explicit Mathematics with the Monotone Fixed Point Principle II: Models”, Journal of Symbolic Logic, 64(2): 517–550. doi:10.2307/2586483 (Scholar)
  • –––, 2002, “Explicit Mathematics with Monotone Inductive Definitions: A Survey”, in Sieg, Sommer, and Talcott 2002: 335–352. (Scholar)
  • –––, 2005a, “An Ordinal Analysis of Stability”, Archive for Mathematical Logic, 44(1): 1–62. doi:10.1007/s00153-004-0226-2 (Scholar)
  • –––, 2005b, “An Ordinal Analysis of Parameter-Free \(\Pi^1_2\)-Comprehension”, Archive for Mathematical Logic, 44(3): 263–362. doi:10.1007/s00153-004-0232-4 (Scholar)
  • –––, 2006, “Theories and Ordinals in Proof Theory”, Synthese, 148(3): 719–743. doi:10.1007/s11229-004-6297-0 (Scholar)
  • –––, 2009, “The Constructive Hilbert Programme and the Limits of Martin-Löf Type Theory”, in Sten Lindström, Erik Palmgren, Krister Segerberg, and Viggo Stoltenberg-Hansen (eds.), Logicism, Intuitionism, and Formalism: What Has Become of Them?, (Synthese Library, 341), Dordrecht: Springer Netherlands, 397–433. (Scholar)
  • –––, 2010, “Investigations of Subsystems of Second Order Arithmetic and Set Theory in Strength Between \(\Pi^1_1\)-CA and \(\Delta^1_2\)-CA+BI: Part I”, in Ralf Schindler (ed.), Ways of Proof Theory, (Ontos Mathematical Logic, 2), Frankfurt: Ontos Verlag, 363–439. (Scholar)
  • –––, 2015, “Goodstein’s Theorem Revisited”, in Kahle and Rathjen 2015: 229–242. doi:10.1007/978-3-319-10103-3_9 (Scholar)
  • –––, 2018 “Proof Theory of Constructive Systems: Inductive Types and Univalence”, in Jäger and Sieg 2018: 385–419. (Scholar)
  • Rathjen, Michael and Sergei Tupailo, 2006, “Characterizing the Interpretation of Set Theory in Martin-Löf Type Theory”, Annals of Pure and Applied Logic, 141(3): 442–471. doi:10.1016/j.apal.2005.12.008 (Scholar)
  • Rathjen, Michael and Andreas Weiermann, 1993, “Proof-Theoretic Investigations on Kruskal’s Theorem”, Annals of Pure and Applied Logic: 60(1): 49–88. doi:10.1016/0168-0072(93)90192-g (Scholar)
  • Ravaglia, Mark, 2003, Explicating the Finitist Standpoint, PhD Dissertation, Carnegie Mellon University. (Scholar)
  • Reck, Erich H., 2003, “Dedekind’s Structuralism: An Interpretation and Partial Defense”, Synthese, 137(3): 389–419. doi:10.1023/b:synt.0000004903.11236.91 (Scholar)
  • –––, 2013, “Frege, Dedekind, and the Origins of Logicism”, History and Philosophy of Logic, 34(3): 242–265. doi:10.1080/01445340.2013.806397 (Scholar)
  • Richter, Wayne and Peter Aczel, 1973, “Inductive Definitions and Reflecting Properties of Admissible Ordinals”, in Jens E. Fenstad and P. G. Hinman (eds.), 1973, Generalized Recursion Theory: Proceedings of the 1972 Oslo Symposium, (Studies in Logic and the Foundations of Mathematics, 79), Amsterdam: North Holland, 301–381. doi:10.1016/s0049-237x(08)70592-5 (Scholar)
  • Robertson, Neil and Paul Seymour, 2004, “Graph Minors. XX. Wagner’s conjecture”, Journal of Combinatorial Theory (Series B), 92(2): 325–357. doi:10.1016/j.jctb.2004.08.001 (Scholar)
  • Schmidt, Diana, 1979, Well-Partial Orderings and Their Maximal Order Types, Habilitationsschrift, Heidelberg, 77 pages. (Scholar)
  • Schönfinkel, M., 1924 [1967], “Über die Bausteine der mathematischen Logik”, Mathematische Annalen, 92(3–4): 305–316. English translation in van Heijenoort 1967: 355–366. doi:10.1007/BF01448013 (de) (Scholar)
  • Schütte, Kurt, 1950, “Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie”, Mathematische Annalen, 122(5): 369–389. doi:10.1007/bf01342849 (Scholar)
  • –––, 1960a, “Syntactical and Semantical Properties of Simple Type Theory”, Journal of Symbolic Logic, 25(4): 305–326. doi:10.2307/2963525 (Scholar)
  • –––, 1960b, Beweistheorie, (Grundlehren der mathematischen Wissenschaften, 103), Berlin: Springer. Revised version translated to English as Schütte 1977. (Scholar)
  • –––, 1964, “Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik”, Archiv für Mathematische Logik und Grundlagenforschung, 7(1–2): 45–60. doi:10.1007/bf01972460 (Scholar)
  • –––, 1965, “Predicative Well-Orderings”, in J.N. Crossley and M.A.E. Dummett (eds.), Formal Systems and Recursive Functions, (Studies in Logic and the Foundations of Mathematics, 40), Amsterdam: North Holland, 280–303. doi:10.1016/s0049-237x(08)71694-x (Scholar)
  • –––, 1977, Proof Theory, ( Grundlehren der mathematischen Wissenschaften, 225), J.N. Crossley (trans.), Berlin: Springer. Translation of a revised version of Schütte 1960b. doi:10.1007/978-3-642-66473-1 (Scholar)
  • Schwichtenberg, Helmut, 1971, “Eine Klassifikation der \(\varepsilon_0\)-Rekursiven Funktionen”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 17: 61–74. doi: 10.1002/malq.19710170113 (Scholar)
  • –––, 1977, “Proof Theory: Some Applications of Cut-Elimination”, in Barwise 1977: 867–895. doi:10.1016/s0049-237x(08)71124-8 (Scholar)
  • Schwichtenberg, Helmut and Stanley S. Wainer, 2012, Proofs and Computations, (Perspectives in Logic), Cambridge: Cambridge University Press. doi:10.1017/cbo9781139031905 (Scholar)
  • Setzer, Anton, 1998, “A Well-Ordering Proof for the Proof Theoretical Strength of Martin-Löf Type Theory”, Annals of Pure and Applied Logic, 92(2): 113–159. doi:10.1016/s0168-0072(97)00078-x (Scholar)
  • –––, 2000, “Extending Martin-Löf Type Theory by One Mahlo-Universe”, Archive for Mathematical Logic, 39(3): 155–181. doi:10.1007/s001530050140 (Scholar)
  • Shoenfield, J.R., 1959, “On a restricted \(\omega\)-rule”, Bulletin de L’Académie Polonaise des Sciences, Série des sciences Mathématiques, Astronomiques et Physiques, 7: 405–407. (Scholar)
  • Sieg, Wilfried, 1977, Trees in Metamathematics (Theories of Inductive Definitions and Subsystems of Analysis), Ph.D. Thesis, Stanford. (Scholar)
  • –––, 1981, “Inductive Definitions, Constructive Ordinals, and Normal Derivations”, in Buchholz et al. 1981: 143–187. doi:10.1007/bfb0091897 (Scholar)
  • –––, 1985, “Fragments of Arithmetic”, Annals of Pure and Applied Logic, 28: 33–71. doi:10.1016/0168-0072(85)90030-2 (Scholar)
  • ––– (ed.), 1990, Logic and Computation, (Contemporary Mathematics, 106), Providence, Rhode Island: American Mathematical Society. doi:10.1090/conm/106 (Scholar)
  • –––, 1991, “Herbrand Analyses”, Archive for Mathematical Logic, 30(5–6): 409–441. doi:10.1007/bf01621477 (Scholar)
  • –––, 2010, “Searching for Proofs (and Uncovering Capacities of the Mathematical Mind)”, in Proofs, Categories, and Computations: Essays in Honor of Grigori Mints, Solomon Feferman and Wilfried Sieg (eds), London: College Publications, 189–215. (Scholar)
  • –––, 2012, “In the Shadow of Incompleteness: Hilbert and Gentzen”, in P. Dybjer, Sten Lindström, Erik Palmgren, and G. Sundholm (eds.), Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, Dordrecht, Heidelberg: Springer, 87–128. doi:10.1007/978-94-007-4435-6_5 (Scholar)
  • –––, 2013, Hilbert’s Programs and Beyond, Oxford: Oxford University Press. (Scholar)
  • Sieg, Wilfried and Rebecca Morris, forthcoming, “Dedekind’s Structuralism: Creating Concepts and Deriving Theorems”, to appear in: Logic, Philosophy of Mathematics, and Their History: Essays in Honor of W.W. Tait, London: College Publication. (Scholar)
  • Sieg, Wilfried and Dirk Schlimm, 2005, “Dedekind’s Analysis of Number: Systems and Axioms”, Synthese, 147(1): 121–170. doi:10.1007/s11229-004-6300-9 (Scholar)
  • –––, 2017, “Dedekind’s Abstract Concepts: Models and Mappings”, Philosophia Mathematica, 25(3): 292–317. doi:10.1093/philmat/nku021. (Scholar)
  • Sieg, Wilfried, Richard Sommer, and Carolyn Talcott (eds.), 2002, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, (Lecture Notes in Logic, 15), Urbana, IL: Association for Symbolic Logic. (Scholar)
  • Simpson, Stephen G., 1985, “Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume”, Archiv für Mathematische Logik und Grundlagenforschung, 25(1): 45–65. doi:10.1007/bf02007556 (Scholar)
  • ––– (ed.), 1987, Logic and Combinatorics, (Contemporary Mathematics, 65), Providence, Rhode Island: American Mathematical Society. doi:10.1090/conm/065 (Scholar)
  • –––, 1999, Subsystems of Second Order Arithmetic, Berlin: Springer. (Scholar)
  • Sinaceur, Mohammed-A., 1974, “L’infini et les nombres: Commentaires de R. Dedekind à « Zahlen » La correspondance avec Keferstein”, Revue d’histoire des sciences, 27(3): 251–278. doi:10.3406/rhs.1974.1089
  • Spector, Clifford, 1962, “Provably Recursive Functions of Analysis: A Consistency Proof of Analysis by An Extension of Principles Formulated in Current Intuitionistic Mathematics”, in J.C.E. Dekker (ed.), Recursive Function Theory: Proceedings of the Fifth Symposia in Pure Mathematics, New York, April 6–7, 1961, pp. 1–27. doi:10.1090/pspum/005/0154801 (Scholar)
  • Tait, W.W., 1966, “A Nonconstructive Proof of Gentzen’s Hauptsatz for Second Order Predicate Logic”, Bulletin of the American Mathematical Society, 72(6): 980–983. (Scholar)
  • –––, 1970, “Applications of the Cut Elimination Theorem to Some Subsystems of Classical Analysis”, in Kino, Myhill, and Vesley 1970: 475–488. doi:10.1016/s0049-237x(08)70772-9 (Scholar)
  • –––, 1981, “Finitism”, Journal of Philosophy, 78(9): 524–546. doi:10.2307/2026089 (Scholar)
  • –––, 2002, “Remarks on Finitism”, in Sieg, Sommer and Talcott 2002: 410–419. (Scholar)
  • –––, 2015, “Gentzen’s Original Consistency Proof and the Bar Theorem”, in Kahle and Rathjen 2015: 213–228. doi:10.1007/978-3-319-10103-3_8 (Scholar)
  • Takahashi, Moto-o, 1967, “A Proof of Cut-Elimination in Simple Type Theory”, Journal of the Mathematical Society of Japan, 19(4): 399–410. doi:10.2969/jmsj/01940399 (Scholar)
  • Takeuti, Gaisi, 1953, “On a Generalized Logic Calculus”, Japanese Journal of Mathematics, 24: 149–156. doi:10.4099/jjm1924.23.0_39 (Scholar)
  • –––, 1967, “Consistency Proofs of Subsystems of Classical Analysis”, Annals of Mathematics, 86(2): 299–348. doi:10.2307/1970691 (Scholar)
  • –––, 1975, “Consistency Proofs and Ordinals”, in Diller and Müller 1975: 365–369. doi:10.1007/bfb0079562 (Scholar)
  • –––, 1985, “Proof Theory and Set Theory”, Synthese, 62(2): 255–263. doi:10.1007/bf00486049 (Scholar)
  • –––, 1987, Proof Theory, second edition, Amsterdam: North-Holland. (Scholar)
  • –––, 2003, Memoirs of a Proof Theorist: Gödel and Other Logicians, translated into English by Mariko Yasugi and Nicholas Passell, River Edge, NJ: World Scientific. doi:10.1142/5202 (Scholar)
  • Takeuti, Gaisi and Mariko Yasugi, 1973, “The Ordinals of the Systems of Second Order Arithmetic with the Provably \(\Delta^1_2\)-Comprehension and the \(\Delta^1_2\)-Comprehension Axiom Respectively”, Japanese Journal of Mathematics, 41: 1–67. doi:10.4099/jjm1924.41.0_1 (Scholar)
  • Torretti, Roberto, 1978 [1984], Philosophy of Geometry from Riemann to Poincaré, Dordrecht: D. Reidel. doi:10.1007/978-94-009-9909-1 (Scholar)
  • Troelstra, Anne S. (ed.), 1973, Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, (Lecture Notes in Mathematics, 344), Heidelberg, Berlin: Springer. doi:10.1007/bfb0066739 (Scholar)
  • Troelstra, A.S. and H. Schwichtenberg, 2000, Basic Proof Theory, second edition, Cambridge: Cambridge University Press. doi:10.1017/cbo9781139168717 (Scholar)
  • Turing, A.M., 1936, “On Computable Numbers with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, series 2, 42(1): 230–265. doi:10.1112/plms/s2-42.1.230 (Scholar)
  • –––, 1939, “Systems of Logic Based on Ordinals”, Proceedings of the London Mathematical Society, series 2, 45(2239): 161–228. doi:10.1112/plms/s2-45.1.161 (Scholar)
  • van Atten, Mark, 2007, Brouwer Meets Husserl: On the Phenomenology of Choice Sequences, (Synthese Library, 335), Dordrecht: Springer Netherlands. doi:10.1007/978-1-4020-5087-9 (Scholar)
  • van Heijenoort, Jean (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press (reprinted 1970). (Scholar)
  • Veblen, Oswald, 1908, “Continuous Increasing Functions of Finite and Transfinite Ordinals”, Transactions of the American Mathematics Society, 9(3): 280–292. doi:10.1090/s0002-9947-1908-1500814-9 (Scholar)
  • von Neumann, J., 1927, “Zur Hilbertschen Beweistheorie”, Mathematische Zeitschrift, 26: 1–46. doi:10.1007/bf01475439 (Scholar)
  • von Plato, Jan, 2008, “Gentzen’s Proof of Normalization for Natural Deduction”, Bulletin of Symbolic Logic, 14(2): 240–257. doi:10.2178/bsl/1208442829 (Scholar)
  • –––, 2009, “Gentzen’s logic”, in D.M. Gabbay and J. Woods (eds), Handbook of the History of Logic 5, Logic from Russell to Church, Amsterdam: Elsevier, 667–721. doi:10.1016/s1874-5857(09)70017-2 (Scholar)
  • –––, 2017, Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic and Foundations of Mathematics, Berlin: Springer. doi:10.1007/978-3-319-42120-9 (Scholar)
  • Wainer, S.S., 1970, “A Classification of the Ordinal Recursive Functions”, Archiv für Mathematische Logik und Grundlagenforschung, 13(3–4): 136–153. doi:10.1007/bf01973619 (Scholar)
  • Wang, Hao, 1981, “Some Facts About Kurt Gödel”, Journal of Symbolic Logic, 46(3): 653–659. doi:10.2307/2273764 (Scholar)
  • Weiermann, A., 1996, “How to Characterize Provably Total Functions by Local Predicativity”, Journal of Symbolic Logic, 61(1): 52–69. doi:10.2307/2275597 (Scholar)
  • Weyl, Hermann, 1918, Das Kontinuum, Leipzig: Veit. (Scholar)
  • –––, 1946, “Mathematics and Logic”, American Mathematical Monthly, 53(1): 2–13. doi:10.2307/2306078 (Scholar)
  • Zach, Richard, 1999, “Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic”, Bulletin of Symbolic Logic, 5(3): 331–366. doi:10.2307/421184 (Scholar)
  • –––, 2003, “The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert’s Program”, Synthese, 137(1–2): 211–259. doi:10.1023/a:1026247421383 (Scholar)
  • –––, 2004, “Hilbert’s ‘Verunglückter Beweis’, the First Epsilon Theorem, and Consistency Proofs”, History and Philosophy of Logic, 25(2): 79–94. doi:10.1080/01445340310001606930 (Scholar)
  • Zermelo, E., 1932, “Über Stufen der Quantifikation und die Logik des Unendlichen”, Jahresberichte der Deutschen Mathematiker-Vereinigung, 41: 85–88. (Scholar)
  • Zucker, J.I., 1973, “Iterated Inductive Definitions, Trees, and Ordinals”, in Troelstra 1973: 392–453. doi:10.1007/bfb0066745 (Scholar)

Generated Mon Aug 3 00:53:20 2020