# A question about the canonical constructible square sequence

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:

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

General Questions:

1. What is the complexity of $C$? By "complexity," I mean in the same sense that the canonical constructible well-order is $\Sigma _1$.
2. 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))$

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

2. 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)?

3. 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?

-
Amit, I haven't looked at everything here carefully, but I can get you started: The global square sequences as here tend to be fairly absolute in their definitions, and particularly so in $L$. Essentially they are built by looking for each cardinal $\kappa^+$ at the $L_\gamma$ that are elementary in $L_{\kappa^+}$ (this is absolute), and using them to define fine structural embeddings (which are completely determined by a few parameters, which in turn are also determined from the situation). The actual clubs are then defined in terms of the critical points of the resulting embeddings. –  Andres Caicedo Dec 22 '10 at 2:42
Actually there is an issue that concerns me: The global sequence has the property that if $\kappa$ is a cardinal, then the sequence defined in $L_\kappa$ or $V_\kappa$ or $H_\kappa$ is just the restriction to $\kappa$ of the global sequence. But this is far from meaning it is absolute (it is important that $\kappa$ is a cardinal, not just that it "looks" like a cardinal, so if $\kappa$ is not a cardinal but $L_\gamma$ thinks that $\kappa$ is a cardinal, for "many" $\gamma$ past $\kappa$, this still does not guarantee that the sequence as defined in $L_\kappa$ coincides with the global one.) –  Andres Caicedo Dec 24 '10 at 2:59
Hi Andres, why does this concern you? It sounds like a pretty good answer to my General Question 2, and a positive answer to my Specific Question 2 (since we're talking about the true $\omega _2$, and not mereley $\omega _2 ^L$). Do you know a good reference where I can learn about the fact you're mentioning here? –  Amit Kumar Gupta Dec 24 '10 at 3:31
@Amit: Oh, sure, the proof of this fact answers your question 2. The issue is the $\Delta_0$ (or $\Sigma_1$) complexity of the formula. I think that Jensen's original paper deals with global square. I have been thinking of a good additional reference; my problem is that the ones I know are written for more general contexts, where you need to know more fine structure (since the constructions work for inner models with large cardinals). –  Andres Caicedo Dec 24 '10 at 3:45