Skip to main content
SpringerLink
Log in

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

  • Chapter
Logicism, Intuitionism, and Formalism

Part of the book series: Synthese Library ((SYLI,volume 341))

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 229.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 299.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 299.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. ml.kva.se/preprints/archive2000-2001.php

    Google Scholar 

  2. J. Barwise: Admissible Sets and Structures (Springer, Berlin 1975).

    MATH  Google Scholar 

  3. P. Bernays: Hilbert, David, Encyclopedia of Philosophy, Vol. 3 (Macmillan and Free Press, New York, 1967) 496–504.

    Google Scholar 

  4. E. Bishop: Foundations of Constructive Analysis (McGraw-Hill, New York, 1967).

    MATH  Google Scholar 

  5. L.E.J. Brouwer: Weten, willen, spreken (Dutch). Euclides 9 (1933) 177–193.

    Google Scholar 

  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. 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.

    Article  MATH  MathSciNet  Google Scholar 

  8. W. Buchholz, S. Feferman, W. Pohlers, W. Sieg: Iterated Inductive Definitions and Subsystems of Analysis (Springer, Berlin, 1981).

    MATH  Google Scholar 

  9. H.B. Curry, R. Feys: Combinatory Logic, vol. I. (North-holland, Amsterdam, 1958)

    MATH  Google Scholar 

  10. R. Diestel: Graph Theory (Springer, New York-Berlin-Heidelberg, 1997).

    MATH  Google Scholar 

  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. M. Dummett: Elements of Intuitionism. 2nd edition (Clarendon Press, Oxford, 2000).

    MATH  Google Scholar 

  13. S. Feferman: A Language and Axioms for Explicit Mathematics, Lecture Notes in Math. 450 (Springer, Berlin, 1975), 87–139.

    Google Scholar 

  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. 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. 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. S. Feferman, H. Friedman, P. Maddy, J. Steel: Does mathematics need new axioms? Bulletin of Symbolic Logic 6 (2000) 401–446.

    Article  MATH  MathSciNet  Google Scholar 

  18. H. Friedman: personal communication to L. Harrington (1977).

    Google Scholar 

  19. H. Friedman, N. Robertson, P. Seymour: The metamathematics of the graph minor theorem, Contemporary Mathematics 65 (1987) 229–261.

    MathSciNet  Google Scholar 

  20. G. Gentzen: Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift 39 (1935) 176-210, 405–431.

    Article  MathSciNet  Google Scholar 

  21. G. Gentzen: Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen 112 (1936) 493–565.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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).

    Article  MathSciNet  Google Scholar 

  24. D. Hilbert and P. Bernays: Grundlagen der Mathematik II (Springer, Berlin, 1938).

    Google Scholar 

  25. P. Hinman: Recursion-theoretic hierarchies (Springer, Berlin, 1978).

    MATH  Google Scholar 

  26. W.A. Howard: The Formulae-as-Types Notion of Construction. (Privately circulated notes, 1969).

    Google Scholar 

  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. 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. 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. 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. P. Martin-Löf: Intuitionistic Type Theory, (Bibliopolis, Naples, 1984).

    MATH  Google Scholar 

  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.

    MATH  MathSciNet  Google Scholar 

  33. J. Myhill: Constructive Set Theory, J. Symbolic Logic 40 (1975) 347–382.

    Article  MATH  MathSciNet  Google Scholar 

  34. B. Nordström, K. Petersson and J.M. Smith: Programming in Martin–Löf’s Type Theory, (Clarendon Press, Oxford, 1990).

    MATH  Google Scholar 

  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. 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. 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. D. Prawitz: Meaning and proofs: on the conflict between classical and intuitionistic logic. Theoria 43 (1977) 11–40.

    MathSciNet  Google Scholar 

  39. M. Rathjen: Proof-Theoretic Analysis of KPM, Arch. Math. Logic 30 (1991) 377–403.

    Article  MATH  MathSciNet  Google Scholar 

  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. M. Rathjen: Proof theory of reflection. Annals of Pure and Applied Logic 68 (1994) 181–224.

    Article  MATH  MathSciNet  Google Scholar 

  42. M. Rathjen: The recursively Mahlo property in second order arithmetic. Mathematical Logic Quarterly 42 (1996) 59–66.

    Article  MATH  MathSciNet  Google Scholar 

  43. M. Rathjen, E. Palmgren: Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic 94 (1998) 181–200.

    Article  MATH  MathSciNet  Google Scholar 

  44. M. Rathjen: Explicit mathematics with the monotone fixed point principle. II: Models. Journal of Symbolic Logic 64 (1999) 517–550.

    Article  MATH  MathSciNet  Google Scholar 

  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. M. Rathjen: Realizing Mahlo set theory in type theory. Archive for Mathematical Logic 42 (2003) 89–101.

    Article  MATH  MathSciNet  Google Scholar 

  47. M. Rathjen: The constructive Hilbert programme and the limits of Martin-Löf type theory Synthese 147 (2005) 81–120.

    Article  MATH  MathSciNet  Google Scholar 

  48. B. Russell: Mathematical logic as based on the theory of types. American Journal of Mathematics 30 (1908) 222–262.

    Article  MathSciNet  Google Scholar 

  49. T. Setzer: Proof theoretical strength of Martin–Löf type theory with W–type and one universe (Thesis, University of Munich, 1993).

    MATH  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  51. A. Setzer: Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic (2000) 39: 155–181.

    Article  MATH  MathSciNet  Google Scholar 

  52. S. Simpson: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume, Archiv f. Math. Logik 25 (1985) 45–65.

    Article  MATH  MathSciNet  Google Scholar 

  53. S. Simpson: Partial realizations of Hilbert’s program. Journal of Symbolic Logic 53 (1988) 349–363.

    Article  MATH  MathSciNet  Google Scholar 

  54. S. Simpson: Subsystems of second order arithmetic (Springer, Berlin, 1999).

    MATH  Google Scholar 

  55. W. Tait: Finitism. Journal of Philosophy 78 (1981) 524–546.

    Article  Google Scholar 

  56. B. van der Waerden: Moderne Algebra I/II (Springer, Berlin, 1930/31)

    Google Scholar 

  57. H. Weyl: Philosophy of Mathematics and Natural Sciences. (Princeton University Press, Princeton, 1949)

    Google Scholar 

  58. W.H. Woodin: Large cardinal axioms and independence: The continuum problem revisited, The Mathematical Intelligencer vol. 16, No. 3 (1994) 31–35.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Pure Mathematics, University of Leeds, Leeds LS2 9JT, UK

    Michael Rathjen

Authors
  1. Michael Rathjen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. Historical, Philosophical and Religious Studies, Umeå University, SE-901 87 Umeå, Sweden

    Sten Lindström

  2. Department of Mathematics, Uppsala University, Box 480, 751 06 Uppsala, Sweden

    Erik Palmgren  & Viggo Stoltenberg-Hansen  & 

  3. Department of Philosophy, Uppsala University, Box 627, 751 26 Uppsala, Sweden

    Krister Segerberg

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Rathjen, M. (2009). The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory. In: Lindström, S., Palmgren, E., Segerberg, K., Stoltenberg-Hansen, V. (eds) Logicism, Intuitionism, and Formalism. Synthese Library, vol 341. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-8926-8_17

Download citation

Publish with us

Policies and ethics

Search

Navigation