Inaccessibility in constructive set theory and type theory
From MaRDI portal
Publication:1295396
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)
constructive set theoryconstructivityinaccessible cardinalsMartin-Löf's intuitionistic type theoryAczel's constructive set theoryinaccessible setsMahlo's \(\pi\)-numbers
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
