Consider the first Cohen model, i.e. let $M$ be a countable transitive model of ZFC + $V=L$, let $\mathbb P$ be the poset consisting of finite partial functions from $\omega\times\omega$ to $2$, let $M[G]$ the generic extension adding a sequence $\{a_n\}_{n\in\omega}$ of generic subsets of $\omega$, and let $M\subset N\subset M[G]$ the symmetric model consisting of the sets $\sigma_G$, where $\sigma\in SM^\mathbb P$ is a hereditarily symmetric name, where $\sigma$ is symmetric if there exists a finite set $x\subset\omega$ such that each permutation $f$ of $\omega$ fixing $x$ induces an automorphism of $\mathbb P$ which induces a map $M^\mathbb P\longrightarrow M^\mathbb P$ that fixes $\sigma$.

Now, the ultrafilter $G$ does not belong to $N$, and so, the map $SM^\mathbb P\longrightarrow N$ given by $\sigma\mapsto \sigma_G$ is not definable in $N$.

However, for each finite $x\subset \omega$, we can consider the set (class in $M$) $SM^\mathbb P_x$ of all $\sigma\in SM^\mathbb P$ fixed by all permutations fixing $x$, as well as $N_x=\{\sigma_G\mid \sigma\in SM^\mathbb P_x\}$.

I guess that the map $SM^\mathbb P_x\longrightarrow N_x$ given by $\sigma\mapsto \sigma_G$ should be definable in $N$ from the set $A=\{a_n\mid n\in\omega\}\in N$, the map $f_x:x\longrightarrow N$ given by $f_x(n)=a_n$ (notice that $f_x\in N$) and maybe other parameters in $M$.

My question is if this is true, and the motivation is that I am trying to simplify the exposition of Halpern and Lévy "The Boolean Prime Ideal Theorem does not Imply the Axiom of Choice" by showing that the Cohen model is a model of the theory SP described there, but avoiding the formal languaje used to formulate it. I see that all the axioms have a clear translation in standard terms of forcing but the last one, which asserts more or less what I am trying to prove.

Anyway, do you know if something like this is already done?


While not an answer to your question directly, here is some information which you might consider useful. (See edit for that part.)

In Jech The Axiom of Choice he points out that the proof of Halpern-Levy is much more difficult than the proof of Halpern that $\sf BPI$ holds in the Mostowski permutation model. He points out that it seems impossible to escape the technically difficult Halpern-Lauchli lemma.

Chapter 5 includes a proof that in Cohen's first model the order principle holds, and a similar construction is given. You might want to look at that.

Flegner's book Models of ZF Set Theory also has a section devoted for this proof. However the book itself was written when forcing was still being developed, and it's often not as readable as other modern sources, making it less ideal source for learning actual proofs.

I don't recall any other major books about the axiom of choice where the proof is presented. But one perhaps can give a whole other proof using the following information.

We say that $M\models\mathsf{SVC}(s)$ if for every $x\in M$ there is (in $M$) an ordinal $\alpha$ such that $M$ knows about a surjection from $s\times\alpha$ onto $x$.

Every model of $\sf AC$ is a model of $\sf SVC(\{\varnothing\})$, but symmetric extensions are always models of $\sf SVC$ for some set. In the paper where the axiom was suggested by Andreas Blass the following theorem is given:

Suppose that $M$ satisfies $\mathsf{SVC}(s)$, then $M$ satisfies $\sf BPI$ if and only if there exists an ultrafilter $U$ on $s^{<\omega}$ such that for every $x\in s$, $\{p\in s^{<\omega}\mid s\in\operatorname{range}(p)\}\in U$.

It might be worth pursuing this approach, if one just wants to show the consistency of $\sf\lnot AC+BPI$.

Note that if $D$ is any class of hereditarily symmetric names such that for some finite $E\subseteq\omega$ every permutation fixing all the elements in $E$ fixing all the names in $D$, then the following class name is also symmetric: $$f=\{(1,\langle(\dot x)^\check{},\dot x\rangle^\bullet)\mid \dot x\in D\}$$ (Where the $\bullet$ indicates some canonical encoding of the name for the ordered pair from the names appearing in it)

To see this, note that if $\pi$ is a function fixing $E$ (and thus all the names in $\dot D$) then we have $$\begin{align} \pi f &=\{(\pi1,\pi\langle(\dot x)^\check{},\dot x\rangle^\bullet)\mid \dot x\in D\}\\ &=\{(1,\langle\pi(\dot x)^\check{},\pi\dot x\rangle^\bullet)\mid \dot x\in D\}\\ &=\{(1,\langle(\dot x)^\check{},\dot x\rangle^\bullet)\mid \dot x\in D\}\\ &=f \end{align}$$

Now we have that $f_\sigma(\dot x)=\dot x_\sigma$, for every $\dot x\in D$.

  • $\begingroup$ Thank you very much! I will think carefully about all you have said. I did not pretend to avoid the Halpern-Lauchli lemma, but just the specific way Halpern and Lévy describe the sets of $N$. $\endgroup$ – Carlos Jan 5 '14 at 16:06
  • $\begingroup$ Oh, I didn't say that you do try to avoid it. I just pointed out that if one wants to write a full exposition on the independence of the Boolean Prime Ideal theorem from the Axiom of Choice, then it's going to be hard to avoid formal arguments at one point of another. $\endgroup$ – Asaf Karagila Jan 5 '14 at 16:11
  • $\begingroup$ Carlos, I've added an answer to your actual question. Let me know if it helps you out. $\endgroup$ – Asaf Karagila Jan 5 '14 at 17:39
  • $\begingroup$ Thanks again, Asaf! I had never seen class names, and so I have a doubt. Does the class name $f$ really define a class in $N$? If the generic ultrafilter would be available in $N$ the answer would be clearly yes. For instance, we can assign an ordinal rank to each name, and restrict $f$ to a set name $f_\alpha$ defined for names in $D$ of rank $\leq \alpha$. Then the sequence $\{f_\alpha\}_{\alpha\in ON^M}$ is definable in $M$ and each $(f_\alpha)_G\in N$, but, is the map $\alpha\mapsto (f_\alpha)_G$ definable in $N$? I cannot see this. $\endgroup$ – Carlos Jan 5 '14 at 19:05
  • $\begingroup$ Anyway, I will try to check if working witn large enough $\alpha$ suffices to follow the proof of Halpern and Lévy. $\endgroup$ – Carlos Jan 5 '14 at 19:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.