Inaccessibility in constructive set theory and type theory

DOI10.1016/S0168-0072(97)00072-9zbMath0926.03074MaRDI QIDQ1295396

Michael Rathjen, Erik Palmgren, Edward R. Griffor

Publication date: 23 November 1999

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

zbMATH Keywords

constructive set theoryconstructivityinaccessible cardinalsMartin-Löf's intuitionistic type theoryAczel's constructive set theoryinaccessible setsMahlo's \(\pi\)-numbers

Mathematics Subject Classification ID

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

Related Items

Inaccessible set axioms may have little consistency strength ⋮ From type theory to setoids and back ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Dependent products and 1-inaccessible universes ⋮ Realization of analysis into Explicit Mathematics ⋮ Induction-recursion and initial algebras. ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ A cumulative hierarchy of sets for constructive set theory ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ 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 ⋮ A general formulation of simultaneous inductive-recursive definitions in type theory ⋮ The constructive Hilbert program and the limits of Martin-Löf type theory

Cites Work

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