Prikry Forcing and Gitik's Singular-Cardinal Model

First fix a colouring $c:[\kappa {]}^m\to \lambda$, where $\lambda <\kappa$. If $m=0$, its singleton domain makes it constant. If $m=1$ and no colour class belongs to $U$, the complement of every colour class belongs to $U$. Their intersection belongs to $U$ by $\kappa$-completeness, but it is empty, a contradiction. Thus some measure-one set is homogeneous in the unary case. Notice also that every tail $\kappa \setminus (\alpha +1)$ is in $U$: intersect the complements of its fewer than $\kappa$ singleton points.

Induct on $m$. Assume the result for $m$ and consider $c:[\kappa {]}^{m+1}\to \lambda$. For every $\alpha <\kappa$, extend the tail colouring $t\mapsto c(\{\alpha \}\cup t)$ from $[\kappa \setminus (\alpha +1){]}^m$ to all of $[\kappa {]}^m$ by assigning one fixed value of $\lambda$ off the tail. Apply the induction hypothesis to this total extension, obtaining a homogeneous $H_{\alpha }\in U$, and put $B_{\alpha }=H_{\alpha }\cap (\kappa \setminus (\alpha +1))\in U$. Its restriction to the tail is the original colouring, so $B_{\alpha }$ is homogeneous for that colouring; call its constant value $i_{\alpha }<\lambda$. Using Choice, make these selections simultaneously. The diagonal intersection $D=\{\beta <\kappa :(\mathrm{\forall }\alpha <\beta )\beta \in B_{\alpha }\}$ belongs to $U$.

Apply the unary case to $\alpha \mapsto i_{\alpha }$ and take $X\in U$ on which it has constant value $i$. Put $A=D\cap X$. If ${\alpha }_0<\cdots <{\alpha }_m$ lie in $A$, then ${\alpha }_j\in B_{{\alpha }_0}$ for every $0<j\le m$, by the definition of $D$. Consequently $c(\{{\alpha }_0,\dots ,{\alpha }_m\})=i_{{\alpha }_0}=i$. This proves the fixed-arity claim for every finite $m$.

For every $n<\omega$, use the fixed-arity claim to choose $A_n\in U$ on which $c_n$ is constant. Since $\omega <\kappa$, countable completeness gives $A={\bigcap }_{n<\omega }{A}_n\in U$. Restricting a constant colouring remains constant, so this $A$ works for every $n$, including $n=0$. Choice selects the family $⟨B_{\alpha }:\alpha <\kappa ⟩$ at each induction stage and the countable family $⟨A_n:n<\omega ⟩$; the filter calculations after those selections are choice-free. [F1, F3, step 3.1, discharge-induction] $\mathrm{\square }$

For each $n<\omega$ and $t\in [A{]}^n$, listed increasingly, colour $t$ by $0$ if some upper part $B_t$ makes $(s^{⌢}t,B_t)$ a condition forcing $\phi$, by $1$ if some such condition forces $\mathrm{\neg }\phi$, and by $2$ if neither exists. Colours $0$ and $1$ cannot both apply: two witnesses have the same stem, so F1 gives a common extension, while persistence would make that extension force both alternatives. By F2, shrink $A$ to one $A^{\mathrm{\prime }}\in U$ on which every arity-colouring is constant, and set $q=(s,A^{\mathrm{\prime }}){\le }^{\ast }p$.

Decision density below $q$ gives a condition $r\le q$ deciding $\phi$. Let $n$ be the number of entries which the stem of $r$ adds after $s$, and let $t$ be that increasing $n$-tuple. Then $t\in [A^{\mathrm{\prime }}{]}^n$ and its colour is $0$ or $1$, according to the decision made by $r$; it is not $2$. Write $\epsilon \in \{0,1\}$ for this homogeneous colour at arity $n$.

For every $m<\omega$, the homogeneous colour at arity $n+m$ is also $\epsilon$. Indeed, start with a witness at $t$ having colour $\epsilon$ and choose $m$ further increasing points from its measure-one upper part intersected with $A^{\mathrm{\prime }}$; strengthening by those points preserves its decision, so the resulting $(n+m)$-tuple has colour $\epsilon$. Homogeneity at that arity gives the claim, including $m=0$. Only finite selection is made here; the arbitrary simultaneous measure-one choices occurred inside F2 and are the precise AC use propagated from The Axiom of Choice.

