The strength of Martin-Löf type theory with a superuniverse. I
From MaRDI portal
Publication:1976875
DOI10.1007/S001530050001zbMath0953.03065OpenAlexW4236196131MaRDI QIDQ1976875
Publication date: 23 January 2001
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s001530050001
Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15)
Related Items (10)
Inaccessible set axioms may have little consistency strength ⋮ From type theory to setoids and back ⋮ Wellordering proofs for metapredicative Mahlo ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Dependent products and 1-inaccessible universes ⋮ The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice ⋮ Universes in explicit mathematics ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Universes over Frege structures ⋮ Transfinite dependent choice and ω-model reflection
This page was built for publication: The strength of Martin-Löf type theory with a superuniverse. I
