Uniqueness of standardization So I'm reading Kanovei's and Reeken's book "Nonstandard Analysis, Axiomatically" and there is something which I'm not quite understanding.
So, in page 15, it is stated that a "standardization" of a set is unique, i.e one of the axioms is:
$$\forall{X} \exists^{st}{S} (X \cap \mathbb{S} = S \cap \mathbb{S})$$
and it is said that this set $S$ is unique
To put it into context:
So, in this universe (the HST one), there is a fundamental unary predicate $st(\bullet)$ which is used to say that a certain set is standard. Since this is supposed to correspond to our usual ZFC universe, it assumed that the standard sets satisfy a standardization of ZFC, meaning a subset of the axioms of HST is $\text{ZFC}^{st}$ which means substituting $\forall{x}\phi$ for $\forall^{st}{x}\phi := \forall{x}(st(x) \implies \phi)$ and $\exists{x}\phi$ by $\exists^{st}{x}\phi:= \exists{x} (st(x) \wedge \phi)$, where recursively, the quantification step in a construction of a formula is the only step where anything changes.
Then, we have internal sets, which are sets $x$ such that $\exists^{st}{y} (x \in y)$.
And if $\mathbb{S}$ denotes the universe of standard sets and $\mathbb{I}$ the universe of internal sets, right away we will get that $\mathbb{S} \subseteq \mathbb{I}$, but a priori they're not the same. Well, if $\mathbb{S}$ is a $\text{ZFC}^{st}$ universe, doesn't the extensionality axiom imply that a standard set is determined by its standard elements? But what about its internal (but nonstandard) elements? Am I interpreting all of this correctly? So, we would have kind of an "overspill" axiom? If so, can anyone give me an idea of why we would want it to be this way?
Thank you for all the help in advance :)
 A: Based on the comments, I hope the following will mostly answer the questions.
I.

Well, if $S$ is a ZFC$~^{st}$ universe, doesn't the extensionality axiom imply that a standard set is determined by its standard elements?

Indeed, if two standard sets $x,y$ have the same standard elements, then they are the same set, so $x=y$. This means that if two standard sets have the same standard elements, then they have the same nonstandard elements as well.
If you have managed to prove that $\mathbb{N}$ and some other standard set $S$ have exactly the same standard elements, then by transfer it follows that they have the same elements (standard or nonstandard, $\forall x. x \in \mathbb{N} \leftrightarrow x \in S$). By the axiom of extensionality, this means that $\mathbb{N} = S$. In particular, a nonstandard $\omega \in \mathbb{N}$ would also satisfy $\omega \in S$.
II.
While all standard sets are internal (if $x$ is standard, then so is $\{x\}$, and $x \in \{x\}$), not all internal sets are non-standard. For example, the set of natural numbers $\mathbb{N}$ is infinite, so it will contain some nonstandard ("infinite") natural $\omega \in \mathbb{N}$.
Moreover, notice that the nonstandard set $T = \{x \in \mathbb{N} \:|\: x < \omega\}$ and the standard set $\mathbb{N}$ have the same standard elements. However, $T \neq \mathbb{N}$, since $\omega \in \mathbb{N}$ but $\omega \not\in T$.
III.

If so, can anyone give me an idea of why we would want it to be this way?

Here's how I think about it. Your friend, who lives in the extended/nonstandard universe, thinks of a function $f: \mathbb{N} \rightarrow \{0,1\}$. , e.g. the indicator function of some nonstandard $\omega \in \mathbb{N}$ (i.e. $f(x) = 1 \leftrightarrow x = \omega$).
You, living in the standard universe, try to understand which function your friend is thinking of. So you ask a couple of questions:

*

*What is the value of $f(0)$? Your friend answers $0$.

*What is the value of $f(1)$? Your friend answers $0$.

*What is the value of $f(2)$? Your friend answers $0$.

*What is the value of $f(3)$? ...

and so on until you exhaust all the numbers in your standard universe. From your perspective, your friend just stated that the function takes the value zero on all numbers. You never asked about $\omega$, simply because there's no such number in your universe!
So you rightfully conclude, based on the information provided, that your friend's function must be the constant zero function! If it wasn't, there'd have to be some number $k$ such that $f(k) \neq 0$, but you've just checked that there isn't.
So it's not so much that we "want" this, but that we must have it this way: every function clearly determines some standard function, but two functions have to be the same if they take the same values on every argument, and this fact has to hold in the standard universe. And that's why standardization works the way it does.
