What are the minimal requirements for the definable hyperreal field plus transfer? It is interesting that to prove the transfer principle for the definable hyperreal field, one requires no more choice than for proving, for instance, the countable additivity of the Lebesgue measure. The usual ultrapower construction of a hyperreal field $\mathbb{R^N}/\mathcal{F}$ is not functorial due to the dependence on $\mathcal{F}$. Kanovei and Shelah developed a functorial alternative to this, by providing a construction of a definable hyperreal field. 
The idea is as follows. One starts with the set (possibly empty; this will depend on the background model of set theory) of free ultrafilters $\mathcal{F}$ on $\mathbb{N}$ parametrized by the least ordinal that can map surjectively onto such an $\mathcal{F}$. One orders them lexicographically. One introduces a tensor product operation that enlarges the index set to Cartesian products of finitely many $\mathbb{N}$. One exploits the tensor product to organize the various ultrapowers into a direct limit, whose elements are ``threads'' generated as unions. Since finitely many elements already coalesce at a finite stage in the direct limit, the proof of the transfer principle only uses the axiom of countable choice (ACC). 
The Kanovei-Shelah (KS) construction can therefore be viewed as a functor which, given a model of set theory, produces a hyperreal field. A transfer theorem here can apparently be proved using only the axiom of countable choice (ACC). It would be interesting to separate the issue of the satisfaction of transfer from the issue of properness of the extension. 
Question. What would be a collection of minimal foundational conditions to guarantee that (1) the KS construction goes through, and (2) the resulting extension satisfies a transfer principle? 
This seems of philosophical interest because apparently very little is required here, contrary to popular belief that the full power of AC is needed to make transfer work. The latter may be true in the model-theoretic approach using the compactness theorem, but passing via ultrapowers seems to reduce the foundational requirements. Whatever model of ZF+ACC one starts with, one hopes to get a KS hyperreal field that will satisfy transfer. Here some models will be proper extensions and others not, but the proof should work in general. The point is to prove transfer without committing oneself to any free ultrafilters yet. To guarantee that the extension is proper of course requires an ultrafilter. 
The KS construction requires in addition to ZF, the existence of a least ordinal mapping surjectively to $\mathcal{P}(\mathbb{N})$. Such an ordinal is used in the KS construction. The minimality of the ordinal apparently serves to ensure that the construction is definable, by virtue of the uniqueness of the said ordinal. Once one has the KS extension, transfer apparently follows from ACC, or alternatively from WO since ACC is apparently only applied to subsets of $\mathcal{P}(\mathbb{N})$.
 A: Since ACC is only applied to subsets of $\mathcal{P}(\mathbb{N})$ - that is, to families of sets of reals - the answer is that only the well-ordering of $\mathbb{R}$ is needed. Indeed, if $\mathbb{R}$ is well-ordered by $\prec$, then given any family of nonempty sets of reals $F=\{A_i: i\in I\}$, we may define a choice function for $F$ by picking the $\prec$-least element of each $A_i$: $$f(i)=r\iff [r\in A_i\wedge\forall s\in A_i(s\not=r\implies r\prec s)].$$ So no additional choice is needed.
Meanwhile, the following are equivalent over ZF (in fact, over much less):


*

*(i) $\mathbb{R}$ is well-orderable.

*(ii) There is some ordinal $\alpha$ which surjects onto $\mathbb{R}$.

*(iii) There is a least ordinal $\alpha$ which surjects onto $\mathbb{R}$.
Proof: (i) implies (ii): every well-ordered relation on a set is in bijection with some ordinal. 
(ii) implies (iii): every nonempty set of ordinals has a smallest element; apply this to the set of ordinals surjecting onto $\mathbb{R}$.
(iii) implies (i): Suppose $\alpha$ surjects onto $\mathbb{R}$ via $f$ (we need not assume $\alpha$ is the least such - this is equally a proof from (ii), which is trivially implied by (iii)). For $r\in\mathbb{R}$, let $g(r)$ be the least $\beta<\alpha$ such that $f(\beta)=r$; $g(r)$ is always defined since any set of ordinals has a least element. Now let $r\prec s$ iff $g(r)<g(s)$; it is easy to see that this is a well-ordering on $\mathbb{R}$.
A: Fairly minimal requirements seem to be ZF plus countable choice plus existence of a free ultrafilter with well-orderable base, as noted by Vladimir in a comment above.  See also this answer.
