To construct the hyperreals via ultrapower the Boolean prime ideal theorem apparently suffices. However, to prove the transfer principle for the extension $\mathbb{R}\subset{}^\ast\mathbb{R}$ apparently a stronger version of choice is needed. Does anybody have the details?
$\begingroup$ $\endgroup$
Add a comment |
1 Answer
$\begingroup$ $\endgroup$
4 The transfer principle, if I understand your question correctly, is the localized version of Łoś theorem for ultraproducts.
How much choice is needed in general for Łoś theorem? It was shown that BPI+Łoś imply choice over $\sf ZF$. But in models where there are no free ultrafilters, Łoś theorem is trivially true.
If you localize it to the case of $\Bbb R$ with the language of ordered rings, and only consider ultrapowers by $\Bbb N$ as an index set, then the answer is probably going to be something like "It is sufficient that Łoś theorem holds for ultrapowers of $\Bbb R$ by free ultrafilters - which are assumed to exist - over $\Bbb N$".
It's a disappointing answer, I agree.
If you want something sufficient and not optimal, then $|\Bbb R|=\aleph_1$ would certainly suffice.
- $\begingroup$ Wait a minute, I am precisely asking under what conditions Łoś's theorem is going to be true. Is it known for example that assuming boolean prime ideal is insufficient? $\endgroup$Mikhail Katz– Mikhail Katz2014-12-04 12:04:28 +00:00Commented Dec 4, 2014 at 12:04
- $\begingroup$ It is a theorem that BPI+Łoś implies AC. It is also known that if every ultrafilter is principal Łoś theorem is trivially true (since every ultraproduct is isomorphic to one of the structures in the product). So BPI is certainly not enough. $\endgroup$2014-12-04 12:08:55 +00:00Commented Dec 4, 2014 at 12:08
- 1$\begingroup$ I am a bit confused by the wording of your answer. As far as I understand it, BPI would imply the existence of a nonprincipal ultrafilter. Why do you need to mention the clause "which are assumed to exist"? Do you have a reference for BPI+Los->AC? $\endgroup$Mikhail Katz– Mikhail Katz2014-12-04 12:31:19 +00:00Commented Dec 4, 2014 at 12:31
- $\begingroup$ This should do nicely: dx.doi.org/10.1090/S0002-9939-1975-0384548-X $\endgroup$2014-12-04 12:47:03 +00:00Commented Dec 4, 2014 at 12:47