In 2003 Kanovei and Shelah constructed a definable hyperreal field. The ultrapower used exploits a fairly large index set so that it is clear that the usual proof of Los and transfer does not go through with merely ACC (countable choice). IS there a model of ZF+ACC where transfer actually fails for the definable hyperreal field of Kanovei and Shelah?

3$\begingroup$ Don't we expect models of ZF+ACC where the definition fails, simply by lack of ultrafilters? $\endgroup$ – Joel David Hamkins Jun 20 '16 at 13:19

$\begingroup$ @JoelDavidHamkins, the definition is a formula in ZF. Otherwise one couldn't speak about a definable object at all. The magic trick is that in order to prove that the extension is actually proper you need more axiomatic material. In other words, models where there are no ultrafilters will simply give you the same field you started with.Notice that transfer happens to be true for the trivial extension :) $\endgroup$ – Mikhail Katz Jun 20 '16 at 13:30
In this arxiv post (to appear in Journal of Symbolic Logic) we prove the existence of an explicitly definable settheoretic construction in ZF (without if/else clauses) of a hyperreal extension ${}^\ast\mathbb R$. If in addition countable choice is assumed then we prove that the transfer principle holds for this $^{\ast}\mathbb R$. Assumping the existence of a free ultrafilter on $\mathbb N$ with wellorderable base (an assumption weaker than the wellordering of $\mathbb R$) we show that the extension $\mathbb {R}\hookrightarrow{}^\ast\mathbb R$ is proper.
As mentioned for this definable model ACC proves transfer so transfer can't fail in ZF+ACC.

1$\begingroup$ Do you mean something precise and robust when you say "without if/else clauses"? For example, is your definition a positive formula? Otherwise, one could imagine simply disguising an if/else clause with a logical variant, but of course that is not what you mean. So what is it that you mean? $\endgroup$ – Joel David Hamkins Jul 4 '17 at 12:25

$\begingroup$ @JoelDavidHamkins, I would have liked to say that our formula works in intuitionistic logic but I don't know enough about it to be able to make such a claim. Perhaps some of the experts here can help. It any rate it is a completely deterministic explicit construction of an ultrafilter by specifying a suitable ordinal and considering all surjections from this ordinal to free ultrafilters on N. This gives an index set. By tensoring together different ultrapowers and using "threads" (Keisler's terminology) in a direct limit of all these tensors, we get the required definable ultrafilter. $\endgroup$ – Mikhail Katz Jul 4 '17 at 13:43

$\begingroup$ By the way no mention of "if/else" clauses appears in the article; it was my way (as you point out, imperfect) of characterizing the construction. $\endgroup$ – Mikhail Katz Jul 4 '17 at 14:02

$\begingroup$ "we get the required definable ultrafilter" Do you really mean a definable ultrafilter, or definable *hyperreal extension"? $\endgroup$ – Noah Schweber Jul 4 '17 at 16:09

$\begingroup$ Is the idea that you are taking a direct limit of all ultrapowers and thereby avoiding the need to pick a particular one? $\endgroup$ – Joel David Hamkins Jul 4 '17 at 17:33