The Partition Principle does not imply Choice

Proof. For an ideal U, choose elements whose heights approach \sup\rho[U], and replace their successive initial segments by their finite joins. This gives a nondecreasing sequence (n_i) in U with heights approaching the same supremum. If d\in U divides none of the n_i, then

for every i, contradicting convergence to the supremum. Prepending 1 makes n_0=1. The proof applies in the stated extension as well; its choices are made in that \ZFC universe.□

Proof. Normal forms. Let S be the direct limit of the sets M under the maps x\mapsto xd_i. Write [x,i] for the image of x at stage i. Equality in this direct limit means equality at a finite common stage. The transition maps need not be injective: no right cancellation has been assumed. Nevertheless the left M-action on S is injective for each multiplier. Indeed, equality after multiplying two letters by an old u becomes uX=uY at a common stage, where left cancellation gives X=Y.

There are well-defined equivariant maps

The identity d_ic_{i+1}=c_i proves well-definedness. Before imposing the second relation in Equation (2.5), the normal forms are strings

including j=0. The letter [x,i] represents xp_i. Old factors between new generators are absorbed into the following letter, and the transition relations are precisely equality in S. Multiplication concatenates strings, using the left action to absorb the terminal old factor of the first string.

The remaining reductions are

where t is a letter of S or a terminal old element. The quotient t is unique because the left b-action is injective. Each reduction removes one new letter. The only overlapping reductions occur in s\,(bt)\,(bu), with the final factor possibly terminal. Reducing in either order gives the same result by

Disjoint reductions commute by associativity of the action. By Newman’s lemma [13] (see [5, Lemma 5.13]), these local diamonds and termination give unique irreducibles: besides the old elements, they are strings whose first letter is arbitrary and whose later letters and terminal factor are not left-divisible by b.

Old left multipliers act injectively on these forms. Left multiplication by a letter s either prepends s, when the input is not a b-multiple, or sends bZ to h(s)Z. Both cases are injective. Their ranges are disjoint, because

To see this, s\in xS implies x\sqsubseteq k(s), whereas k(s)e\not\sqsubseteq k(s) by conicality and left cancellation. Thus every left multiplication is injective. A new word can become old only by consuming its first letter, at which point it is a multiple of h(s)\ne1. It cannot equal 1, proving conicality.

Old cones and the first-letter blocks. For s\in S, let B_s consist of all irreducibles beginning with s. For old x the normal forms give

At a common stage in the direct limit, xS\cap yS is (x\vee y)S if the old join exists, and is empty if the old cones are disjoint. Thus old comparisons, their right factors, joins and nonjoins are unchanged. Notice that this conclusion has not used a join theorem for arbitrary new words.

Exits and gates. Fix an irreducible w=sY. Right multiplication either leaves its first letter intact or eventually consumes that letter. We prove the following precise alternative: the set wM'\setminus B_s is empty, or it is one cone g(w)M' whose root g(w) is old. Thus the gate will describe every exit from the fixed-head block, not only the old multiples of w.

The first letter is consumed exactly when the suffix becomes a b-multiple, so first calculate YM'\cap bM'. If Y is old, Equation (2.9) gives the old join Y\vee b, or an empty intersection. If Y is new with head t, irreducibility gives t\notin bS. No member of B_t is then a b-multiple. By induction on the number of letters in the suffix, all possible exits of Y form the old-rooted cone g(Y)M', if there are any. Its intersection with bM' is calculated by the old join g(Y)\vee b.

In either case the suffix intersection is empty or is zM' for an old z=bu with old u. The factor u is old by conservation of old comparisons. In the nonempty case, multiplication by s and the reduction sbu=h(s)u give

This cone cannot return to B_s: every new head in it belongs to h(s)S, whereas s\notin h(s)S by Equation (2.8). This proves the exit alternative. Every old multiple of w lies outside B_s, so g(w) is in particular its least old multiple.

We record also the right factor c(w) with wc(w)=g(w). If Y is old, it is the old quotient of z by Y. If Y is new and Yc(Y)=g(Y), it is

All quotients in this recursion are old except the already constructed c(Y). This explicit calculation will ensure conservation of right factors when the same presentation is simulated over a larger base.

Append an old d to w. If the product leaves B_s, its first letter has been consumed; that reduction can occur only after all intervening letters have been consumed. The result is then entirely old. Since the gate cone is disjoint from B_s, the hypothesis g(w)\sqsubseteq wd implies just such an exit. This proves Equation (2.3).

All conditional joins. For two forms with the same head, cancel that head and intersect their suffix cones, using induction on the total number of new letters. For old x and new w\in B_s, either s\in xS, in which case x\sqsubseteq w, or every common multiple must leave B_s. The latter intersection is computed through g(w) and an old join. For w\in B_s and v\in B_t with s\ne t, an intersection inside B_s requires g(v) to divide a member of B_s. By Equation (2.9) it then divides all of B_s, so v\sqsubseteq w. The symmetric case is the same. Otherwise a common multiple must leave both blocks, and the intersection is computed by the old join of their gates. Missing gates or missing old joins give an empty intersection. This proves conditional joins in every case.

The prescribed divisor profile. For any letter s, the old divisors of every element of B_s form

This is an ideal: common-stage representatives and old joins prove join closure. For the head [1,0] of m=p_0, it is precisely \bigcup_i\downarrow_M n_i, and the gate is ae. The defining relation gives mb=ae. Since ae\not\sqsubseteq a, no member of B_{[1,0]} divides a; in particular m\not\sqsubseteq a.

Now let x be a new divisor of a. It is outside that block and has an old gate g(x)\sqsubseteq a. If x\sqsubseteq m, the comparison leaves its block, so g(x)\sqsubseteq m, and the old profile puts g(x) below some n_i. Conversely x\sqsubseteq n_i implies x\sqsubseteq m. If x\not\sqsubseteq m, its gate also fails to divide m. The possibility m\sqsubseteq x is excluded by x\sqsubseteq a. The gate calculation consequently gives x\vee m=g(x)\vee m=ae. The corresponding assertions for old x follow directly from its block membership. This proves Equation (2.6), including new divisors of a.□

Proof. Use P_s from Equation (2.12), and put A_s=\sup\rho[P_s]. We place the whole block B_s in a short height interval above its old divisors and below \rho(h(s)). Here h(s) is the gate of the bare letter s; the gate of a longer word in B_s, when present, is a multiple of h(s) and need not equal it. The interval must leave enough room for the costs of both the old divisors and the new words. More precisely, there are positive u_s,\delta_s with

Indeed, put p=\rho(k(s))-A_s\geq0 and q=\rho(h(s))-\rho(k(s))>0. For d\sqsubseteq k(s) missing P_s, every x\in P_s misses d, and the old margin yields \epsilon_d<\rho(k(s))-\rho(x). The supremum of these costs is at most p. The supremum for d\sqsubseteq h(s) not dividing k(s) is strictly below q. Thus the full supremum on the right of Equation (2.13) is strictly less than p+q=\rho(h(s))-A_s, also when p=0. This leaves the required positive room for u_s and \delta_s.

Define recursively on irreducibles

These choices give heights in (0,1) and costs in (0,1]. We verify all comparisons, including the suprema.

For two elements in one block B_s, a divisor of the upper element from outside that block also divides the lower one. An old divisor belongs to P_s; a new divisor with a different head must enter by its old gate, which then divides every member of B_s. Inside the block, cancellation removes s, and the margin follows by induction from the factor \delta_s in both height differences and cost bounds.

Suppose an old x lies strictly below sY. Then x\in P_s. A missed divisor outside B_s is old in P_s, or has an old gate there of at least its cost. For such an old divisor d missing x, the join x\vee d lies in P_s, and hence

