Skip to main content
To KTH's start page

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

Time: Thu 2024-10-03 13.00 - 15.00

Location: Albano house 1, floor 3, room 11 (Kovalevsky)

Participating: Peter Dybjer (Chalmers)

Export to calendar

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.