In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.

We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.