In the the book The Axiom of Choice section 5.5, Jech presents a proof of the independence of the axiom of choice from the ordering principle (every set can be linearly ordered). There are some statements that are unclear to me.
In there $\mathcal{M}$ denotes de ground model, $\mathscr{G}$ the subgroup of permutations, $\mathscr{F}$ de normal filter, and $HS$ the class of hereditarily symmetric. $\mathcal{N}$ the corresponding symmetric extension. The statements that are a little bit unclear to me are the following:
We shall make an assumption that simplifies matters for us a little. We shall assume that $\mathcal{M}$ is a class of the model $\mathcal{N}$. This is the case, e.g., when $\mathcal{M} = L$, but in general it need not to be true. More generally, let us say that a class $C \subseteq HS$ is symmetric if $\{\pi \in \mathscr{G} : \pi"C = C\} \in \mathscr{F}$.
We make the assumption that for each symmetric class $C$, its interpretation $i_G(C) = \{i_g(x) : x \in C\}$ is a class of the model $\mathcal{N}$
Since I'm trying to understand the proof, and also translate it to the ctm approach to forcing, I think I can achieve the first assumption by working in an extended language with $\mathcal{M}$ as a new constant symbol, as explained in (for example) Kunen's book. Then $\cal{M}$ would always be definable. But then it wouldn't be necessary to have $\mathcal{M} = L$, and would work for any $\mathcal{M}$, so probably not doing something right.
In general I would like to better understand why are these assumptions necessary, and also why can we make those assumptions.
Also. Would it be right to maybe do the whole construction of the class of supports inside some $V_\alpha^\mathcal{M}$ (with $\alpha$ limit ordinal), to avoid working with classes. Those maybe achieving the independence result, but not the uniform version of it?
Finally. Is there another source for this result (with the symmetric extensions approach, but not ramified forcing)?
Edit (Follow up question): While I'm very interested on @asaf answer. I think it might be a little bit much for me right now. I wanted to try proving something "simpler", maybe something that just works with the example at hand. So I started trying to prove that symmetric classes of hereditaely symmetric names, map via interpretation to classes of $\mathcal{N}$. Then I stumbled with a very similar doubt posted in MO https://mathoverflow.net/questions/153650/a-question-about-the-first-cohen-model. And sure enough, also answered by @asaf.
While trying to prove this thing I actually got to the same problems posted in the comments of @asaf answer there. Defined the same $f_\alpha$'s, but then what about the map $\alpha \mapsto f_\alpha$. I would like it to be definable in $\mathcal{N}$. But it seems circular, since $\alpha \mapsto f_\alpha$ is also a symmetric class of symmetric names.
In the same comments @asaf writes that is acutally not known if these calsses are necessarily definable in $\mathcal{N}$. My questions are:
Is this resolved? Maybe by things related to @asaf answer here?
I'm also having trouble to identify $M=L$ role here. Does $M=L$ suffices to show that these classes are definable in $\cal{N}$?
Actually, we know now that the assumption that $\cal M$ is a class of $\cal N$ is in fact a theorem, not an assumption. Although back in the 1970s this was not known.
Namely, if $\cal M$ is a model of $\sf ZFC$ and $\cal N$ is a symmetric extension of $\cal M$, then $\cal M$ is definable in $\cal N$. Here the assumption of $\sf ZFC$ is very important. For the specific case of symmetric extensions this is a fairly straightforward application of several theorems that were known in the 1970s (along with the ground model definability in $\sf ZFC$ which was proved in the 2000s), but Usuba have developed a (possibly) broader context in which this definability assumption holds in the past few years using the concept of Löwenheim–Skolem cardinals.
In general, if you read closely, what Jech is proving in his context, is that there is a global linear ordering of the Cohen model, which is something that relies very heavily on the fact that the ground model is not only definable, but also definably well-ordered. That is, that global choice holds in the ground model. Of course, this need not be the case, in which case we do have to resort to using $V_\alpha^\cal M$ as a local parameter to get that every set can be linearly ordered.
Let me explain how to prove the definability of the symmetric ground, which was something I noticed in my Ph.D. years, but shortly thereafter, Usuba had his bigger and better result.
Grigorieff showed that if $G\subseteq\Bbb P$ is an $\cal M$-generic filter for $\Bbb P$, and $(\Bbb P,\mathscr{G,F})\in\cal M$ is a symmetric system, then there is a homogeneous forcing in $\rm HS_{\scr F}^G=\cal N$ such that $G$ is generic for it. In other words, $\mathcal M[G]$ is a generic extension of $\cal N$ by a homogeneous forcing.
If $\cal M\models\sf ZFC$, then it is definable in $\mathcal M[G]$ using a parameter from $\cal M$, and therefore it is definable in $\cal N$ using that parameter. Simply ask which elements of $\cal N$ are going to satisfy the predicate in $\mathcal M[G]$. By the homogeneity, the maximum element must have decided such statements on all the elements of $\cal N$, as long as the parameters are in $\cal N$, let alone in $\cal M$.
If $A\subseteq\cal N$ is a class of $\mathcal M[G]$ definable using parameters from $\cal N$ then it is a class of $\cal N$. This is the same argument as above. Since $\cal N$ is a class of $\mathcal M[G]$, we can ask, given a class of $\mathcal M[G]$ which is definable only using parameters in $\cal N$, if an element of $\cal N$ is in that class or not. By homogeneity, the answer will not depend on the generic filter, so this is definable in $\cal N$. And so, it is not hard to see that given a symmetric class name, it defines a class in $\mathcal M[G]$ which does not depend on the generic (as it is symmetric). This is particularly true in the case of the Cohen model where the original forcing is homogeneous as well. And so, we get that the global linear order, or the choice of minimal support, is something that is globally definable.
There is, of course, another way. If you think of the Cohen model as $L(A)$ or $V(A)$, where $A$ is the set of Cohen reals, then one can simply write out a definition for these global functions.