Review by Pavol Zlatoš of

Nonstandard Analysis, Axiomatically V. Kanovei, M. Reeken

published by the AMS as MR2093998 on MathSciNet.

Nonstandard analysis, in its early period of development, shortly after having been established by A. Robinson ^{1}, dealt mainly with nonstandard extensions of some traditional mathematical structures. The system of its foundations, referred to as ”model-theoretic foundations” in the book under review, was proposed by Robinson and E. Zakon ^{2}. Their approach was based on the type-theoretic concept of superstructure V (S) over some set of individuals S and its nonstandard extension (enlargement) ^{∗}V (S), usually constructed as a (bounded) ultrapower of the ”standard” superstructure V (S). They formulated few principles concerning the elementary embedding V (S) →^{∗} ^{∗}V (S), enabling the use of methods of nonstandard analysis without paying much attention to details of construction of the particular nonstandard extension. Such an approach—in spite of having been applicable to any classical mathematical structure (not just a first-order one) —was still perceived as a kind of ad hoc foundation, raising the need to search for philosophically more satisfactory ones, allowing the extension of the whole set-theoretic universe of contemporary mathematics to some richer ”nonstandard universe” of a suitably modified set theory, providing at the same time all the classical mathematical structures with canonic nonstandard extensions, described in a uniform way.

