An axiomatics for nonstandard set theory, based on von Neumann-Bernays-Godel Theory

We present an axiomatic framework for nonstandard analysis-the Nonstandard Class Theory (NCT) which extends von Neumann-Godel-Bernays Set Theory (NBC) by adding a unary predicate symbol St to the language of NBC (St(X) means that the class X is standard) and axioms-related to it-analogs or Nelson's idealization, standardization and transfer principles. Those principles are formulated as axioms, rather than axiom schemes, so that NCT is finitely a xiomatizable. NCT can be considered as a theory of definable classes of Bou nded Set Theory by V. Kanovei and Nit. Reeken. In many aspects NCT resemble s the Alternative Set Theory by P. Vopenka. For example there exist semiset s (proper subclasses or sets) in NCT and it can be proved that a set has a standard finite cardinality iff it does not contain any proper subsemiset. Semisets can be considered as external classes in NCT. Thus the saturation principle can be formalized in NCT.