How to more rigorously formalise “value of (Weaver's) P-name” in set theory forcing (recursion)?

Question

Background

I have been reading some introductory material on forcing, specifically Nik Weaver's Forcing for mathematicians. What Weaver calls a “$P$-name”, I will call “Weaver's $P$-name” because it differs slightly from other definitions in the literature.

Definition. (Weaver's $P$-name) Fix a countable transitive $\in$-model $M$ of ZFC (in an appropriate sense), and $\varnothing \neq P \in M$. Build a hierarchy $(V_\alpha^P)$ as follows:

1. $V_0^P = \varnothing$;
2. $V_{\alpha^+}^P = \mathcal{P}(V_{\alpha}^P \times P)$;
3. $V_{\alpha}^P = \bigcup\limits_{\beta < \alpha}{V_{\beta}^P}$ if $\alpha$ is a limit ordinal.

Call the elements of the class $V^P = \bigcup \limits_{\alpha \in \mathrm{Ord}}{V_{\beta}^P}$ the $P$-names, and the hierarchy $(V_\alpha^P)$ is the hierarchy of $P$-names. From this we separate out the “upward $\subseteq$-closed P-names” in another hierarchy $(\bar{V_{\alpha}^P})$: $$\tau \in \bar{V_{\alpha}^P} \Longleftrightarrow \tau \in V_{\alpha}^P \wedge (\forall\sigma\in \operatorname{dom} \tau)\, (\forall p, q \in P) \left( (\sigma, p) \in \tau \wedge p\subseteq q \Rightarrow (\sigma, q) \in \tau \right).$$ Finally, define $N_{\alpha}^P = \bar{V_{\alpha}^P} \cap M$, and call this the “hierarchy of Weaver P-names”. The smallest ordinal $\alpha_0$ such that $\tau \in N_{\alpha_0}^P$ (if it exists) is called the (Weaver's) name rank of $\tau$.

The definition of these hierarchies uses theorems of transfinite recursion. The general kind where we get an $\mathrm{Ord}$-sequence (in the class sense). More specifically, the type where successor and limit ordinals are treated separately. Even more precicely, the parametric version of that recursive definition theorem; the set $P$ takes the place of the parameter in this case (and possibly $M$, depending on some choices).

Question

So that is the $P$-names out of the way. Next we take a set $G \subseteq P$, and define “$G$-values of Weaver's P-names” as follows. ($G$ is intended to be a generic ideal of $P$ but that is not relevant in this discussion).

Definition. ($G$-value of Weaver's $P$-name) The value $\tau^G$ of a (Weaver) $P$-name $\tau$ is defined recursively on name rank by $$\tau^G = \{ \sigma^G \mid \sigma \in \tau^{-1} (G)\}.$$ Here $\tau^{-1} (G)$ is the relational inverse of $\tau$ of the set $G$.

• What kind of recursion is this exactly?

It does not seem to be the general recursion over $\mathrm{Ord}$ with parameters discussed above. Instead, it goes somehow like this:

i) define $\varnothing^G = \varnothing$;

ii) define $G$-values $\sigma^G$ for all elements $\sigma$ of $\operatorname{name rank}(\sigma) < \alpha \in \mathrm{Ord}$;

iii) for elements $\tau$ with $\operatorname{name rank}(\tau) = \alpha$ define $\tau^G = \{\sigma^G \mid \sigma \in \tau^{-1} (G)\}$.

This definition makes sense because $\sigma \in \tau^{-1}(G) \Leftrightarrow \exists g \in G\, ((\sigma, p) \in \tau) \Rightarrow \operatorname{name rank}(\sigma) < \operatorname{name rank}(\tau)$. The required definitions of $\sigma^G$ will thus be done by the time $\tau^G$ is to be defined.

• How is this formalised more rigorously?

The more rigorous formalisation is where I ask for help. The difficulty for me is that the definition of value is more of an “individual definition” (for a specific Weaver $P$-name $\tau$, define its value $\tau^G$) instead of a “collective definition” (take all Weaver $P$-names from below, $V_\alpha^P$, and as a whole define all Weaver $P$-names in $V_{\alpha^+}^P$). Is it an $\in$-recursion of some sort? Do we do some sort of collective definition first, in the background, and only then identify $\tau \leftrightarrow \tau^G$ in a separate step?

Answer 1

Given the set $G\subseteq P$ (usually the generic filter, but as you say that does not really matter), we can define the relation ${\in_G}\subseteq V^P\times V^P$ as follows:

$$\sigma\in_G\tau\quad\Leftrightarrow\quad\sigma\in\tau^{-1}(G)\quad\ \Leftrightarrow\quad \exists p\in G(\langle\sigma,p\rangle\in \tau)$$

Note that this is a well-founded relation, since $\sigma\in_G\tau$ implies that $\mathrm{rank}(\sigma)<\mathrm{rank}(\tau)$, where the rank are the ordinals that you defined (although you could also take the usual von Neumann rank, it doesn't matter).

Let $H$ be a class function, then the transfinite recursion theorem (for the well-founded relation $\in_G$) states that there exists a unique function $F$ such that for all $\tau\in V^P$ we have $$F(\tau)=H(\tau, F\restriction \{\sigma\in P\mid \sigma \in_G \tau\}).$$

We want a function $F$ that sends $\tau\mapsto \tau^G$, i.e. we want $F(\tau)=\{F(\sigma)\mid \sigma\in_G \tau\}=\{\sigma^G\mid \sigma\in_G \tau\}$, and thus the function $H$ we have to choose should be rather elementary: $H(x,y)=\mathrm{ran}(y)$ as long as $y$ is a function, and $H(x,y)$ is arbitrary otherwise. Now in the case of $F(\tau)$ we see that the choice of $y$ is $F\restriction\{\sigma\in P\mid \sigma\in_G\tau\}$, which is a function, and its range is $\{F(\sigma)\mid \sigma\in_G\tau\}$.