1Non-standard analysis, North-Holland, Amsterdam, 1966; MR0205854 (34 #5680)

2Applications of Model Theory to Algebra, Analysis, and Probability (Internat. Sympos., Pasadena, Calif., 1967), 109–122, Holt, Rinehart and Winston, New York, 1969; MR0239965 (39 #1319) and improved by Zakon, Victoria Symposium on Nonstandard Analysis (Univ. Victoria, Victoria, B.C., 1972), 313–339. Lecture Notes in Math., 369, Springer, Berlin, 1974; MR0476500 (57 #16060)

From among the early versions of axiomatic ”nonstandard” set theories the internal set theory IST introduced by E. Nelson^{3} seems to have attracted the most followers. IST is formulated in the language containing the binary symbol ∈ for the membership relation and an additonal unary symbol st denoting the standardness predicate. The universe of IST consists entirely of ”internal” sets, i.e., those corresponding in ”model-theoretic foundations” to the elements of ^{∗}V (S); however, unlike ^{∗}V (S), it satisfies all the axioms of ZFC. On the other hand, the fact that some parts of sets, defined by formulas involving the predicate st, do not form sets in IST is a source of— mostly minor but rather frequent—technical inconveniences. However, the main obstacle barring a traditionally educated ”standard” mathematician from accepting IST is perhaps of a psychological nature. The IST view of the ideal world of mathematics is at odds with mathematical Platonism. In IST all the classical infinite sets, e.g., ℕ or ℝ, acquire new, nonstandard elements (like ”infinite” natural numbers or ”infinitesimal” reals). At the same time, the families ^{σ}ℕ = {x ∈ ℕ: stx} or ^{σ}ℝ = {x ∈ ℝ: stx} of all standard, i.e., ”true,” natural numbers or reals, respectively, are not sets in IST at all. Thus, for a traditional mathematician inclined to ascribe to mathematical objects a certain kind of objective existence or reality, accepting IST would mean confessing that (s)he has lived in confusion, mistakenly having regarded as, e.g., the set ℕ just its tiny part^{σ}ℕ (which is not even a set) and overlooked the rest. Not surprisingly, many are not willing to reconsider their point of view so dramatically.

Within ”model-theoretic foundations” this psychological obstacle is less acute. Classical sets like ℕ or ℝ remain unchanged. They just gain some standard companions ^{∗}ℕ or ^{∗}ℝ, respectively, and, identifing each element x with its ∗-image ^{∗}x, become equal to the sets of all standard elements of their extensions ^{∗}ℕ or ^{∗}ℝ.

Almost simultaneously with Nelson, K. Hrbček introduced several ”nonstandard” set theories dealing with standard, internal and external sets (with the class of internal sets corresponding to the universe of all sets in IST) ^{4}. The main reason for that multitude and for the lack of a canonical nonstandard set theory was his discovery of what is now known as the Hrbaček paradox: besides the axiom of Regularity which necessarily fails already for external sets of internal sets, the extension of a rather weak basic nonstandard set theory by the scheme of Collection (or Replacement) for st-∈-formulas, Standardization, Saturation for families of internal sets of size not bounded by any in advance given classical cardinal, and either of the axioms of Power Set or Choice turns out to be inconsistent. As a consequence, any consistent nonstandard set theory has to sacrifice at least one of these axioms or to weaken it to a form compatible with the rest. Naturally, there arise several solutions.

3Bull. Amer. Math. Soc. 83 (1977), no. 6, 1165–1198; MR0469763 (57 #9544)

4Fund. Math. 98 (1978), no. 1, 1–19; MR0528351 (84b:03084); Amer. Math. Monthly 86 (1979), no. 8, 659–677; MR0546178 (81c:03055)

The present book is devoted to Hrbaček set theory HST, an axiomatic ”nonstandard” set theory formulated by the authors as the extension of Hrbaček’s theory N S_{1}(ZFC) by the axioms of Regularity over 𝕀, Standard Size Choice and Dependent Choice (see below). However, it should be pointed out that HST does not coincide with any of Hrbaček’s original theories and the authors’ contribution—both to its development and its detailed (meta)mathematical analysis—is so enormous that should it be properly acknowledged: the theory—especially if it becomes widely accepted —would be more adequately called Hrbaček-Kanovei-Reeken set theory and denoted by HKR.

The general view and more detailed structure of the universe of HST, the way it can be used as ”working foundations of nonstandard mathematics”, its merits as well as connections to other—both ”standard” and ”nonstandard”— set theories, and related metamathematical issues will emerge when reviewing the book by chapters, necessarily in a rather selective way.

Chapter 1. Getting started. In spite of its relaxed title, this chapter is crucial because the whole axiomatic system of HST is introduced here. Therefore, we dwell a bit longer on it.

The language of HST consists of the binary membership relation symbol ∈ and the unary standardness predicate symbol st. The world of HST is a vast all-comprising ”external” universe ℍ, and three of its subuniverses are singled out: the universe 𝕊 = {x: stx} of all standard sets, the universe 𝕀 = {x: intx} of all internal sets, where intx means ∃y (sty ∧ x ∈ y), and the universe 𝕎𝔽 = {x: wfx} of all well-founded sets, where wfx stands for the ∈-formula ”there exists a transitive set X such that x ⊆ X and ∈ is well-founded on X”.

The external universe (ℍ; ∈, st) satisfies all the axioms of ZFC except for the axioms of Power Set, Regularity and Choice, with the schemata of Separation and Collection (i.e., Replacement as well) for all st-∈-formulas.

The universe of standard sets (𝕊, ∈) satisfies literally all of the axioms of ZFC (with the schemata of Separation and Collection just for ∈-formulas). The inclusion 𝕊 ⊆ 𝕀 is an immediate consequence. Additionally, the universe (𝕀; ∈) of all internal sets satisfies the axiom of Transitivity: ⋃ 𝕀 ⊆ 𝕀, i.e., 𝕀 is a transitive class. The specific ”nonstandard character” of the theory is guaranteed by the following two axioms. Transfer: Φ^{st} ⟺ Φ^{int}, for any closed ∈-formula Φ with standard parameters; in other words, the universe (𝕀; ∈) of all internal sets is an elementary extension of the universe (𝕊 ∈) of all standard sets.

Standardization: ∀X ∃^{st}Y (X ∩ 𝕊 = Y ∩ 𝕊); this necessarily unique Y is denoted by ^{S}X. As a consequnce, the only sets in ℍ consisting entirely of standard sets are those of the form ^{σ}Y = Y ∩ 𝕊 where Y ∈ 𝕊.

The failure of Regularity in ℍ is compensated by the axiom of Regularity over 𝕀: X ≠ ∅ ⟹ ∃x ∈ X(x ∩ X ⊆ 𝕀). Thus ℍ is built over 𝕀 as a kind of urelements, similar to the way 𝕎𝔽 is built over the empty set ∅.

The last group of axioms deals with sets of the form {f(x): x ∈ X ∩ 𝕊}, where X is any set, called sets of standard size.

The third specific ”nonstandard axiom” is that of standard size Saturation of the class 𝕀: if X ⊆ 𝕀 is a set of standard size, such that x ≠ ∅ and x∩y ∈ X for any x, y ∈ X, then ⋂ X ≠ ∅.

The available amount of choice in ℍ is given by the last two axioms in the list. Standard Size Choice ensures the existence of a choice function for any set of standard size containing just nonempty sets as elements.

Finally, Dependent Choice postulates the existence of an ω-sequence of choices, in case the domain of the n-th choice depends on the result of the preceding choice.

Thus, the authors’ solution of the Hrbaček paradox consists in sacrificing Choice and Power Set by weakening the former to its standard size form and retaining the latter in the universe 𝕎𝔽 of well-founded sets.

By well-founded induction, there is a unique map 𝕎𝔽 →^{∗} →𝕊 such that ∗w = ^{S}{^{∗}u: u ∈ w} for any w ∈ 𝕎𝔽. Using the principles formulated so far, it is possible to show that the star map is an isomorphism of (𝕎𝔽; ∈) onto (𝕊, ∈) and a proper elementary embedding of (𝕎𝔽, ∈) into (𝕀, ∈), and that way reproduce the ”model-theoretic” ∗-Transfer in HST, as well. This style of argumentation, referred to as the ”scheme 𝕎𝔽 →^{∗} →𝕀 [in ℍ]”, is preferred in the book. Similarly, even more in the ”model-theoretic style” of nonstandard analysis, given any ”classical” structure M ∈ 𝕎𝔽 for a finite first order language L, the restriction of the ∗-map to the base set of M gives rise to the canonic elementary embedding of M into the standard size saturated L-structure ^{∗}M ∈ 𝕀. If L ∈ 𝕎𝔽 is infinite then ^{∗}M ∈ 𝕀 becomes a structure of the extended language ^{∗}L; however, the ∗-map is still a canonic elementary embedding of M into the L-reduct ^{∗}M ↾ L of ^{∗}M. Though ^{∗}M ↾ L itself does not belong to 𝕀, its base set and all its relations and operations do, i.e., ^{∗}M ↾ L is internally presented and standard size saturated.

The other way round, putting emphasis on the universe 𝕀 of all internal sets and its subuniverse 𝕊, i.e., on the ”scheme 𝕊 ⊆ 𝕀”, makes it possible to argue in HST entirely in the style of the axiomatic approach typical for IST. In both schemes, the external universe ℍ serves as a useful source of auxilliary sets.

One of the main advantages of HST is the unlimited Saturation: any system of internal sets with (external) cardinality equal to any classical cardinal and having the finite intersection property has an element in common. As a (perhaps psychologically difficult to accept) consequence, (externally) infinite internal sets are indeed huge: however ”big” set X ⊆ 𝕎𝔽 or X ⊆ 𝕊 and however ”small” (in particular, ∗-finite) infinite set Y ∈ 𝕀 we choose, there is an injection X → Y. In other words, the external cardinality of any infinite internal set is bigger than any classical, i.e., well-founded cardinal.

Another impressive consequence of the standard size Saturation and the closedness properties of 𝕎𝔽 is the collapse of the hierarchy over internal sets built by alternating application of unions and intersections of standard size (ss) families. Any such a set belongs to the class Δ_{2}^{ss} = Σ_{2}^{ss} ∩ Π_{2}^{ss}, which is closed with respect to projections as well. In other words, every set X ⊆ 𝕀, definable by an st-∈-formula with parameters from 𝕀, is of the form X = ⋃_{α∈A} ⋂_{β∈B} u_{αβ} = ⋂_{γ∈C} ⋂_{δ∈D} v_{γδ}, where u_{αβ}, v_{γδ} are internal sets and A, B, C, D are some well-founded sets.

Chapter 2. Elementary real analysis in the nonstandard universe. This chapter serves primarily as an illustration of how the fundamentals of real nonstandard analysis can be developed in HST. Besides the traditional ”compulsory” parts, Euler’s famous factorization of the sine function is proved in an intrinsically nonstandard way, making rigorous the intuitively appealing, though sometimes obscure, use of infinitesimals and infinitely large numbers in the original argument. The fairly elementary proof of the Jordan curve theorem gives some idea of the strength of methods of nonstandard analysis.

All of those particular topics could be developed within any satisfactory foundational framework of nonstandard analysis. The advantage of the present approach, besides the unlimited Saturation, is that the nonstandard extensions of classical structures need not be constructed—they are already given, and are unique and canonical in a well defined sense.

Chapter 3. Theories of internal sets. Inspecting what HST says about just internal and standard sets, it comes out that the structure (𝕀; ∈,st) is not a model of IST. In particular, in IST there is a(n internal) set containing (among other elements) all the standard sets; no such set exists in the HST universe 𝕀. However, (𝕀; ∈,st) still satisfies the bounded set theory BST, a modification of IST introduced by Kanovei ^{5} by weakening the axiom of Idealization to Basic Idealization and adding the axiom of Inner Boundedness: every (internal) set is an element of a standard set. The chapter is devoted to a detailed foundational study of BST, IST and their common part, the basic internal set theory BIST, as well as to clarifying some relations between them.

Generalizing Nelson’s translation algorithm, it is proved that any st-∈- formula ϕ(x_{1}, …, x_{n}) is equivalent in BST to a Σ_{2}^{st} formula, i.e., to a formula of the form ∃^{st}y∀^{st}z ϕ(x_{1}, …, x_{n}, y, z) for some ∈-formula ϕ(x_{1}, …, x_{n}, y, z). As a consequence, BST is shown to be finitely axiomatizable and to admit certain natural coding of ”external sets” definable by st-∈-formulas.

A remarkable feature of IST is the existence of a uniform definition of truth for closed ∈-formulas in its universe 𝕊 of all standard sets. As (𝕊; ∈) satisfies ZFC, one would expect that IST is stronger than ZFC. However, as proved in Chapter 4, both theories are equiconsistent.

Finally, the ”second edition” of Nelson’s IST is considered, stronger in some respect than IST itself ^{6}. A widespread misinterpretation of three results true within the stronger framework as being provable in IST itself (referred to as three ”myths” of IST) is rectified.

Chapter 4. Metamathematics of internal theories. The main metamathematical properties of BST and IST are established here. Either theory is equiconsistent with and a conservative extension of ZFC.

The notion of standard core interpretation, enabling the assessment of the difference between various nonstandard set theories, is introduced. Roughly speaking, a nonstandard set theory T (i.e., a theory in a language containing ∈ and st with the usual meaning) is standard core interpretable in a standard set theory U (i.e., a theory in a langauge containing ∈ but not st) if every model v = (V; ∈, …) of U can be extended to a model w = (W; ∈, st, …) of T in such a way that the universe V of v coincides with the standard core 𝕊^{(w)} = {x ∈ W: stx} of w.

5Uspekhi Mat. Nauk 46 (1991), no. 6(282), 3–50, 240; MR1164200 (93i:03097)

6E. Nelson, Ann. Pure Appl. Logic 38 (1988), no. 2, 123–134; MR0938372 (89i:03121)

It turns out that BST is ”realistic”, in the sense of being standard core interpretable in ZFC, while IST is not, as the minimal transitive model of ZFC is not standard core extendable to a model of IST. On the other hand, IST is standard core interpretable in ZF GT, the extension of ZFC by a global choice function and a truth predicate for ∈-formulas.

A fairly general construction of quotient power, generalizing ultrapowers, ultralimits and limit ultrapowers, is introduced and systematically exploited as the main technical tool throughout the chapter.

Chapter 5. Definable external sets and metamathematics of HST. The results on BST are used as the starting point in examining the metamathematics of HST. As an intermediate step, the elementary external set theory EEST is introduced, describing the minimal extension 𝔼 of the BST universe 𝕀 by its external subsets definable by st-∈-formulas with parameters. The collapse of the standard size projective hierarchy over internal sets to the Δ_{2}^{ss} level proved in Chapter 2 implies that every such a set can be written in the form ⋃_{a∈A∩𝕊} ⋂_{b∈B∩𝕊} p(a, b) (as well as in the dual form) for some standard sets A, B and an internal function p with domain A × B, hence coded by the triple (A, B, p) ∈ 𝕀.

The main purpose of EEST and 𝔼 is to serve as a base for the construction of a more complex universe 𝕃[𝕀] of sets constructible from internal sets, containing (besides sets from 𝔼) also definable sets of sets from 𝔼, definable sets of such sets, etc. 𝕃[𝕀] is described and coded in 𝕀 as the minimal cummulative extension of 𝔼 along well-founded trees decorated by internal sets. (𝕃[𝕀]; ∈, st) is shown to satisfy HST, proving what is called internal core interpretability of HST in BST, as well as standard core interpretability of HST in ZFC. In particular, HST is a ”realistic” nonstandard set theory like BST. The equiconsistency of HST with both BST and ZFC immediately follows.

The constructible HST model 𝕃[𝕀] exhibits some special features, not provable in HST alone, e.g., ∗-infinite internal sets with different internal cardinalities remain externally non-equinumerous in 𝕃[𝕀]; moreover, there exist externally non-equinumerous infinite ∗-finite internal sets in 𝕃[𝕀].

Chapter 6. Partially saturated universes and the Power Set problem. Unlimited Saturation implies that the external subsets of any infinite internal set form a proper class; henceforth it is incompatible with the Power Set axiom. However, for each well-founded infinite cardinal κ, the universes 𝕀 and ℍ admit certain subuniverses 𝕀_{κ} ⊆ 𝕀 and 𝕃[𝕀_{κ}] ⊆ 𝕃[𝕀] ⊆ ℍ, satisfying HST with Saturation (a bit stronger than that) restricted to families of size ≤ κ plus (full) Power Set and Choice restricted to families of size ≤ 2^{κ}. Here, 𝕀_{κ} consists of all internal sets belonging to standard sets of internal cardinality ≤ ^{∗}κ.

There is also another version, with suitable subuniverses I ⊆ 𝕀_{κ} and 𝕎𝔽[I] ⊆ ℍ satisfying even full Choice and Power Set along with HST with Saturation restricted to families of internal sets of size ≤ κ.

A unifying idea behind the constructions consists in extending the universe 𝕊 of standard sets to the universe 𝕊[w] = {f(w): f ∈ 𝕊is a function ∧ w ∈ domf ⊆ 𝕀} of sets standard relative to a given internal set w. In particular, 𝕀_{κ} = 𝕊[^{∗}κ].

Chapter 7. Forcing extensions of the nonstandard universe. Regarding internal sets as a kind of urelements and using the Regularity of ℍ over 𝕀, a method of forcing respecting Standardization (i.e., producing no new standard sets) is developed and applied to models of HST.

As the first result, it is shown how two internal sets of different infinite internal cardinalities in a ground model of HST (ℍ = 𝕃[𝕀], say) can be made equinumerous in its appropriate generic extension. Together with the results of Chapter 5 this shows that, for instance, the statement ”the internal sets ∗ℕ and ^{∗}ℝ have the same (external) cardinality” is independent of HST.

A more involved application is the proof of consistency with HST of the isomorphism property IP introduced by C. W. Henson ^{7}: there is a model of HST in which any two elementarily equivalent internally presented structures of any first order language of standard size are isomorphic. In particular, under IP any two (externally) infinite internal sets (i.e., structures of the language of pure equality) are equinumerous. A rather welcome consequence is the essential uniqueness of the canonic extensions of classical first order structures. More precisely, if M = (M; …) ∈ 𝕎𝔽 is a structure of a standard size first order language L, then any internally presented Lstructure elementarily equivalent to M is isomorphic to its canonic extension ∗ML. In particular, this applies to the canonic extensions ^{∗}ℕ and ^{∗}ℝ of the classical natural numbers ℕ and real numbers ℝ, respectively. This makes IP into a promising candidate for an additional axiom extending HST but incompatible with the ”axiom of constructibility” ℍ = 𝕃[𝕀].

Chapter 8. Other nonstandard theories. As a matter of fact, there is currently no generally accepted ”canonic” foundational framework for nonstandard analysis. If the authors were not convinced that their theory is the right candidate for that task, they hardly would undertake the immense work in writing the present book. Therefore, the comparison of HST with other nonstandard set theories by them is a delicate issue, as one could easily apply to other theories improper standards, adequate for HST but falling short for others. The authors seem aware of that and one has to appreciate their fairness in taking care not to forget to mention any merits of the ”rival” theories.

7J. Symbolic Logic 39 (1974), 717–731; MR0360263 (50 #12713)

It would not make much sense to review here the authors’ reviews of the nonstandard theories by Kawaï, Hrbaček, Ballard-Hrbaček, Benci-di Nasso, Gordon, etc., and it would not be possible within a reasonable length. Let us just mention that, among other aspects, particular attention is payed to different measures applied in order to avoid the Hrbaček paradox than those adopted by HST.

Chapter 9. ”Hyperfinite” descriptive set theory. Given an internal (typically even a hyperfinite) set, one can build the usual Borel and projective hierarchy over its internal (hyperfinite) subsets in essentially the same way (in particular using just countable unions and intersections and not the standard size ones) as over open sets in a Polish, i.e., separable metric space. There is a handful of results in ”hyperfinite” descriptive set theory which are quite analogous to their Polish counterparts, whith Saturation replacing completeness or compactness in some arguments. Several proofs, however, making use of Transfer and hyperfinite combinatorial arguments, are often rather different. Additionally, the ”hyperfinite” projective hierarchy is part of a more extensive system of the so-called countably determined (CD) sets, with nice closure properties and no direct analogue in Polish spaces. These results require just Saturation restricted to countable families of internal sets and could equally well be (in fact originally were) proved within different nonstandard frameworks providing a sufficient supply of external sets.

Applications include results on Loeb measures and probability theory in hyperfinite domains, some intrinsically nonstandard topics concerning cardinalitiy theories for Borel and CD sets and some hyperfinite Ramsey type theorems for CD sets.

Let us mention two intuitively appealing results on Borel and CD cardinals. If A, B are two infinite ∗-finite sets with internal cardinalities m, n ∈ ∗ℕ ∖ ℕ, then there is a bijection A → B with Borel graph if and only if m/n is infinitely close to 1, and there is a bijection A → B with countably determined graph if and only if m/n is neither infinitely big nor infinitesimal.

Finally, we quote a Ramsey type result, using this opportunity to fix a mistake in the conclusion of Theorem 9.7.7, reproduced also in its (otherwise correct) proof. If k ∈ ℕ, ν ∈ ^{∗}ℕ ∖ ℕ and E is a CD equivalence relation on the set [ν]^{k} of all k-element subsets of ν = {0, 1, …, ν − 1}, such that there is no infinite internal pairwise E-inequivalent set I ⊆ [ν]^{k}, then there is an infinite internal E-homogeneous set A ⊆ ν (i.e., uEv for all u, v ∈ [A]^{k}). With A ⊆ [ν]^{k}, as stated, this would not make much sense.

Having passed through the book, the reviewer agrees with the authors in the point that HST seems so far to be the only nonstandard theory disposing of a satisfactory universe of external sets, which at the same time is ”realistic,” i.e. interpretable in ZFC in such a way that the class of all standard sets coincides with the ZFC universe, provides every classical structure M with a canonic elementary extension ^{∗}M, with the degree of saturation not limited by any in advance chosen cardinal, and guarantees enough space for ”peaceful coexistence” of the model-theoretic and IST-like versions of nonstandard analysis.

So has the problem of finding the nonstandard set theory finally been solved and decided in favour of HST? Well, from the philosophical and metamathematical point of view the positive answer seems very likely. However, it is neither philosophy nor metamathematics but the ”nonstandard practicioners” who will decide. And this could be a problem. As a—most probably unavoidable— byproduct of having successfully mastered all the above-mentioned problems, the axiomatic system of HST became rather a sophisticated one. Comparing with standard set theories, like ZFC, formulated in a single universe, in the formulation of HST from the very beginning four(!) universes 𝕎𝔽, 𝕊, 𝕀 and ℍ are involved. Thus—unlike, say, ZFC—to grasp HST intuitively, before rather detailed acquaintance with its formal system and at least some experience with nonstandard analysis, seems impossible and requires a serious study even from a reader well trained in logic and set theory.

Fortunately, HST includes a considerably simpler fragment, namely the bounded set theory BST (with just two universes 𝕊 and 𝕀), which could be adopted by the IST followers almost without any change in their habits, with the extra advantage of legalizing the informal use of external sets and backward reference to classical (i.e., well-founded) set-theoretical structures. One only has to be careful in applying external Choice and the Power Set operation. Under the same caution HST can serve the ”model-theoretic nonstandard analysts” as well, offering them the luxury of unlimited Saturation and breaking the walls of their traditional ad hoc ”superstructure prisons”.

Of course, luxury is not free, nor does it free one from longing for the former lucky modesty. This needs not become manifest as long as nonstandard analysis is used just as a tool for proving results about mathematical structures sitting firmly in the ”standard” ZFC universe. However, as soon as nonstandard analysis starts to deal with its intrinsic problems, formulated from the beginning in terms of standard, internal and external sets (which seems to be an increasing trend), there naturally arise questions about the minimal degree of Saturation needed for their proof, or, more generally, about the frameworks within which they can be proved or refuted, transcending the limits of any single nonstandard set theory. However, even in such a case HST seems to offer a sufficient variety of subuniverses or consistent extensions by additonal axioms that can be used to deal with such questions.