Internal Set Theory (IST)

Origin. Edward Nelson, "Internal set theory: a new approach to nonstandard analysis" (Bulletin of the AMS 83, 1977). Robinson's nonstandard analysis (1966) built the hyperreals as an ultrapower and needed model theory to justify transfer; Nelson's move was syntactic — leave the universe alone, add a predicate to the language, and axiomatize it. Kanovei, Reeken, and Hrbáček developed the theory and its variants; Kanovei (1993) showed the reduction algorithm does not extend to all IST formulas.

Models. ZFC's universe, unaltered, with a predicate st(x) reading "x is standard" laid over it. Infinitesimals are not new objects — they are ordinary real numbers that happen to be nonstandard, and ℝ is the same ℝ. What is new is the ability to say things ZFC cannot say, since the predicate is not definable in ∈. The price is stated exactly: separation and replacement do not extend to formulas containing st.

Formalism.

Language: L_IST = L_ZFC ∪ {st}, a new unary predicate. Internal formula: one not containing st. External: one that does. Abbreviations: ∀^st x φ for ∀x(st(x) → φ); ∃^st x φ for ∃x(st(x) ∧ φ); ∀^{st fin} for the standard-and-finite relativization.

Axioms: all of ZFC — with separation and replacement restricted to internal formulas — plus three schemata, one per initial:

(I) Idealization. For internal φ with arbitrary (possibly nonstandard) parameters: ∀^{st fin} x ∃y ∀z ∈ x φ(z,y) → ∃y ∀^st x φ(x,y)

(S) Standardization. For arbitrary φ (internal or external): ∀^st x ∃^st y ∀^st z (z ∈ y ↔ z ∈ x ∧ φ(z))

(T) Transfer. For internal φ with standard parameters only: ∀^st t₁ … ∀^st t_k [∀^st x φ(x, t₁,…,t_k) → ∀x φ(x, t₁,…,t_k)]

What follows immediately: Idealization gives a finite set containing every standard object, and an ℕ with nonstandard elements. An infinitesimal is a real x with |x| < 1/n for every standard n ∈ ℕ; Idealization produces one. Transfer says a standard object with a standard-parameter description is uniquely determined — so "the set of standard reals" is not a set, since Separation is internal only. That restriction is what blocks Russell-style contradiction.

Conservativity (Nelson 1977): IST is a conservative extension of ZFC: every internal theorem of IST is a theorem of ZFC. The proof is a syntactic reduction algorithm turning external proofs into internal ones — eliminate st-quantifiers, apply (S) to form standard parts, use (I) for finite approximations, and (T) to strip the superscripts. Hence Con(ZFC) → Con(IST), and nonstandard analysis proves no new classical theorems.

Limits of the reduction (Kanovei 1993): there is an L_IST sentence not IST-equivalent to any ∈-sentence. The reduction algorithm works for bounded formulas with standard parameters and does not extend to the full language.

Relatives: Hrbáček set theory, and the Kanovei–Reeken systems, which allow external sets. Vopěnka's Alternative Set Theory (1979) — a different route to the same phenomena. P, the finite-type nonstandard system over Gödel's T (van den Berg, Briseid, Safarik), used for extracting computational content.

Symbols.

Metatheory. Conservativity over ZFC is the theorem the system exists for: it says nonstandard analysis is a way of writing proofs, not a way of getting new ones, and that infinitesimal arguments are eliminable in principle. The restriction of Separation and Replacement to internal formulas is not a technicality but the whole consistency argument — "the set of all standard naturals" would be a bounded non-inductive subset of ℕ, and it is not a set because the defining formula is external. Placement here follows the criteria: IST's individuation is a signature (∈, st) and axioms over classical first-order logic, and the departure from ZFC is axiomatic rather than logical. Kanovei's result bounds the syntactic reading — IST says more than ZFC even though it proves no more internally.

Applies to. Nonstandard analysis as practiced — infinitesimal calculus, measure theory, stochastic analysis (Nelson's Radically Elementary Probability Theory, 1987), and the treatment of large finite sets as infinite ones. Reverse mathematics and proof mining, through nonstandard fragments with computational content. Formalized asymptotics, where the standard/nonstandard split replaces limit bookkeeping. Teaching calculus without ε-δ, which was part of Nelson's stated motivation.

Limitations. Nothing new is proved: conservativity cuts both ways, and any internal theorem of IST is available in ZFC by an eliminable detour. External formulas cannot be used for set formation, which forbids the constructions users most want and is easy to violate by inattention — the standard beginner's error. Idealization's finite set containing all standard objects reads as a contradiction until one sees that "finite" is internal. The st predicate has no definable meaning in ZFC, so IST is not a definitional extension, and the standard/nonstandard split is not intrinsic to any object. Kanovei's theorem shows the reduction algorithm is not the whole story.

© 2026 Lingenic LLC