There is this lemma in Kanamori's book in the iterated ultrapowers section, which to me seems an important part of the theory, and I don't get part of the proof. So I decided to ask here.
Just to give a little bit of context: Here suppose we have an iteration of ultrapowers of some $M$ and some $M$-ultrafilter $U$, where $M$ is a transitive model of ZFC$^-$[ZFC minus the powerset axiom]. And $\tau$ is the length of the iteration, i.e. the first ordinal where we encounter ill-foundedness. And the $\kappa_\gamma$'s are the critical points of the respective embeddings.
Also for such $U$ and $n \lt \omega$, let:
$$U^n = \{X \in P([κ]^n) \cap M \mid \exists H \in U([H]^n \subseteq X)\} .
$$
Lemma. For any formula $\varphi(v_0,\dots,v_n)$ of $L_∈$, $x \in M$, and $\gamma_1 \lt \dots \lt \gamma_n \lt \alpha \in \tau$,
$$\langle M_\alpha, \in \rangle \models \varphi[i_{0\alpha}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n}] \text{
iff } \hspace{6cm}$$
$$ \hspace{4cm}\langle M, \in, U\rangle \models \{\{\xi_1,\dots,\xi_n\} ∈ [κ]^n\mid \varphi[x, \xi_1,\dots,\xi_n]\} \in U^n.$$
Proof. Proceed by induction on $n$; the case $n = 0$ is immediate. Generally,
$$\langle M_\alpha, \in \rangle \models \varphi[i_{0\alpha}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n}]$$
$$\text{ iff } \langle M_{\gamma_n+1}, \in \rangle \models \varphi[i_{0,\gamma_n+1}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n}]$$
$$\text{ iff } \langle M_{\gamma_n}, \in, U_{\gamma_n}\rangle \models \{\xi \lt \cup U_{\gamma_n} \mid \varphi[i_{0\gamma_n}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_{n−1}}, \xi ]\} \in U_{\gamma_n}
$$
$$\text{ iff }(*) \langle M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_{n−1}\} \in [κ]^{n−1} \mid \{\xi \lt \cup U \mid \varphi[x, \xi_1,\dots,\xi_{n−1}, \xi ]\} \in U\} \in U^{n−1}
$$
$$\text{ iff } \langle M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_n\} \in [κ]^n \mid \varphi[x, \xi_1,\dots,\xi_n]\} \in U^n.
$$
(Of course, $\cup U_{\gamma_n}$ is $\kappa_{\gamma_n}$ and $\cup U$ is $\kappa$.)
The part I don't understand is $(*)$. I assume he is using the induction hypothesis there but at that stage we are dealing with the satisfaction relation of a structure in the language $L_\in(\dot{A})$ and even the formula is using the constant. So we can't use the induction hypothesis. What is he doing there?
This is Lemma $19.9$ of Kanamori's "The Higher Infinite". $2$nd edition, page $253$.
Best Answer
This seems like one these situations where one has to strengthen the claim in order to get through the induction. It may be much too complicated what I am doing here, but as a wise man once said, if it works it ain't stupid. Let $\Sigma$ be the following set of $\{\in, \dot A\}$-formulas:
Essentially we allow $\dot A$ as long as we do not quantify over it.
I claim that the lemma holds true for all $\Sigma$-formulas.
Annoyingly, we have to backtrack quite a bit to do it. First let me show that $(M, \in, U)$ satisfies a form of replacement with respect to $\Sigma$-formulas, that is for any $\Sigma$-formula $\varphi$ and parameter $p\in M$, the function $F:\kappa\rightarrow \mathcal{P}(\kappa)$ given by $$F(\alpha)=\{\beta<\kappa\mid\varphi(\alpha,\beta, p)^M\}$$ is in $M$. We prove this by induction on the complexity of $\varphi$. The only nontrivial case arises when $$\varphi(x, y, z)= \{u\in\bigcup \dot A\mid \psi(u, x, y, z)\}\in\dot A$$ Let $h:\kappa\rightarrow\kappa\times\kappa$ be a bijection in $M$. By induction, the function $G:\kappa\rightarrow\mathcal{P}(\kappa)$ given by $$G(\delta)=\{\gamma<\kappa\mid\psi(\gamma, h(\delta)_0, h(\delta)_1, p)^M\}$$ is in $M$. By weak amenability, we have $$X=\{\delta<\kappa\mid G(\delta)\in U\}\in M$$ But now $$F(\alpha)=\{\beta<\kappa\mid h^{-1}(\alpha,\beta)\in X\}$$ and thus $F\in M$. It follows immediately (from weak amenability) that $M$ satisfies the corresponding form of separation with respect to $\Sigma$-formulas that is: For any $\Sigma$-formula $\varphi$ and parameter $p\in M$ we have $$\{\alpha<\kappa\mid\varphi(\alpha, p)\}^M\in M$$
We now prove Los's theorem for the $\Sigma$-formulas in our context. Again, almost everyhing is trivial or works as in the usual proof. Note that the $\exists$-case goes through as in that case $\dot A$ is not allowed to appear in the formula. For the new part, suppose $\varphi=\{x\in\bigcup\dot A\mid \psi(x, y)\}\in \dot A$. We look at when $$(M_1,\in, U_1)\models \{\beta< \kappa_1\mid\psi(\beta, [f])\}\in U_1$$ holds. Note that $\{\beta< \kappa_1\mid\psi(\beta, [f])\}^{M_1}$ is really a set in $M_1$ and furthermore if we define $g:\kappa\rightarrow M$ by $$g(\alpha)=\{\beta<\kappa\mid\psi(\beta, f(\alpha))\}^M$$ then $g\in M$ and $$[g]=\{\beta< \kappa_1\mid\psi(\beta, [f])\}^{M_1}$$ Thus by definition of $U_1$, $$(M_1,\in, U_1)\models [g]\in U_1\Leftrightarrow (M, \in, U)\models\{\alpha<\kappa\mid g(\alpha)\in U\}\in U$$ and thus $$(M_1, \in, U_1)\models\varphi([f])\Leftrightarrow (M,\in, U)\models\{\alpha<\kappa\mid\varphi(f(\alpha))\}\in U$$ which is what we had to show.
Finally, we can tackle the lemma in our strenghtened form. Let us go through it to see that now, everything works out fine. Again the case $n=0$ is immediate, as our Los theorem for $\Sigma$ implies that the embeddings $i_{\alpha, \beta}$ are elementerary w.r.t. $\Sigma$-formulas. In the inductive step from $n-1$ to $n$:
$$(M_\alpha, \in, U_\alpha) \models \varphi(i_{0\alpha}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n})$$
$$\text{ iff } (M_{\gamma_n+1}, \in, U_{\gamma_{n+1}})\models \varphi(i_{0,\gamma_n+1}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_n})$$
$$\text{ iff }(\ast)_0 (M_{\gamma_n}, \in, U_{\gamma_n}) \models \{\xi \lt \cup U_{\gamma_n} \mid \varphi(i_{0\gamma_n}(x), \kappa_{\gamma_1} ,\dots,\kappa_{\gamma_{n−1}}, \xi )\} \in U_{\gamma_n} $$ $$\text{ iff }(\ast)_1 (M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_{n−1}\} \in [κ]^{n−1} \mid \{\xi \lt \cup U \mid \varphi(x, \xi_1,\dots,\xi_{n−1}, \xi )\} \in U\} \in U^{n−1} $$ $$\text{ iff } (M, \in, U \rangle \models \{\{\xi_1,\dots,\xi_n\} \in [κ]^n \mid \varphi(x, \xi_1,\dots,\xi_n)\} \in U^n. $$
The step $(\ast)_1$ is now perfectly justified by our inductive hypothesis. In the step $(\ast)_0$, we used Los's theorem for the $\Sigma$-formulas. This finishes the proof.