Gitik's finite-support symmetric submodel

The stated maps form a group: coordinate supports remain finite under products and inverses, and composition is coordinatewise. For $\pi \in \mathcal{G}$, let $P^{\pi }$ contain the conditions $(p,U)$ whose coordinate domain contains the support of $\pi$, whose sections at $\alpha$ and ${\mathrm{cf}}^{\mathrm{\prime }}(\alpha )$ have equal length, and whose trunk already contains every moved value which can occur in $U$ at a moved coordinate. This class is dense: add the finite ${\mathrm{cf}}^{\mathrm{\prime }}$-closure of the support, equalize the finitely many section lengths by legal successors, and prune each uniform successor set away from the finitely many moved values not already in the trunk.

For finite $e,f$, $H_e\cap H_f=H_{e\cup f}$, and coordinate preservation gives $\pi H_e{\pi }^{-1}=H_e$. Thus the upward closure of the $H_e$ is a normal filter of subgroups. Closing $e$ under ${\mathrm{cf}}^{\mathrm{\prime }}$ remains finite, and $H_{\mathrm{cl}(e)}\subseteq H_e$; hence all finite sets and finite closed sets generate the same filter. F4 now defines $\mathrm{H}\mathrm{S}$ and makes $N_G$ transitive.

On $P^{\pi }$, apply ${\pi }_{\alpha }$ to every value at coordinate $\alpha$ in both the trunk and upper tree. The finite permutations preserve injectivity and every uniform filter because the image of a filter member differs from it by only finitely many points. Only the type-2 indexing clause needs more: if its fresh index value at ${\mathrm{cf}}^{\mathrm{\prime }}(\alpha )$ were moved, the domain condition from step 1.1 would put that value already in the trunk, contradicting injectivity at the fresh slot. Thus the index is fixed and the successor filter is unchanged. All remaining tree clauses commute with the coordinatewise bijection, so $\pi :P^{\pi }\to P^{\pi }$ preserves and reflects the order, with inverse ${\pi }^{-1}$.

First verify the set-likeness needed for the completion. If a ground-definable antichain were a proper class, the ground global well-order would recursively enumerate a proper-class sub-antichain. Thin to a fixed finite support size and section-length pattern, and let $i$ be the least support position unbounded in the resulting class. All earlier positions are bounded by some $\beta$; thin again so the finite supports above $\beta$ are pairwise disjoint and, since $P_{{\beta }^{+}}$ is a set, so all bounded restrictions agree. F2 then amalgamates any two selected conditions, a contradiction. Hence every ground-definable antichain is a set. A dense-domain order automorphism now induces an automorphism of the regular-open completion: send a regular open class to the regularization of the image of its intersection with $P^{\pi }$. Density makes this independent of representatives, and the inverse construction uses ${\pi }^{-1}$. F3 then gives the total rank-recursive action on names.

Every hereditarily symmetric name is a set name, so its transitive closure uses a set of finite coordinate supports and is bounded by a regular $\theta$. The same finite support $e$ witnesses symmetry after restriction to $P_{\theta }$, and evaluation uses only $G_{\theta }$, giving $N_G\subseteq {\bigcup }_{\theta }{N}_{G_{\theta }}$. Conversely, extend a $P_{\theta }$-name recursively to a $P_3$-name by viewing each stage condition in the complete forcing and retaining its finite support. The action agrees on that complete subforcing, so hereditary symmetry and value are unchanged; hence every $N_{G_{\theta }}$ lies in $N_G$. This proves both inclusions.