Namba forcing and semiproperness

Semiproperness of Namba forcing is indeed equivalent to SCC. Here by SCC I mean the version which appears in Chapter XII, Theorem 2.5 part (2) of Shelah's book: for all large $\theta$ and all wellorders $w$ on $H_\theta$ and all countable $N \prec (H_\theta,\in,w)$ and all $\alpha < \omega_2$, there is an $N' \sqsupset N$ such that $N' \prec (H_\theta,\in,w)$ and $\alpha \le \text{sup}(N' \cap \omega_2)$.

The forward direction is in Shelah's book, and the backward direction appears in Section 3 of Doebler's "Rado's Conjecture implies that all stationary set preserving forcings are semiproper", and is attributed to "folklore". Since the Doebler article doesn't appear on arxiv, and since the version of SCC he uses is slightly different from above, I sketch his short proof here. Assume SCC as in the first paragraph. We show that II has a (very easy) winning strategy in the game that Goldstern described in the comment above. As the game progresses, Player II will construct a $\subset$-increasing sequence $X_n$ of countable elementary submodels of $(H_\theta,\in,w)$, and at the $n$-th move player II simply plays the ordinal $X_n \cap \omega_1$. The model $X_{n+1}$ is chosen so that $F_{n+1} \in X_{n+1}$ and $X_n \subset X_{n+1}$. Let $X_\omega$ be the union of the $X_n$'s and $\delta_\omega = X_\omega \cap \omega_1$. Suppose for a contradiction that II loses the game; then there is some $\alpha_0 < \omega_2$ such that for all $\beta \in [\alpha_0, \omega_2)$ there is an $n_\beta \in \omega$ such that $F_{n_\beta}(\beta) \ge \delta_\omega$. By SCC there is a $Y \sqsupset X_\omega$ with $\alpha_0 \le \text{sup}(Y \cap \omega_2)$ and $Y \prec (H_\theta,\in,w)$. Pick any $\beta \in Y \cap [\alpha_0, \omega_2)$. Since $F_{n_\beta} \in X_{n_\beta} \subset Y$ then $F_{n_\beta}(\beta) \in Y \cap \omega_1 = \delta_\omega$. Contradiction.

Regarding the large cardinal strength: The Sharpe-Welch paper mentions an unpublished proof of Magidor that semiproperness of Namba forcing is equiconsistent with a measurable cardinal. However I don't know the proof, and haven't seen it.

Here is a direct construction of semigeneric conditions for Namba forcing (actually for Namba$^{\prime}$ for convenience) using $SCC$, without using games.

Let $\theta$ be large enough and regular, $X\prec H_\theta$ countable and $p\in X\cap Nm^\prime$. We construct a descending sequence $\langle p_n\mid n<\omega\rangle$ of condtions and make sure that the $n$th level remains constant after $n$ steps, so that we get a fusion $p_\omega$ in the end. Let $\langle \dot \xi_n\mid n<\omega\rangle $ be an enumeration of all names for countable ordinals in $X$. Put $p_0=p$ and assume $p_n$ is constructed. Let $\eta$ be on the $n$th level of $p_n$. Find $r_\eta\leq p_n\upharpoonright \eta$ that has stem $\eta$ and decides as many of the $\dot\xi_0,\dots, \dot\xi_n$ as possible and let $\zeta_\eta$ be the supremum of the relevant decisions. We get $p_{n+1}$ by replacing all such subtrees $p_n\upharpoonright \eta$ by the corresponding $r_\eta$.

By making sure that all our choices are minimal with respect to some wellorder in $X$, we can make sure that all $p_n$ are in $X$ (even though $p_\omega$ is not). Even more, whenever $X\subseteq Y\prec H_\theta$ and $\eta\in p_\omega\cap Y$ then $\zeta_\eta\in Y$.

Now we will thin out $p_\omega$ (we need $SCC$ to make sure that we do not cut off too many branches). Let $$q=\{\eta\in p_\omega\mid \exists Y\text{ countable with } X\sqsubseteq Y\prec H_\theta\wedge \eta\in Y\}$$ I claim that $q$ is semigeneric for $X$. First we have to see that $q$ is a condition. Suppose that $\eta\in q$ and that $Y$ witnesses this. Let $n=lh(\eta)$. Note that the direct successors of $\eta$ in $p_\omega$ are the same as the ones in $p_{n+1}\in Y$, so that we can find an enumeration $(\mu_\alpha)_{\alpha<\omega_2}\in Y$ of them. By $SSC$, there are unboundedly many $\beta<\omega_2$ for which there are countable $Y\sqsubseteq Z\prec H_\theta$ with $\beta\in Z$ an thus $\mu_\beta\in Z$. Hence every point in $q$ has $\omega_2$-many successors.

Finally suppose that $r\leq q$ decides $\dot \xi_n$ as $\xi$. Let $\eta$ be the stem of $r$, we may assume that $lh(\eta)\geq n$. By the construction of $p_{lh(\eta)+1}$, $\xi\leq\zeta_\eta$. Now let $Y$ witness that $\eta\in q$. We thus have $\xi\leq\zeta_\eta\in Y\cap\omega_1=X\cap\omega_1$ so that $\xi\in X$, as desired.