Proof Theory of Constructive Systems: Inductive Types and Univalence

DOI10.1007/978-3-319-63334-3_14zbMath1429.03213arXiv1610.02191OpenAlexW2529868088MaRDI QIDQ5214792

Michael Rathjen

Publication date: 5 February 2020

Published in: Outstanding Contributions to Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1610.02191

zbMATH Keywords

proof-theoretic strengthMartin-Löf type theoryexplicit mathematicsunivalence axiomconstructive Zermelo-Fraenkel set theory

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Models of arithmetic and set theory (03C62) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Type theory (03B38)

Related Items

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ A New Foundational Crisis in Mathematics, Is It Really Happening? ⋮ On Relating Theories: Proof-Theoretical Reduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Proof-theoretic analysis of KPM
• The constructive Hilbert program and the limits of Martin-Löf type theory
• Proof-theoretical analysis: Weak systems of functions and classes
• Monotone inductive definitions in a constructive theory of functions and classes
• Goodman's theorem and beyond
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Constructivism in mathematics. An introduction. Volume II
• Well-ordering proofs for Martin-Löf type theory
• Inaccessibility in constructive set theory and type theory
• The strength of some Martin-Löf type theories
• On the proof-theoretic strength of monotone induction in explicit mathematics
• Extending Martin-Löf type theory by one Mahlo-universe
• Inaccessible set axioms may have little consistency strength
• The strength of Martin-Löf type theory with a superuniverse. I
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
• Constructive set theory
• Axiom of Choice and Complementation
• The theory of the Gödel functionals
• Relativized realizability in intuitionistic arithmetic of all finite types
• Explicit mathematics with the monotone fixed point principle
• Explicit mathematics with the monotone fixed point principle. II: Models
• Conservativity of equality reflection over intensional type theory
• A well-ordering proof for Feferman's theoryT 0
• Monotone inductive definitions in explicit mathematics
• On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics
• On the intuitionistic strength of monotone inductive definitions
• Systems of predicative analysis
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Systems of predicative analysis, II: Representations of ordinals
• A formulation of the simple theory of types
• Universes in explicit mathematics
• The strength of Martin-Löf type theory with a superuniverse. II
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms