Club guessing at the double successor of an uncountable regular cardinal

Put $S=E_{\kappa }^{\theta }$. Both ${\kappa }^{+}$ and $\theta$ are regular by F4, and $S$ is stationary by F2 since $\kappa <\theta =\mathrm{cf}(\theta )$. For each $\delta \in S$, F3 supplies a cofinal subset of size $\kappa$. Enumerate it by $\kappa$ and build a continuous strictly increasing cofinal sequence in $\delta$: at successors exceed the previous value and the next enumerated value, and at nonzero limits take the supremum. Each intermediate supremum is below $\delta$ by F3. F5 supplies this recursion, and its range $C_{\delta }^0$ is closed, cofinal and has order type $\kappa$. AC selects these witnesses simultaneously for the set $S$.

For every club $E\subseteq \theta$, $E^{\mathrm{\prime }}$ is club and contained in $E$. Indeed, above any $\gamma <\theta$ take a strictly increasing countable sequence in $E$ by repeatedly taking the least larger point. Its supremum is below $\theta$ by F3 and lies in $E^{\mathrm{\prime }}$ above $\gamma$. If nonzero limit $\eta <\theta$ is an accumulation point of $E^{\mathrm{\prime }}$, every $\gamma <\eta$ has some $\zeta \in E^{\mathrm{\prime }}\cap \eta$ above it and then a point of $E\cap \zeta$ above $\gamma$. Thus $\sup (E\cap \eta )=\eta$, so $\eta \in E^{\mathrm{\prime }}$. Closure of $E$ gives $E^{\mathrm{\prime }}\subseteq E$. For $\delta \in S\cap E^{\mathrm{\prime }}$, both $C_{\delta }^0$ and $E\cap \delta$ are clubs of $\delta$. Their intersection is club by F1, since $2<\kappa =\mathrm{cf}(\delta )$. Its order type is at most $\kappa$ as a subset of $C_{\delta }^0$, and its cardinality is at least $\kappa$ by F3; hence its order type is exactly $\kappa$.

Consider the assertion that some club $E\subseteq \theta$ has the following property: every club $D\subseteq \theta$ contains $C_{\delta }^0\cap E$ for some $\delta \in S\cap E^{\mathrm{\prime }}$. If it failed, for each club $E$ the set of clubs $D$ satisfying $C_{\delta }^0\cap E\subseteq ̸D$ for all $\delta \in S\cap E^{\mathrm{\prime }}$ would be nonempty. These witness sets are subsets of $\mathcal{P}(\theta )$; A1 fixes a choice $D(E)$ on this set-indexed family. By F5 define $E_0=\theta$, $E_{\alpha +1}=(E_{\alpha }\cap D(E_{\alpha }){)}^{\mathrm{\prime }}$, and $E_{\gamma }={\bigcap }_{\alpha <\gamma }{E}_{\alpha }$ at nonzero limits, for $\alpha ,\gamma <{\kappa }^{+}$. Each is club by step 2.1 and F1, since all intersection lengths are below $\theta$. The sequence decreases by inclusion, and $E_{\ast }={\bigcap }_{\alpha <{\kappa }^{+}}{E}_{\alpha }$ is also club because ${\kappa }^{+}<\mathrm{cf}(\theta )$.

F2 gives $\delta \in S\cap E_{\ast }$. For every $x\in C_{\delta }^0\setminus E_{\ast }$, let $r(x)<{\kappa }^{+}$ be the least stage with $x\mathrm{\notin }{E}_{r(x)}$. There are at most $\kappa$ such stages because $\mathrm{\mid }{C}_{\delta }^0\mathrm{\mid }=\kappa$. F3 and the regularity of ${\kappa }^{+}$ from F4 give an $\alpha <{\kappa }^{+}$ at least all of them; if there are none, take $\alpha =0$. Then $C_{\delta }^0\cap E_{\alpha }=C_{\delta }^0\cap E_{\ast }=C_{\delta }^0\cap E_{\alpha +1}$. But $\delta \in E_{\alpha +1}\subseteq E_{\alpha }^{\mathrm{\prime }}$, so the choice of $D(E_{\alpha })$ gives an $x\in C_{\delta }^0\cap E_{\alpha }$ outside $D(E_{\alpha })$. Since $E_{\alpha +1}\subseteq D(E_{\alpha })$, that $x$ is outside $E_{\alpha +1}$, contradicting the equality. Consequently the assertion of step 3.1 holds.

Take a successful $E$ and set $C_{\delta }=C_{\delta }^0\cap E$ for $\delta \in S\cap E^{\mathrm{\prime }}$, and $C_{\delta }=C_{\delta }^0$ for the remaining $\delta \in S$. Each is club of order type $\kappa$ by steps 1.1–2.1. For any club $D\subseteq \theta$, the success property supplies $\delta \in S\cap E^{\mathrm{\prime }}$ with $C_{\delta }=C_{\delta }^0\cap E\subseteq D$. This is the required sequence on all of $S$. QED.