I'm reading Todorcevic's "Localized Reflection and Fragmens of PFA" and have a rather specific question about the proof. To avoid being too specific, I'll ask a more general question first, and afterwards include my more specific question. Let me also say that I'm just as happy to get references to papers/books where I can find answers to my questions as I am happy to get direct answers here.

Let $C$ denote the canonical constructible square sequence -- that is, "$y = C(x)$" is equivalent to some formula which, when $x$ is restricted to ordinals which are singular in $L$, defines a class function $\langle C_{\alpha} : \alpha \in \mathrm{Ord}, \mathrm{cf}^L(\alpha) < \alpha \rangle$ satisfying:

- $C_{\alpha}$ is a club in $\alpha$ of order type $< \alpha$, and
- $C_{\alpha} = C_{\beta} \cap \alpha$ whenever $\alpha$ is a limit point of $C_{\beta}$

**General Questions**:

- What is the complexity of $C$? By "complexity," I mean in the same sense that the canonical constructible well-order is $\Sigma _1$.
- How absolute is the definition of $C$? Do $V$, $L$, $V _{\alpha}$, $H _{\alpha}$, $L _{\alpha}$ agree on what $C$ is up to $\alpha$, for arbitrary ordinals (or in the case of $H _{\alpha}$, cardinals) $\alpha$?

The reason I ask this question comes from a more specific question, but to ask that question I need to give some background -- all of this comes from Stevo's article mentioned above:

Let $\mathrm{PFA}(\omega _1)$ be the statement that if $P$ is a proper notion of forcing, and $\mathcal{D}$ an $\omega _1$-sequence of predense subsets of $P$, each of size at most $\omega _1$, then there exists a $(P, \mathcal{D})$-generic filter.

**Lemma**: $\mathrm{PFA}(\omega _1)$ holds iff for every $\Delta _0$-formula $\varphi$ and a parameter $a \in H _{\omega _2} $, if some proper poset forces that $\exists x \varphi (x, a)$ is true in some transitive model then $H _{\omega _2}$ already satisfies $\exists x \varphi (x, a)$.

In a later lemma, Stevo claims that the following formula is $\Delta _0$ in order to apply the lemma quoted above: $\psi (x,y,a)$ is the formula which says:

- $x$ is a set of ordinals, all singular in $L$
- $x$ has order type $\omega _1$
- $x$ is closed in its supremum
- $y$ is a function from $x$ into $\mathbb{N}$ such that $y(\alpha) \neq y(\beta)$ whenever $\alpha, \beta \in x$ and $\alpha \in \mathrm{lim}(C_{\beta})$
- $L_{\mathrm{sup}(x)} \vDash \varphi (a)$ where $\varphi$ was some arbitrary formula from earlier in the proof (with no restrictions on its complexity)

I can't believe this formula is $\Delta _0$, but in order to apply the previous lemma we really only need it to be $\Sigma _1$, which I might believe is the case. We would also need to throw in $\omega _1$ as a parameter, but we're free to do that since we could take $\{ a, \omega _1 \}$ to be our parameter from $H _{\omega _2}$ in applying the above lemma. I can see why most of this is $\Sigma _1$ but there is a subformula for which I can't see this, and the problem I'm having is that I don't know the complexity of $C$.

**Specific Questions**:

Consider the subformula: $\forall \alpha, \beta \in x$, $(\alpha \in \mathrm{lim}(C_{\beta}) \rightarrow y(\alpha) \neq y(\beta))$

Is it $\Sigma _1$, and if so why? It would suffice to know that $c = C_{\beta}$ is $\Sigma _1$ in $c$ and $\beta$.

Later on in the proof it seems to be tacitly assumed that $H _{\omega _2}$ computes $C$ correctly. Can I be sure that $H _{\omega _2}$ computes $C$ correctly (up to $\omega _2$ of course)?

Stevo proves the lemma in question using some pretty big guns - the Covering Lemma and the canonical constructible square sequence. He also uses a proper forcing which, unless you knew how it was going to be used beforehand, appears like it would be of no use in proving the lemma. Does anyone know of a more direct proof of the lemma I'm talking about? Or, since I often find in reading Stevo's work that he uses forcing posets which I would never think to use, can anyone put this proof in perspective, and motivate why it makes sense to do the proof this way?