Let $a\le q$ be arbitrary and let $m$ be the number of its new stem entries after $s$. Extend that stem by $n$ points from its upper part. Its resulting $(m+n)$-tuple has colour $\epsilon$ by step 3.1, so a same-stem witness forces the corresponding alternative. Intersecting the two upper parts as in F1 gives a common strengthening of $a$ which forces that alternative. Thus that alternative is dense below $q$, and F3 implies that $q$ itself forces it. Hence $q$ decides $\phi$ without changing the stem of $p$. [F1, F3, step 3.1] $\mathrm{\square }$

Any two conditions in $G$ have a common stronger condition because $G$ is a filter. Their stems are therefore both initial segments of the common stem and hence are comparable by end-extension. Thus $g=\bigcup \{s_p:p\in G\}$ is a function whose domain is an initial segment of $\omega$, and F1 makes it strictly increasing.

For each $n<\omega$, let $D_n$ consist of conditions whose stems have length at least $n$. It is dense: from $(s,A)$ add finitely many increasing points from the nonempty successive measure-one tails of $A$. The definition of $D_n$ and this density proof are in $M$. By F3, $G$ meets $D_n$ for every ground-model natural number $n$; transitivity makes these all actual natural numbers. Hence $\mathrm{dom}(g)=\omega$.

A measure-one set is unbounded in $\kappa$. Otherwise it would be contained in some $\alpha <\kappa$, while $\kappa \setminus \alpha$ belongs to $U$ because it is the intersection of fewer than $\kappa$ complements of singleton sets; this contradicts properness. For each $\alpha <\kappa$, the set $E_{\alpha }$ of conditions with a nonempty stem whose last entry exceeds $\alpha$ is consequently dense: extend once using a point of the upper part above $\alpha$. Since $E_{\alpha }\in M$, F3 gives $p\in G\cap E_{\alpha }$, and an entry of $g$ exceeds $\alpha$. Thus $g$ is cofinal in $\kappa$.

The canonical name for the union of generic stems evaluates to $g$, and the truth lemma places the preceding statements in $M[G]$. By F5, $g:\omega \to \kappa$ cofinal gives $\mathrm{cf}(\kappa )\le \omega$. No finite sequence is cofinal in the infinite limit ordinal $\kappa$, since its finite range has a maximum below $\kappa$; therefore $\mathrm{cf}(\kappa )$ is not finite and equals $\omega$. [F4, F5, step 2.1, step 2.2] $\mathrm{\square }$

For each pair $(r,\xi )$ with $r{\le }^{\ast }p$ and $\xi <\gamma$, F1 makes the set of direct extensions of $r$ deciding ``$\check{\xi }\in \dot{x}$'' nonempty. By F4 choose one such extension for every pair. This fixed selector, rather than an unstated sequence of arbitrary choices, will drive the recursion.

Write $p=(s,A_0)$. By transfinite recursion on $\xi <\gamma$, keep the stem $s$: at a successor use the selector from step 1.1 to obtain $p_{\xi +1}{\le }^{\ast }{p}_{\xi }$ deciding ``$\check{\xi }\in \dot{x}$'', and at a nonzero limit $\delta <\gamma$ take upper part ${\bigcap }_{\xi <\delta }{A}_{\xi }$. The latter is in the measure because $\delta <\gamma <\kappa$. Hence every $p_{\xi }$ is a condition and the sequence is direct-extension decreasing.

Intersect all upper parts used in the recursion, including the original one, to obtain $B\in U$, and put $q=(s,B)$. This also covers $\gamma =0$, when the intersection has just the original factor. Define in the ground model $x=\{\xi <\gamma :p_{\xi +1}⊩\check{\xi }\in \dot{x}\}$. For every $\xi <\gamma$, $q\le p_{\xi +1}$, so $q$ forces the positive membership statement exactly when $\xi \in x$, and otherwise forces its negation.

Let $G$ be any generic filter containing $q$. Since $q\le p$, the hypothesis gives ${\dot{x}}_G\subseteq \gamma$; step 3.1 says for every $\xi <\gamma$ that $\xi \in {\dot{x}}_G$ exactly when $\xi \in x$. Extensionality yields ${\dot{x}}_G=x$. By the semantic equivalence in F3, $q⊩\dot{x}=\check{x}$. The case $\gamma =0$ says simply that every subset of zero is empty, and was already included in step 3.1. [F3, step 3.1] $\mathrm{\square }$

