The notations $ M[X] $ and $ V[A] $ and intermediate models

Question

I am confused about Jech's notations $ M[X] $ and $ V[A] $.

---

Let us begin with exercise 13.34 (see [Jec02, p. 199]).

Let $ \mathbf{M} $ be a transitive model of $ \mathsf{ZF} $ containing all the ordinals and let $ X $ be a subset of $ \mathbf{M} $. Then there is a least model $ \mathbf{M}[X] $ of $ \mathsf{ZF} $ such that $ \mathbf{M} \subseteq \mathbf{M}[X] $ and $ X \in \mathbf{M}[X] $ and, if $ \mathbf{M} \models \mathsf{AC} $, then $ \mathbf{M}[X] \models \mathsf{AC} $.

One must realize that this is really a theorem schema as we are talking about proper classes: In fact, for each formula $ \phi(x) \equiv x \in \mathbf{M} $ we have to find another formula $ \psi(x, X) \equiv x \in \mathbf{M}[X] $ such that ...

Q1: Can someone give me a hint more helpful than Jech's one?

---

This leads to my next question. As far as I understand, forcing over $ V $ and the notation $ V[G] $ (where $ G \notin V $ is a generic filter for some forcing poset $ P \in V $) is just a sloppy notation. More precisely, one should always use a large enough finite fragment $ \mathsf{ZFC}^* $ and some c.t.m. $ M $ for $ \mathsf{ZFC}^* $ (i.e. a set model) as $ G \notin V $ is nonsense from a formalist's point of view.

Q2: So, how can I formalize Jech's results Lemma 15.40 up to Lemma 15.43 (see [Jec02, p. 247]) using the c.t.m. approach?

I am particularly puzzled as the analogue of exercise 13.34 for set models seems to fail.

---

[Jec02] Thomas Jech: "Set Theory: The Third Millennium Edition, revised and expanded". Springer, 2002

Answer 1

It is way too late to post an answer but let me take a crack at it anyways. So let $M$ be an inner model of $\text{ZF}$. We want to show that there exists a least inner model $M[X]$ of $\text{ZF}$, where $X\subseteq M$ and such that $M\subseteq M[X]$ and $X\in M[X]$.

We use relative constructibility over sets. For every $\alpha\in \text{ORD}$, define $L_0((V_{\alpha}\cap M) \cup \{X\})=(V_{\alpha}\cap M)\cup \{X\}$. At successor stages let $L_{\alpha+1}((V_{\alpha}\cap M) \cup \{X\})=Def_{\mathcal{P}}(L_{\alpha}((V_{\alpha}\cap M) \cup \{X\}))$ (definable power set). At limit stages $\gamma$, let $L_{\gamma}((V_{\alpha}\cap M) \cup \{X\})=\bigcup_{\alpha<\gamma}((V_{\alpha}\cap M) \cup \{X\})$. Then let $L((V_{\alpha}\cap M) \cup \{X\})=\bigcup_{\gamma\in\text{ORD}}L_{\gamma}((V_{\alpha}\cap M) \cup \{X\})$.

Finally define $M[X]=\bigcup_{\alpha\in\text{ORD}}L((V_{\alpha}\cap M) \cup \{X\})$. Doing this ensure that $M\subseteq M[X]$, because $M[X]$ contains every chunk of $M$, as these are contained in the $L((V_{\alpha}\cap M) \cup \{X\})$. Since also $\{X\}\subseteq M[X]$ then $X\in M[X]$. $M[X]$ satisfies $\text{ZF}$. If $M\models \text{AC}$, then wellorder $X$. Then for every $\alpha, L((V_{\alpha}\cap M) \cup \{X\})\models \text{AC}$ (which is not true in general). Feel free to add to this, I did it very quickly.