Consider the following result (which is Lemma 2.8 in Mitchell and Steel's paper on Fine Structure and Iteration Trees):


**Lemma 2.8** Let $\pi \colon \mathcal{H} \to \mathcal{M}$ be generalized $r \Sigma\_{k}$
 elementary, where $\mathcal M$ is a ppm (not of type III) and $1
 \leq k < \omega$. Suppose that $\rho\_{k}^{\mathcal{M}} \subseteq
 \mathcal{H}$ and $\pi \restriction \rho\_{k}^{\mathcal{M}} =
 \operatorname{id}$. Suppose also that $\pi(r)$ is the $k$th standard parameter of
 $(\mathcal{M}, \pi(q))$ and that $\pi(r)$ is $k$-solid and
 $k$-universal over $(\mathcal{M}, \pi(q))$. Then


1. $\rho\_{k}^{\mathcal{H}} = \rho\_{k}^{\mathcal{M}}$,
2. $r$ is the $k$th standard parameter of $(\mathcal{H},q)$ and
3. $r$ is $k$-universal over $(\mathcal{H}, q)$.


The proofs of items $1.$ and $2.$ are included in this paper and in
both cases it seems that the $k$-solidity of $\pi(r)$ over
$(\mathcal{M}, \pi(q))$ isn't actually needed. Hence I decided to
prove item $3.$ to see how $k$-solidity comes into play. However, if
my argument is correct, it doesn't rely on $k$-solidity either.


Here is my proof of item $3.$:


**Proof** *(of $3.$).* Let $A \in \mathcal{H}$ be such that $A \subseteq
 \rho\_{k}^{\mathcal{H}}$. Then $\pi(A) \cap \rho\_{k}^{\mathcal{M}}
 \in \mathcal M$. By the $k$-universality of $\pi(r)$ over
 $(\mathcal{M}, \pi(q))$ there is hence some generalized Skolem term
 $\tau \in S\_{\kappa}$ and some $\vec{\alpha} \in ^{< \omega}
 \rho\_{k}^{\mathcal{M}}$ s.t.
 $$
 \pi(A) \cap \rho\_{k}^{\mathcal{M}} =
 \tau^{\mathcal{M}}[\vec{\alpha}, \pi(r), \pi(q)] \cap \rho\_{k}^{\mathcal{M}}.
 $$
 Let $B := \tau^{\mathcal{H}}[\vec{\alpha},r,q] \cap \rho\_{k}^{\mathcal{H}}$. Combining the fact
 that $\pi$ is generalized $r \Sigma\_{k}$-elementary, $\rho\_{k}^{\mathcal{H}}=
 \rho\_{k}^{\mathcal{M}} \subseteq \mathcal{H}$ and $\pi \restriction
 \rho\_{k}^{\mathcal M} = \operatorname{id}$ we have that
 \begin{align\*}
 \mathcal{H} \models A \cap \rho\_{k}^{\mathcal{H}} = B &\iff \mathcal{H} \models A \cap \rho\_{k}^{\mathcal{H}} = \tau^{\mathcal
 H}[\vec{\alpha},
 r,q] \cap
 \rho\_{k}^{\mathcal{H}}
 \\
 &\iff
 \mathcal{M}
 \models
 \pi(A) \cap
 \rho\_{k}^{\mathcal{M}}
 =
 \tau^{\mathcal{M}}[\vec{\alpha},\pi(r),\pi(q)]
 \cap \rho\_{k}^{\mathcal{M}}.
 \end{align\*}
 Since the last line is true, it follows that
 $A \cap \rho\_{k}^{\mathcal{H}}
 =\tau^{\mathcal{H}}[\vec{\alpha},r,q] \cap \rho\_{k}^{\mathcal{H}}$. Thus $r$ is indeed
 $k$-universal over $(\mathcal{H}, q)$. *Q.E.D.*


**Question**: Did I miss something and this result actually relies on the $k$-solidity of $\pi(r)$ over $(\mathcal{M},\pi(q))$ or can this assumption be dropped?


If $k$-solidity is needed, I'd like to understand where exactly in the proof it is used and ideally I'd like to see an example in which Lemma 2.8 fails without $k$-solidity.




---


PS: I am aware that this question isn't exactly 'ongoing research' and I strongly considered posting it over at MSE. However, since the group of people able to answer this question is more likely to be encountered here and since a [somewhat similar question](https://mathoverflow.net/questions/123577/a-question-about-mitchell-steel-fine-structure-and-iteration-trees) has been asked and well-received here, I decided to go with mathoverflow.



Mitchell, Steel. FSIT. Lemma 2.8: Is $k$-solidity actually needed?
In my question I already verified that (assuming 1. and 2.) item 3. is provable without assuming that $\pi(r)$ is $k$-solid over $(\mathcal{M},q)$. To see that we can actually drop $k$-solidity in this lemma, it hence suffices to see that 1. and 2. also don't require that $k$-solidity of $\pi(r)$.


If $\rho\_{k}^{\mathcal{M}} = \operatorname{Ord}^{\mathcal{M}}$, then $\pi = \operatorname{id}$
 and the lemma trivially holds. Thus assume that
 $\rho\_{k}^{\mathcal{M}} < \operatorname{Ord}^{\mathcal{M}}$.


1. Let $\alpha \leq \rho\_{k}^{\mathcal M}$. Since
$\pi \restriction \rho\_{\kappa}^{\mathcal{M}} = \operatorname{id}$
and since $\pi$ is generalized $r \Sigma\_{k}$-elementary, we have - up
to a slight abuse of notation -
\begin{align\*}
 \operatorname{Th}\_{k}^{\mathcal{H}}(\alpha \cup \{ s \})
 &= \{(\phi, \vec{a}, s) \mid \vec{a} \in ^{< \omega}{\alpha}
 \wedge \mathcal{H} \models \phi[\vec{a}, s] \} \\
 &= \{(\phi, \vec{a}, s) \mid \vec{a} \in ^{< \omega}{\alpha}
 \wedge \mathcal{M} \models \phi[\vec{a}, \pi(s)] \}
\end{align\*}
In particular, for any $\phi \in r \Sigma\_{k}$ and any $\vec{a} \in ^{<
 \omega}{\alpha}$, we have
$$
 (\phi, \vec{a}, s) \in
 \operatorname{Th}\_{k}^{\mathcal{H}}(\alpha \cup \{s \}) \iff
 (\phi, \vec{a}, \pi(s)) \in
 \operatorname{Th}\_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}).
