A Mahlo-Universe of Effective Domains with Totality
Dag Normann · Cambridge University Press eBooks · 1999
We construct a typed hierarchy of effective algebraic domains with totality of height the first recursively Mahlo ordinal. The hierarchy is based on the empty type and the domains for singleton, boolean values and natural numbers, and it is closed under dependent sums and pro-ducts of effectivly parameterised families of types, and under universes closed under a very general universe operator.