Editing Internal set theory (section)

=== Idealisation ===
*For any internal formula <math>\phi</math> without a free occurrence of ''z'', the universal closure of the following formula is an axiom:
*:<math>\forall^\mathrm{st}z\,(z\text{ is finite}\to\exists y\,\forall x\in z\,\phi(x,y,u_1,\dots,u_n))\leftrightarrow\exists y\,\forall^\mathrm{st}x\,\phi(x,y,u_1,\dots,u_n).</math>
*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 {{tmath|R(g, f)}} holds for all ''f'' in ''F'', then there is a particular ''G'' such that for ''any standard'' ''f'' we have {{tmath|R(g, f)}}, and conversely, if there exists ''G'' such that for any standard ''f'', we have {{tmath|R(g, f)}}, then for each finite set ''F'', there exists a ''g'' such that {{tmath|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 {{tmath|R(g, f)}}: ''g'' and ''f'' are not equal and ''g'' is in ''S''.  Since "''For every standard finite set F there is an element g in S such that {{tmath|g \ne f}} for all f in {{itco|F}}''" is false (no such ''g'' exists when {{math|''F'' {{=}} ''S''}}), we may use Idealisation to tell us that "''There is a G in S such that {{tmath|g \ne f}} for all standard {{itco|f}}''" is also false, i.e. all the elements of ''S'' are standard.

If ''S'' is infinite, then we take for the relation {{tmath|R(g, f)}}: ''g'' and ''f'' are not equal and ''g'' is in ''S''. Since "''For every standard finite set F there is an element g in S such that {{tmath|g \ne f}} for all f in {{itco|F}}''" (the infinite set ''S'' is not a subset of the finite set {{itco|''F''}}), we may use Idealisation to derive "''There is a G in S such that {{tmath|g \ne f}} for all standard {{itco|f}}''."  In other words, every infinite set contains a nonstandard element (many, in fact).

The power set of a standard finite set is standard (by Transfer) and finite, so all the subsets of a standard finite set are standard.

If ''S'' is nonstandard, we take for the relation {{tmath|R(g, f)}}: ''g'' and ''f'' are not equal and ''g'' is in ''S''. Since "''For every standard finite set F there is an element g in S such that {{tmath|g \ne f}} for all f in {{itco|F}}''" (the nonstandard set ''S'' is not a subset of the standard and finite set {{itco|''F''}}), we may use Idealisation to derive "''There is a G in S such that {{tmath|g \ne f}} for all standard f.''"  In other words, every nonstandard set contains a nonstandard element.

As a consequence of all these results, all the elements of a set ''S'' are standard if and only if ''S'' is standard and finite.

==== Applied to the relation &lt; ====
Since "''For every standard, finite set of natural numbers F there is a natural number g such that {{tmath|g > f}} for all f in {{itco|F}}''" (say, {{math|''g'' {{=}} max(''F'') + 1}}), we may use Idealisation to derive "''There is a natural number G such that {{tmath|g > f}} for all standard natural numbers {{itco|f}}''."  In other words, there exists a natural number greater than each standard natural number.

==== Applied to the relation ∈ ====
We take {{tmath|R(g, f)}}: ''g'' is a finite set containing element ''f''. Since "''For every standard, finite set F, there is a finite set g such that {{tmath|f \in G}} for all f in {{itco|F}}''" (e.g. {{math|''g'' {{=}} ''F''}}), we may use Idealisation to derive "''There is a finite set G such that {{tmath|f \in G}} for all standard {{itco|f}}''."<!--  In other words, all standard sets can be contained in a finite set as elements. --> For any set ''S'', the intersection of ''S'' with the set ''G'' is a finite subset of ''S'' that contains every standard element of ''S''. ''G'' is necessarily nonstandard, by the ZFC [[Axiom of regularity|regularity]] axiom.