There are at most $\kappa$ finite stems. To see this without hiding cardinal arithmetic, use F4 to fix a bijection $b:\kappa \times \kappa \to \kappa$, recursively code a nonempty finite sequence by repeated application of $b$, and tag the code with its length. This injects all finite sequences from $\kappa$ into $\omega \times \kappa$, whose cardinality is $\kappa$ by F4 because $0<\omega \le \kappa$. The ambient dependency The Axiom of Choice is not used in this count: one existing bijection is fixed and the recursion is finite.

Given ${\kappa }^{+}$ conditions, if all their stems were distinct, step 1.1 would inject ${\kappa }^{+}$ into $\kappa$, contrary to F5. Two therefore have the same stem, and F1 makes them compatible. Thus no antichain has cardinality ${\kappa }^{+}$; under ZFC, any antichain of cardinality at least ${\kappa }^{+}$ contains a ${\kappa }^{+}$-sized subfamily. By F3, ${\mathbb{P}}_U$ is ${\kappa }^{+}$-cc.

For every $\alpha <\kappa$, the tail $A_{\alpha }=\kappa \setminus (\alpha +1)$ lies in $U$: it is the intersection of the fewer than $\kappa$ complements of the singleton points at most $\alpha$. Hence $p_{\alpha }=(⟨\alpha ⟩,A_{\alpha })$ is a condition. If $\alpha \mathrm{\ne }\beta$, a common extension would have a stem end-extending both distinct one-entry stems, which is impossible. Thus $\{p_{\alpha }:\alpha <\kappa \}$ is an antichain of size $\kappa$. Since $\kappa$ is uncountable, F3 shows that the forcing is not ccc.

Every ground cardinal $\lambda <\kappa$ remains a cardinal. Otherwise in $M[G]$ some ordinal $\alpha <\lambda$ would be bijective with $\lambda$, by F7. In $M$, cardinal absorption supplies a bijection coding $\alpha \times \lambda$ by an ordinal $\rho <\kappa$ (the finite cases are immediate and the infinite case uses F6). The graph of the alleged bijection therefore codes a new subset of $\rho$, but F1 says that subset, and hence the graph, belongs to $M$. This contradicts that $\lambda$ was a ground cardinal. Choice is used only through the ground cardinal comparisons and coding already stated in F6 and F7.

The ordinal $\kappa$ also remains a cardinal. If it were equinumerous in $M[G]$ with some $\alpha <\kappa$, let $\mu =\mathrm{\mid }\alpha {\mathrm{\mid }}^M<\kappa$ and obtain an injection $e:\kappa \to \mu$. Since F3 makes $\kappa$ a limit cardinal, the ground successor cardinal ${\mu }^{+}$ is still below $\kappa$; it remains a cardinal by step 1.1. Restricting $e$ to ${\mu }^{+}$ would inject that preserved successor cardinal into $\mu$, contradicting the defining minimality in F7.

Write the infinite cardinal $\kappa$ as ${\mathrm{\aleph }}_{\alpha }$ using F5. Then ${\kappa }^{+}={\mathrm{\aleph }}_{\alpha +1}$ by the successor convention in F7, and F5 makes ${\kappa }^{+}$ regular under Choice. F2 and F4 now imply that every ground cardinal at least ${\kappa }^{+}$ is preserved. Together with steps 1.1 and 2.1, this covers every ground cardinal.

Cardinal preservation is not cofinality preservation at $\kappa$: F8 supplies in $M[G]$ a cofinal map from $\omega$ into the still-cardinal ordinal $\kappa$, and proves $\mathrm{cf}(\kappa )=\omega$. Thus the two promised conclusions coexist without treating the cofinality change as a collapse.

The coordinate filters exist with exactly the advertised completeness. For a strongly compact $\kappa \le \alpha$ with $\alpha$ regular, the co-bounded filter on $\alpha$ is proper and $\kappa$-complete: the union of fewer than $\kappa$ sets of size below $\alpha$ still has size below regular $\alpha$. F1 extends it to a $\kappa$-complete ultrafilter, which is uniform because it contains every co-bounded set. Apply this once at type 1 and at every ${\kappa }_{\nu }^{\alpha }$ for type 2, then use $W_O$ to take the least choices. F2 confirms the equivalent fine-measure formulation of the large-cardinal input, but no normal fine measure or supercompactness is smuggled into the selected uniform filters.

