Summary: We deal with ontological problems concerning basic systems of explicit mathematics, as formalized in Jäger’s language of types and names. We prove a generalized inseparability lemma, which implies a form of Rice’s theorem for types and a refutation of the strong power type axiom $\text{POW}^+$. Next, we show that $\text{POW}^+$ can already be refuted on the basis of a weak uniform comprehension without complementation, and we present suitable optimal refinements of the remaining results within the weaker theory.