Their supremum is at most A_s-\rho(x). Divisors inside B_s have cost at most \delta_s. Equation (2.13) makes \rho(sY)-\rho(x) strictly larger than both bounds.

Suppose sY lies strictly below an old y. Then h(s)\sqsubseteq y. Every divisor of y missing sY is old outside P_s, or has a gate there with at least its cost: a gate in P_s would put the divisor below all of B_s. Among these old costs, those for divisors of h(s) are bounded by Equation (2.13). If y\ne h(s), the remaining costs have supremum strictly below \rho(y)-\rho(h(s)) by the old margin. The total gap \rho(y)-\rho(sY) is the sum of two positive gaps and exceeds both cost suprema. This proves this comparison case.

Distinct comparable new blocks have an intervening old gate, so the preceding cases apply transitively. To justify this use, if x<z<y, any divisor of y missing x either divides z and misses x, or misses z; the sum of the two positive height gaps strictly dominates both relevant suprema.

Finally, for old x<y, any new divisor d of y missing x has an old gate g(d)\sqsubseteq y missing x, with \epsilon_d\leq\epsilon_{g(d)}. No new cost increases the old supremum, while every old divisor remains present. The supremum is therefore exactly unchanged. This also proves persistence of the margins at unions of a conservative tower of these extensions.□

Proof. Let D be the prescribed quotient of the copies, writing t_i x for the image of x in copy i. This quotient carries one layer of the required overlaps; strings of its elements will complete that layer to a monoid. It is a right M-set and each map x\mapsto t_i x is injective. On D use the order z\sqsubseteq w when zq=w for some q\in M; left cancellation and conicality inside a representing copy make this a partial order. Its right cones have conditional joins. Within one copy this is the old join. For elements represented in different copies, every common multiple must lie in their specified overlap, if there is one. In each copy join the element with the start of that overlap; transfer the two resulting elements into the overlap and join there. A missing join at any step means that the original cones are disjoint. This calculates exactly their intersection, because every common multiple must pass through both of those preliminary joins.

Adjoin generators l_i with the specified relations l_i a_{ij}=l_j a_{ji}. The normal forms are

including j=0. Each relation acts inside a new-generator/old-factor pair, exactly as in D; it changes neither the number of new letters nor the preceding old coefficient. This proves uniqueness of the forms. Multiplication acts by the leading old coefficient of the second word on the last D-letter of the first, and then appends the remaining letters. For a fixed z=t_i a, the map y\mapsto zy is injective by left cancellation in copy i. Together with old left cancellation, this proves cancellation for arbitrary products of forms. Letter count proves conicality and that no new word divides an old element.

Unlike the probe extension, this construction never consumes a new letter. Its cones are therefore read from the final letter rather than from the first-letter blocks used above. For a positive-length word, right multiplication fixes the prefix before its final letter, advances that letter within its D-cone, and possibly appends further letters. More explicitly, compare xz_1\cdots z_p and yt_1\cdots t_q with p,q>0. A common multiple requires x=y and equality of the letters before position \min(p,q). If p=q, their intersection is obtained by joining z_p and t_p in D, or is empty if that join is absent. If p<q, a common multiple exists exactly when z_p divides t_p in the right M-set D; then the first word divides the second and the second is their join. The case q<p is symmetric. An old x and a positive-length word with head y have a common multiple exactly when x\sqsubseteq y, in which case x divides that word. Two old words use their old join, because the heads of common multiples are precisely their old common multiples. These descriptions prove conditional joins and preserve old comparisons, quotients and nonjoins. The words l_i x have exactly the identifications in D, as required.

It remains to supply margins. If the number of copies is r, set

Each coordinate is nondecreasing along a comparison, and some coordinate increases strictly in a proper comparison. Choose positive costs with

For u<v in D, classify a divisor d of v missing u by a copy representing d. That copy also represents v. If it represents u, its old margin bounds the supremum of these costs strictly below its coordinate increase divided by r. Otherwise that increase is at least \rho(1), while each such cost is at most \rho(1)/(2r). There are only finitely many copies, so their strict bounds still give the required strict supremum bound for \rho_D(v)-\rho_D(u).

Choose \theta,\phi>0 with \theta+\phi<1, and recursively set

For comparable new words of equal length only their last letters vary; missed divisors of that length are handled by the scaled D-margin, and all shorter divisors divide both words. For a word w compared with wz, every missed divisor has the new length and prefix w, so its cost is at most (1-\rho(w))\theta/2, strictly less than the height increase. An arbitrary comparison factors through these comparisons, and, when the lower word is old, an old comparison of leading coefficients. Transitivity of the margin, proved in Lemma 2.4, finishes the check. Old cost suprema are unchanged because there are no new old divisors.□

Proof. For the last assertion, the only nontrivial transitivity check passes through three copies. In the middle copy, intersect the two prescribed overlap starts. If their old cones are disjoint, conservativity keeps them disjoint. Otherwise their old join and its right quotients are unchanged. Every later common multiple is a multiple of that join. The two endpoint identifications at the join already agree in a valid prescription over B, so right multiplication gives agreement at all later common multiples. This proves validity over M. Conversely, restrict a valid prescription to B. Comparisons between its old parameters have their quotients in B, so no identification or transitivity witness between elements of B requires leaving B. The restriction has exactly the indicated pair relations and is valid.

For probes, equality of two letters in the smaller direct limit is preserved and reflected because it is an equality at a common finite stage. If an old b\in B divides a smaller letter [x,i] in the larger direct limit, there is a common stage at which

Both endpoints of this comparison belong to B, so its right factor y belongs to B. Thus divisibility of a smaller letter by an old smaller multiplier, including its quotient, is unchanged. The same irreducible words therefore embed. The gate recursion uses only the previous gates and old joins and quotients, so it has the same outcome, including the absence of a gate. The join calculations in Lemma 2.3 now preserve and reflect joins and nonjoins.

For clarity, preservation of right quotients between new forms follows by a separate division argument. If both forms are old, use the base hypothesis. If the divisor is old and the dividend new, divide its first direct-limit letter by the preceding common-stage calculation, and retain its suffix. If both forms have the same new head, cancel that head and recurse on their suffixes. In the remaining cases the new divisor must leave its first-letter block. Factor through its gate, using the quotient in Equation (2.11), and divide that old gate into the dividend by the first two cases. Every factor obtained lies in the smaller extension. Left cancellation makes their product the unique required quotient.

For mergers, representation in an overlap and intersections of cones in D were calculated solely using old joins and their right quotients. These calculations are consequently unchanged. The normal forms in Equation (2.15) then preserve comparisons, their right factors, joins and nonjoins. This proves conservative simulation for both operations.□

Proof. A merger introduces no new divisor of the old a. At a probe extension, a new x\sqsubseteq a has an old gate g(x)\sqsubseteq a. If x also divides the old probe, its gate lies below that probe and hence below some original path element; then x does too. If x does not divide the old probe, its gate does not either. The old probe cannot divide x, because it does not divide a. The join calculation through the gate therefore gives ae in this case. This proves both alternatives at a successor step. At a limit every tested element has already appeared, and all comparisons and joins have been preserved. Conservativity directly preserves joins between existing probes.□

Proof of Theorem 2.2. Saturating the geometric requirements. Start with the free monoid on e. For n<\omega, for example, put

These satisfy Equation (2.1). Perform \omega_1 rounds. At the start of a round schedule every available probe datum (a,b,(n_i)) with the fixed e, and every available finite valid merger. For each probe datum schedule \mu successive insertions. Execute the resulting wellordered list with the two lemmas, and take unions at limits. Lemma 2.6 keeps every scheduled merger valid until it is executed.

