I'm trying to understand the proof in Kunen's book (Set Theory) of $PFA \implies SOCA.$ (Proper Forcing Axiom, Semi Open Coloring Axiom.) I do not think you need to know all the details to the proof to answer my questions. So you may want to skip these definitions and the proof.
Given $W\subseteq E\times E$ symmetric (with respect to the diagonal) a subset of $T$ of $E$ is called $W$-connected if $T\times T \setminus \Delta T$ is contained in $W$ and $W$-free if $T\times T \setminus \Delta T$ is disjoint from $W$. (Where $\Delta T$ is $T$'s diagonal.)
$SOCA$ is the statement: Whenever $E$ is an uncountable separable metric space and $W$ is an open susbet of $E\times E \setminus \Delta E$ with $W$ symmetric, there is an uncountable subse $T$ of $E$ such that either $T$ is $W$-connected or $T$ is $W$-free.
$\textbf{My first question:}$ Kunen uses the Countable Transitive Model approach to forcing. I make sense of this proof this way: We assume $PFA$. We fix $M$ a countable transitive model for ZFC and fix an uncountable separable metric space $E$ in it, and we show that $SOCA$ holds for it. This proves $PFA$ implies $SOCA$ as if it is true for an arbitrary metric space of an arbitrary countable model, then it is true for every model of ZFC and hence a consequence of ZFC. As if we get a model of ZFC where $SOCA$ fails we could get a countable transitive model where it fails. Is this reasoning correct?
$\textbf{My second question:}$ As I want $SOCA$ to be true in my fixed countable transitive $M$, I need the set (third paragraph) $\{e_\eta:\eta\in I\}$ to be an element of $M$, but to get this I probably need $I$ to be an element of $M$ as well. But as $I$ uses $G$ in its definition it seems likely that it is not actually an element of $M$. How do I fix this problem? How do I check that $\{e_\eta:\eta\in I\}\in M$? Or is this not what I want?
I appreciate very much any kind of help. Thank you for reading.
Your first question is a very natural, and a very typical question when first trying to understand forcing axioms, or generally forcing as it is actually used "in nature".
We generally care very little about the meta-mechanics of forcing. If you open Jech, who approaches to forcing via Boolean-valued models, or Halbeisen that uses finite fragments of $\sf ZFC$, all of them, at the end, use the same approach when proving something with forcing. You work inside your model, so in general, you just always force over the universe.
Therefore in this case, if you want to resort to the full meta-mechanics of forcing, you'd start with a countable model of $\sf ZFC+PFA$ and prove that the model also satisfies $\sf SOCA$. But in reality, you don't really do that. In fact, when it comes to forcing axioms, you don't actually go above and beyond to produce those generic extensions. You instead argue that the forcing you're interested in is ccc/proper/semi-proper/SSP/etc. and therefore you can apply the forcing axiom on a "small family of dense open sets".
Finally, for the second question, you are interested in $W$ which is in the ground model, in the universe. So if you have a condition that forces $(e_\xi,e_\eta)\in W$, then it has to be the case that this is true, because this is a $\Delta_0$-statement about the ground model involving only canonical names.
What happened was that we arranged a sequence $D_\alpha$ of dense open sets for $\alpha<\omega_1$. Then we used $\sf PFA$ to find $G$ inside our universe which meets those open sets. This $G$ is not fully-generic, but it is sufficiently generic to interpret enough information to allow us to find an uncountable set $T$ which acts as a surrogate for $\mathring T$ in an actual generic extension. But since $G$ was sufficiently generic, $T\subseteq W$ is $W$-connected.