Yuta Takahasi: On the Mahlo Universe Type in Martin-Löf Type Theory

Invitation pdf

Yuta Takahasi (Aomori University, Japan): On the Mahlo Universe Type in Martin-Löf Type Theory

Abstract
The Mahlo universe type, which is a type-theoretic analogue of recursively Mahlo ordinals, was introduced into Martin-Löf type theory (MLTT) by Anton Setzer. The strength of this universe type consists in the following reflection property: for any function on families of small types in the Mahlo universe, there always exists a subuniverse closed under this function. The original motivation of introducing the Mahlo universe type comes from ordinal analysis in proof theory, that is, it was introduced in order to obtain an extension of MLTT which is able to prove the well ordering property of an ordinal notation system built on one recursively Mahlo ordinal. However, the subsequent work, including Setzer's, is not limited to this motivation, since the Mahlo universe type has its own interest from the type-theoretic point of view. This talk discusses our ongoing work on this universe. In particular, we examine the conceptual problem of how to justify the impredicativity of the Mahlo universe type.