In this article we show how the universe of BST, bounded set theory can be enlarged by definable subclasses of sets so that Separation and Replacement are true in the enlargement for all formulas, including those in which the standardness predicate may occur. Thus BST is strong enough to incorporate external sets in the internal universe in a way sufficient to develop topics in nonstandard analysis inaccessible in the framework of a purely internal approach, such as Loeb measures.

Nonstandard set theory is an attempt to generalise nonstandard analysis to cover the whole of classical mathematics. Existing versions (Nelson, Hrbáček, Kawai) are unsatisfactory in that the unlimited idealisation principle conflicts with the wish to have a full theory of external sets. I re-analyse the underlying requirements of nonstandard set theory and give a new formal system, stratified nonstandard set theory, which seems to meet them better than the other versions.