Editing Internal set theory (section)

== Formal axioms ==
IST is an axiomatic theory in the [[first-order logic]] with equality in a [[signature (logic)|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
:<math>\begin{align}\exists^\mathrm{st}x\,\phi(x)&=\exists x\,(\operatorname{st}(x)\land\phi(x)),\\
\forall^\mathrm{st}x\,\phi(x)&=\forall x\,(\operatorname{st}(x)\to\phi(x)).\end{align}</math>
IST includes all axioms of the [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]] (ZFC). Note that the ZFC schemata of [[Axiom of separation|separation]] and [[Axiom of replacement|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: '''I'''dealisation, '''S'''tandardisation, and '''T'''ransfer.

=== 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.

=== Standardisation ===
*If <math>\phi</math> is any formula (it may be external) without a free occurrence of ''y'', the universal closure of
*:<math>\forall^\mathrm{st}x\,\exists^\mathrm{st}y\,\forall^\mathrm{st}t\,(t\in y\leftrightarrow(t\in x\land\phi(t,u_1,\dots,u_n)))</math>
:is an axiom.
*In words: If ''A'' is a standard set and P any property, internal or otherwise, then there is a unique, standard subset ''B'' of ''A'' whose standard elements are precisely the standard elements of ''A'' satisfying ''P'' (but the behaviour of ''B''<nowiki>'</nowiki>s nonstandard elements is not prescribed).

=== Transfer ===
*If <math>\phi(x,u_1,\dots,u_n)</math> is an internal formula with no other free variables than those indicated, then
*:<math>\forall^\mathrm{st}u_1\dots\forall^\mathrm{st}u_n\,(\forall^\mathrm{st}x\,\phi(x,u_1,\dots,u_n)\to\forall x\,\phi(x,u_1,\dots,u_n))</math>
:is an axiom.
*In words: If all the parameters  ''A'', ''B'', ''C'', ..., ''W'' of an internal formula ''F'' have standard values then {{nowrap|''F''(''x'', ''A'', ''B'',..., ''W'')}} holds for all ''x''{{'}}s as soon as it holds for all standard ''x''{{'}}s&mdash;from which it follows that all uniquely defined concepts or objects within classical mathematics are standard.