Return to Answer

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M$ and for each good $G$, a surjection $i_G : M^P\to M[G]$. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$ with $p\in G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M[G]$. So for each good $G$, we will have a surjection $i_G : M^P\to M[G]$, interpreting the terms. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$ with $p\in G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M$ and for each good $G$, a surjection $i_G : M^P\to M[G]$. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M$ and for each good $G$, a surjection $i_G : M^P\to M[G]$. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$ with $p\in G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M$ and for each good $G$, a surjection $i_G : M^P\to M[G]$. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,a,\sigma)\in P\times M\times M^P : p\vDash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M$ and for each good $G$, a surjection $i_G : M^P\to M[G]$. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.