A monoid of size at most \mu has at most \mu^{\aleph_0}=\mu countable paths and at most \mu finite prescriptions. A probe extension uses a quotient of M\times\omega and finite strings; a merger uses finitely many copies and finite strings. Thus every operation preserves size at most \mu, and each round has at most \mu steps. The union of \omega_1 such rounds still has size at most \mu. The margin lemmas ensure that old values are never changed and that old missed-cost suprema never increase, so the final union T has Equation (2.1) as well as all the algebraic properties.

Given an ideal in \downarrow_T a, use Lemma 2.1 to obtain a cofinal path starting at 1. Its elements, a,b, and all its transition and terminal quotients occur before one round: the set is countable and the rounds have cofinality \omega_1. Alternatively, quotient conservativity already puts every quotient into any stage containing its endpoints. The corresponding requirement is scheduled. Its final lower closure is the given ideal, and Lemma 2.7 therefore gives Equation (2.2) for the \mu insertions. For any earlier and later insertion with the same datum, the earlier probe is old but is not a divisor of a, so it is not an old divisor of the new probe. Joining through the new probe’s gate gives ae. This join persists in the final union, proving independence.

Every final finite overlap prescription has its parameters in one stage. Its validity reflects to that stage by Lemma 2.6, and the schedule realizes it later. The realization remains exact by conservation of comparisons and quotients: equality l_i x=l_j y in a later stage must still factor through the preserved join of the two roots, with its prescribed quotients. Thus later right factors add exactly the stipulated identifications and no others. Finally use a=1,b=e and U=\{1\}. Its probes have no old divisor e, so there are \mu elements of T\setminus eT. This proves both cardinality assertions.

Extracting a countable initial base. It remains to prove the local construction property for this same T. We first select countably many operations containing any prescribed countable set of elements, and then perform all omitted operations over their union. The resulting tower must retain the gate rule: this is what will let a later descent replace a position by one born at an earlier stage. Regard the entire schedule as a continuous tower (M_\alpha)_{\alpha\leq\lambda} of individual operations. Record each parameter by a finite word in previous generators. Every element of the presented monoid has such a word, and each equality has a finite derivation from the relations. This does not assert that a whole countable path has finite support.

Choose a sufficiently large regular \Theta and a countable elementary submodel N of H_\Theta containing the tower, its presentations and an enumeration of the prescribed countable subset of T. Countable objects in N, in particular the parameter paths of operations indexed in N, have all their entries in N. First perform just the operations whose indices belong to N, in their original order. Let S_\alpha denote this subconstruction using selected indices below the cut \alpha.

At cuts \alpha\in N we have

with a conservative inclusion in M_\alpha. Here is the induction justifying the assertion. Old comparisons, their quotients and joins in an elementary intersection are reflected by elementarity; a nonjoin remains a nonjoin in the larger monoid. Before a selected operation, every parameter is already present: its finite term code belongs to N, and all entries of a countable path in N belong to N. Conservative simulation makes that operation legal in the subconstruction and embeds its result. Conversely, every element of M_\alpha\cap N has by elementarity a finite term code in N; all of its finitely many generator indices belong to N and precede \alpha. It is therefore produced by the selected subconstruction. This proves Equation (2.17) and the successor step of the induction. At a cut \alpha\notin N, fix the finitely many words in a comparison or join test. If they use selected operation indices, let \gamma be the greatest such index and put \beta=\gamma+1; if there are no such indices, put \beta=0. Then \beta\in N, \beta<\alpha, and all the words belong to S_\beta=M_\beta\cap N. The original inclusion M_\beta\subseteq M_\alpha is conservative. Any right quotient or conditional join required by the test therefore already lies in M_\beta and, by elementarity, in N, hence in S_\beta. This also preserves nonjoins and proves conservation at \alpha. Unions introduce no additional finite relation. This completes the induction.

The resulting selected submonoid T_0 is countable: the initial monoid is countable, there are countably many selected steps, and each operation over a countable base adds only countably many elements. It contains the prescribed sequence by its finite term codes. The set of selected indices need not be an initial segment; the argument has used Equation (2.17) only at cuts belonging to N.

Reinserting the omitted operations. Append now the omitted steps in their original order. Before an omitted step \alpha, the current presentation is the union of the original relations below \alpha and all selected relations. It has an alternative realization: start with M_\alpha, and then perform the selected steps at indices at least \alpha in their order. Indeed S_\alpha\subseteq M_\alpha is conservative, and repeatedly simulating the selected subconstruction makes all these operations legal. Each extends its whole base conservatively, so this alternative realization conservatively contains M_\alpha. It has precisely the same generators and relations as the current reordered presentation. Consequently the original operation at \alpha is legal over the current base, by conservative simulation again. Induction validates every appended step. At limits the presentations are their unions; at the end their union is exactly the original presentation of T.

Each step of this reordered tower is one of the two operations. The merger has no new old divisors, and the probe extension has its least-old-multiple rule, including Equation (2.3). Conservation allows those comparisons to be tested in T. This proves the last assertion and completes the theorem.□

Proof. If m is not in that submonoid, take its first birth step in the reordered tower. It has the old multiple n_N, so this is a probe step and its gate satisfies g(m)\sqsubseteq n_N. Choose an admissible replacement with n_N\sqsubseteq md. The quotient d belongs to the initial submonoid and is therefore old at this step. Conservation and Equation (2.3) imply that md belongs to the strictly earlier base. Repeat if necessary. Each repetition strictly lowers the birth ordinal, so the process terminates after finitely many repetitions. The resulting position lies in the countable initial submonoid.□

Proof. A descending countable sequence has its union as a lower bound. Deciding the entries of a name for a sequence in a ground set and then taking such a lower bound shows that no new countable sequence in that set is added. This also preserves \omega_1^V.

We recall the relevant delta-system argument to identify the exact cardinal bound. A family of \mu countable sets has a delta-system subfamily of size \mu. Code its union into \mu, and write its members as S_\alpha\subseteq\mu, for \alpha<\mu. There is a club of \delta<\mu such that S_\alpha\subseteq\delta whenever \alpha<\delta. On the stationary part of this club of cofinality \omega_1, each S_\alpha\cap\alpha is bounded in \alpha. The pressing-down lemma makes a bound constant, say \gamma<\mu, on a stationary subset. There are at most |\gamma|^{\aleph_0}+\aleph_0<\mu possible countable subsets of \gamma, by Equation (3.1) and its preceding bound. Regularity of \mu therefore makes S_\alpha\cap\alpha one fixed set on a stationary subset. For \alpha<\beta in that subset, S_\alpha\subseteq\beta, so their intersection is this fixed root.

Apply this to the domains of \mu Cohen conditions. There are at most 2^{\aleph_0}=\mathfrak c<\mu assignments on the countable root. Thinning once more gives two, indeed \mu, conditions agreeing on the root. They are compatible, which proves the chain condition. The usual antichain bound then preserves all cardinals at least \mu: the possible values at any one coordinate of a name for an ordinal-valued function are covered by fewer than \mu ground ordinals, and regularity handles the case of \mu itself. Countable closure and the chain condition together preserve all cardinals when \mu=\aleph_2. In a general ground we assert no preservation of cardinals strictly between \kappa and \mu.

Finally, any sequence of ground elements has its values in some ground rank segment: their ranks have an ordinal bound, and forcing preserves ordinals. Thus the assertion about sequences in ground sets covers all countable sequences of ground elements.□

