Abstract

We prove that in IST, Nelson's internal set theory, the Uniqueness and Collection principles, hold for all (including external) formulas. A corollary of the Collection theorem shows that in IST there are no definable mappings of a set X onto a set Y of greater (not equal) cardinality unless both sets are finite and #(Y) ≤ n #(X) for some standard n. Proofs are based on a rather general technique which may be applied to other nonstandard structures. In particular we prove that in a nonstandard model of PA, Peano arithmetic, every hyperinteger uniquely definable by a formula of the PA language extended by the predicate of standardness, can be defined also by a pure PA formula