Dense-equivalent forcing presentations

The conditions a and a' have the same extension set A, hence are mutually ${\le }^{\ast }$-equivalent. Neither is equivalent to b, which is incompatible with both. Also 1 is not ${\le }^{\ast }$-below either atom: the other atom witnesses failure. Thus the quotient classes are exactly $\{1\},A,B$, with the two atom classes below the top.

Downward open subsets of P are exactly $\mathrm{\varnothing },A,B,A\cup B,P$. The closure of A is $A\cup \{1\}$, since a condition is in its closure exactly when its extension cone meets A; its interior is A because the cone below 1 also includes b. Likewise B regularizes to B. The set $A\cup B$ meets every cone, so its closure and regularization are P. Therefore the regular opens are exactly the four sets displayed. Their meets are intersections, their complements exchange A and B and exchange empty and P, and $A\vee B=P$. The nonzero order is the same three-point order as the quotient; Boolean zero is omitted.

Every P-generic meets the ground dense set $A\cup B$. If it meets A, upward closure and the mutual inequalities force it to be $G_A=\{1,a,a^{\mathrm{\prime }}\}$; if it meets B it is $G_B=\{1,b\}$. It cannot meet both by directedness. Conversely these two filters meet every dense set: such a set must contain some member of A and must contain b, by testing a and b themselves. Hence these are exactly the generics. The quotient generics are $\{1,A\},\{1,B\}$ and the Boolean generics are $\{P,A\},\{P,B\}$, by the identical atom argument. They exist through every condition. All six filters are finite sets in M.

Let $e:P\to \mathrm{RO}(P{)}^{+}$ send 1 to P, a and a' to A, and b to B. Recursively replace each coefficient s of a name by e(s), translating its subnames at the same time. For the listed corresponding generic pair $(G_A,H_A)$ or $(G_B,H_B)$, s belongs to the first filter exactly when e(s) belongs to the second. Induction on name rank in F4 therefore proves equality of valuations. For the quotient use the identical construction with coefficients replaced by their classes. Conversely replace coefficients A,B and the top by the fixed representatives a,b and 1 respectively, recursively on names; the same coefficient test proves agreement in the reverse direction. These are three explicitly fixed representatives, not a choice from an arbitrary family of classes.

For each of these finite ground filters, valuation of a name in M can be performed internally in M and agrees with the external recursion by induction on subnames. Thus all name values lie in M. F5 gives the reverse inclusion, so each generic extension is M itself.

By step 2.1 generics exist through every condition, so F3 applies. The generic lists correspond bijectively and, by step 3.1, translated parameters have equal values in the identical models of step 3.2. Therefore the truth test in all corresponding generics gives equal forced formulas at corresponding conditions. For instance the top has two generic tests, whereas either atom has just its one test; duplicate a and a' give the same test. This completes the quotient, Boolean and name computations without AC.