In this paper we discuss extensions of Feferman's theory T0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recusion-theoretic models for (fairly strong) systems of explicit mathematics which is based on nonmonotone inductive definitions.