A question about the first Cohen model

Question

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?

Answer 1

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$.