Internal set theory

Definition

Internal set theory (IST) is the first-order theory in the language of set theory with one extra unary predicate $\operatorname{st}$, read "is standard". A formula is internal if it does not contain $\operatorname{st}$, and external otherwise. Write $\forall^{\mathrm{st}} x$ for "for all standard $x$", $\exists^{\mathrm{st}} x$ for "there is a standard $x$", and $\forall^{\mathrm{st\,fin}} z$ for "for all standard finite sets $z$". The axioms of IST are the following.

1. The axioms of ZFC, where the schemes of separation and replacement are taken only for internal formulas.
2. Idealization: for each internal formula $B(x, y)$, possibly with other free variables, $$\forall^{\mathrm{st\,fin}} z \, \exists x \, \forall y \in z \; B(x, y) \;\leftrightarrow\; \exists x \, \forall^{\mathrm{st}} y \; B(x, y).$$
3. Standardization: for each formula $C(z)$, internal or external, possibly with other free variables, $$\forall^{\mathrm{st}} x \, \exists^{\mathrm{st}} y \, \forall^{\mathrm{st}} z \, \bigl(z \in y \leftrightarrow (z \in x \wedge C(z))\bigr).$$
4. Transfer: for each internal formula $A(x, t_1, \dots, t_k)$ with no other free variables, $$\forall^{\mathrm{st}} t_1 \cdots \forall^{\mathrm{st}} t_k \, \bigl(\forall^{\mathrm{st}} x \, A(x, t_1, \dots, t_k) \to \forall x \, A(x, t_1, \dots, t_k)\bigr).$$