Extending Martin-Löf type theory by one Mahlo-universe

DOI10.1007/S001530050140zbMath0943.03046OpenAlexW1968916436MaRDI QIDQ1568707

Anton Setzer

Publication date: 5 September 2000

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001530050140

zbMATH Keywords

constructive type theoryMartin-Löf's type theoryproof-theoretical strengthMahlo ordinal

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15)

Related Items (12)

Induction-recursion and initial algebras. ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Reflections on reflections in explicit mathematics ⋮ Inaccessibility in constructive set theory and type theory ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Indexed induction-recursion ⋮ An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe ⋮ The constructive Hilbert program and the limits of Martin-Löf type theory

This page was built for publication: Extending Martin-Löf type theory by one Mahlo-universe