Finiteness makes the cut in clause 3 of $P_2$ unique: below the cut all high section-domains have the larger common length and from the cut onward all have the smaller common length. Adding the next value preserves clauses 1 and 2 automatically in the type-1 case; in the type-2 case it does so exactly when the index slot at ${\mathrm{cf}}^{\mathrm{\prime }}(\alpha (p))$ is already filled. This proves both directions of the displayed extendability equivalence and makes ${\mathrm{\Phi }}_p$ well-defined.

Clauses 3–10 make every upper part a nonempty predecessor-closed branching system above its trunk, with each required successor set in the filter indexed by step 2.1. A full tree of all legal finite successors above any coherent trunk witnesses nonemptiness. A proposed pruning is an upper part only when it still satisfies every clause, including the union closure in clause 6; shrinking successor sets separately does not by itself prove this. The later pruning arguments therefore use intersections of coherent cone trees to restore clause 6 after their measure-one successor choices. Thus the definition supplies actual conditions without asserting a false blanket closure property.

The forcing order is reflexive. It is transitive because restriction composes: if $W\upharpoonright {\mathrm{dom}}_1(q)\subseteq V$ and $V\upharpoonright {\mathrm{dom}}_1(p)\subseteq U$, then $W\upharpoonright {\mathrm{dom}}_1(p)\subseteq U$. A fixed-trunk shrinking which remains an upper part under clauses 3–10 is consequently a direct refinement. For fixed regular $\theta$, all stems and all their upper trees are subsets of sets built from $\theta \times \omega \times \theta$, so $P_{\theta }$ is a set; unbounded coordinate domains make their union a proper class.

Put $U\upharpoonright a=\{q\upharpoonright a:q\in U\}$. For a Gitik condition $(p,U)$, clauses 1–4 and 7–9 of F1 plainly survive restriction to a closed support. For the small-coordinate successor clause, lift a projected trunk $r$ and use clause 7 to replace its lift by one agreeing with $p$ off $a$; the old measure-one successor set is contained in the projected one. For union/tree monotonicity, use the lifts $p\cup r_i$ and clause 6 before projecting. For predecessors, choose a lift with the least finite number of added triples; clause 10's last triple must then lie in the projection. Thus $(p\upharpoonright a,U\upharpoonright a)$ is a condition.

If $s\in U$, the cone $U_s=\{t\in U:s\subseteq t\}$ satisfies all ten clauses: clauses 5–7 follow by first adjoining the small part of $s$ with clauses 6–7, and the remaining clauses are inherited. If $b\supseteq {\mathrm{dom}}_1(p)$ is finite and closed under ${\mathrm{cf}}^{\mathrm{\prime }}$, extending every trunk coherently to $b$ gives a condition by the same clause-by-clause induction. Two upper trees with a common trunk may be intersected because every relevant coordinate filter is closed under finite intersections. Combining these operations aligns compatible trunks on the union of two finite closed supports and then intersects their upper trees, proving the asserted amalgamation.

Let $A\subseteq P_{\theta }$ be a maximal antichain and $c=(p,U)\in P_3$. The restriction $c\upharpoonright \theta$ is compatible with some $r\in A$; take a common refinement $d=(q,V)\in P_{\theta }$ and first directly lengthen its finitely many trunk sections to a common finite length. Choose $t\in U$ whose restriction to the old coordinates below $\theta$ is the corresponding part of $q$, and pass to the cone above $t$. The union $t\cup q$ is a coherent trunk: on the overlap the two functions agree, while outside it their coordinate domains are disjoint. Support extension and intersection of the two lifted upper trees, as in step 2.1, produce a condition refining both $c$ and $d$, hence both $c$ and $r$. Thus every maximal antichain of $P_{\theta }$ remains maximal in $P_3$, which is the complete-subforcing assertion. If $G\subseteq P_3$ is generic for the ground-definable dense classes, $G_{\theta }=G\cap P_{\theta }$ consequently meets every ground dense subset of $P_{\theta }$. Finally, the transitive closure of a set name is a set; the union of the finite coordinate supports of all conditions occurring in it is therefore a set of ordinals and is bounded by a regular $\theta$. Induction on name rank makes the name a $P_{\theta }$-name. Evaluating it uses only $G_{\theta }$, proving the displayed union of extensions.

