Dense forcing name translations preserve forcing

We first record a refinement calculation. If $q\le e(p_1),\dots ,e(p_n)$, choose $a$ with $e(a)\le q$. Compatibility reflection makes $a$ compatible with $p_1$, so refine $a$ below $p_1$. Its image is still below $q$ and hence compatible with $e(p_2)$; reflect compatibility again and continue. After finitely many steps obtain $r\le p_1,\dots ,p_n$ with $e(r)\le q$. For $n=0$ this is image density. Consequently the image of $\{r:r\le p\}$ is dense below $e(p)$. Also, if $e(a)\le e(b)$, every extension of $a$ is compatible with $b$, and conditions below $b$ are dense below $a$. Only finitely many existential instantiations are involved.

Apply F5 on the subname relation F4. The rule for $T$ takes a set image of the entries. The rule for $R$ takes a subset of the product of the entry set with $P$, then its set image. Both outputs are names by F4. These operations are definable and use no chosen inverse of $e$. Their recursion exists internally in any ground ZF model. For a transitive ground containing the data, induction on subnames identifies its output with the external translation: each entry and each tested coefficient ranges over the same ground sets, and the already translated subnames agree. The displayed definition shows that $TR(\tau )$ has entries $⟨TR(v),e(p)⟩$ for every entry $⟨v,q⟩\in \tau$ and every $p$ with $e(p)\le q$; this is a coefficient refinement, not literal equality with $\tau$.

Here are the equality rules needed below, proved directly from F1. Induction on name rank gives $p⊩a=a$ for all $p$: for an entry of $a$ and a tested common extension use that same entry and the induction hypothesis for its subname. Symmetry is built into the two subset tests. For transitivity induct on the decreasing lexicographic order of the three name ranks sorted in nonincreasing order. Suppose $p⊩a=b$ and $p⊩b=c$. For an entry $⟨u,s⟩\in a$ and $q\le p,s$, the first equality refines $q$ to $r$ below the coefficient of an entry $⟨v,t⟩\in b$, forcing $u=v$. The second refines $r$ to $w$ below the coefficient of $⟨z,h⟩\in c$, forcing $v=z$. Persistence and transitivity at the smaller triple $(u,v,z)$ give $w⊩u=z$. This verifies $a\subseteq c$; exchanging $a,c$ and using symmetry verifies $c\subseteq a$. The triple strictly decreases because all three entries are proper subnames.

If $p⊩a=b$ and $p⊩a\in c$, any extension of $p$ refines to an entry of $c$ with $a$ forced equal to its subname. Symmetry and transitivity from the preceding equality rules replace $a$ by $b$, proving $p⊩b\in c$. If $p⊩c=d$ and $p⊩a\in c$, first obtain an entry $⟨u,s⟩\in c$ with $a=u$ forced and coefficient above the current condition. Apply the $c\subseteq d$ test to obtain an entry of $d$ with subname forced equal to $u$; transitivity gives the required membership witness in $d$. Density closure proves both membership substitution assertions at $p$. Transitivity itself gives substitution in equality, in either argument.

We prove $p{⊩}_{P}a=b$ iff $e(p){⊩}_{Q}T(a)=T(b)$ by induction on the sorted pair of source name ranks. For the forward direction, an entry $⟨T(u),e(s)⟩$ of $T(a)$ comes from an entry $⟨u,s⟩$ of $a$. Given $q\le e(p),e(s)$, the refinement calculation supplies $r\le p,s$ with $e(r)\le q$. The source subset test refines $r$ to a coefficient of an entry $⟨v,t⟩\in b$ and forces $u=v$. The smaller-pair induction transports this equality, giving the target witness. Apply this reasoning to both subset directions. For the reverse direction, given $⟨u,s⟩\in a$ and $r\le p,s$, apply the target test below $e(r)$ to find $q\le e(r),e(t)$ and an entry $⟨v,t⟩\in b$ with $q{⊩}_{Q}T(u)=T(v)$. Refine to $w\le r,t$ with $e(w)\le q$; persistence and the smaller-pair induction give $w{⊩}_{P}u=v$. Again apply this to both subset directions. Duplicate image entries require only one witnessing source entry at a time.

For each $Q$-name $a$, every $Q$-condition forces $TR(a)=a$, by induction on its name rank. For an entry $⟨TR(u),e(s)⟩$ of $TR(a)$ coming from $⟨u,t⟩\in a$ with $e(s)\le t$, every tested condition below $e(s)$ is already below $t$ and forces $TR(u)=u$ by induction. This verifies $TR(a)\subseteq a$. For the other direction, given $⟨u,t⟩\in a$ and a condition $q$ below its coefficient and the condition being tested, image density gives $e(s)\le q$. The entry $⟨TR(u),e(s)⟩$ exists in $TR(a)$ and induction and symmetry give the required equality. These are exactly the two subset clauses. In particular, this proves forced equality for the coefficient closure, rather than assuming that closure leaves a name literally unchanged.

