Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
I believe that I can prove that it is consistent with IST that from the given notion of standardness we can define another alternative notion of standardness, which also fulfills IST in the same universe of sets.
@MikhailKatz No, we are talking about different things, and this is now a side issue to the main question, so perhaps best to just drop it. (I was not referring to constructing $\mathbb{R}^*$ inside IST, but rather to the question of whether the concept of "standard" is categorical in a given model of IST, and I believe that it is not. Since "standard" is not definable in the internal language, it follows by the Beth definability theorem that there will be models with the same sets, but different notions of standardness.)
I think it has to do with the non-categoricity of the concept of "standard" and "nonstandard". A given IST set theoretic universe can admit diverse inequivalent standardness concepts in such a way so as still to realize IST, and they do not all have isomorphic $\mathbb{R}$s.
@MikhailKatz That is indeed the question. If CH fails, then in ZFC there are many nonisomorphic countably saturated real-closed fields of size continuum. Presumably this would show up in IST as non-categoricity for $\mathbb{R}$ (that is, for what other people call the hyperreals $\mathbb{R}^*$). I would want to hear from the IST experts. Same question for $\mathbb{N}$. I have pointed to the lack of a categoricity result for $\mathbb{R}^*$ as an important part of the explanation for hesitancy toward nonstandard analysis in mathematics.
@JesseElliott No, this is a different kind of independence. In ZFC, we can prove that there is a unique class of all sets, just like we can prove there is a unique complete ordered field up to isomorphism and a unique model of Dedekind arithmetic up to isomorphism. But we have no such account in ZFC of "the" hyperreals. We are lacking a categorical theory. (But in ZFC+CH, there is such a categorical account--the hyperreals are the smallest countably saturated real-closed field.)