Work below a fixed condition on $a$. For every type-2 tail coordinate $\alpha \in a\setminus \kappa$ whose ${\mathrm{cf}}^{\mathrm{\prime }}(\alpha )$ coordinate lies below $\kappa$, choose the least index ${\lambda }_{\alpha }$ for which ${\kappa }_{{\lambda }_{\alpha }}^{\alpha }\ge \kappa$. Prune the lower-coordinate successor sets so that every later value used as an index is at least the maximum of the finitely many relevant ${\lambda }_{\alpha }$. This is dense by the uniformity of those successor filters. Call the resulting dense set $J$. On $J$, split every trunk as $r=r_0\cup r_1$ below and above $\kappa$. Map $(r,R)$ to its lower restriction $(r_0,R_0)$ together with the lower-forcing name whose pairs are the tail projections $r^{\mathrm{\prime }}\upharpoonright (a\setminus \kappa )$, placed under the lower trunk condition $R_0\uparrow (r^{\mathrm{\prime }}\upharpoonright (a\cap \kappa ))$. Clauses 8–10 in F1 say exactly that this name evaluates to a tail condition with $\kappa$-complete successor filters. Conversely, strengthen a proposed pair in $E\ast \dot{Q}$ to decide its tail trunk, follow its lower tree below $\kappa$, and recursively admit a successor $\xi$ above $\kappa$ precisely when some lower refinement forces that tail successor into the named tree. The forced measure-one clauses supply a ground measure-one subset at every node, so the reconstructed combined tree is a condition in $J$. The two constructions preserve restriction and tree inclusion and the second refines every proposed iteration condition; hence this is a dense embedding.

The lower forcing $E$ has size $\mu <\kappa$: it uses finitely many coordinates below the inaccessible $\kappa$; F3 bounds the finite products of possible triples, and the strong-limit part of F2 bounds the power sets coding their upper trees. Let $H$ be $E$-generic and let $U$ be any ground $\kappa$-complete tail ultrafilter. In the extension define $U^{\ast }=\{X:(\mathrm{\exists }Y\in U)Y\subseteq X\}$. To decide a new $X\subseteq I$ below any lower condition, choose for every $i\in I$ a stronger condition deciding $i\in \dot{X}$ and partition $I$ by the deciding condition and truth value. There are fewer than $\kappa$ cells, so $\kappa$-completeness and ultrafilterhood put one cell in $U$; the corresponding condition forces that cell into $X$ or its complement. These conditions are dense, so $U^{\ast }$ is an ultrafilter. For a sequence of $\delta <\kappa$ members of $U^{\ast }$, maximal antichains of size at most $\mu$ list ground witnesses for each member. Intersecting all fewer than $\kappa$ listed witnesses gives one ground $U$-set contained in their intersection. Thus $U^{\ast }$ is $\kappa$-complete in $M[H]$.

A descending sequence of fewer than $\kappa$ fixed-trunk tail conditions has a lower bound obtained by intersecting their trees. At every surviving node the successor set is the intersection of fewer than $\kappa$ members of the relevant $U^{\ast }$ and is therefore measure one by step 4.1; predecessor and coherence clauses survive intersection. This is precisely $\kappa$-closure in F6. The empty tail is the trivial forcing and satisfies the same conclusion.

Fix $(s,S)\in Q$ and a sentence $\phi$. Cycle from left to right through the finitely many tail coordinates, thereby enumerating the unfilled slots and levels above $s$. At a level $j$, colour a trunk $r$ by $0$, $1$, or $2$ according as some upper subtree with trunk $r$ forces $\phi$, forces $\mathrm{\neg }\phi$, or neither; same-trunk intersection makes the first two alternatives exclusive. Define the colour at earlier levels backwards: at a node $r$, take the unique colour whose successor set is in the ultrafilter at $r$. Countable completeness permits simultaneous intersection over all later levels, and AC chooses these prunings at every node, producing one tree $W\subseteq S$. If two extensions of $(s,W)$ forced opposite alternatives, extend the shorter trunk through finitely many measure-one intersections until both trunks have the same level. Backward homogeneity then assigns them the same colour, a contradiction. By decision density, some extension decides $\phi$; since the opposite alternative occurs nowhere below $(s,W)$, its chosen alternative is dense there, and F4 makes $(s,W)$ itself decide it without changing $s$.

