Peter Dybjer: Predicativity of the Mahlo universe in type theory (joint work with Anton Setzer)

Abstract

We provide a constructive, predicative justification of Setzer's Mahlo universe in type theory. Our approach is closely related to Kahle and Setzer's construction of an extended predicative Mahlo universe in Feferman's explicit mathematics. However, we work directly in Martin-Löf type theory extended with a Mahlo universe and obtain informal meaning explanations which extend (and slightly modify) those in Martin-Löf's article Constructive Mathematics and Computer Programming. We also present mathematical models in set-theoretic metalanguage and explain their relevance to the informal meaning explanations.