Uniform inseparability in Explicit Mathematics

We deal with ontological problems concerning basic systems of explicit mathematics, as formalized in Jaeger'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 POW'. Next, we show that 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. Introduction