Recall that given a finite language $\mathcal{L}$, we say that an $\mathcal{L}$-structure is computably saturated (or recursively saturated) if for any computable set $\Sigma(\bar{x},y)$ of $\mathcal{L}$-formulas in the variables $\bar{x}y$ and any $\bar{a} \in M^{\bar{x}}$, if $\Sigma(\bar{a},y)$ is finitely satisfiable in $M$, then it is satisfied in $M$. An easy inductive argument shows that every countable $\mathcal{L}$-structure has a countable computably saturated elementary extension. Another easy argument shows that any expansion of a computably saturated structure by finitely many constants is still computably saturated.
One important property of countable computably saturated structures is resplendence, which for our purposes can be defined like this: An $\mathcal{L}$-structure $M$ is resplendent if for any finite extensions $\mathcal{L}' \supseteq \mathcal{L}$ and any $\mathcal{L}'$-sentence $\varphi$ that is consistent with $\mathrm{Th}(M)$, there is an expansion $M'$ of $M$ that is a computably saturated model of $\mathrm{Th}(M)\cup\{\varphi\}$.
All countable computably saturated structures are resplendent. Moreover, the same is true after any expansion by any finite number of constants.
Forcing is typically defined in terms of well-founded models of $\mathsf{ZFC}$, but, as discussed in the answers to this question, forcing ultimately makes sense over arbitrary models of $\mathsf{ZFC}$: Given an model $M$ of $\mathsf{ZFC}$ and a forcing poset $\mathbb{P} \in M$, we can consider the language that contains $\in$, $\mathbb{P}$, and a unary predicate $G$. There is a single sentence $\chi(\mathbb{P},G)$ in this language that says that $\mathbb{P}$ is a forcing poset and $G$ is a generic filter on $\mathbb{P}$. As Emil Jeřábek points out in his answer to that question, $\mathsf{ZFC} \cup \{\chi(\mathbb{P},G)\}$ is a conservative extension of $\mathsf{ZFC}$. (The rest of the work of a forcing argument is showing that $(M,\mathbb{P},G)$ interprets an end extension of $M$ modeling $\mathsf{ZFC}$ in which $G$ is a set. We don't really need to worry about that for the sake of this question.)
We have, furthermore, that the theory $\mathrm{eldiag}(M) \cup \{\chi(\mathbb{P},G)\}$ is consistent. If $M$ is a countable computably saturated model of $\mathsf{ZFC}$, then, by resplendence, we have that for any forcing poset $\mathbb{P}\in M$, there is a $G \subseteq \mathbb{P}$ which is $M$-generic such that $(M,\mathbb{P},G)$ is computably saturated. (In particular, this means that the actual forcing extension $M[G]$ will be computably saturated as well.)
My question is about whether this always happens, 'usually' happens, or 'usually' doesn't happen for various choices of $G$.
Question 1: Let $M$ be a countable computably saturated model of $\mathsf{ZFC}$, and let $\mathbb{P} \in M$ be a forcing poset. If $G \subseteq \mathbb{P}$ is an $M$-generic filter, does it follow that $(M,\mathbb{P},G)$ is computably saturated?
I doubt that this does in fact always hold, but I don't know how to build a counterexample. What's less certain to me is whether a 'sufficiently generic' $M$-generic filter results in a computably saturated expansion.
To state this carefully, we need the following observation: Fix a countable computably saturated model $M$ of $\mathsf{ZFC}$ and a forcing poset $\mathbb{P} \in M$. Let $A$ be the set of all elements $\alpha$ of $\mathbb{P}^\omega$ such that for each $i<\omega$, $\alpha(i+1) \leq \alpha(i)$. $\mathbb{P}^\omega$ can easily be identified with Baire space, and $A$ is a $G_\delta$ subset of $\mathbb{P}^\omega$ and therefore itself a Polish space. It's easy to see that the set $$B = \{\alpha \in A : \alpha\text{ generates an }M\text{-generic filter}\}$$ is comeager in $A$. (This is essentially the Rasiowa–Sikorski lemma.) For any $\alpha \in A$, let $G_\alpha = \{p \in \mathbb{P} : p \geq \alpha(i)\text{ for some }i\}$. (This is what we mean by 'generating' a filter.)
Question 2: Is the set $$\{\alpha \in B : (M,\mathbb{P},G_\alpha)\text{ is computably saturated}\}$$ always comeager in $A$?
I would also be interested in answers involving a weaker set theory than $\mathsf{ZFC}$.
Best Answer
Lemma 1. $(M,\mathbb{P},G)$ is parametrically definable in $M[G]$.
Lemma 2. $M[G]$ is recursively saturated.
Lemma 3. Any structure that is parametrically definable in a computably saturated structure is also computably saturated.
Lemma 1 is due independently to Laver and Woodin, who proved that $M$ is parametrically definable in $M[G]$; see this MO post of Hamkins for more detail.
Lemma 2 was proved as part of the proof of Theorem 2.6 of this paper of mine. You can also find a proof of Lemma 2 in this blogpost of Kameryn Williams (see the third proposition). The same blogpost also includes a reference to another result of mine which shows that Lemma 2 can fail if $\mathbb{P}$ is a proper class notion of forcing in $M$.
Lemma 3 follows from the definitions involved.
Finally, let me point out that Lemma 2 is true for all models $M$ of ZF, but I do not know the status of Lemma 1 for a model of ZF in which AC fails.