Proof. The probes from Theorem 2.2 for a=1,b=e,U=\{1\} give \mu distinct elements m with me=e. None belongs to eT: if m=ex, left cancellation would give xe=1, contrary to conicality and e\neq1. Hence |T\setminus eT|=\mu. Define r(ex)=p(x), using left cancellation, and fill the complement injectively in I\setminus D_p, including J\setminus D_p. Both the size of that complement in T and the strict inequality \mu<|I| give the first assertion.

For the second assertion, identify the copies of T exactly where their labels in I coincide. The hypothesis says that these identifications have the form required by the finite-merger property; their transitivity and absence of collapse within a copy follow from actual equality of labels. Let l_i\in T realize this merger. On \bigcup_i l_iT, assign l_ix the value s_i(x). The exact-overlap property makes this well defined and injective. Extend it injectively to the rest of T. The resulting r satisfies r_{l_i}=s_i.

For the last assertion, the prescribed domain and range each have size at most \mu. Their complements in I both have cardinality \mu^+, so a bijection between the complements extends the partial bijection to a permutation. Fresh images can first be chosen off the excluded set, whose size is still at most \mu, and then the same argument applies. All these choices occur in V.□

Proof. Apply the set-forcing symmetric-extension theorem [11, Section 2.1, p. 4] to \mathbb Q, G, and the normal subgroup filter verified above. Its internal formulation concerns all hereditarily symmetric names and yields the full Separation and Replacement schemata, as well as Foundation; this formulation is recalled in Lemma 8.2. It requires no countable-completeness assumption on the filter. External transitivity of V permits the usual recursive name evaluation and gives the displayed literal inclusions. For an arbitrary countable ground, Lemma 8.3 instead gives truth in the membership-closed symmetric quotient; it makes no assertion of external well-foundedness.□

Proof. If the first assertion fails, there are s_0,s_1\leq p forcing contrary answers in V[F]. Choose d_0,d_1\in F witnessing those answers in the factorized forcing relation. Their restrictions to D_p\times\kappa are compatible. By Lemma 3.2, choose \pi\in\Fix(D_p) so that, outside D_p, the coordinates of s_1,d_1 move away from those of s_0,d_0. The diagrams s_0,\pi s_1 meet exactly in their common subdiagram p, so have a common extension. The conditions d_0,\pi d_1 agree on the root and have disjoint supports off it, so are compatible. All parameter names are fixed by \pi. Equation (3.2) now gives two contrary assertions forced by compatible product conditions, a contradiction. This argument does not assert that \pi d_1 belongs to F.

For the second assertion, put \delta=d\restriction D_s. If \delta does not force the indicated factorized assertion, there is c\leq\delta forcing its negation. Choose \pi\in\Fix(D_s) moving \supp_I(d)\setminus D_s off \supp_I(c)\setminus D_s. The condition \pi d is compatible with c. It forces the original factorized assertion, by product symmetry, because s and all its parameter names are fixed. This contradicts the assertion forced by c.□

Proof. Take d\in F witnessing the equality forced at v. Both parameter supports lie in D_v, so Lemma 3.4 allows us to replace d by d\restriction D_v. Set \delta=d\restriction D_{s_0}. We will combine the translates of \sigma_0 into one D_p-supported name. A translate contributes its value only when the generic contains the corresponding translate of (\delta,s_0); the value of the new name will be the union of these contributing values. Thus the main task is to prove that any two contributing copies agree. For this coherence argument, allow both factors of the product generic to vary. We will return to the fixed F after constructing the name.

For every \pi\in\Fix(D_p), call the copy \pi\sigma_0 active when its trigger (\pi\delta,\pi s_0) belongs to the product generic. We first prove that any two active copies have equal values.

Consider two copies whose diagrams \bar s,\bar s' have intersection exactly D_p. If they can be unequal while active, some product condition (c,t) extends both triggers and forces the inequality. Place a copy u of s_1 over p, with the rest of its range fresh relative to D_t\cup\supp_I(c). Extend the respective placements of (s_0,s_1) onto (\bar s,u) and (\bar s',u) to placements of v, producing diagrams v',v''. Use the same placement on all of D_{s_1} in both cases. Choose all remaining coordinates freshly, so that the ranges have the intersections shown in Figure 2:

Every intersection in this display is its indicated common subdiagram. The required partial maps agree on the root, and their domain and range sizes are at most \mu; Lemma 3.2 therefore supplies the ground permutations realizing these placements.

