$PFA \implies SOCA$. (Or using forcing to prove theorems unrelated to consistency.)

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.

• If you understand why $\sf MA(\aleph_1)$ implies there are no Suslin trees, then you already understand 60% of the needed ideas for this proof. Proofs using "strong" forcing axioms are slightly different because they usually involve collapsing something to be $\omega_1$ and then applying some ccc, or otherwise interesting, forcing. But then you just consider the two-step iteration from the original ground model as a forcing in your class of forcings on which your forcing axiom applies---just like in the case of MA and Suslin trees. – Asaf Karagila Oct 30 '16 at 6:54

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.

• Thank you! Just checking: If I understand correctly the filter $G$ and hence the sets $I$ and $\{e_\eta:\eta\in I\}$ are actually elements of my ground model, and apparently my confusion was thinking $G$ was fully-generic and so $\textit{not}$ an element of the ground model. P.S. I don't see why it is important that the $D_\alpha$ are open. Is it? – JKEG Oct 30 '16 at 16:02
• Yeah. That's the key point. We start with "There are names for these objects because Q ensures that", we move to "These are ground model 'surrogates' to these names, as given by the partially-generic filter". The reason we need the sets to be open is that (1) that's the formulation of forcing axioms; and (2) consider the forcing $2^{<\kappa}$, now consider the two dense sets $D_0$ of sequences whose length is an even length ordinal and $D_1$ which is those of odd length. Both are dense, neither is open, what is their intersection? – Asaf Karagila Oct 30 '16 at 16:19