$$
By enlarging $\alpha$, if necessary, we may assume that $\alpha$
is primitive recursively closed and hence uniformly code
\begin{align\*}
 \{(\phi, \vec{a}) \mid (\phi, \vec{a}, s) \in
 \operatorname{Th}\_{k}^{\mathcal{H}}(\alpha \cup \{ s \}) \} \\
 = \{(\phi, \vec{a}) \mid (\phi, \vec{a}, \pi(s)) \in
 \operatorname{Th}\_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}) \}
\end{align\*}
as a subset $A \subseteq \alpha$. Since
$\alpha < \rho\_{k}^{\mathcal{M}}$, we have
$\operatorname{Th}\_{k}^{\mathcal{M}}(\alpha \cup \{ \pi(s) \}) \in
\mathcal{M}$ and hence $A \in \mathcal{M}$. By the strong
acceptability of $\mathcal{M}$ - observing that
$\rho\_{k}^{\mathcal{M}}$ is an $\mathcal{M}$-cardinal - this
yields
$$
 A \in \mathcal{J}\_{\rho\_{k}^{\mathcal{M}}}^{\mathcal M} = \left(
 H\_{\rho\_{k}^{\mathcal{M}}} \right)^{\mathcal{M}} \overset{\pi
 \restriction \rho\_{k}^{\mathcal{M}} = \operatorname{id}}{=} \left(
 H\_{\rho\_{k}^{\mathcal{M}}}\right)^{\mathcal{H}} \subseteq \mathcal{H}.
