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?
$\begingroup$
$\endgroup$
2
asked Jun 20, 2016 at 7:07
-
4$\begingroup$ Don't we expect models of ZF+ACC where the definition fails, simply by lack of ultrafilters? $\endgroup$– Joel David HamkinsCommented Jun 20, 2016 at 13:19
-
1$\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 KatzCommented Jun 20, 2016 at 13:30
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
7
In this arxiv post (to appear in Journal of Symbolic Logic) we prove the existence of an explicitly definable set-theoretic 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 well-orderable base (an assumption weaker than the well-ordering 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.
answered Jul 4, 2017 at 8:03
-
2$\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$ Commented Jul 4, 2017 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$ Commented Jul 4, 2017 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$ Commented Jul 4, 2017 at 14:02
-
1$\begingroup$ "we get the required definable ultrafilter" Do you really mean a definable ultrafilter, or definable *hyperreal extension"? $\endgroup$ Commented Jul 4, 2017 at 16:09
-
1$\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$ Commented Jul 4, 2017 at 17:33