Proof theory of constructive systems: inductive types and univalence

DOI10.1007/978-3-319-63334-3_14zbMATH Open1429.03213arXiv1610.02191OpenAlexW2529868088MaRDI QIDQ5214792FDOQ5214792

Authors: Michael Rathjen 

Publication date: 5 February 2020

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

Abstract: In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky's univalence axiom. A further goal is to investigate the strength of intuitionistic theories of generalized inductive definitions in the framework of intuitionistic explicit mathematics that lie beyond the reach of Martin-Lof type theory.

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

Recommendations

• Constructive set theory with operations
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
• scientific article; zbMATH DE number 2247249
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• The constructive Hilbert program and the limits of Martin-Löf type theory

zbMATH Keywords

univalence axiomproof-theoretic strengthexplicit mathematicsconstructive Zermelo-Fraenkel set theoryMartin-Löf type theory

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (13)

• Inaccessible set axioms may have little consistency strength
• A New Foundational Crisis in Mathematics, Is It Really Happening?
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Bar induction is compatible with constructive type theory
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
• On Relating Theories: Proof-Theoretical Reduction
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• Proof-search in type-theoretic languages: An introduction
• Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

This page was built for publication: Proof theory of constructive systems: inductive types and univalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5214792)