$$
Therefore
$$
 \operatorname{Th}\_{k}^{\mathcal{H}}(\alpha \cup \{ s \}) = \{
 (\phi, \vec{a}, s) \mid \langle \phi, \vec{a} \rangle \in A \}
 \in \mathcal{H}
$$
and $\rho\_{k}^{\mathcal{M}} \leq \rho\_{k}^{\mathcal{H}}$.


On the other hand, suppose that
$\rho\_{k}^{\mathcal{M}} < \rho\_{k}^{\mathcal{H}}$. Then
$\operatorname{Th}\_{k}^{\mathcal{H}}(\rho\_{k}^{\mathcal{M}} \cup
\{(r,q)\}) \in \mathcal{H}$. Let
$A \subseteq \rho\_{k}^{\mathcal{M}}$, $A \in \mathcal{H}$ be a
uniform code for
$$
 \{ (\phi, \vec{a}) \mid (\phi, \vec{a}, (r,q)) \in
 \operatorname{Th}\_{k}^{\mathcal{H}}(\rho\_{k}^{\mathcal{M}} \cup
 \{(r,q)\})\}.
$$
Then $A = \pi(A) \cap \rho\_{k}^{\mathcal{M}} \in \mathcal{M}$
witnesses (as above) that
$\operatorname{Th}\_{k}^{\mathcal{M}}(\rho\_{k}^{\mathcal{M}} \cup
\{ \pi(r), \pi(q)\}) \in \mathcal{M}$. This contradicts the fact
that $\pi(r)$ is the $k$th standard parameter of
$(\mathcal{M},\pi(q))$!
2. The proof above also shows that
$\operatorname{Th}\_{k}^{\mathcal{H}}(\rho\_{k}^{\mathcal{H}} \cup
\{ (r,q)\}) \not \in \mathcal{H}$. Hence it suffices to show that
for all $s <\_{\operatorname{lex}} r$
$$
 \operatorname{Th}\_{k}^{\mathcal{H}}(\rho\_{k}^{\mathcal{H}} \cup
 \{ (s,q)\}) \in \mathcal{H}.
$$
So, fix $s <\_{\operatorname{lex}} r$. Then
$\pi(s)<\_{\operatorname{lex}} \pi(r)$ and hence
$$
 \operatorname{Th}\_{k}^{\mathcal{M}}(\rho\_{k}^{\mathcal{H}} \cup
 \{ (\pi(s),\pi(q))\}) \in \mathcal{M}.
$$
Let $A \subseteq \rho\_{k}^{\mathcal{M}}$, $A \in \mathcal{M}$ be
the code of this fact as above. Since $\pi(r)$ is $k$-universal
over $(M, \pi(q))$ there is some $\tau \in \operatorname{Sk}\_{k}$
and $\vec{a} \in ^{< \omega}{\rho\_{k}^{\mathcal{M}}}$ such that
$A = \tau^{\mathcal{M}}[\vec{a}, \pi(r), \pi(q)] \cap
\rho\_{k}^{\mathcal{M}}$. Let
$$
 B = \tau^{\mathcal{H}}[\vec{a}, \pi(r), \pi(q)] \cap
 \rho\_{k}^{\mathcal{M}}.
$$
Since $\pi$ is *generalized* $r \Sigma\_{k}$-elementary we have,
for all $\xi < \rho\_{k}^{\mathcal{M}} = \rho\_{k}^{\mathcal{H}}$
$$
 \mathcal{M} \models \xi \in
 \tau^{\mathcal{M}}[\vec{a},\pi(r),\pi(q)] \iff \mathcal{H}
 \models \xi \in \tau^{\mathcal{H}}[\vec{a},r,q].
$$
Thus $B = A \in \mathcal{H}$ witnesses that
$\operatorname{Th}\_{k}^{\mathcal{H}}(\rho\_{k}^{\mathcal{H}} \cup
\{(s,q)\}) \in \mathcal{H}$ and hence the
$<\_{\operatorname{lex}}$-minimality of $r$.


