Forcing is typically done over well-founded models. There are lots of good reasons for this, but it can feel confining at times. Fortunately, we can equally well force over non-well-founded models! It takes a bit more work to show that everything remains nice, but basically the internal Boolean-valued model can be constructed in the usual way. See ??? for details.
Forcing over illfounded models has a number of serious applications, so let’s ignore those and do something silly instead. One thing we can do is make a “freshman’s dream” about forcing actually correct:
Freshman’s dream. If $\mathbb{P}$ is a homogeneous notion of forcing, then any two extensions by $\mathbb{P}$ are isomorphic.
This is of course false - indeed, any nontrivial forcing yields many pairwise nonisomorphic extensions, as long as our base model is well-founded and hence rigid (assuming enough generics exist in the first place, of course). However, in the context of nonstandard models, we can make the dream come true!
Of course, this takes a bit of work to make precise. Here’s what I mean:
Definition. (Within a ground model $V$.) A model $M$ of $ZFC$ has unique forcing extensions (UFE) if for all $\mathbb{P}\in M$, if $M\models$ "$\mathbb{P}$ is homogeneous" then $$V\models \mbox{ "$\Vdash_{\mathbb{P}^2}M[G_0]\cong M[G_1]$"},$$ where we conflate $\mathbb{P}$ (the element of $M$) with the $V$-partial order $(\{x: x\in M, M\models x\in\mathbb{P}\}, \{(x, y): M\models x\le_\mathbb{P} y\})$ to make sense of forcing over $V$ with $\mathbb{P}^2$.
We could of course replace “homogeneous” with, say, “almost homogeneous” here — I’m just using the stronger notion for simplicity.
It is easy (via a back-and-forth argument) to see that if $M$ is saturated, then $M$ has UFE (this also leads to a fun proof that “a homogeneous forcing extension of a saturated model of $ZFC$ is saturated” - where we force over $V$, and compute saturation of $M[G]$ in $V[G]$). Moreover, it is easy to see that saturation is strictly stronger than UFE: we can kill saturation by forcing in $V$, but we can’t kill UFE this way.
My question is whether this notion has been studied before. In particular, there are a few things about it which look particularly interesting:
Question 1. Do homogeneous forcings preserve UFE? Specifically, suppose $M$ has UFE, $\mathbb{P}\in M$ is a forcing which $M$ knows is homogeneous, and $G$ is $\mathbb{P}$-generic over $V$ (not just $M$!). Does $V[G]$ think that $M[G]$ has UFE? The obvious iteration doesn’t seem to necessarily be homogeneous, so I don’t know how to proceed here.
Question 2. My main motivation — there is a kind of Keisler-order-iness going on here, although I’m not sure how solid this vague connection really is: For $K$ a definable class of forcings, we can define $K$-UFE as above but restricting attention to forcings which $M$ think lie in $K$. Then we can ask how these notions compare for various $K$s. For example, if $M$ has $\{$c.c.c.$\}$-UFE, does $M$ have $\{$countably closed$\}$-UFE? I suspect that for the most part, questions like this reduce to just comparing the classes involved — e.g. since there are countably closed, non-c.c.c. forcings, the answer to the previous specific question should be “no” — but I don’t see how to prove this yet.
Question 3. How much weaker is UFE than full saturation, really? For example: suppose $\kappa$ is a cardinal such that no saturated models of ZFC exist with cardinality $\kappa$. Can there be a model of cardinality $\kappa$ which does have UFE? And relatedly, the observation that UFE is preserved by forcing shows that really, UFE is a version of “every constructible type over a small parameter set is realized” (where an $M$-type $p$ over a set $A\subset M$ is constructible if $V$ satisfies “whenever $N$ is a copy of $M$ with ordinal domain, there is a $q$ in $L[N]$ which pulls back to $p$”). Is UFE strictly weaker than “constructible saturation?” If so, there should be a good explicit-ish counterexample . . .