The two placed copies of d agree on D_u. They agree with c on D_{\bar s} and D_{\bar s'}, respectively, because c extends the two placed copies of \delta. On the remaining coordinates freshness gives compatibility. Thus the Cohen conditions have a common extension. The three diagrams v',v'',t also have a common extension by Equation (3.3) and finite amalgamation. The two transported \sigma_1 names are literally equal, since the placements agree on the entire D_{s_1}. The equalities transported from (d,v) therefore contradict the inequality forced by (c,t).

For two active copies with arbitrary overlap, start again with any proposed inequality-forcing common extension (c,t). Place a third copy of s_0 over p, independent of t off the root, and place its Cohen trigger compatibly with c. It has a common product extension with (c,t). The independent case just proved applies between this third copy and each of the original ones, contradicting the inequality. This proves coherence of all active copies, below every possible inequality witness.

Define a mixture using all joint strengthenings:

This is a set name. Left multiplication in \Fix(D_p) permutes its entries, so it is supported by D_p. Its member names are translates of member names of \sigma_0 and hence are \HS. In any product generic its value is the union of the values of the active copies. Both inclusions in this description follow from directedness of the generic: all common strengthenings, rather than a selected one, occur in Equation (3.4). When the original trigger is active, coherence makes this union exactly the value of \sigma_0. Return now to the fixed F. Since \delta\in F, the original trigger is active in every product generic with this Cohen factor and with s_0 in its diagram filter. It follows that s_0\forces_{\mathbb P}\sigma[F]=\sigma_0[F]. The equality with \sigma_1[F] holds below v. Its parameters are supported by D_{s_1}, so Lemma 3.4 makes it hold already below s_1.

No step imposed a rank bound. For the subset assertion, replace the mixture by its intersection with A, using the normalization in the next paragraph.□

Proof. Let \sigma be a ground \HS name, and let p have D_p as a support for \sigma. Form the graph name

where \operatorname{op} denotes the canonical ordered-pair name. This name is invariant, and all its member names are \HS.

Its value is a partial function on A. Indeed, suppose two contributing pairs have equal first coordinates. Label distinctness gives \pi(p(1))=\rho(p(1)). There is a common extension r\in H of \pi p,\rho p; write \pi p=r_n and \rho p=r_m. The equality of centers and injectivity of r give n=m. Consequently \pi p=\rho p pointwise, so \rho^{-1}\pi\in\Fix(D_p). It fixes \sigma, and hence \pi\sigma=\rho\sigma literally. The two values therefore agree. This argument concerns names under compatible diagram conditions, not an action on one fixed symmetric model.

The orbit construction gives invariant partial functions. We now form a set-indexed family of them whose ranges cover X. Choose an \HS name \tau for X. The set M of member names appearing in \tau is a ground set of \HS names. In V, enumerate by an ordinal \eta the set

Every member name has a support of size at most \mu, and Lemma 3.2 provides supporting diagrams. We include all such diagrams, because one chosen diagram need not belong to the generic filter. The corresponding sequence of graph names \dot h_{\sigma,p} is a ground sequence of invariant \HS names. Its canonical sequence name is itself invariant and \HS, so its interpretation \langle h_i:i<\eta\rangle belongs to W.

These partial functions cover X. For x\in X, an active member name \sigma of \tau has value x. The set of diagrams whose ranges contain a fixed support of \sigma is ground dense, by Lemma 3.2. Thus some such p belongs to H. The identity entry of \dot h_{\sigma,p} maps A_{p(1)} to x.

All remaining definitions take place in W. For nonempty X, fix one x_0\in X, and define

Separation and Replacement form this function on A\times\eta, and coverage makes it surjective. The one default element uses only nonemptiness of X. The enumeration above is over M\times\mathbb P, a set depending on the particular name \tau; no restriction to names below a fixed rank was made.□

Proof. We first treat a family \langle X_\xi:\xi<\eta\rangle of nonempty subsets of A. Start below a product condition (d_0,p) forcing this assertion for an \HS family name. By extending the diagram, arrange that D_p contains its support and \supp_I(d_0). The assertions that a given graph is a function and has nonempty subset values are absolute between W and the full extension. Consequently this use of ordinary forcing follows equally from a symmetric-forcing hypothesis. Names for the individual X_\xi can be obtained by the membership forcing relation from the family and \check\xi; they retain support D_p. Choose once and for all q with q_e=p. This same q will work for every family index. Witnesses already available on p need no move; for witnesses on proper extensions of p, the probes place independent copies inside q and Cohen genericity activates one of them.

Fix F containing d_0, and fix \xi<\eta. In V[F], some t\leq p and j\in I satisfy

This follows by deciding a witness in the ground index set I for membership in A. Extend t to include j in its range, and write p=t_b. Choose d\in F witnessing the displayed forcing assertion, and restrict it to D_t by Lemma 3.4. If b=1, then t=p, so q already forces a witness whose index belongs to D_q.

Suppose b\neq1. The probes of Theorem 2.2, with a=1,U=\{1\}, give \mu elements m satisfying mb=e and mT\cap m'T=eT for distinct probes. Thus

Each q_m is a copy of t over p. Choose in V a permutation \pi_m\in\Fix(D_p) taking t to q_m. The conditions \pi_m d all restrict on D_p to d_*=d\restriction D_p, and their coordinate supports off that root are pairwise disjoint.

For these fixed ground data, the set

is dense in \mathbb R. Given c compatible with d_*, first extend it by d_*. Its support is countable, so it meets the nonroot support of only countably many of the pairwise disjoint copies. Choose a remaining probe and extend c by its placed condition \pi_m d. This proves density. Because d_*\in F, the generic meets the second alternative of Equation (3.7). For the resulting m, product symmetry and \pi_m X_\xi=X_\xi give

Since q\leq q_m and \pi_mj\in D_q, this supplies the required witness in A[D_q]=\{A_j:j\in D_q\}.

The condition q was chosen before \xi. Although t,d,j were chosen in the argument after F, each is an individual ground object. The dense set in Equation (3.7) therefore belongs to V, and F meets it. No sequence of witnesses for all \xi is being selected or imported into W. For each \xi<\eta the argument shows that q forces X_\xi\cap A[D_q]\neq\varnothing in V[F]. It forces the universal statement as well: a condition forcing a counterexample could be strengthened to decide its index in \check\eta to one ground \xi, contradicting the assertion for that index. Since this holds for every F containing d_0, the product condition (d_0,q) forces the universal meeting property.

A ground enumeration of D_q yields a sequence of its labels with an \HS name supported by D_q. Distinctness of labels turns that enumeration into a wellordering of A[D_q] in W. Taking the first element of each X_\xi in this wellordering defines the required choice function by Replacement in W. The argument works below an extension of every starting condition forcing the subset-family hypothesis, and hence proves choice for all such families in W.

Finally let \langle Y_\xi:\xi<\eta\rangle be any family of nonempty sets in W. For \eta=0 use the empty function. Otherwise Proposition 3.6, applied once to the union of the family, gives a surjection h:A\times\theta\to\bigcup_{\xi<\eta}Y_\xi in W. For each \xi, take the least \alpha_\xi<\theta whose slice meets Y_\xi, and form

These are a family of nonempty subsets of A in W. The subset case chooses a_\xi\in B_\xi; then h(a_\xi,\alpha_\xi) is the desired choice from Y_\xi.□

Proof. Suppose an \HS name is forced to be a function from an ordinal \eta onto A. Choose a forcing condition (d,p) whose diagram range contains the name’s support and \supp_I(d). Fix j\notin D_p, which exists since |D_p|^V=\mu<|I|^V. Strengthen to a product condition (c,t) deciding a ground \beta<\eta with value A_j, and extend the diagram further to have j\in D_t.

Choose \pi\in\Fix(D_p) moving all coordinates of t,c outside D_p to fresh ones. Then t,\pi t are independent over p and have a common extension; c,\pi c are also compatible. The function name and \check\beta are fixed. Their common product extension would therefore force that one entry has both values A_j and A_{\pi j}. They are distinct because j\notin D_p and \pi moved it freshly. This is a contradiction.□

Proof. Choose a product \HS name \tau for f. In V[F], the ordinary \mathbb P-truth lemma supplies a condition in H forcing that \tau[F] is a function \check\omega\to\check X. Extend within H to a diagram p whose range covers a support of \tau. For each n<\omega, the ordinary forcing theorem supplies an extension of p and some x\in X forcing \tau[F](n)=\check x. Both \tau and the check-name parameters are supported by D_p, so Lemma 3.4 makes p itself force that equality. There is exactly one such x, since p forces functionhood.

The forcing relation is definable in V[F]. Replacement there therefore forms the sequence of these unique values, a function g:\omega\to X in V[F]. Then g=f in V[F][H], because p\in H. By Lemma 3.1, \mathbb R adds no countable sequences in the ground set X, so g\in V. Thus f\in V. The final assertion follows by bounding the ranks of the entries of any countable sequence of ground elements, as in the proof of Lemma 3.1.□

Proof. For an element choose a representative \tau and a diagram t\le r forcing \tau=[\dot A_j]_E for some j\in D_t. The ordinary forcing theorem permits deciding a representative label; extending the diagram includes its index. Write r=t_b. By Cohen restriction in Lemma 3.4, there is d\in F, supported in D_t, witnessing this \mathbb P-forcing assertion. Record the triple

where t^{-1}d is the partial binary function on T\times\kappa obtained by replacing each coordinate t(y) with y. Its domain has size less than \kappa. The ground set of possible records has size at most \mu, since |T|=\mu, \kappa\le\mu, and \mu^{<\kappa}=\mu. Its ground enumeration remains an enumeration in V[F].

Suppose two chosen representatives \tau_1,\tau_2 have the same record, witnessed by t_1,t_2,d_1,d_2,j_1,j_2. The ground bijection t_1(y)\mapsto t_2(y) agrees with the identity on D_r: in both diagrams r=(t_i)_b. It maps points outside D_r to points outside D_r. Extend it to a ground permutation \pi of I fixing D_r. This is possible since the two ranges have size \mu<|I| and their complements have the same cardinality |I|. Then

Product symmetry makes d_2 witness at t_2 equality of both \tau_1 and \tau_2 with [\dot A_{j_2}]_E. Since d_2\in F, t_2 forces \tau_1=\tau_2 in V[F]. Decision at r gives the same equality there. Thus distinct elements have distinct records. Choosing representatives and records uses Choice in the ordinary extension V[F], not in the symmetric model.□

Proof. Both sets contain 1 and are downward closed by inclusion of subdiagrams. Suppose n,n'\in U_h and put k=n\vee n'. The ranges of r_n,r_{n'} intersect exactly in D_{r_k}. Choose supported names for their representations of h. They are forced equal by r. Lemma 3.5, with root r_k, supplies a D_{r_k}-supported name equal to them. Normalize it without changing support. Decision at r_k shows it is an E-class there: its negation would persist to the extension r. Thus k\in U_h. For labels the identical argument is the literal equality of cone intersections, without any name descent.

For the final assertion, apply Lemma 2.1 in V[F]. The ground monoid, order, heights and costs retain their meanings there, so every nonempty ideal has a countable cofinal sequence. It consists of ground elements of T, so countable closure of \mathbb R puts it in V. Its downward closure, computed with the unchanged ground order, is the original ideal. The argument applies to every ideal in V[F], not only to ground ideals.□

Proof. The common root p will separate the copies used in this proof. We first find a class with no representation supported by D_p. Copying it into diagrams whose unwanted intersections are exactly D_p will then rule out both coincidences between copies and availability at forbidden subdiagrams, by support descent.

A class unavailable at the root. Enumerate \mathcal X(p) in V as (\tau_\xi:\xi<\lambda). The canonical name for the sequence of its evaluations is hereditarily symmetric with support D_p. Explicitly, its entries are the canonical pairs (\check\xi,\tau_\xi), each placed under every product condition. Every member of \Fix(D_p) fixes each entry literally. The range of this sequence is wellorderable inside W: map each value to its least index of occurrence. If it contained every E-class, the same map restricted to A/E would wellorder that quotient. The hypothesis therefore implies, ordinarily below (d_0,p), that some E-class lies outside the evaluations of all names in \mathcal X(p).

Fix F containing d_0. By the ordinary forcing theorem choose t\le p and j\in D_t such that t forces the class of A_j outside that entire evaluation list. Choose a witnessing Cohen condition d\in F supported in D_t, using Lemma 3.4. Write p=t_b. Necessarily b\ne1, since a class represented by a label in D_p has a name in \mathcal X(p).

Independent copies with active Cohen conditions. As p=r_{ae}, the probe property of Theorem 2.2 supplies \mu elements m with mb=ae and the prescribed ideal U. The diagrams r_m are copies of t over p, with pairwise intersection exactly D_p. Choose the ground permutations taking t to these diagrams and fixing D_p, and transport d and the class name along them. Their nonroot coordinate sets are disjoint. This is the role of the earlier extension q_e=p: the availability pattern is prescribed among divisors of a, while the common root lies at ae, strictly beyond a.

There are \mu copies whose transported Cohen conditions belong to F. To see this without any \mu-closure assertion, partition the ground family into \mu ground subfamilies of size \mu. In each subfamily the conditions extending at least one transported copy of d form a dense set below d\restriction D_p. Indeed, a Cohen condition uses countably many coordinate indices; among the pairwise disjoint nonroot ranges there is one it misses, and on the root the two conditions agree. Their union is a Cohen condition. Genericity meets each of these ground dense sets. A hit in each disjoint subfamily yields \mu different hits.

Distinct classes with the prescribed exact ideal. Each hit gives a D_{r_m}-supported class name forced at r_m to lie outside the evaluations of \mathcal X(p). The diagram r_m extends p but need not extend q; we use its class name, not a set \mathcal D_F(r_m). As r extends r_m, this name represents a symbolic class in the defined set \mathcal D_F(r). Two such classes cannot be equal there: support descent over their common root p would supply a name in \mathcal X(p) for their common value, contrary to the outside assertion. If n\in U, then n\sqsubseteq m, so r_n extends r_m and the class is available at r_n. If n\sqsubseteq a and n\notin U, the exact probe intersection gives

Availability at r_n would again descend to a name in \mathcal X(p), a contradiction. Its exact availability ideal is therefore U. This gives \mu distinct elements of B_{r,U}(F); Lemma 4.1 bounds that fiber from above.

The label fiber. For labels use the probe centers r(m). Their availability ideals are exactly \downarrow m\cap\downarrow a=U, and distinct probes have distinct centers. This supplies a ground \mu-subset of L_{r,U}; the upper bound follows from |D_r|=\mu.□

Proof. Let v=(r,U), w=(r_n,U_n), and first take a symbolic class available at r_n. Its full availability ideal J at r contains n. For z\sqsubseteq a, ideal closure gives

Write z\vee n=nx. Availability at r_{z\vee n} is exactly the corresponding availability at the subdiagram (r_n)_x of r_n. Thus the restricted ideal at r_n determines the full ideal at r. If that restricted ideal is U_n, the last test is equivalent to z\vee n\in U, and hence to z\in U. Conversely, an element of B_v(F) is available at r_n because n\in U, and its restricted ideal is U_n. This proves surjectivity; injectivity follows from Equation (4.1). For labels use the same argument with literal membership in ranges. Commutation follows because all the symbolic maps retain the same representative names.□

Proof. Choose the countable-base tower of Theorem 2.2 so that its initial submonoid T_0 contains all n_i and all right quotients between them. For \pi\in G_C, consider its alignments with contractions of the chosen vertex:

This set is nonempty: the moved chain is cofinal in C, so one of its terms is a successor of v_0. Every second coordinate m of an alignment divides some n_N, by cofinality of (n_i) in U.

To apply Lemma 2.8, fix (l,m)\in\mathcal A_\pi and any N. Choose l'\ge l so that \pi v_{l'} is a successor of v_N. Its diagram is r_k for some k\in U with n_N\sqsubseteq k. Let d\in T_0 be the right quotient n_ld=n_{l'}. Then

Injectivity of r gives k=md. Consequently md\in U, n_N\sqsubseteq md, and (l',md)\in\mathcal A_\pi. These are exactly the replacement hypotheses of Lemma 2.8. Its conclusion supplies an alignment (l,m) with m\in T_0.

There are countably many resulting alignment pairs (l,m)\in\omega\times T_0. Two permutations giving the same pair agree pointwise on D_{r_{n_l}}; if they are \pi and \rho, then \pi^{-1}\rho\in\Fix(D_{r_{n_l}})\subseteq K_C. Enumerate the pairs, and assign to each coset the first pair realized by any of its members. Distinct cosets receive distinct pairs. This proves the bound.□

Proof. Choose N such that k fixes D_{r_{n_N}} pointwise. For i\ge N it fixes r_{n_i} and every name in \mathcal X(r_{n_i}) literally. Consequently each particular ground code c represents b at F if and only if the same code represents T_k^F(b) at kF. The forcing symmetry lemma proves this on the tail; the definition ignores the remaining finite prefix. Thus the sets of functioning codes are identical, and their minima under the fixed ground wellorder are identical. This proves the order assertion. Also L_C\subseteq D_{r_{n_i}} for every i, so k fixes its every member.□

Proof. If k\in K_C, it fixes all s_{\delta,i} once i is sufficiently large. Replacing \pi with \pi k therefore changes each detector sequence in only finitely many places, proving representative independence.

Suppose \pi K_C\ne\pi'K_C. Use the detector for \delta=(\pi^{-1}\pi')K_C and write \pi^{-1}\pi'=\gamma_\delta k with k\in K_C. Eventually k(s_{\delta,i})=s_{\delta,i}, and hence

Distinct label indices give distinct Cohen rows. For each of these tail positions choose a bit where the two rows differ. The countably many bit ordinals are bounded below regular \kappa. Above that bound the two restricted sequences disagree at every position on a tail, so are unequal modulo eventual equality. There are countably many pairs of cosets; a further countable supremum supplies one bound that distinguishes all pairs. These choices take place in V[F]. They use regularity of \kappa, not closure of \mathbb P.

At the least distinguishing \alpha, choose the coset whose pattern is least in the fixed ground wellorder. If \Gamma_C is trivial, choose its sole element and use \alpha=0. For \sigma\in G_C, label transport gives, for every s\in I, A_{\sigma s}^{\sigma F}=A_s^F. Thus

The actual ground pattern objects on the two sides are equal. Left multiplication permutes the coset set, so the least distinguishing bound is unchanged and the same pattern object is minimal. This proves Equation (6.4).□

Proof. We first finish the construction for the equivalence relation fixed at the start of Section 4. Use canonical equivariant ordered-pair names and form the product name

The superscript denotes the name for the ordered pair. This is a set name: every index ranges over a ground set and the defining forcing relation is a ground relation. Equation (6.9) sends each entry under \pi\in G_q to another entry. Applying \pi^{-1} gives equality of the sets of entries, so G_q fixes \dot J literally. Each member name is a pair of HS names; thus \dot J is HS with support D_q. The individual member names may have different supports. Hereditary symmetry does not require all of them to use D_q.

Take a product generic (F,H) containing (d_0,q). For every r\in H below q, the graph contains exactly the local assignments of Equation (6.7). In detail, whenever \Phi(F,r,j,\tau) holds, the \mathbb R truth lemma gives a condition of F forcing it; strengthening with d_0 retains a condition of F, and Equation (6.10) includes its entry. Conversely, every active entry forces its asserted assignment. All classes are represented by names in their symbolic equivalence classes, so the local assignments are complete.

We check the comparison when the diagram is strengthened. Suppose t\le r\le q, r=t_b, and j\in D_r. The availability ideal of j at t contains b. Hence

is a contraction. Equation (6.7) therefore gives the same assigned symbolic element under inclusion. In particular, its product-name evaluations are equal in every \mathbb P-generic containing t.

Any two active entries of \dot J occur together below a common stronger diagram in H. At that diagram the union of the exact-fiber bijections is a bijection D_t\to\mathcal D_F(t): availability ideals partition both sets. The preceding comparison proves single-valuedness and injectivity of \dot J^{F,H}. Distinct symbolic elements are forced unequal there by local decision, and distinct indices have distinct Cohen labels. Thus these are also single-valuedness and injectivity for the actual sets of the graph.

Every label index belongs to a diagram in H below q, by the density of extending diagrams to contain prescribed supports. Therefore the graph has domain A. To reach an arbitrary E-class, take any label belonging to that class and include its index in such a diagram r. Its canonical supported class name represents an element of \mathcal D_F(r). The local fiber bijection is onto the fiber containing that element, so the graph reaches the class. This is a pointwise existence argument; no simultaneous selection of representatives of all classes has been made. The range is exactly A/E. The graph belongs to W because its name is HS.

The construction was made on an extension of an arbitrary symmetric condition asserting the nonwellorderable-quotient hypothesis. Applying the symmetric forcing theorem and truth lemma therefore proves in W that every such quotient A/E is in bijection with A. Finally, for a surjection h:A\to Y in W, form its kernel relation E in W. The map [a]_E\mapsto h(a) is a bijection A/E\to Y, defined by its unique values without choosing class representatives. If Y is nonwellorderable, so is A/E, and composing this bijection with the one just constructed proves the theorem.□

Proof. We will use two elementary observations about images of A. If h:A\longrightarrow B is onto and \varnothing\ne S\subseteq B, then S is also an image of A. Indeed, fix one s_0\in S and define

This proves an existence assertion for one given nonempty subset; it does not choose a default element simultaneously for a family. Also, the image of a wellorderable set under any function is wellorderable: order its image by the least preimages in a fixed wellordering of its domain. Both observations are theorems of \ZF.

Fix a surjection f:X\longrightarrow Y. If Y=\varnothing, the empty function is the desired injection. Otherwise X is nonempty. Choose a surjection s:A\times\eta\longrightarrow X from the first assumption. Define, for i<\eta,

Separation and Replacement form these sequences. Every y\in Y belongs to f[B_i] for some i, and its least such index is the unique index for which y\in Y_i. Thus the Y_i partition Y. The S_i are pairwise disjoint because their f-images lie in the pairwise disjoint Y_i. Moreover,

is onto for every i. The sets S_i need not cover X.

Before choosing any injections, define

Power Set and Separation give each candidate set, and Replacement gives the sequence \langle\mathcal J_i:i<\eta\rangle. We show that every candidate set is nonempty, fixing an arbitrary i<\eta.

If Y_i is empty, its empty injection belongs to \mathcal J_i. Suppose next that Y_i is nonempty and wellorderable. Choose a wellordering of this one set. The nonempty fibers

can be indexed by an ordinal using that wellordering. The second assumption gives a choice function on them. Since different fibers are disjoint, this function is an injection Y_i\longrightarrow S_i. It therefore belongs to \mathcal J_i.

Finally, suppose that Y_i is nonwellorderable. Then S_i is nonempty and nonwellorderable, by the second elementary observation and the surjectivity of f|S_i. The map a\mapsto s(a,i) surjects from A onto B_i. The first observation makes the nonempty subset S_i\subseteq B_i an image of A, and composition with f|S_i makes Y_i an image of A as well. By the third assumption both S_i and Y_i are bijective to A. Composing one of these bijections with the inverse of the other gives an injection Y_i\longrightarrow S_i, again in \mathcal J_i.

We have proved (\forall i<\eta)\ \mathcal J_i\ne\varnothing. The pointwise proof selected neither a sequence of wellorderings nor a sequence of quotient bijections. Apply the second assumption now to the already defined sequence of candidate sets. It supplies \langle j_i:i<\eta\rangle with j_i\in\mathcal J_i. Set

The disjointness of the Y_i makes this a function with domain Y. If j(y)=j(y'), that value lies in both corresponding source pieces S_i. Their disjointness makes the indices equal, and injectivity of that j_i gives y=y'. Thus j:Y\longrightarrow X is an injection.

Every construction in this proof takes place in the same model of \ZF. No rank bound on X or Y, and no uniform choice of auxiliary presentations for the slices, has been used.□

Proof. Suppose c were a choice function for this family, and let \lambda be the Hartogs ordinal of A, so there is no injection \lambda\longrightarrow A. Foundation gives A\notin A. By transfinite recursion define a:\lambda\longrightarrow A\cup\{A\} as follows. At stage \alpha, put S_\alpha=A\setminus\ran(a|\alpha) and set

If every S_\alpha were nonempty, the recursion would choose a different member of A at every stage, giving an injection \lambda\longrightarrow A. Hence there is a least \alpha<\lambda with S_\alpha=\varnothing. Before that stage no value is the sentinel A, and a|\alpha is a bijection onto A. This wellorders A, a contradiction. Hartogs’ theorem and the recursion used here are available in \ZF.□

Proof. The symmetric system is for one set forcing, with the set group and normal filter specified above. The set-forcing symmetric-model theorem, in its internal form, therefore gives full \ZF, the canonical ground embedding, and preservation of the interpreted ordinals. For an externally transitive ground its evaluated hereditarily symmetric interpretation is transitive. These are pure-set models, so Foundation and the full Separation and Replacement schemata are included.

Proposition 3.6 gives the first hypothesis of Lemma 7.1 inside W, and Proposition 3.7 gives the second, for all ordinal-indexed families in W. Theorem 6.3, together with Remark 7.2, gives the third. The lemma proves \PP for every surjection in W, with its witnessing injection in W.

Proposition 3.8 proves that A is not wellorderable in W. Applying Lemma 7.4 inside W gives the displayed family and failure of \AC there. Finally, Proposition 3.9 supplies the assertion about countable sequences. This last assertion concerns the symmetric model itself; it does not require countable closure of the full product forcing.□

Proof. The constructible-universe theorem proves, in \ZF, the relativization to L of every \ZF axiom, of Choice, and of V=L. These are assertions for each individual axiom instance, including the instances of Separation and Replacement. See [17, Theorem 4.7, Lemma 4.10, Corollary 4.13, and Theorems 4.14 and 4.18].

Relativization commutes with Boolean connectives and preserves first-order inference when quantifiers are restricted to the nonempty interpreted domain. A finite contradiction proof from \ZFC+V=L would therefore yield, by relativizing each line and using the finitely many required interpreted axioms, a contradiction proof from \ZF. This proves the consistency implication. The same constructible-universe theorem proves GCH in L, hence proves GCH from \ZFC+V=L.□

Proof. Atomic forcing is defined by the usual recursion on names. For a fixed formula, extend these atomic definitions through its finitely many connectives and quantifiers, restricting quantified names to \HS_{\mathcal S}. For example, define

Existential forcing is characterized by

The set D_{\varphi,\vec\tau} exists by Separation from \mathbb Q. The class of names and the hereditary symmetry predicate are definable by set-theoretic recursion. Thus all the displayed relations are ordinary first-order predicates. This construction is a schema indexed externally by formulas; it asserts no single satisfaction predicate for all formulas.

The logical and symmetry rules follow by induction on a fixed formula, with the internal name recursion supplying the atomic case. The resulting symmetric-model theorem and its forcing relation are standard; see [10, Equations (15.39)–(15.41) and Lemma 15.51] and [11, Section 2.1, p. 4]. We recall the parts that ensure the full axiom schemata.

Fix an arbitrary formula \varphi(x,\vec a) and hereditarily symmetric names \sigma,\vec\tau for its set and parameters. A Separation name uses the pairs (\rho,q)\in\dom(\sigma)\times\mathbb Q for which

The intersection of the stabilizers of \sigma and the finitely many parameter names fixes this name. That intersection belongs to \mathcal F, and every member name is hereditarily symmetric. The atomic forcing rules and Equation (8.2) verify that it is the required subset. No restriction on \varphi or on the rank of \sigma has been imposed.

Write \operatorname{nrk}(\eta) for the name-rank

For Replacement, fix a formula \psi(x,y,\vec a), a domain name \sigma, and parameter names \vec\tau. For each pair (\rho,q)\in\dom(\sigma)\times\mathbb Q for which some hereditarily symmetric name \eta satisfies

take the least possible name-rank of such an \eta. This defines an ordinal-valued function on a ground set. Replacement in the ground bounds all these ranks strictly below one ordinal \beta. All \mathbb Q-names of name-rank less than \beta form a set. Consequently

is a set name. Every automorphism preserves name-rank and hereditary symmetry, so \dot B_\beta is fixed by the whole group and belongs to \HS_{\mathcal S}.

Below a condition forcing totality of the relation on \sigma, local witnesses from Equation (8.2) can therefore be replaced, at the same witnessing conditions, by names occurring in \dot B_\beta. This gives a set bounding the required witnesses. When the relation is functional, Separation in that set gives its image. The bound \beta depends on the particular domain name and formula; it is not a bound on the universe of names.

For Power Set, normalize a name for a subset of \sigma using member names from \dom(\sigma) and the forcing tests for membership in that subset. The normalized names lie in the ground set \mathcal P(\dom(\sigma)\times\mathbb Q). Use all hereditarily symmetric candidates, under the conditions forcing that they are subsets of \sigma. The stabilizer of \sigma permutes this collection, giving a hereditarily symmetric power-set name. Every symmetric subset has such a normalization, so the name supplies the entire internal power set. Check names and the canonical pairing and union constructions supply the remaining elementary existence axioms.

The usual internal name-rank argument verifies Foundation. Equivalently, the interpreted hereditary class is membership-closed inside the ordinary forcing extension: an element of an HS-valued set has an active member name of an HS name. Extensionality and Foundation then inherit their witnesses from the ordinary extension. This argument concerns first-order Foundation and does not assume that an arbitrary model is externally well founded.

All these name constructions and forcing verifications are proofs in the ground theory, for the chosen formula. They prove the asserted schema. They use local existential witnesses rather than a maximum principle for symmetric forcing; that maximum principle need not hold [12, Proposition 10.26].□

Proof. Induct externally on the finite syntax of the standard formula, using atomic formulas, conjunction, negation, and existential quantification. The atomic case is Equations (8.3) and (8.4); atomic symmetric forcing agrees with ordinary forcing. Conjunction uses a common strengthening of two conditions in G and monotonicity.

For negation, the set of conditions deciding the particular formula is an internally definable dense subset of \mathbb Q. It belongs to M by the Separation instance for its defining forcing predicate. Genericity gives a deciding condition in G. The induction hypothesis excludes the wrong decision, and directedness excludes conditions in G forcing opposite answers.

Suppose p\in G symmetrically forces an existential statement. The set of local witness conditions in Equation (8.2), together with the conditions incompatible with p, is another internally definable dense set. Genericity meets its first part. The internal witness is an actual element of |M| which M regards as an HS name. Its equivalence class is a witness in W by induction. Conversely, a witness in W has an internal HS representative; apply induction to that representative and the elementary existential forcing rule.

This proves the truth equivalence for every standard formula. Lemma 8.2, applied in M to each standard \ZF axiom instance, now gives W\models\ZF. The proof never evaluates a name by external recursion over E^M. Nor does it require a truth predicate in M for all formulas, including its possible nonstandard formula codes.□

Proof of Theorem 1.1. Assume \Con(\ZF). By Lemma 8.1, \ZFC+V=L is consistent. Completeness and downward Löwenheim–Skolem give a countable model M of this theory. No transitivity or external well-foundedness is asserted.

Interpret the construction inside M and choose an external M-generic filter on its internal poset as above. Form the symmetric quotient W using Equations (8.3) and (8.4). Lemma 8.3 gives full \ZF in W. The same lemma, applied to Equation (8.1), gives

Soundness therefore yields \Con(\ZF+\PP+\ACwo+\neg\AC), as required.

Equivalently, one can extract the consistency implication directly from finite proofs. A purported contradiction proof from the target theory uses only finitely many \ZF instances. Translate its lines into symmetric forcing. The logical forcing rules preserve its inferences; Lemma 8.2 supplies its \ZF axioms; and Equation (8.1) supplies \PP, \ACwo, and \neg\AC. This would make a nonempty poset force a contradiction, contrary to its atomic forcing laws. It therefore gives a contradiction proof in \ZFC+V=L, which the constructible interpretation translates into one in \ZF. This argument uses no stronger model-existence assumption.□

Proof of Theorem 1.2. Work in a \ZFC metatheory, and let V be the given countable transitive model of \ZFC. Carry out Theorem 7.5 inside V, using its parameters

These are the arbitrary-choice-ground parameters of the construction.

Enumerate externally the dense subsets of the constructed poset which belong to V, and recursively choose a descending sequence meeting them. Its upward-generated filter G is V-generic. Here genuine well-founded recursion on ground names is available, since V is transitive. Define

The set symmetric-extension theorem gives transitive models V\subseteq W\subseteq V[G] with the same ordinals, and gives all of \ZF in W. Theorem 7.5 supplies \PP, \neg\AC, and \ACwo in this same W, together with its stated preservation of countable sequences from any fixed ground set. To obtain the last assertion of Theorem 1.2, let f\in W be a countable sequence of elements of V. Its rank in V[G] is bounded by a ground ordinal \alpha, since forcing preserves the ordinals. Ranks of ground sets are absolute between these transitive models, so the range of f lies in the ground set (V_\alpha)^V. The preservation assertion of Theorem 7.5 applied to this set gives f\in V. This proves the stated transitive-model conclusion.

This is a separate model-existence deduction. The ordinary consistency proof permits an externally ill-founded ground and does not itself assert the existence of a transitive model.□