Characterizing the interpretation of set theory in Martin-Löf type theory

DOI10.1016/J.APAL.2005.12.008MaRDI QIDQ2500469zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

axiom of choiceconstructive set theoryformulae-as-classes interpretationMartin-Löf type theory

Mathematics Subject Classification ID

Axiom of choice and related propositions (03E25) Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Other constructive mathematics (03F65)

Recommendations

• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• The generalised type-theoretic interpretation of constructive set theory
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• A construction of non-well-founded sets within Martin-Löf's type theory
• scientific article; zbMATH DE number 3853066
• Realizing Mahlo set theory in type theory
• scientific article; zbMATH DE number 1302058
• scientific article; zbMATH DE number 65535
• Domain interpretations of Martin-Löf's partial type theory

Cites work

• Axiom of Choice and Complementation
• Constructive set theory
• Constructivism in mathematics. An introduction. Volume I
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3668598 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 3494394 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1176133 (Why is no real title available?)
• scientific article; zbMATH DE number 5064954 (Why is no real title available?)
• scientific article; zbMATH DE number 3259043 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• Power set recursion
• Realization of analysis into Explicit Mathematics
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• The formulae-as-classes interpretation of constructive set theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• The strength of some Martin-Löf type theories

Cited in

(32)

• Inaccessibility in constructive set theory and type theory
• The strength of some Martin-Löf type theories
• Realizing Mahlo set theory in type theory
• Non-deterministic inductive definitions
• Kripke models for subtheories of \textsf{CZF}
• CZF does not have the existence property
• The axiom of multiple choice and models for constructive set theory
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• A construction of non-well-founded sets within Martin-Löf's type theory
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• A characterization of ML in many-sorted arithmetic with conditional application
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 1088206 (Why is no real title available?)
• From the weak to the strong existence property
• scientific article; zbMATH DE number 2085163 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• Homotopy type-theoretic interpretations of constructive set theories
• Proof theory of constructive systems: inductive types and univalence
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Computer Science Logic
• A cumulative hierarchy of sets for constructive set theory
• The formulae-as-classes interpretation of constructive set theory
• The generalised type-theoretic interpretation of constructive set theory
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Integrating classical and intuitionistic type theory
• From type theory to setoids and back
• Domain interpretations of Martin-Löf's partial type theory
• Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)

This page was built for publication: Characterizing the interpretation of set theory in Martin-Löf type theory

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