Inaccessibility in constructive set theory and type theory

DOI10.1016/S0168-0072(97)00072-9zbMATH Open0926.03074MaRDI QIDQ1295396FDOQ1295396

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)

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructive set theory
• Title not available (Why is that?)
• The strength of some Martin-Löf type theories
• Title not available (Why is that?)
• Proof-theoretic analysis of KPM
• Ordinal notations based on a weakly Mahlo cardinal
• Title not available (Why is that?)
• Title not available (Why is that?)
• Well-ordering proofs for Martin-Löf type theory
• An information system interpretation of Martin-Löf's partial type theory with universes
• Title not available (Why is that?)
• Extending Martin-Löf type theory by one Mahlo-universe
• A generalization of Mahlo's method for obtaining large cardinal numbers
• Title not available (Why is that?)

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 type theory to setoids and back
• From mathesis universalis to provability, computability, and constructivity
• 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
• Heyting-valued interpretations for constructive set theory
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

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)