Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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
J. Barwise: Admissible Sets and Structures (Springer, Berlin 1975).
P. Bernays: Hilbert, David, Encyclopedia of Philosophy, Vol. 3 (Macmillan and Free Press, New York, 1967) 496–504.
E. Bishop: Foundations of Constructive Analysis (McGraw-Hill, New York, 1967).
L.E.J. Brouwer: Weten, willen, spreken (Dutch). Euclides 9 (1933) 177–193.
D.K. Brown: Functional Analysis in Weak Subsystems of Second Order Arithmetic. Ph.D. Thesis (Pennsylvania State University, University Park,1987).
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.
W. Buchholz, S. Feferman, W. Pohlers, W. Sieg: Iterated Inductive Definitions and Subsystems of Analysis (Springer, Berlin, 1981).
H.B. Curry, R. Feys: Combinatory Logic, vol. I. (North-holland, Amsterdam, 1958)
R. Diestel: Graph Theory (Springer, New York-Berlin-Heidelberg, 1997).
M. Dummett: The philosophical basis of intuitionistic logic. In: H.E. Rose et al.(eds.): Logic Colloquium ’73 (North-Holland, Amsterdam, 1973) 5–40.
M. Dummett: Elements of Intuitionism. 2nd edition (Clarendon Press, Oxford, 2000).
S. Feferman: A Language and Axioms for Explicit Mathematics, Lecture Notes in Math. 450 (Springer, Berlin, 1975), 87–139.
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.
S. Feferman: Why a little bit goes a long way. In: S. Feferman: In the Light of Logic(Oxford University Press, Oxford, 1998).
S. Feferman: Weyl vindicated: “Das Kontinuum" 70 years later. In: S. Feferman: In the Light of Logic(Oxford University Press, Oxford, 1998).
S. Feferman, H. Friedman, P. Maddy, J. Steel: Does mathematics need new axioms? Bulletin of Symbolic Logic 6 (2000) 401–446.
H. Friedman: personal communication to L. Harrington (1977).
H. Friedman, N. Robertson, P. Seymour: The metamathematics of the graph minor theorem, Contemporary Mathematics 65 (1987) 229–261.
G. Gentzen: Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift 39 (1935) 176-210, 405–431.
G. Gentzen: Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen 112 (1936) 493–565.
K. Gödel: The present situation in the foundations of mathematics. In: Collected Works, vol. III (Oxford University Press, New York, 1995).
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).
D. Hilbert and P. Bernays: Grundlagen der Mathematik II (Springer, Berlin, 1938).
P. Hinman: Recursion-theoretic hierarchies (Springer, Berlin, 1978).
W.A. Howard: The Formulae-as-Types Notion of Construction. (Privately circulated notes, 1969).
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).
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.
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.
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).
P. Martin-Löf: Intuitionistic Type Theory, (Bibliopolis, Naples, 1984).
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.
J. Myhill: Constructive Set Theory, J. Symbolic Logic 40 (1975) 347–382.
B. Nordström, K. Petersson and J.M. Smith: Programming in Martin–Löf’s Type Theory, (Clarendon Press, Oxford, 1990).
E. Palmgren: An information system interpretation of Martin-Löf’s partial type theory with universes, Information and Computation1106 (1993) 26–60.
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.
J. Paris, L. Harrington: A mathematical incompleteness in Peano arithmetic. In: J. Barwise (ed.): Handbook of Mathematical Logic (North Holland, Amsterdam, 1977) 1133–1142.
D. Prawitz: Meaning and proofs: on the conflict between classical and intuitionistic logic. Theoria 43 (1977) 11–40.
M. Rathjen: Proof-Theoretic Analysis of KPM, Arch. Math. Logic 30 (1991) 377–403.
M. Rathjen: The strength of some Martin–Löf type theories. Preprint, Department of Mathematics, Ohio State University (1993) 39 pp.
M. Rathjen: Proof theory of reflection. Annals of Pure and Applied Logic 68 (1994) 181–224.
M. Rathjen: The recursively Mahlo property in second order arithmetic. Mathematical Logic Quarterly 42 (1996) 59–66.
M. Rathjen, E. Palmgren: Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic 94 (1998) 181–200.
M. Rathjen: Explicit mathematics with the monotone fixed point principle. II: Models. Journal of Symbolic Logic 64 (1999) 517–550.
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.
M. Rathjen: Realizing Mahlo set theory in type theory. Archive for Mathematical Logic 42 (2003) 89–101.
M. Rathjen: The constructive Hilbert programme and the limits of Martin-Löf type theory Synthese 147 (2005) 81–120.
B. Russell: Mathematical logic as based on the theory of types. American Journal of Mathematics 30 (1908) 222–262.
T. Setzer: Proof theoretical strength of Martin–Löf type theory with W–type and one universe (Thesis, University of Munich, 1993).
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.
A. Setzer: Extending Martin-Löf type theory by one Mahlo-universe. Archive for Mathematical Logic (2000) 39: 155–181.
S. Simpson: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume, Archiv f. Math. Logik 25 (1985) 45–65.
S. Simpson: Partial realizations of Hilbert’s program. Journal of Symbolic Logic 53 (1988) 349–363.
S. Simpson: Subsystems of second order arithmetic (Springer, Berlin, 1999).
W. Tait: Finitism. Journal of Philosophy 78 (1981) 524–546.
B. van der Waerden: Moderne Algebra I/II (Springer, Berlin, 1930/31)
H. Weyl: Philosophy of Mathematics and Natural Sciences. (Princeton University Press, Princeton, 1949)
W.H. Woodin: Large cardinal axioms and independence: The continuum problem revisited, The Mathematical Intelligencer vol. 16, No. 3 (1994) 31–35.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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
DOI: https://doi.org/10.1007/978-1-4020-8926-8_17
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-8925-1
Online ISBN: 978-1-4020-8926-8
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)