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

DOI10.1007/s11229-004-6208-4zbMath1108.03056OpenAlexW4234140767MaRDI 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

surveyconstructive type theoryHilbert's programsubsystems of analysisproof-theoretic investigations

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) History of mathematical logic and foundations (03-03) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (7)

Error and Predicativity ⋮ On Relating Theories: Proof-Theoretical Reduction ⋮ A constructive type-theoretical formalism for the interpretation of subatomically sensitive natural language constructions ⋮ Constructibility and Geometry ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Feferman on Set Theory: Infinity up on Trial ⋮ Predicativity and constructive mathematics

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

This page was built for publication: The constructive Hilbert program and the limits of Martin-Löf type theory