The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory

  • Michael Rathjen
Part of the Synthese Library book series (SYLI, volume 341)


Type Theory Elimination Rule Peano Arithmetic Introduction Rule Universe Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Aczel, M. Rathjen: Notes on constructive set theory, Technical Report 40, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences, 2001). http://www. Google Scholar
  2. 2.
    J. Barwise: Admissible Sets and Structures (Springer, Berlin 1975).zbMATHGoogle Scholar
  3. 3.
    P. Bernays: Hilbert, David, Encyclopedia of Philosophy, Vol. 3 (Macmillan and Free Press, New York, 1967) 496–504.Google Scholar
  4. 4.
    E. Bishop: Foundations of Constructive Analysis (McGraw-Hill, New York, 1967).zbMATHGoogle Scholar
  5. 5.
    L.E.J. Brouwer: Weten, willen, spreken (Dutch). Euclides 9 (1933) 177–193.Google Scholar
  6. 6.
    D.K. Brown: Functional Analysis in Weak Subsystems of Second Order Arithmetic. Ph.D. Thesis (Pennsylvania State University, University Park,1987).Google Scholar
  7. 7.
    D.K. Brown, S. Simpson: Which set existence axioms are needed to prove the separable Hahn-Banach theorem? Annals of Pure and Applied Logic 31 (1986) 123–144.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    W. Buchholz, S. Feferman, W. Pohlers, W. Sieg: Iterated Inductive Definitions and Subsystems of Analysis (Springer, Berlin, 1981).zbMATHGoogle Scholar
  9. 9.
    H.B. Curry, R. Feys: Combinatory Logic, vol. I. (North-holland, Amsterdam, 1958)zbMATHGoogle Scholar
  10. 10.
    R. Diestel: Graph Theory (Springer, New York-Berlin-Heidelberg, 1997).zbMATHGoogle Scholar
  11. 11.
    M. Dummett: The philosophical basis of intuitionistic logic. In: H.E. Rose et al.(eds.): Logic Colloquium ’73 (North-Holland, Amsterdam, 1973) 5–40.Google Scholar
  12. 12.
    M. Dummett: Elements of Intuitionism. 2nd edition (Clarendon Press, Oxford, 2000).zbMATHGoogle Scholar
  13. 13.
    S. Feferman: A Language and Axioms for Explicit Mathematics, Lecture Notes in Math. 450 (Springer, Berlin, 1975), 87–139.Google Scholar
  14. 14.
    S. Feferman: Constructive theories of functions and classes. In: Boffa, M., van Dalen, D., McAloon, K. (eds.), Logic Colloquium ’78 (North-Holland, Amsterdam, 1979) 159–224.Google Scholar
  15. 15.
    S. Feferman: Why a little bit goes a long way. In: S. Feferman: In the Light of Logic(Oxford University Press, Oxford, 1998).Google Scholar
  16. 16.
    S. Feferman: Weyl vindicated: “Das Kontinuum" 70 years later. In: S. Feferman: In the Light of Logic(Oxford University Press, Oxford, 1998).Google Scholar
  17. 17.
    S. Feferman, H. Friedman, P. Maddy, J. Steel: Does mathematics need new axioms? Bulletin of Symbolic Logic 6 (2000) 401–446.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    H. Friedman: personal communication to L. Harrington (1977).Google Scholar
  19. 19.
    H. Friedman, N. Robertson, P. Seymour: The metamathematics of the graph minor theorem, Contemporary Mathematics 65 (1987) 229–261.MathSciNetGoogle Scholar
  20. 20.
    G. Gentzen: Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift 39 (1935) 176-210, 405–431.CrossRefMathSciNetGoogle Scholar
  21. 21.
    G. Gentzen: Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen 112 (1936) 493–565.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    K. Gödel: The present situation in the foundations of mathematics. In: Collected Works, vol. III (Oxford University Press, New York, 1995).Google Scholar
  23. 23.
    D. Hilbert: Über das Unendliche. Mathematische Annalen 95 (1926) 161–190. English translation In: J. van Heijenoort (ed.): From Frege to Gödel. A Source Book in Mathematical Logic, 1897–1931.(Harvard University Press, Cambridge, Mass.,1967).CrossRefMathSciNetGoogle Scholar
  24. 24.
    D. Hilbert and P. Bernays: Grundlagen der Mathematik II (Springer, Berlin, 1938).Google Scholar
  25. 25.
    P. Hinman: Recursion-theoretic hierarchies (Springer, Berlin, 1978).zbMATHGoogle Scholar
  26. 26.
    W.A. Howard: The Formulae-as-Types Notion of Construction. (Privately circulated notes, 1969).Google Scholar
  27. 27.
    G. Jäger and W. Pohlers: Eine beweistheoretische Untersuchung von Δ12 –CA+ BI und verwandter Systeme, Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch–Naturwissenschaftliche Klasse (1982).Google Scholar
  28. 28.
    G. Kreisel: Ordinal logics and the characterization of informal concepts of proof. In: Proceedings of the 1958 International Congress of Mathematicians, (Edinburgh, 1960)289–299.Google Scholar
  29. 29.
    P. Martin-Löf: An intuitionistic theory of types: predicative part. In: H.E. Rose and J. Sheperdson (eds.): Logic Colloquium ’73 (North-Holland, Amsterdam, 1975) 73–118.Google Scholar
  30. 30.
    P. Martin-Löf: Constructive mathematics and computer programming. In: L.J. Cohen, J. Los, H. Pfeiffer, K.-P. Podewski: LMPS IV (North-Holland, Amsterdam, 1982).Google Scholar
  31. 31.
    P. Martin-Löf: Intuitionistic Type Theory, (Bibliopolis, Naples, 1984).zbMATHGoogle Scholar
  32. 32.
    P. Martin-Löf: On the meanings of the logical constants and the justifications of the logical laws, Nordic Journal of Philosophical Logic 1 (1996) 11–60.zbMATHMathSciNetGoogle Scholar
  33. 33.
    J. Myhill: Constructive Set Theory, J. Symbolic Logic 40 (1975) 347–382.zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    B. Nordström, K. Petersson and J.M. Smith: Programming in Martin–Löf’s Type Theory, (Clarendon Press, Oxford, 1990).zbMATHGoogle Scholar
  35. 35.
    E. Palmgren: An information system interpretation of Martin-Löf’s partial type theory with universes, Information and Computation1106 (1993) 26–60.Google Scholar
  36. 36.
    E. Palmgren: On universes in type theory. In: G. Sambin, J. smith (eds.): Twenty-five Years of Type Theory (Oxford University Press, Oxford, 1998) 191–204.Google Scholar
  37. 37.
    J. Paris, L. Harrington: A mathematical incompleteness in Peano arithmetic. In: J. Barwise (ed.): Handbook of Mathematical Logic (North Holland, Amsterdam, 1977) 1133–1142.Google Scholar
  38. 38.
    D. Prawitz: Meaning and proofs: on the conflict between classical and intuitionistic logic. Theoria 43 (1977) 11–40.MathSciNetGoogle Scholar
  39. 39.
    M. Rathjen: Proof-Theoretic Analysis of KPM, Arch. Math. Logic 30 (1991) 377–403.zbMATHCrossRefMathSciNetGoogle Scholar
  40. 40.
    M. Rathjen: The strength of some Martin–Löf type theories. Preprint, Department of Mathematics, Ohio State University (1993) 39 pp.Google Scholar
  41. 41.
    M. Rathjen: Proof theory of reflection. Annals of Pure and Applied Logic 68 (1994) 181–224.zbMATHCrossRefMathSciNetGoogle Scholar
  42. 42.
    M. Rathjen: The recursively Mahlo property in second order arithmetic. Mathematical Logic Quarterly 42 (1996) 59–66.zbMATHCrossRefMathSciNetGoogle Scholar
  43. 43.
    M. Rathjen, E. Palmgren: Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic 94 (1998) 181–200.zbMATHCrossRefMathSciNetGoogle Scholar
  44. 44.
    M. Rathjen: Explicit mathematics with the monotone fixed point principle. II: Models. Journal of Symbolic Logic 64 (1999) 517–550.zbMATHCrossRefMathSciNetGoogle Scholar
  45. 45.
    M. Rathjen: The superjump in Martin-Löf type theory. In: S. Buss, P. Hajek, P. Pudlak (eds.): Logic Colloquium ’98, Lecture Notes in Logic 13. (Association for Symbolic Logic, 2000) 363–386.Google Scholar
  46. 46.
    M. Rathjen: Realizing Mahlo set theory in type theory. Archive for Mathematical Logic 42 (2003) 89–101.zbMATHCrossRefMathSciNetGoogle Scholar
  47. 47.
    M. Rathjen: The constructive Hilbert programme and the limits of Martin-Löf type theory Synthese 147 (2005) 81–120.zbMATHCrossRefMathSciNetGoogle Scholar
  48. 48.
    B. Russell: Mathematical logic as based on the theory of types. American Journal of Mathematics 30 (1908) 222–262.CrossRefMathSciNetGoogle Scholar
  49. 49.
    T. Setzer: Proof theoretical strength of Martin–Löf type theory with W–type and one universe (Thesis, University of Munich, 1993).zbMATHGoogle Scholar
  50. 50.
    A. Setzer: A well-ordering proof for the proof theoretical strength of Martin-Löf type theory, Annals of Pure and Applied Logic 92 (1998) 113–159.zbMATHCrossRefMathSciNetGoogle Scholar
  51. 51.
    A. Setzer: Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic (2000) 39: 155–181.zbMATHCrossRefMathSciNetGoogle Scholar
  52. 52.
    S. Simpson: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume, Archiv f. Math. Logik 25 (1985) 45–65.zbMATHCrossRefMathSciNetGoogle Scholar
  53. 53.
    S. Simpson: Partial realizations of Hilbert’s program. Journal of Symbolic Logic 53 (1988) 349–363.zbMATHCrossRefMathSciNetGoogle Scholar
  54. 54.
    S. Simpson: Subsystems of second order arithmetic (Springer, Berlin, 1999).zbMATHGoogle Scholar
  55. 55.
    W. Tait: Finitism. Journal of Philosophy 78 (1981) 524–546.CrossRefGoogle Scholar
  56. 56.
    B. van der Waerden: Moderne Algebra I/II (Springer, Berlin, 1930/31)Google Scholar
  57. 57.
    H. Weyl: Philosophy of Mathematics and Natural Sciences. (Princeton University Press, Princeton, 1949)Google Scholar
  58. 58.
    W.H. Woodin: Large cardinal axioms and independence: The continuum problem revisited, The Mathematical Intelligencer vol. 16, No. 3 (1994) 31–35.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  • Michael Rathjen
    • 1
  1. 1.Department of Pure MathematicsUniversity of LeedsLeeds LS2 9JT

Personalised recommendations