Q:

Transfinite Recursion Theorem

I have the following homework assignment:
Let $\textbf{V} \models ZFC$ and let $\mathbb{P} = (P, \leq)$ be a forcing partial order in $\textbf{V}$. Define a class function $F: \textbf{V} \to \textbf{V}$ such that using the transfinite recursion theorem there exists a function $G: \Omega \to \textbf{V}$ such that for all $\alpha \in \Omega$:
$$ G(\alpha) = V_\alpha^{\mathbb{P}}$$
What follows is my answer, can you please tell me if I have it right:
(i) For $\alpha = \emptyset $ we want $G(\alpha) = V_\emptyset^\mathbb{P} = 0 =: F(0)$
(ii) For $\alpha = 1$ we want $G(1) = V_1^\mathbb{P} = \mathcal{P}( V_\emptyset^\mathbb{P}\times \mathbb{P}) = \mathcal{P}( \emptyset \times \mathbb{P}) \cong \mathcal{P}(\emptyset) = \{\emptyset\} = 1 =: F(G|_1)$
For $\alpha = 2$ we want $G(2) = V_2^\mathbb{P} = \mathcal{P}(V_1^\mathbb{P} \times \mathbb{P}) = \mathcal{P}(\{\emptyset\} \times \mathbb{P}) =: F(G|_2)$
So for a successor ordinal $\alpha \in \Omega$ we define $F(G|_{\alpha + 1}) := \mathcal{P}(F(G|_\alpha) \times \mathbb{P})$
(iii) For a limit ordinal $\alpha \in \Omega$, we have $V_\alpha^\mathbb{P} = \cup_{\beta \in \alpha} V_\beta^\mathbb{P}$ and so we want to define $G(\alpha) = \cup_{\beta \in \alpha} V_\beta^\mathbb{P} = \cup_{\beta \in \alpha} F(G|_\beta) =: F(G|_\alpha)$
Is this all I need to do? Or do I need to show that $F$ is well-defined or anything else? Many thanks for your help!

A:

This is hardly an answer, but an attempt to convey some ideas.  (And is more of a response to Matt's comment/question to me above.)
To answer a small question, by an $\alpha$-sequence we simply mean any function with domain $\alpha$ (where $\alpha$ is an ordinal).  And we will follow standard notation that by $\langle x_\xi \rangle_{\xi<\alpha}$ we denote the $\alpha$-sequence $g$ where $g (\xi) = x_\xi$ for all $\xi < \alpha$.
I'm not certain how pedantic you are supposed to be in your own solution, but since they are even asking you to do this, you might have to be fairly thorough, so let's look at the Recursion Theorem closely.  It says that given $F : V \to V$ there is a (unique) $G : \mathrm{On} \to V$ such that for all $\alpha$
$$
G ( \alpha ) = F ( G \restriction \alpha ).
$$
Looking at the right-hand-side, we have "the value of $F$ at the argument $G \restriction \alpha$."  Clearly, $G \restriction \alpha$ is an $\alpha$-sequence, so we should focus our main attention to defining $F$ on $\alpha$-sequences.  As we intend to define the "$\mathrm{On}$-sequence" $G = \langle V_\alpha^P \rangle_{\alpha \in \mathrm{On}}$, we note for $\alpha \in \mathrm{On}$ that $G \restriction \alpha = \langle V_\xi^P \rangle_{\xi < \alpha}$.  So the case that we are really, really interested in is when we have an $\alpha$-sequence of the form $\langle V_\xi^P \rangle_{\xi < \alpha}$.  Now how to you move from this to $V_\alpha^P$?  Clearly this will depend on whether $\alpha$ is a successor or a limit ordinal, but I am sure that by looking at these cases closely for a few seconds you will see how to do this -- and we have thus begun our definition of $F$.  Whatever you do will likely be easily extended to arbitrary $\alpha$-sequences, where the values of the sequence are not necessarily of the form desired, so you might as well define $F$ in this similar way (it doesn't hurt), and then take $F (x) = \emptyset$ whenever $x$ is not an $\alpha$-sequence for any $\alpha$.  In this way we will get $F : V \to V$.

