Characterizing the interpretation of set theory in Martin-Löf type theory
From MaRDI portal
Publication:2500469
DOI10.1016/j.apal.2005.12.008zbMath1103.03050OpenAlexW2060433450MaRDI QIDQ2500469
Michael Rathjen, Sergei Tupailo
Publication date: 16 August 2006
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2005.12.008
Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65) Second- and higher-order arithmetic and fragments (03F35) Axiom of choice and related propositions (03E25)
Related Items
From type theory to setoids and back, CZF does not have the existence property, Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience, Non-deterministic inductive definitions, From the weak to the strong existence property, Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory, A cumulative hierarchy of sets for constructive set theory, Homotopy type-theoretic interpretations of constructive set theories, Kripke models for subtheories of \textsf{CZF}, Proof Theory of Constructive Systems: Inductive Types and Univalence, Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
Cites Work
- The lack of definable witnesses and provably recursive functions in intuitionistic set theories
- Constructivism in mathematics. An introduction. Volume I
- The strength of some Martin-Löf type theories
- Power set recursion
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- Constructive set theory
- Axiom of Choice and Complementation
- Realization of analysis into Explicit Mathematics
- The disjunction and related properties for constructive Zermelo-Fraenkel set theory
- 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
