The constructive Hilbert program and the limits of Martin-Löf type theory

DOI10.1007/s11229-004-6208-4zbMath1108.03056MaRDI QIDQ813417

Michael Rathjen

Publication date: 8 February 2006

Published in: Synthese (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11229-004-6208-4

zbMATH Keywords

survey; constructive type theory; Hilbert's program; subsystems of analysis; proof-theoretic investigations

Mathematics Subject Classification ID

03A05: Philosophical and critical aspects of logic and foundations

03-03: History of mathematical logic and foundations

03F35: Second- and higher-order arithmetic and fragments

03F50: Metamathematics of constructive systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-theoretic analysis of KPM
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Well-ordering proofs for Martin-Löf type theory
• Inaccessibility in constructive set theory and type theory
• An information system interpretation of Martin-Löf's partial type theory with universes
• Taking formalism seriously
• Proof theory of reflection
• Realizing Mahlo set theory in type theory
• Extending Martin-Löf type theory by one Mahlo-universe
• Which set existence axioms are needed to prove the separable Hahn-Banach theorem?
• Untersuchungen über das logische Schliessen. I
• Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees
• Partial realizations of Hilbert's program
• Hilbert's program relativized; Proof-theoretical and foundational reductions
• Constructive set theory
• Explicit mathematics with the monotone fixed point principle. II: Models
• The Recursively Mahlo Property in Second Order Arithmetic
• Does Mathematics Need New Axioms?
• The consistency of arithmetics