In Woodin's "In the Search of Ultimate-$L$", in section $3.5$ on extenders, he uses an example which I have a hard time understanding. He essentially constructs two transitive models of $\mathsf{ZFC}^-$ with an elementary embedding between them, which is cofinal and is the identity on the ordinals but is not the identity!
I would appreciate any clarification on this. First let me quote the relevant bit:
Let $L[G]$ be a generic extension of $L$ for adding $\omega_2^L$ many Cohen reals and let $L[G][g]$ be a generic extension of $L[G]$ for adding $\omega_2^L$-many Cohen reals.
Now define $$M=L_{\omega_2^L}(\mathbb{R}^{L[G]})[G]$$ and define $$N=L_{\omega_2^L}(\mathbb{R}^{L[G][g]})[G][g],$$ where each is viewed as a transitive set. Thus in each case we are constructing
over the reals from an additional predicate. Note that $P(\omega)$ exists in both
$M$ and $N$ but for example, $P(\omega_1)$ does not exist in either $M$ or $N$.It follows by the homogeneity of Cohen forcing that both $M$ and $N$ are
models of ZFC\Powerset with the usual formulation of the Axiom of Choice
and that the natural map $$\pi:M\rightarrow N,$$ where $\pi(\mathbb{R}^M)=\mathbb{R}^N$ is an elementary embedding.
Now I think I understand the construction and I think that the natural map is given by exactly setting $\pi(\mathbb{R}^M)=\mathbb{R}^N$ and $\pi|\mathbb{R}^M=\operatorname{id}_{\mathbb{R}^M}$ and for other sets in $M$, since we build it level by level with definable subsets and we know where to send each parameter, we know where to send each $x\in M$ level by level.
Now what I have trouble with, would be to check that elementarity and that these are models of $\mathsf{ZFC}^-$. As hinted, I tried to use homogeneity of the Cohen forcing to show elementarity, but for formulas that have parameters in $M$, I don't see how we can get rid of the parameters. And also between the axioms of $\mathsf{ZFC}^-$, choice is the one which is the most elusive for me, as although I don't have a formal argument for the others, but they seem plausible and usually in these circumstances we don't have choice. So my questions are: How can we show that $1) \mbox{ }\pi$ is elementary and $2) \mbox{ } M$ and $N$ are models of $\mathsf{ZFC}^-$, especially choice?
EDIT: I have doubts on why $\pi$ is even well-defined, as I have defined it above. Going level by level we may encounter several formulas with other parameters which define the same $x\in M$. And checking this is crucial in another sense, since later on when we prove elementarity, these different formulas should indeed correspond in a well-defined manner.
EDIT II: I was informed about this post from MO, which actually solves half of my question! By the argument in that proof $\pi$ is readily seen to be well-defined and elementary. But I am still not sure how we can show that $M$ and $N$ satisfy $\mathsf{ZFC}^-$, especially choice.
Best Answer
Edit: I have added an argument that shows choice in $M$ in terms of existence of choice functions.
Replacement in M: Here is an argument that shows $ZF^-$ in $M$ (the same works for $N$ of course):
Let $\mathbb R^G$ denote $\mathbb R^{L[G]}$. In a first step, we will see that in $M$ any definable map $f:\mathbb R^G\rightarrow \omega_2$ is bounded. In a second step I will explain how replacement follows. In $M$, all sets are definable from ordinal parameters, reals and proper initial segments of $G$. Since any real and any proper inital segment of $G$ is in an intermediate extension $L[G\upharpoonright \alpha]$ and since $L[G]$ is a further $Add(\omega, \omega_2)$-extension from there, we might as well assume that all parameters in the definition of $f$ are from the ground model and will suppress them in what follows. If $\dot x$ is a $Add(\omega, \omega)$-name, then by ccc, there is $\alpha_{\dot x}<\omega_2$ so that $1\Vdash f^{L_{\check\omega_2}(\mathbb R^\dot G)[G]}(\dot x)<\check\alpha_{\dot x}$. If $\dot y$ is any $Add(\omega, \omega_2)$-nice name for a real then there is an automorphism $\pi$ of $Add(\omega, \omega_2)$ that turns $\dot y$ into an $Add(\omega, \omega)$-name $\hat\pi(\dot y)$. But then $$1\Vdash f^{L_{\check\omega_2}(\mathbb R^\dot G)[\dot G]}(\hat\pi(\dot y))<\check\alpha_{\hat\pi(\dot y)}$$ implies $$ 1\Vdash f^{L_{\check\omega_2}(\mathbb R^{\widehat{\pi^{-1}}(\dot G)})[\widehat{\pi^{-1}}(\dot G)]}(\dot y)<\check\alpha_{\hat\pi(\dot y)}$$ Note that $f$ does not change as all the parameters in its definiton are in the ground model. Furthermore, it is easy to see that $$1\Vdash L_{\omega_2}(\mathbb R^{\widehat{\pi^{-1}}(\dot G)})[\widehat{\pi^{-1}}(\dot G)] = L_{\omega_2}(\mathbb R^{\dot G})[\dot G]$$ using that $\pi$ is definable in $M$. Thus $f^M(y)<\alpha_{\hat\pi(\dot y)}$ so that $f^M$ is bounded by $$\operatorname{sup}\{\alpha_{\dot x}\mid \dot x \text{ is a }Add(\omega, \omega)\text{-name}\}<\omega_2$$ We can use this to show that reflection is true in $M$.
Proof: We will do it by induction on the complexity of $\varphi$. The only difficult case is if $\varphi = \exists x \psi(x)$. Note that in $M$, any set is the surjective image of $\mathbb R^G\times\omega_1$ in $M$ (as all $L_\alpha(\mathbb R^G)[G]$, $\alpha<\omega_2$ are such an image). Even better, $\omega_1$ is the surjective image of $\mathbb R^G$ in $M$ so that all sets are the surjective image of a function with domain $\mathbb R^G$. Let $D$ be an $M$-definable club that witnesses our induction hypothesis for $\psi$. We can close some $L_\beta(\mathbb R^G)[G]$ with $\beta\in D$ under witnesses for $\varphi$ as follows: Find a surjection $f:\mathbb R^G\rightarrow [L_\beta(\mathbb R^G)[G]]^{<\omega}$ in $M$ and map a real $x$ to the least level of the hierachy in which a witness to $\varphi(\vec p)$ (if there is one) exists where $f(x)=\vec p$. This function must be bounded so that there is a least $\gamma\in D$ so that $L_\gamma(\mathbb R^G)[G]$ contains witnesses for $\varphi$ with parameters from $L_\beta(\mathbb R^G)[G]$. This map $\beta\mapsto \gamma$ is definable in $M$ and the closure points of this map form a club with the desired properties.$\Box$
Now replacement (and even better, collection) is an easy consequence of the reflection principle above.
Choice in M: The axiom of choice in $M$ (in terms of existence of choice functions) follows by somewhat similar arguments:
First note that for any $\alpha<\omega_2$ there is a map $C_\alpha:\mathbb R^G\rightarrow\mathbb R^G$ in $M$ so that $C_\alpha(x)$ is (better: codes canonically a) $Add(\omega, \omega)$-generic over $L[G\upharpoonright\alpha, x]$ for any $x$. For any $x\in\mathbb R^G$ there is some $\alpha\leq\beta<\alpha+\omega_1$ so that the section of $G$ starting at $\beta$ with length $\omega$ is generic over $L[G\upharpoonright\alpha][x]$. Let $C_\alpha(x)$ be this section with $\beta$ as small as possible. Then $C_\alpha$ is definable over $(L_{\alpha+\omega_1}(\mathbb R^G)[G];\in, G)$ and hence is in $M$.
[Here the use of the predicate $G$ is crucial! No such function $C$ exists in $L_{\omega_2}(\mathbb R^G)$, so in particular the map $x\mapsto \{y\mid y$ is $Add(\omega, \omega)$-generic over $L[x]\}$ does not have a choice function there.]
Now let $f\in M$ be a function we want to find a choice function for. Since replacement holds in $M$ and all sets there are surjective images of $\mathbb R^G$ we may assume that $f:\mathbb R\rightarrow\mathcal P(\mathbb R)^M\setminus\{\emptyset\}$. Let $\alpha<\omega_2$ be large enough so that $f$ is definable in $M$ from paraters in $L[G\upharpoonright\alpha]$ (remeber that these parameters can be chosen to be ordinals, reals and initial segments of $G$ so such an $\alpha$ exists).
Proof: For notational reasons we assume $\alpha=0$, so that $L[G\upharpoonright\alpha] = L$. Work in $L[x]$. Note that $L[x]$ is either $L$ or a Cohen extension thereof. Also $g$ is generic over $L[x]$. Thus $G$ factors into $h\times H^\prime$ so that $L[x]=L[h]$ and $H^\prime$ is $Add(\omega, \omega_2)$-generic over $L[x]$ with $L[G]=L[x][H^\prime]$. Similarly, we can take an isomorphis $\mu:Add(\omega, \omega_2)\rightarrow Add(\omega, \omega)\times Add(\omega, \omega_2)$ so that $H^\prime$ factors again (via $\pi^{-1}$) into $g\times H$. In $L[x]$ we can find a nice name $\dot y$ so that $$1\Vdash^{L[x]}_{Add(\omega, \omega_2)} \dot y \in f(\check x)^{L_{\check\omega_2}(\mathbb R^{\dot G})[\dot G]}$$ Using the ccc, we can further find an automorphism $\pi$ of $Add(\omega, \omega_2)$ so that $\mu\circ\pi$ shifts $\dot y$ completely into the first factor $Add(\omega, \omega)$. With the same strategy as in the boundedness arguments, using that all parameters defining $f$ are in the ground model, we can see that in fact $$z=\widehat{\mu\circ\pi}(\dot y)^{g\times H^\prime}\in f(x)$$ But the evaluation of $\widehat{\mu\circ\pi}(\dot y)$ depends only on $g$ so that $z\in L[x][g]$ witnesses the claim to hold.
If $\alpha\neq 0$, replace $L$ by $L[G\upharpoonright\alpha]$ in the argument above, work from there and use that $L[G]$ is still a $Add(\omega,\omega_2)$-extension from there. $\Box$
It is now straight forward to define a choice function for $f$ in $M$: Just map a real $x$ to the $<_{L[x, C_\alpha(x)]}$-least element of $f(x)$ (where $<_{L[x, C_\alpha(X)]}$ denotes the canonical wellorder on the reals of $L[x, C_\alpha(x)]$).