Consistency strength of lifting through a lot of collapsing

What is the consistency strength of the following situation?

1. $$j : V \to M$$ is an elementary embedding definable from parameters in $$V$$, with critical point $$\kappa$$.
2. $$\mathbb P$$ is a forcing that collapses all ordinals between $$\kappa$$ and $$j(\kappa)$$.
3. $$j$$ can be lifted through $$\mathbb P$$.

One can deduce that $$j(\kappa)$$ is regular in $$V$$. The only examples I know of such liftings involve almost-huge cardinals.

• If the answer is not known, you can define a new notion "pretty huge", and argue that since almost huge is pretty huge, is it always the case that a pretty huge cardinal is almost huge? Aug 6, 2020 at 8:29
• You can deduce stronger hypotheses. Let $G$ be $\mathbb P$-generic. Then $\kappa$ is regular in $V[G]$ since it is the critical point of an elementary embedding of $V[G]$ in some outer model. Similarly, $j(\kappa) = (\kappa^+)^{V[G]}$. By assumption, $j(\kappa)\leq (\kappa^+)^{V[G]}$. For the other direction, $j(\kappa)\geq (\kappa^+)^{V[G]}$ since $j(\kappa)$ is the target of the critical point of an elementary embedding of $V[G]$ in some outer model. (The target model $Q$ of this embedding must contain $P^{V[G]}(\kappa)$ and therefore $j(\kappa)\geq\kappa^{+Q}\geq \kappa^{+V[G]}$.) Aug 6, 2020 at 22:22

$$\text{AD}^{L(\mathbb R)}$$ suffices. The situation actually holds in the model $$H = \text{HOD}^{L(\mathbb R)}$$. We will have $$\kappa = \omega_1$$ and $$j : H\to \text{Ult}(H,U)$$ equal to the ultrapower of $$H$$ by the club measure $$U$$ over $$\omega_1$$ as computed in $$L(\mathbb R)$$ (using all functions in $$L(\mathbb R)$$).

For any number $$n$$, the $$\Sigma_n$$-satisfaction predicate of $$L(\mathbb R)$$ with ordinal parameters is definable over $$H$$ from its restriction to ordinals less than $$\Theta$$, so any subclass of $$H$$ that is ordinal definable over $$L(\mathbb R)$$ is definable from parameters over $$H$$. In particular, $$j$$ is definable from parameters over $$H$$.

Let $$N$$ be a $$\mathbb P_\text{max}$$-extension of $$L(\mathbb R)$$. Note that $$H = \text{HOD}^N$$ by the homogeneity and definability of $$\mathbb P_\text{max}$$. Let $$\mathbb P\in H$$ be the Vopenka algebra of $$N$$ for adding a subset of $$\omega_2$$ to $$H$$. There is a set $$A\subseteq \omega_2$$ such that $$N= L[A]$$, and so $$N = H[G_A]$$ where $$G_A\subseteq \mathbb P$$ is the $$H$$-generic ultrafilter associated to $$A$$.

In $$N$$, $$\text{NS}_{\omega_1}$$ is saturated. Let $$G\subseteq P(\omega_1)\setminus\text{NS}_{\omega_1}$$ be $$N$$-generic, and in $$N[G]$$ let $$i : N\to \text{Ult}(N,G)$$ be the generic ultrapower embedding associated to $$G$$ (using functions in $$N$$).

Now as usual, we cite a theorem due to Woodin: $$j = i\restriction H$$. This follows from Theorem 4.53 in The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal.

Now in $$H$$, we have the situation you were looking for with $$\kappa = \omega_1.$$ Note that $$i(\omega_1) = (\omega_2)^N$$ by saturation, which means that all $$H$$-cardinals between $$\kappa$$ and $$j(\kappa)$$ are collapsed to $$\kappa$$ in $$N$$. Moreover $$j$$ lifts through the forcing $$\mathbb P$$ (to $$i$$) by construction.

• What happens if you require a "super" kind of modification, namely that $j(\kappa)$ can be unbounded when ranging over possible $j$s, how far does this blow up the consistency strength? Aug 7, 2020 at 6:48
• Very interesting. How does the extender in $H$ corresponding to $j$ relate to standard large cardinal notions? I wonder how it interacts with other forcings. Aug 7, 2020 at 8:19
• The model $H$ can be presented as a fine structure model. It's an open question whether $j$ is the branch extender of an iteration tree by the sequence of this model. The short part of $j$ is just the $\omega_2$-length linear iteration of the unique normal ultrafilter over $\omega_1$ in $H$. Aug 7, 2020 at 15:18
• @AsafKaragila I have no idea, I don't see how to get something like that from AD. Aug 7, 2020 at 15:48
• Oh, I thought it was obvious you can't. But maybe it's not that obvious... Aug 7, 2020 at 15:52