Internal set theory (IST) is a mathematical theory of sets developed by Edward Nelson that provides an axiomatic basis for a portion of the nonstandard analysis introduced by Abraham Robinson. Instead of adding new elements to the real numbers, Nelson's approach modifies the axiomatic foundations through syntactic enrichment. Thus, the axioms introduce a new term, "standard", which can be used to make discriminations not possible under the conventional ZFC axioms for sets. Thus, IST is an enrichment of ZFC: all axioms of ZFC are satisfied for all classical predicates, while the new unary predicate "standard" satisfies three additional axioms I, S, and T. In particular, suitable nonstandard elements within the set of real numbers can be shown to have properties that correspond to the properties of infinitesimal and unlimited elements.
Nelson's formulation is made more accessible for the lay-mathematician by leaving out many of the complexities of meta-mathematical logic that were initially required to justify rigorously the consistency of number systems containing infinitesimal elements.
Whilst IST has a perfectly formal axiomatic scheme, described below, an intuitive justification of the meaning of the term standard is desirable. This is not part of the formal theory, but is a pedagogical device that might help the student interpret the formalism. The essential distinction, similar to the concept of definable numbers, contrasts the finiteness of the domain of concepts that we can specify and discuss, with the unbounded infinity of the set of numbers; compare finitism.
The term standard is therefore intuitively taken to correspond to some necessarily finite portion of "accessible" whole numbers. The argument can be applied to any infinite set of objects whatsoever – there are only so many elements that one can specify in finite time using a finite set of symbols and there are always those that lie beyond the limits of our patience and endurance, no matter how we persevere. We must admit to a profusion of nonstandard elements—too large or too anonymous to grasp—within any infinite set.
The following principles follow from the above intuitive motivation and so should be deducible from the formal axioms. For the moment we take the domain of discussion as being the familiar set of whole numbers.
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
\begin{align}\existsstx\phi(x)&=\existsx(\operatorname{st}(x)\land\phi(x)),\\ \forallstx\phi(x)&=\forallx(\operatorname{st}(x)\to\phi(x)).\end{align}
\phi
\forallstz(zisfinite\to\existsy\forallx\inz\phi(x,y,u1,...,un))\leftrightarrow\exists
| stx\phi(x,y,u | |
| y\forall | |
| 1,...,u |
n).
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.
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 "For every standard finite set F there is an element g in S such that for all f in F" is false (no such g exists when), we may use Idealisation to tell us that "There is a G in S such that for all standard f" is also false, i.e. all the elements of S are standard.
If S is infinite, then we take for the relation 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 for all f in F" (the infinite set S is not a subset of the finite set F), we may use Idealisation to derive "There is a G in S such that for all standard 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 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 for all f in F" (the nonstandard set S is not a subset of the standard and finite set F), we may use Idealisation to derive "There is a G in S such that 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.
Since "For every standard, finite set of natural numbers F there is a natural number g such that for all f in F" – say, – we may use Idealisation to derive "There is a natural number G such that for all standard natural numbers f." In other words, there exists a natural number greater than each standard natural number.
More precisely we take for 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 for all f in F" – say by choosing itself – we may use Idealisation to derive "There is a finite set G such that for all standard f." 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.
\phi
\forallstx\existssty\forallstt(t\iny\leftrightarrow(t\inx\land\phi(t,u1,...,un)))
is an axiom.
\phi(x,u1,...,un)
| stx\phi(x,u | |
| \forall | |
| 1,...,u |
n)\to\forallx\phi(x,u1,...,un))
is an axiom.
Aside from the intuitive motivations suggested above, it is necessary to justify that additional IST axioms do not lead to errors or inconsistencies in reasoning. Mistakes and philosophical weaknesses in reasoning about infinitesimal numbers in the work of Gottfried Leibniz, Johann Bernoulli, Leonhard Euler, Augustin-Louis Cauchy, and others were the reason that they were originally abandoned for the more cumbersome real number-based arguments developed by Georg Cantor, Richard Dedekind, and Karl Weierstrass, which were perceived as being more rigorous by Weierstrass's followers.
The approach for internal set theory is the same as that for any new axiomatic system—we construct a model for the new axioms using the elements of a simpler, more trusted, axiom scheme. This is quite similar to justifying the consistency of the axioms of elliptic non-Euclidean geometry by noting they can be modeled by an appropriate interpretation of great circles on a sphere in ordinary 3-space.
In fact via a suitable model a proof can be given of the relative consistency of IST as compared with ZFC: if ZFC is consistent, then IST is consistent. In fact, a stronger statement can be made: IST is a conservative extension of ZFC: any internal formula that can be proven within internal set theory can be proven in the Zermelo–Fraenkel axioms with the axiom of choice alone.[1]
Related theories were developed by Karel Hrbacek and others.