For an uncountable cardinal $\lambda,$ a $\square_\lambda$-sequence is a sequence $(C_\alpha: \alpha\in \lim(\lambda^+))$ such that
- Each $C_\alpha$ is a club in $\alpha$ with order type $\le \lambda.$
- For any $\alpha\in \lim(\lambda^+,$ if $\beta\in \lim(C_\alpha),$ then $C_\beta = C_\alpha\cap \beta.$
The forcing that adds a $\square_\lambda$-sequence consists of partial sequences of successor length, i.e. the set of $p$ such that
- $\operatorname{dom}(p) = (\beta+1)\cap \lim(\lambda^+)$ for some $\beta \in \lim(\lambda^+)$
- For all $\alpha\in \operatorname{dom}(p),$ $p(\alpha)$ is a club in $\alpha$ with order type $\le \lambda$
- For all $\alpha\in \operatorname{dom}(p),$ for all $\beta \in \lim(p(\alpha)),$ $p(\beta) = p(\alpha)\cap\beta.$
It's not even immediately clear (or wasn't immediately clear to me, at least) that for any $\beta <\lambda^+$. $\{p: \operatorname{dom}(p)> \beta\}$ is dense, which is necessary for this to work as advertised.
In Cummings' chapter in the Handbook of Set Theory (p. 796 of the book or p. 22 of this pdf of the chapter) he gives this as an example of a forcing that is $\mathrm{<}\lambda^+$-strategically closed (but not necessarily $\lambda^+$-strategically closed). This implies both the density condition, and also $\lambda^+$-distributivity, so that no cardinals $\le \lambda^+$ collapse, but I can't see how to prove it.
Skimming one of Cummings' references, I found a simple idea that shows it is $\lambda+1$-strategically closed:
Write $\gamma_\beta =\max(\operatorname{dom}(p_\beta)).$ Fix a club $C\subset \lambda$ of minimal order type. If it's your turn at a successor stage $\alpha = \beta+1 $ in the game, let $\gamma_\alpha =\gamma_\beta+ \omega$ and let $p_{\alpha}\upharpoonleft \gamma_\beta = p_\beta$ and $p_{\alpha}(\gamma_{\alpha}) = \{\gamma_\beta + n:n\in \omega\}.$
At a limit stage $\alpha\le \lambda$ of the game, let $\gamma_\alpha = \lim_{\beta<\alpha}\gamma_\beta$ and $p_\alpha\upharpoonleft \gamma_\beta = p_\beta$ for all $\beta < \alpha.$ If $\alpha\notin \lim(C),$ take $p_\alpha(\gamma_\alpha) = \{\gamma_\beta: \sup(C\cap \alpha) < \beta < \alpha\},$ and if $\alpha\in \lim(C)$ take $p_\alpha(\gamma_\alpha) = \{\gamma_\beta: \beta \in C\cap \alpha\}.$
It's easy to see by induction that the new club we add to the top preserves the coherence property and has order type $\le \lambda.$
I believe $\lambda+1$-strategic closure suffices for both the density and the $\lambda^+$-distributivity result (correct me if I'm wrong). But I'm still curious how can we extend this to $\alpha > \lambda$ to show $\mathrm{<}\lambda^+$-strategic closure. The strategy for $\alpha \notin \lim(C)$ breaks down since it will give order types $>\lambda $ and I see no obvious way to repair it.
Best Answer
I do not know of any application for which $\lambda+1$-strategic closure does not suffice (let me know if you find one!), but the forcing is indeed ${<}\lambda^+$-strategically closed.
To extend this to $\alpha$-strategic closure for any $\alpha<\lambda^+$, you can do a similar construction relative to a partial $\square_\lambda$-sequence of sufficient length. So assume $\vec C:=\langle C_\beta\mid \beta\in\mathrm{Lim}\cap\alpha\rangle$ is such a sequence (which always exists, as you mention).
We describe a strategy which survives the game of length $\alpha$. I keep the notation from your question. Do the same as before at a successor stage and if it is a limit turn $\delta$ then we extend the play so far by adding $p_{\delta}(\gamma_\delta)=\langle \gamma_{\beta}\mid \beta\in C_\delta\rangle$ as the top club. The properties of $\vec C$ guarantee that this is a legal move, e.g. if $\gamma_\beta$ is a limit point of $p_\delta(\gamma_\delta)$ then we played $p_\beta(\gamma_\beta)=\langle \gamma_\xi\mid \xi\in C_\beta\rangle$ before and since $C_\beta= C_\delta\cap\beta$, we have $p_\delta(\gamma_\delta)\cap\gamma_\beta=p_\beta(\gamma_\beta)$ as desired.
In fact, the strategy you describe is really a special case of the one above: If you consider the sequence $$\vec C':=\langle C_\beta'\mid \beta\in\mathrm{Lim}\cap(\lambda+1)\rangle$$ given by $C_\lambda'=C$, the club you chose in the beginning, and $C_\beta'=\beta-\sup(C\cap\beta)$ then this is a partial $\square_\lambda$-sequence and the above strategy relative to $\vec C'$ is exactly the one you mention in the question.
If there is already a full $\square_\lambda$-sequence then the forcing is even $\lambda^+$-strategically closed instead of just ${<}\lambda^+$-strategically closed. Clearly this is an equivalence as from a winning strategy witnessing $\lambda^+$-strategic closure it is straightforward to construct a $\square_\lambda$-sequence.