Let $G$ be $P$-generic and put $H=\{q:\mathrm{\exists }p\in Ge(p)\le q\}$. It is nonempty and upward closed, and directedness follows by taking a common refinement in $G$. For a ground dense set $D\subseteq Q$, the set $E=\{p:e(p)\in D\}$ need not be dense if $D$ is not open. Instead use $E^{\mathrm{\prime }}=\{p:\mathrm{\exists }d\in De(p)\le d\}$: from $p$, find $d\le e(p)$ in $D$, and then $r\le p$ with $e(r)\le d$. Thus $E^{\mathrm{\prime }}$ is dense; meeting it puts such a $d$ in $H$. Hence $H$ is generic. Certainly $G\subseteq e^{-1}H$. If $e(p)\in H$, take $s\in G$ with $e(s)\le e(p)$. Conditions below $p$ are dense below $s$ by the refinement calculation, so F3 and genericity yield $r\in G$ below $p$, and $p\in G$. This proves $e^{-1}H=G$.

Conversely let $H$ be $Q$-generic and put $G=e^{-1}H$. For a ground dense $D\subseteq P$, the set $\{q:\mathrm{\exists }d\in Dq\le e(d)\}$ is dense in $Q$: first refine to an image, then to the image of a member of $D$. Meeting it gives a member of $D$ in $G$, so $G$ meets every ground dense set and is nonempty. Order preservation gives upward closure. For $p,s\in G$, the set $D_{p,s}=\{r:r\perp p\text{ or }r\perp s\text{ or }r\le p,s\}$ is dense: refine successively toward $p$ and $s$ whenever compatible, and otherwise stop at the corresponding incompatible alternative. A point in $G\cap D_{p,s}$ cannot be incompatible with either, by compatibility preservation and directedness of $H$; it is the needed common refinement in $G$. Finally, for $q\in H$, the image is dense below $q$, and F3 gives $e(p)\in H$ below $q$ for some $p$. Thus $q$ belongs to the upward closure of $e[G]$. The opposite inclusion is upward closure of $H$.

Equality substitution extends to each fixed formula by induction on its construction. Conjunction uses each conjunct. For negation, suppose $p$ forces the parameter equalities and $\mathrm{\neg }\psi (\vec{a})$; an extension forcing $\psi (\vec{b})$ would, by persistence and the induction hypothesis, force $\psi (\vec{a})$, contrary to F2. Reverse the equalities for the converse. For an existential, at every extension obtain its dense name witness, keep that witness fixed, and change the parameters by the induction hypothesis; the same dense-witness clause proves the substituted existential. Atomic cases are the equality and membership substitution calculations. This proves substitution at any condition forcing the parameter equalities, without appealing to generic semantics.

Membership is transported in both directions as well. If $p{⊩}_{P}a\in b$, first refine any $q\le e(p)$ to $e(r)$ with $r\le p$, then use the source membership witness and the equality equivalence. Conversely, for $r\le p$ apply the target membership clause below $e(r)$, obtaining an entry $⟨v,t⟩\in b$ and $q\le e(r),e(t)$ forcing $T(a)=T(v)$. Refine to $w\le r,t$ with $e(w)\le q$ and reflect equality. This is the source membership test. Empty right names fail both membership tests.

Apply the Q-name round trip to $a=T(\sigma )$. Every $e(p)$ forces $T(R(T(\sigma )))=T(\sigma )$, so equality reflection proves that every $p$ forces $RT(\sigma )=\sigma$. Thus both translations are inverse modulo forced equality. The empty name translates to the empty name.

Induction on source name rank and the equality $p\in G⟺e(p)\in H$ give $T(\sigma {)}^H={\sigma }^G$ directly from the valuation clause. For $R$, an active coefficient $p\in G$ coming from $⟨v,q⟩\in \tau$ has $e(p)\le q$, hence $q\in H$. Conversely if $q\in H$, the inverse correspondence supplies $p\in G$ with $e(p)\le q$, so the inverse entry is active. Induction identifies their subname valuations and yields $R(\tau {)}^G={\tau }^H$. These two equalities imply both inclusions of the extensions.

Induct now on each fixed formula for full forcing equivalence. Atomic cases have been proved. Conjunction is immediate from its two clauses. If $p{⊩}_P\mathrm{\neg }\psi (\vec{\sigma })$ and some $q\le e(p)$ forced $\psi (T\vec{\sigma })$, refine to $r\le p$ with $e(r)\le q$ and apply persistence and the formula induction hypothesis to contradict source negation. Conversely any source extension forcing $\psi$ maps to a target extension forcing its translation, which is impossible if $e(p)$ forces its negation.

For the existential forward direction, below any $q\le e(p)$ first find $r\le p$ with $e(r)\le q$, then refine $r$ to a source witness $\sigma$ for the matrix. The induction hypothesis transports that witness to $T(\sigma )$. For the converse, at $r\le p$ the target existential supplies $q\le e(r)$ and a $Q$-name $\tau$ forcing its matrix with parameters $T\vec{\sigma }$. Refine to $s\le r$ with $e(s)\le q$. Every condition forces $TR(\tau )=\tau$, so formula substitution changes this witness to $T(R(\tau ))$. The induction hypothesis for the matrix reflects it to the source witness $R(\tau )$ at $s$. This proves the dense-witness test at $p$, and completes the induction. All names quantified over here belong to the given ground when the proof is performed internally.

All constructions above are set images, Separation, definable recursion and finite refinements. The atomic inductions use ranks of set names; the formula induction is external for each fixed finite formula, interpreted inside the ground. Thus no generics were needed for the forcing equivalence, no external completeness or countability was used, and no choice function was selected. Empty preorders are excluded; singleton preorders and noninjective maps satisfy the same calculations. Boolean zero, if a target is presented as a Boolean algebra, must be removed so that its nonzero part is a forcing preorder. [step 1.2, step 5.1, step 3.4] QED.