Abstract
Proof theory began in the 1920s as a part of Hilbert’s program, which aimed to secure the foundations of mathematics by modeling infinitary mathematics with formal axiomatic systems and proving those systems consistent using restricted, finitary means. The program thus viewed mathematics as a system of reasoning with precise linguistic norms, governed by rules that can be described and studied in concrete terms. Today such a viewpoint has applications in mathematics, computer science, and the philosophy of mathematics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Avigad, J. (2000). Interpreting classical theories in constructive ones. Journal of Symbolic Logic, 65, 1785–1812.
Avigad, J. (2002). Saturated models of universal theories. Annals of Pure and Applied Logic, 118, 219–234.
Avigad, J. (2003). Number theory and elementary arithmetic. Philosophia Mathematica, 11, 257–284.
Avigad, J. (2004). Forcing in proof theory. Bulletin of Symbolic Logic, 10, 305–333.
Avigad, J., & Feferman, S. Gödel’s functional (“Dialectica”) interpretation. In [9] (pp. 337–405).
Barwise, J. (Ed.), (1977). The handbook of mathematical logic. Amsterdam: North-Holland. [Contains a number of introductory articles on proof theory and related topics.]
Beeson, M. J. (1985). Foundations of constructive mathematics. Berlin: Springer.
Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development: Coq’Art: The calculus of inductive constructions. Berlin: Springer.
Buss, S. R. (Ed.). (1998). The handbook of proof theory. Amsterdam: North-Holland. [Provides a definitive overview of the subject.]
Buss, S. R. An introduction to proof theory. In Buss [9] (pp. 1–78).
Buss, S. R. First-order proof theory of arithmetic. In Buss [9] (pp. 79–147)
Feferman, S. Theories of finite type related to mathematical practice. In Barwise [6] (pp. 913–971).
Friedman, H. (to appear). Boolean relation theory and incompleteness. Cambridge University Press.
Goodstein, R. L. (1957). Recursive number theory: A development of recursive arithmetic in a logic-free equation calculus. Amsterdam: North-Holland.
Hájek, P., & Pudlák, P. (1993). Metamathematics of first-order arithmetic. Berlin: Springer.
Harrison, J. (2009). Handbook of practical logic and automated reasoning. Cambridge: Cambridge University Press.
Hilbert, D. (1922). Neubegründung der Mathematik. Erste Mitteilung. Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, 1, 157–177. Translated by Ewald, W. (1996). As the new grounding of mathematics. First report. In Ewald, W. (Ed.), From Kant to Hilbert: A source book in the foundations of mathematics (Vol. 2, pp. 1115–1134) Oxford: Clarendon.
Kaye, R. (1991). Models of Peano arithmetic. Oxford: Clarendon.
Keisler, H. J. (2006). Nonstandard arithmetic and reverse mathematics. Bulletin of Symbolic Logic, 12, 100–125.
Kohlenbach, U. (2008). Applied proof theory: Proof interpretations and their use in mathematics. Berlin: Springer. [An introduction to proof mining.]
Krajíček, J. (1995). Bounded arithmetic, propositional logic, and complexity theory. Cambridge: Cambridge University Press.
Kunen, K. (1980). Set theory: An introduction to independence proofs. Amsterdam: North-Holland.
Negri, S., & von Plato, J. (2008). Structural proof theory. Cambridge: Cambridge University Press.
Paris, J., & Harrington, L. A mathematical incompleteness in Peano arithmetic. In [6] (pp. 1133–1142)
Pierce, B. (2004). Advanced topics in types and programming languages. Cambridge, MA: MIT Press.
Pohlers, W. Subsystems of set theory and second order number theory. In Buss [9] (pp. 209–335).
Pohlers, W. (2009). Proof theory: The first step into impredicativity. Berlin: Springer. [An introduction to ordinal analysis.]
Pudlák, P. The lengths of proofs. In [9] (pp. 547–637).
Robinson, J. A., & Voronkov, A. (Eds.). (2001). Handbook of automated reasoning (Vols. 1 and 2). Amsterdam/New York: Elsevier; Cambridge: MIT Press.
Sambin, G. (Ed.). (1998). Twenty-five years of constructive type theory. Oxford: Clarenden.
Schwichtenberg, H. Proof theory: Some aspects of cut-elimination. In Barwise [6] (pp. 867–895).
Segerlind, N. (2007). The complexity of propositional proofs. Bulletin of Symbolic Logic, 13, 417–481.
Sieg, W. (1985). Fragments of arithmetic. Annals of Pure and Applied Logic, 28, 33–72.
Sieg, W. (1999). Hilbert’s programs: 1917–1922. Bulletin of Symbolic Logic, 5, 1–44.
Simpson, S. G. (1999). Subsystems of second-order arithmetic. Berlin: Springer
Takeuti, G. (1987). Proof theory (2nd ed.). Amsterdam: North-Holland.
Troelstra, A. S. Realizability. In [9] (pp. 407–473).
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory (2nd ed.). Cambridge: Cambridge University Press. [An introductory text.]
Troelstra, A. S., & van Dalen, D. (1988). Constructivism in mathematics: An introduction (vols. 1 and 2). Amsterdam: North-Holland. [An overview of constructive mathematics.]
Urquhart, A. (1995). The complexity of propositional proofs. Bulletin of Symbolic Logic, 1, 425–467.
Wiedijk, F. (2006). The seventeen provers of the world. Berlin: Springer.
Zach, R. (2006). Hilbert’s program then and now. In D. Jacquette (Ed.), Philosophy of logic (pp. 411–447). Amsterdam: Elsevier. [A nice historical overview.]
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Avigad, J. (2018). Proof Theory. In: Hansson, S., Hendricks, V. (eds) Introduction to Formal Philosophy. Springer Undergraduate Texts in Philosophy. Springer, Cham. https://doi.org/10.1007/978-3-319-77434-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-77434-3_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77433-6
Online ISBN: 978-3-319-77434-3
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)