Inaccessibility in constructive set theory and type theory

DOI10.1016/S0168-0072(97)00072-9MaRDI QIDQ1295396zbMATH OpenFDO

Authors Michael Rathjen, Edward R. Griffor, Erik Palmgren

Publication date 23 November 1999

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

constructive set theoryconstructivityinaccessible cardinals[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Martin-L%EF%BF%BD%EF%BF%BDf%27s+intuitionistic+type+theory&go=Go Martin-L��f's intuitionistic type theory]Aczel's constructive set theoryinaccessible setsMahlo's \(\pi\)-numbers

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Other constructive mathematics (03F65) Large cardinals (03E55) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Realizing Mahlo set theory in type theory
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Universes in type theory. I. Inaccessibles and Mahlo
• Inaccessible set axioms may have little consistency strength
• Constructive sets in computable sets

Cites work

• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3825796 (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 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1136111 (Why is no real title available?)
• scientific article; zbMATH DE number 783772 (Why is no real title available?)
• scientific article; zbMATH DE number 922612 (Why is no real title available?)
• A generalization of Mahlo's method for obtaining large cardinal numbers
• An information system interpretation of Martin-Löf's partial type theory with universes
• Constructive set theory
• Extending Martin-Löf type theory by one Mahlo-universe
• Ordinal notations based on a weakly Mahlo cardinal
• Proof-theoretic analysis of KPM
• The strength of some Martin-Löf type theories
• Well-ordering proofs for Martin-Löf type theory

Cited in

(18)

• Realizing Mahlo set theory in type theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Inaccessible set axioms may have little consistency strength
• The constructive Hilbert program and the limits of Martin-Löf type theory
• Induction-recursion and initial algebras.
• Dependent products and 1-inaccessible universes
• Proof theory of constructive systems: inductive types and univalence
• Realization of analysis into Explicit Mathematics
• A general formulation of simultaneous inductive-recursive definitions in type theory
• From mathesis universalis to provability, computability, and constructivity
• From type theory to setoids and back
• Types in class set theory and inaccessible cardinals
• A cumulative hierarchy of sets for constructive set theory
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• Large sets in intuitionistic set theory
• Predicativity and constructive mathematics
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• Heyting-valued interpretations for constructive set theory

This page was built for publication: Inaccessibility in constructive set theory and type theory

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