that the precise bounds of this set vary with time and history). In particular we will not be able to talk about the largest standard number, or the smallest nonstandard number. It will be valid to talk about some finite set that contains all standard numbers—but this non-classical formulation could only apply to a nonstandard set. Formal axioms for IST IST is an axiomatic theory in the first-order logic with equality in a language containing a binary predicate symbol ∈ and a unary predicate symbol st(x). Formulas not involving st (i.e., formulas of the usual language of set theory) are called internal, other formulas are called external. We use the abbreviations IST includes all axioms of the Zermelo–Fraenkel set theory with the axiom of choice (ZFC). Note that the ZFC schemata of separation and replacement are not extended to the new language, they can only be used with internal formulas. Moreover, IST includes three new axiom schemata – conveniently one for each initial in its name: Idealisation, Standardisation, and Transfer. I: Idealisation For any internal formula without a free occurrence of z, the universal closure of the following formula is an axiom: In words: For every internal relation R, and for arbitrary values for all other free variables, we have that if for each standard, finite set F, there exists a g such that R(g, f) holds for all f in F, then there is a particular G such that for any standard f we have R(G, f), and conversely, if there exists G such that for any standard f, we have R(G, f), then for each finite set F, there exists a g such that R(g, f) holds for all f in F. The statement of this axiom comprises two implications. The right-to-left implication can be reformulated by the simple statement that elements of standard finite sets are standard. The more important left-to-right implication expresses that the collection of all standard sets is contained in a finite (nonstandard) set, and moreover, this finite set can be taken to satisfy any given internal property shared by all standard finite sets. This very general axiom scheme upholds the existence of "ideal" elements in appropriate circumstances. Three particular applications demonstrate important consequences. Applied to the relation ≠ If S is standard and finite, we take for the relation R(g, f): g and f are not equal and g is in S. Since