Let $\gamma <\kappa$ and suppose a tail condition forces $\dot{x}\subseteq \gamma$. Recursively apply step 6.1 to decide each statement ``$\xi \in \dot{x}$'' by a fixed-trunk refinement. At limit stages below $\gamma$, and once more at the end, use the direct $\kappa$-closure from step 5.1. The final condition decides all memberships; Separation in the lower extension forms the corresponding set $x\subseteq \gamma$, and F4 gives that the condition forces $\dot{x}=\check{x}$. This includes $\gamma =0$ (the original condition and the empty set) and proves that $Q$ adds no bounded subsets below its completeness bound.

A $P_3$-name is a set whose transitive closure contains only set many conditions. By F1, the union of their finite coordinate supports is bounded by a regular $\theta$, so rank induction makes the name a $P_{\theta }$-name. A finite tuple has a common regular bound, as does that tuple together with any one witness name or condition.

For names $\tau ,\sigma$ and a condition $p$, define $p{⊩}_3\tau \in \sigma$ iff some regular $\theta$ satisfies: for every regular $\eta \ge \theta$, $p\in P_{\eta }$, $\tau ,\sigma$ are $P_{\eta }$-names, and $p{⊩}_{P_{\eta }}\tau \in \sigma$; define equality identically. F1 gives a starting bound. If $\theta \le \eta$, completeness of $P_{\theta }\subseteq P_{\eta }$ preserves the set-forcing value of atomic formulas on $P_{\theta }$-names: a maximal antichain deciding the atomic statement in $P_{\theta }$ remains maximal in $P_{\eta }$. Thus the eventual value exists, is independent of the starting bound, and is first-order definable by F3.

Using the atomic equality relation from step 1.2, define the three new atoms by density below $p$: $p{⊩}_{3}B(\tau )$ iff $\{q\le p:(\mathrm{\exists }x\in M)q{⊩}_3\tau =\check{x}\}$ is dense below $p$; $p{⊩}_{3}A(\tau ,\sigma )$ iff $\{q\le p:(\mathrm{\exists }(a,b)\in P_3)q\le (a,b),q{⊩}_3\tau =\check{a},q{⊩}_3\sigma =\check{b}\}$ is dense below $p$; and $p{⊩}_3{W}_O(\tau ,\sigma )$ iff $\{q\le p:(\mathrm{\exists }x,y\in M)W_O(x,y),q{⊩}_3\tau =\check{x},q{⊩}_3\sigma =\check{y}\}$ is dense below $p$. All quantifiers range over sets satisfying definable class predicates, so these are first-order formulas rather than quantification over a set of all conditions or names.

Suppose $p\in G$ and $\tau ,\sigma$ have a common bound $\theta$. The restriction $G_{\theta }$ is $P_{\theta }$-generic by F1. The set-forcing truth lemma F3 identifies the eventual atomic relations from step 1.2 with ${\tau }_G\in {\sigma }_G$ and ${\tau }_G={\sigma }_G$: evaluation of bounded names by $G$ equals evaluation by every sufficiently large $G_{\eta }$. Conversely, when one of these atomic statements is true, F3 supplies a condition in some $G_{\eta }$ forcing it, and that condition forces the same eventual value.

For every fixed expanded formula, recurse externally through its finite syntax. Use conjunction in the usual way, let $p{⊩}_3\mathrm{\neg }\psi$ iff no $q\le p$ forces $\psi$, and let $p{⊩}_3\mathrm{\exists }x\psi (x,\vec{\tau })$ iff $\{q\le p:(\mathrm{\exists }\text{ set name }\sigma )q{⊩}_3\psi (\sigma ,\vec{\tau })\}$ is dense below $p$. Namehood and $P_3$ are definable classes, so each fixed recursion clause is first order. This is a scheme indexed externally by formulas, not a uniform satisfaction predicate. Induction also gives persistence under strengthening.

The dense clauses have the intended truth values. If $p\in G$ forces $B(\tau )$, genericity meets the dense class below $p$, giving $q\in G$ and $x\in M$ with $q{⊩}_3\tau =\check{x}$; hence ${\tau }_G=x\in M$. Conversely, if ${\tau }_G=x\in M$, atomic set-stage truth gives $q\in G$ forcing $\tau =\check{x}$, and persistence makes every extension of $q$ a witness to the $B$-clause. The $W_O$ proof is identical. For $A$, a forward witness has $q\le (a,b)$ with $q\in G$, so upward closure puts $(a,b)\in G$ and atomic truth gives $({\tau }_G,{\sigma }_G)=(a,b)$. Conversely, if this pair is a condition in $G$, directedness combines it with conditions forcing the two equalities; their common refinement makes the witnesses dense below it.