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})$.