Question: Under large cardinal axioms, what is the intersection of all inner models $M$ of ZFC such that every set in $V$ is set-generic over $M$?
Every set belongs to a generic extension of HOD, and we hope that HOD is canonical in the true $V$, but ordinary large cardinal axioms do not imply that HOD is a canonical well-behaved model. Every countable model $M$ of ZFC is HOD of some model of ZFC (obtained using class forcing over $M$).
However, let $M_∞$ (or $M_\text{Ord}$) be the minimal iterable inner model with a proper class of Woodin cardinals. There is an ordinal definable iterate $M'_∞$ of $M_∞$ such that every set in $V$ is set-generic over $M'_∞$. Specifically, pick an OD set of ordinals $X_0$; iterate the first Woodin cardinal of $M_∞$ to make $X_0$ generic; then pick $X_1$ and iterate the second Woodin cardinal to make $X_1$ generic, and so on. Also, using genericity over local HODs, we can choose $M'_∞$ such that $M'_∞∩H(λ)$ is definable in $H(λ)$ (for $λ>c$) and with every $X⊂λ$ being $M'_∞$-generic for a poset in $M'_∞∩H((2^λ)^+)$ (as usual, $H(λ)=\{x:|\mathrm{tc}(x)|<λ\}$).
But is this bound optimal? For every $M$ in the question and a set of ordinals $s∈M$, is $M_∞(s)$ elementarily embeddable into an $M$-definable submodel of $M$? Does the intersection of all such $M$ equal $M_∞$ with the least measurable cardinal iterated away? And what kind of large cardinals must such $M$ have?
Using $ω$ steps of core model induction, every $M$ as in the question satisfies projective determinacy (PD) in all generic extensions of $M$ (assuming PD in all generic extensions of $V$), but I do not know how far further core model induction can go here.
Note that every set $S$ is generic over some (dependent on $S$) iterate of $M_1$ (the minimal iterable inner model with a Woodin cardinal). Thus, for example, if there is a superstrong cardinal (and every set has a sharp), then there is a generic extension of $M_1$ with a superstrong cardinal. This is analogous to existence of complicated transitive models in $L$; and more Woodin cardinals give genericity over models with more closure.
Formalization note: The answer is presumably the same regardless of whether $M$ is $Σ_2$ definable using parameters in $V$, or we use NBG (plus large cardinal axioms) and treat $M$ as a class. Also, allowing choice to fail in $M$ likely does not change the answer. A likely sufficient large cardinal assumption is that $M_∞$ (above) exists and is fully iterable.
Local versions: A variation is to consider inner models $M$ with (for a specific $λ$) every element of $H(λ)$ generic over $M$ using a forcing in $H(λ)$. Examples include:
- for countable cofinality strong limit $λ$, some iterates of $M_ω$
- for singular strong limit $λ$ of uncountable cofinality, some iterates of the minimal iterable inner model with a measurable number of Woodin cardinals (i.e. $κ$ Woodin cardinals with $κ$ measurable in the model)
- for inaccessible $λ$, some iterates of $M_∞$.
Class forcing:
While some class forcing is set-like, in general class forcing lacks the same kind of closure. For example, even preserving ZFC, we can code the universe into a real even if every set has a sharp. The lack of closure makes it easier to make $V$ generic, and if I understand correctly, it suffices to use an appropriate iterate of the minimal inner model satisfying "Ord is Woodin" (not sure if we need its sharp, or if there are definability isssues), with the class forcing satisfying Ord chain condition (and thus well-behaved). An analogous relation should also hold for a number of extensions to the language of set theory, with both "Ord is Woodin" (and the inner model) and closure properties of classes (and class forcing, or Ord-cc class forcing) strengthened in the same way.
While many iterates should work, a particularly elegant choice and encoding of an iterate is (conjecturally) the 'stability' predicate $S=\{n,α,β: n<ω ∧ H(α) ≺_{Σ_n} H(β)\}$. $(L[S],∈,S)$ is called the stable core (see The Stable Core and Structural Properties of the Stable Core). Caveat (conjectural): The iterate encoded by $S$ (there are different encodings, but if it works, among iterates in which $S$ is definable, the unique iterate that is definable from every iterate in which $S$ is definable) is outside of $(L[S],∈,S)$, though a further iterate is $\text{HOD}^{L[S]}=K^{L[S]}$. Without large cardinal assumptions, the theory of the stable core is not canonical, but we still get the genericity. While the specific choice of $S$ is somewhat arbitrary, I think the use of the cumulative hierarchy is important for the genericity, and presumably a different definition would simply lead to a different iterate that works, or be insufficient or suboptimal.