An Extended Predicative Definition of the Mahlo Universe
Reinhard Kähle, Anton Setzer · 2010
In this article we develop a Mahlo universe in Explicit Mathematics using extended predicative methods.Our approach differs from the usual construction in type theory, where the Mahlo universe has a constructor that refers to all total functions from families of sets in the Mahlo universe into itself; such a construction is, in the absence of a further analysis, impredicative.By extended predicative methods we mean that universes are constructed from below, even if they have impredicative characteristics.