The extended predicative Mahlo Universe in Explicit Mathematics - model construction

This is joint work with Reinhard Kahle, Lisbon. In [3] Setzer introduced the 
Mahlo universe V in type theory and determined its proof theoretic strength. 
This universe has a constructor, which depends on the totality of functions
from families of sets in the universe into itself. 
Essentially for every such function f a subuniverse U_f of V was introduced,
which is closed under f and represented in V.

Because of the dependency on the totality of functions, not all type 
theorists agree that this is a valid principle, if one takes Martin-Löf Type 
Theory as a foundation of mathematics.
 
Feferman's theory of Explicit Mathematics is an alternative framework for 
dealing with constructive aspects of mathematics, in  which we have direct 
access to the set of partial functions. In such a setting, we can avoid the 
reference to the totality of functions on V.  Instead, we can take arbitrary
partial functions f, and try to form a subuniverse U_f closed under f. 
If f is total on U_f, then we add a code for it to V. We have developed a
 universe based on this idea (using mahlo as a name for V and sub as a name for
U), and showed that we can embed the axiomatic Mahlo universe, a version of 
the Mahlo universe similar to that of type theory  in Explicit Mathematics, 
into this universe.  We added as well an induction principle, expressing that
the Mahlo universe  is the least one.

Since the addition of U_f to V depends only on elements of V present 
before U_f was added to V, it can be regarded as being predicative, and we 
called it therefore the extended predicative Mahlo universe. 
 
In this talk we construct a model of the extended predicative
Mahlo universe in a suitable extension of Kripke-Platek set theory,
in order to determine an upper bound for its proof theoretic
strength. The model construction adds only  elements to the Mahlo universe
which are justified by its introduction rules. The model makes use of a new 
monotonicity condition on family sets, the notion
of a monotone operator for defining universes, and a special
condition for closure operators. This is an alternative to Richter's 
[Gamma,Gamma'] operator for defining closure operators.