In the foundations of NSA with ultrapowers, how much can the axiom of choice be weakened? The derivations I've seen of the hyperreals using ultrapowers use the axiom of choice and Zorn's lemma a lot. But looking closer, you can possibly weaken the axioms used in the derivations of some theorems?
For example, to derive a transfer principle, Łoś's theorem for ultraproducts by ultrafilters on ω only requires countable choice. Similarly, since it's possible to construct free filters on the integers (for example, the Frechet filter), the ultrafilter lemma (which only requires ZF + BPIT) implies the existence of a free ultrafilter.
BPIT still implies the existence of non-measurable sets though. Is it also possible to prove the existence of a free ultrafilter on the integers with just dependent or countable choice?
 A: Let's start at the beginning, shall we?
To construct the hyperreals by ultrapowers, we first need:

*

*One free ultrafilter over $\Bbb N$.

*More-or-less countable choice (restricted to sets of reals should be enough).

Neither of these is provable from $\sf ZF$, of course. So we need to assume both of these things. Countable choice comes in because we need the ultrapower embedding to be elementary. For that we need to prove that if $\{n\in\Bbb N\mid\Bbb R\models\exists x\varphi(x)\}\in U$, that is $\Bbb{R^N}/U\models\exists x\varphi(x)$, then there is $f\colon\Bbb{N\to R}$ such that $\Bbb R\models\varphi(f(n))$, which is really a choice function from a countable family of sets of reals. This sounds simplistic, since all the sets are supposedly definable by $\varphi$, but once you add parameters to $\varphi$ these sets vary, and once you remember that in NSA we tend to add predicates and function symbols to the language, it is clear why this is not trivial.
So depending on your exact use of the ultrapowers, you may require the countable choice part (I am willing to bet that just for the most simplistic ultrapower, without additional symbols to the language of ordered fields you might be able to avoid choice, due to quantifier elimination). But for proper use of NSA, you are probably going to need the most of it.
Right. So countable choice for sets of reals, does it imply the existence of a free ultrafilter? Well. No. Even the stronger axiom, Dependent Choice (which is stronger than countable choice, which is certainly stronger than countable choice for sets of reals) is not enough to show that free ultrafilters exists on $\omega$. The reason is that we know about models where this happens, but an even better reason is that a free ultrafilter on $\omega$ shows that there are non-measurable sets (it is a non-measurable subset of the Cantor space with its standard probability measure), and so due to Solovay we know that Dependent Choice is just not enough to get us there.
