Transfer with minimal choice

Question

Let FUF postulate the existence of a Free UltraFilter on $\mathbb{N}$ and ACC the axiom of countable choice. Consider the superstructure on $\mathbb{R}$ and its inclusion in the bounded ultrapower. Is there a reliable source proving that the transfer principle for this extension is provable in ZF+FUF+ACC?

Answer 1

Yes.

The following is due to M. Spector (Ultrapowers without the axiom of choice. J. Symbolic Logic 53 (1988), no. 4, 1208–1219; DOI: 10.1017/S0022481200028024, JSTOR)

The ultrapower embedding $j\colon M\to M^I/U$ is elementary if and only if for every family of non-empty sets indexed by $I$, there is $J\in U$ such that the subfamily indexed by $J$ admits a choice function.

Admittedly, he was talking about internal ultrapowers of the universe by a measure. But the proof is easy enough that you can replicate it for the general theorem.

In the one direction which is the one you are interested (as countable choice ensures a choice function exists), the usual proof of Los' theorem works out of the box. The use of choice comes when you want to prove that if $\{i\mid M\models\exists x\varphi(x)\}\in U$, then there exists $g\colon I\to M$ such that $\{i\mid M\models\varphi(g(i))\}\in U$.

This is exactly the place where we appeal to the choice from $I$ modulo $U$. Here we assume countable choice, then it works fine.