A bounded-name direct-extension fusion

For every direct extension $r{\le }^{\ast }p$ and every $\xi <\gamma$, let $C(r,\xi )$ be the nonempty set of direct extensions of $r$ deciding “$\check{\xi }\in \dot{x}$.” Nonemptiness is F1. Use F4 once to choose $d(r,\xi )\in C(r,\xi )$ simultaneously for all such pairs.

Define $p_{\xi }=(s,A_{\xi })$ for $\xi \le \gamma$. Start with $p_0=p$. Given $p_{\xi }$, put $p_{\xi +1}=d(p_{\xi },\xi )$. At a nonzero limit $\delta \le \gamma$, put $A_{\delta }={\bigcap }_{\xi <\delta }{A}_{\xi }$ and $p_{\delta }=(s,A_{\delta })$. Since $\delta \le \gamma <\kappa$, F3 keeps $A_{\delta }$ in $U$. Thus this is a direct-extension decreasing recursion, and $p_{\xi +1}$ decides the $\xi$th membership question.

Put $B={\bigcap }_{\xi \le \gamma }{A}_{\xi }$ and $q=(s,B)$. The family has cardinality below $\kappa$, so F3 gives $B\in U$ and $q{\le }^{\ast }{p}_{\xi }$ for every $\xi \le \gamma$. Define $x=\{\xi <\gamma :p_{\xi +1}⊩\check{\xi }\in \dot{x}\}\mathrm{.}$ For each $\xi <\gamma$, the stronger condition $q$ preserves the decision of $p_{\xi +1}$; hence it forces membership exactly for the ordinals in $x$. Together with $q\le p$ and $p⊩\dot{x}\subseteq \check{\gamma }$, extensionality gives $q⊩\dot{x}=\check{x}$, the conclusion in F2.

When $\gamma =3$, the recursion has $p_0,p_1,p_2,p_3$. If their three successive decisions are “$0\in \dot{x}$,” “$1\mathrm{\notin }\dot{x}$,” and “$2\in \dot{x}$,” then the defining calculation in step 3.1 gives $x=\{0,2\}$ and $B=A_0\cap A_1\cap A_2\cap A_3$. For $\gamma =0$, there are no decisions, $x=\mathrm{\varnothing }$, and the one-factor intersection returns $q=p$; for $\gamma =1$, there is exactly one deciding direct extension.