In this question, I asked how to interpret a historical claim made by Conway regarding the potential, if not ideal, use of the surreal numbers for nonstandard analysis. In the comments and answers it was noted that the surreals are isomorphic to the proper class-sized hyperreals, as shown in this paper by Philip Ehrlich. Sam Sanders then mentioned the following in his answer:
"Transfer is only available for the surreals via isomorphism at class level with the hyperreals (constructed via a limit ultrapower)."
This claim has also been made before, e.g. in this answer by Mikhail Katz:
"Namely, there is no transfer principle in the surreals other than the one transfered from the hyperreals."
The first question is, is this claim to be interpreted in some rigorous way as an absolute truth, e.g. is there some kind of theorem we have showing this? Or does it simply means that nobody knows how to do it otherwise as of 2022?
The second question is, assuming that it is true, we can then ask how strong of a set theory we need to prove that some kind of undefinable surreal transfer principle is even capable of existing to begin with. That is, the surreals exist in many set theories in which the hyperreals do not. We can directly ask, then, how strong of a set theory we need to be able to show something like: for each first-order-definable function $f: \Bbb R^n \to \Bbb R$, there exists an extension $\mathbf{f}: \mathbf{No}^n \to \mathbf{No}$ that satisfies every first-order property of the original $f$. If we do this, do we get something equivalent in strength to the ultrafilter lemma? Stronger? Weaker?
(I am never quite sure how to formalize some of these questions from a foundational standpoint, whether we should use NBG or just talk about the surreals below some inaccessible cardinal, so will leave it open.)
