@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.)

Oops, yes, but also M Katz,who has also answered here. I have edited.

Apart from any claims made about $F$ or axioms, the logic $L_{\Omega^+,\Omega^+}$ just in the language of $=$ can interpret ZFC on any domain of size at least $\Omega$, since the infinitary language allow us to quantify over objects of size less than $\Omega$, and with this we can talk about well-founded extensional relations coding arbitrary elements of $V_{\Omega}$. For example, there is a tuple coding $V_\Omega$, which is a model of ZFC, and so we can interpret ZFC. Indeed, we can interpret KM this way as well.

It's because every subforcing of a countable forcing notion is countable, hence is itself Cohen forcing.

See mathoverflow.net/a/436348/1946 for reasons why one might view Zorn's lemma, in its entirety, as a pedagogical substitute for transfinite recursion.

I think this is well known, but I don't have a specific reference at hand.