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)
- –––, 2020, Ordinal Analysis with an
Introduction to Proof Theory, Singapore: Springer.
doi.org/10.1007/978-981-15-6459-8 (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.
(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, William A., 1963, “The Axiom of Choice
(\(\Sigma^1_1\)-\(\mathrm{AC}_{01}\)), Bar Induction and Bar
Recursion”, in Reports of the Seminar on the Foundations of
Analysis, Stanford,(mimeographed), Mathematical Sciences Library,
Stanford University, 2.1–2.44. (Scholar)
- –––, 1968, “Functional Interpretation 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, Georg, 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)
- Reck, Erich and Georg Schiemer (eds), 2020, “The Prehistory of Mathematical Structuralism”, Oxford: Oxford University Press. (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)
- –––, 2020, “Methodological Frames: Paul
Bernays, Mathematical Structuralism, and Proof Theory”, in: Reck
and Schiemer 2020: 352–382. (Scholar)
- Sieg, Wilfried and Farzaneh Derakhshan, 2021,
“Human-centered automated proof search”, Journal of
Automated Reasoning, 65: 1153–1190. (Scholar)
- Sieg, Wilfried and Rebecca Morris, 2018, “Dedekind’s
Structuralism: Creating Concepts and Deriving Theorems”, in:
Logic, Philosophy of Mathematics, and Their History: Essays in
Honor of W.W. Tait, London: College Publication,
251–301. (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)
- –––, 2014, “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)