Solovay's Model and Regularity of All Sets of Reals

By F2 every $\alpha <\kappa$ is countable after forcing, whereas the $\kappa$-chain condition preserves $\kappa$ and its uncountability. Hence $\kappa ={\omega }_1^{V[G]}$.

First justify the ordinal decisions. Fix a name $\dot{\gamma }$ forced to be an ordinal and let $\rho$ exceed its name rank. By the rank bound and ordinal preservation in F3, every possible value is some ground ordinal below $\rho$. In the Boolean completion, the join of the set of truth values $\parallel \dot{\gamma }=\check{\alpha }\parallel$ for $\alpha <\rho$ is $1$: otherwise a nonzero remainder would force that $\dot{\gamma }$ is an ordinal below $\rho$ unequal to every such $\alpha$, contradicting the forcing clauses and density closure. A maximal antichain refining these truth values therefore decides $\dot{\gamma }$ as a check ordinal. This proves the needed ordinal-name decision lemma; binary decision density alone was not substituted for it.

Apply step 1.2 to $\dot{f}(n)$ for each $n$. Ambient AC selects a sequence $(A_n{)}_{n<\omega }$ of deciding maximal antichains. The $\kappa$-cc makes every $A_n$ have size below $\kappa$. Each condition has finite support, so regularity in F4 bounds ${\bigcup }_{n<\omega }{\bigcup }_{p\in A_n}\mathrm{supp}(p)$ below some $\xi <\kappa$. Every $A_n\subseteq P_{\xi }$, and replacing each coefficient by its restriction gives a $P_{\xi }$-name whose $G_{\xi }$-value is ${\dot{f}}_G$. A real is the special case of an ordinal-valued omega-sequence.

In $V$, the collection of nice $P_{\xi }$-names for reals has cardinal below $\kappa$: each is coded by countably many antichains in the set $P_{\xi }$, and inaccessibility supplies the required bound. The tail collapse makes that ground set countable. Evaluating an ambient enumeration of its codes gives a surjection from $\omega$ onto ${\mathbb{R}}^{V[G_{\xi }]}$ in $V[G]$. Empty names and the zero real are included; no uniform choice is made inside an inner model.

By F1, choose $\xi <\kappa$ with $f\in V[G_{\xi }]$. Solovay's small-collapse factorization replaces this initial extension by $V[F]$, where $F:\omega \twoheadrightarrow \lambda$ is a $V$-generic collapsing map for some ordinal $\lambda <\kappa$ and $f\in V[F]$. Define

The initial forcing has size below $\kappa$. Solovay's absorption construction recursively embeds its Boolean completion and the tail collapse into a fresh copy of $\mathrm{Lv}(\kappa )$ over $V[f]$: at stage $\alpha <\kappa$, put the next maximal antichain and the next dense set into coordinates above all earlier supports. Regularity of $\kappa$ bounds each stage, and the union is a dense complete embedding. The image of $G$ is therefore a generic $H$ with both inclusions $V[G]\subseteq V[f][H]\subseteq V[G]$. F3 is used exactly to enumerate those dense sets and maximal antichains.

The collapse is weakly homogeneous. Given $p,q$, first move the finitely many coordinates of $p$ away from those of $q$ by coordinate permutations; the moved $p$ is compatible with $q$. If some condition forced a sentence $\phi (\vec{a})$ and another forced its negation, apply such an automorphism. It fixes every $\vec{a}\in V[f]$ and yields compatible conditions forcing opposites, contrary to forcing consistency. Density of decision then makes the Boolean value $0$ or $1$. The omission of $H$ is essential.

Random and Cohen forcing have cardinal below $\kappa$ in each localized model. Insert their Boolean completion as the first small factor in the same absorption recursion. Thus, after adjoining its generic real $x$, the remaining extension is again a homogeneous Lévy collapse over $V[f,x]$.

Hereditary definability makes $M$ transitive, contains every ordinal, and contains every real because a real is itself an $S$-parameter; Extensionality, Foundation, Pairing, Union and Infinity are therefore inherited.

Separation is obtained by conjoining the defining formula of the separated class with the fixed $OD(S)$ definitions of its set parameters. For Replacement, if $f,x\in M$ and $f$ is functional on $x$, the ambient set $f\mathrm{‘}\mathrm{‘}x$ is defined from the fixed hereditary codes of $f$ and $x$ by $y\in f\mathrm{‘}\mathrm{‘}x⟺(\mathrm{\exists }z\in x)(z,y)\in f$; every such $y$ is already in the transitive class $M$, so the image is hereditarily $OD(S)$ and belongs to $M$. No per-value codes are selected or combined. For Power Set, the ambient set $\{y\subseteq x:y\in M\}$ is defined from $x$ by the uniform $OD(S)$ predicate, and all members of its transitive closure lie in $M$. Thus every ZF axiom holds in $M$.

Let $A\subseteq \mathbb{R}$ lie in $M$. Heredity gives a definition of $A$ from $s\in S$ and finitely many ordinals $\vec{\alpha }$. By F2, $s$ lies in a bounded initial extension. The real-capture clause of F3 supplies a real $r$ and ordinal $\beta$ such that $s$ is definable over $V[r]$ from $(r,\beta )$. By F4, $V[r]=L[r]$. The class $L[r]$ is uniformly definable in $V[G]$ from $r$, so syntactically restricting every quantifier in the fixed defining formula to $L[r]$ defines the same unique $s$ in $V[G]$. Substitute that ambient definition of $s$ into the definition of $A$. Thus $A$ is definable in $V[G]$ from $r$ and the finite ordinal tuple $(\beta ,\vec{\alpha })$. Conversely, interleave the natural-number bits of $r$ and the finite tuple $(\beta ,\vec{\alpha })$ into one countable ordinal sequence in $S$. Hence the advertised parameter forms are equivalent, without claiming that an arbitrary ordinal is real-coded or that $M=L(\mathbb{R})$.

Formula, rank and finite ordinal codes together with $s\in S$ give a definable surjection $F:\mathrm{O}\mathrm{r}\mathrm{d}\times S\twoheadrightarrow M$: for a code, return the uniquely defined object, and return $\mathrm{\varnothing }$ for an invalid code.

By ambient AC choose for each $n$ a pair $({\alpha }_n,s_n)$ with $F({\alpha }_n,s_n)=f(n)$. A fixed pairing ${\omega }^2\cong \omega$ interleaves the $s_n$ into one $s\in S$, while the countable ordinal sequence $n\mapsto {\alpha }_n$ is also a member of $S$; interleave these two sequences once more. This is the sole new use of Choice.

The graph of $f$ is definable from that one $S$-parameter and the fixed definition of $F$, and every value has hereditary $OD(S)$ transitive closure. Hence the graph and $f$ belong to $M$. The empty-domain restriction and constant sequences use the same code and require no selection.

In $V[G]$, recursively set $a_0$ as given and, using ambient AC, choose $a_{n+1}\in A$ with $a_{n}R{a}_{n+1}$. Seriality supplies a nonempty successor fibre at every finite stage.

The resulting function maps $\omega$ into $A\subseteq M$, so F1 puts it in $M$. Transitivity makes $M$ compute each assertion $a_{n}R{a}_{n+1}$ correctly. This is precisely DC by F2. If $A$ is a singleton the constant chain works; nonemptiness is essential and supplied.

Induction on the well-founded code gives $B^N=B^W\cap {\mathbb{R}}^N$: basic rational intervals are absolute, and complement and countable union commute with intersection with the shared reals. If the two models have the same reals, evaluations are identical.

A coded open or closed set has the same rational basis/tree description. If a Borel set is null, F2 says that for each $j$ there is a countable elementary-set cover of cost below $2^{-j}$; Countable Choice selects these covers, and pairing their indices and coding their real endpoints gives one real witness. Conversely that displayed witness proves outer measure zero. Thus such a witness remains valid in an outer transitive model, and when the two models have the same reals it transfers in both directions. A displayed sequence of closed nowhere-dense Borel codes behaves identically: closedness and the rational-basis test for empty interior are absolute on shared reals, and the same sequence witnesses meagreness. This is the coded content used below; no claim that the two bare definitions in F2 manufacture witnesses by themselves is made.

A simultaneous induction on a Borel code produces an open-mod-meagre pair together with an explicit sequence of closed nowhere-dense codes covering the error. A basic open code uses itself and the empty sequence; for complements, replace the complement of the current open set by its interior and append its closed nowhere-dense boundary; for countable unions, union the open representatives and pair the two natural indices of all exception sequences. The construction is recursive from the Borel code, so the witness lies in every model containing that code. Countable Choice from F4 closes the meagre ideal under the displayed union, while F4 supplies completeness and countable closure for the null ideal in $M$; the ground and forcing models have ambient Choice.

For a coded closed set in two models with the same reals, nonemptiness is absolute and absence of isolated points is equivalent to the rational splitting test: every basic interval meeting the set contains two disjoint smaller basic intervals meeting it. The real witnesses transfer in both directions. Alternatively, an explicit pruned binary tree whose successor cylinders are disjoint certifies nonemptiness and supplies branches by F4 inside $M$ (and by Choice in the ambient forcing models). These are exactly the two perfect-set transfers used below. A closed code can acquire a new branch in an outer model with new reals, so no such blanket downward absoluteness, and no absoluteness for arbitrary uncoded sets, is claimed.

Borel codes are reals, so F1 and ambient AC enumerate all $N$-coded Borel null sets as $(C_n)$. A real is not random over $N$ exactly when it belongs to one of these null sets (every random-algebra dense failure has such a coded null witness). Thus the nonrandom reals lie in $C={\bigcup }_n{C}_n$, which is null by F2.

Similarly enumerate the $N$-coded closed nowhere-dense sets. A real failing Cohen genericity misses an $N$-coded dense open set, hence belongs to its closed nowhere-dense complement. Their union is meagre by F2, so its complement, the $N$-Cohen generics, is comeagre. Empty coded exceptions and a model with finitely many codes are covered by repeating codes in the enumeration.

For a random real $x$ over $N$, F1 factors the final extension as $N[x][H_x]$ with homogeneous tail forcing $R_x$. In the random forcing language over $N$, let $\psi (\dot{x})$ be the assertion that the top condition of $R_{\dot{x}}$ forces $\phi (\dot{x},a,\vec{\alpha })$. Use F3 to form $b=\parallel \psi (\dot{x})\parallel$ in the completed random algebra and choose an $N$-coded Borel representative $B$ of $b$. For every $N$-random $x$, the random-forcing truth lemma gives $x\in B$ iff $N[x]\models \psi (x)$. Homogeneity says the Boolean value of $\phi (x,a,\vec{\alpha })$ in $R_x$ is $0$ or $1$, and the tail truth lemma applied to the actual $H_x$ therefore gives $N[x]\models \psi (x)$ iff $N[x][H_x]=V[G]\models \phi (x,a,\vec{\alpha })$. Thus $B$ represents final-extension truth on every $N$-random real; no absoluteness from $N[x]$ to its tail extension was used.

In Cohen forcing use the analogous assertion $\psi (\dot{x})$ that the top of the homogeneous tail forces $\phi (\dot{x},a,\vec{\alpha })$. F3 supplies its regular-open Boolean value, with an $N$-coded regular-open representative $U$ whose boundary is nowhere dense. The Cohen-forcing truth lemma and the same homogeneous-tail argument from step 1.1 show that, for every $N$-Cohen generic $x$, final-extension truth is equivalent to $x\in U$. Thus $U$ is already a Borel representative, and it differs from an open set by the empty, hence meagre, set. The statement deliberately leaves all nongenerics as exceptions; their largeness is used only by later items after its countability hypothesis has been verified.

Use F2 to choose a bounded $N$ containing F1's sole real definition parameter; the finitely many ordinal parameters require no localization. F4 gives an $N$-coded Borel set $B$ agreeing with $A$ on every $N$-random real. In the ambient final extension enumerate the $N$-coded null Borel sets as $(C_n{)}_{n<\omega }$, as in F3's proof, and let $c$ be the real Borel code of their union $C$. Every nonrandom real lies in $C$, so $A\mathrm{△}B\subseteq C$. The code $c$ generally need not lie in $N$, but F1 says that $M$ and the final extension have the same reals; hence $c\in M$.

The code of $B$ is a real of $N$, hence a real of the final extension; F1's same-reals conclusion puts that code in $M$ without requiring the false class inclusion $N\subseteq M$. Step 1.1 likewise puts the code of $C$ in $M$. F5 makes $B$ Borel and $C$ null internally and supplies completeness of the null ideal, so every subset of $C$ is measurable; hence $A=B\mathrm{△}(A\mathrm{△}B)$ is measurable. This includes $A=\mathrm{\varnothing }$, $A=\mathbb{R}$, and zero exception $C=\mathrm{\varnothing }$.

Use F2 to choose a bounded $N$ containing F1's real parameter; the ordinal parameters remain explicit. F3 gives an $N$-coded Borel set $B$ agreeing with $A$ on every $N$-Cohen generic. In the ambient final extension, enumerate the $N$-coded closed nowhere-dense sets as $(C_n{)}_{n<\omega }$, as in the proof of F3's generic-largeness component, and let $d$ be the real Borel code for $D={\bigcup }_n{C}_n$. Every nongeneric real lies in $D$, so $A\mathrm{△}B\subseteq D$. The code $d$ need not lie in $N$, but F1 says that $M$ and the final extension have the same reals, hence $d\in M$; F4 makes its evaluation and meagreness absolute to $M$. Apply F4 inside $M$ to the code of $B$ to obtain a coded open $U$ and coded meagre $E$ with $B\mathrm{△}U\subseteq E$.

The explicit codes for $D$ and $E$ lie in $M$, and F4 closes the meagre ideal under their finite union (equivalently, interleave their two coded nowhere-dense witness sequences). Thus $A\mathrm{△}U\subseteq D\cup E$ is meagre in $M$, which is exactly BP. Empty and whole-space cases use $U=\mathrm{\varnothing }$ and $U=\mathbb{R}$.

The initial forcing producing $N$ and the interval forcing $Q$ both have size below $\kappa$. Nice names for subsets of $Q$ and $Q^2$ are coded by subsets of a ground set of size below $\kappa$; strong inaccessibility bounds the collection of those codes below $\kappa$. The remaining Lévy collapse therefore makes $\mathcal{P}(Q{)}^N$ and $\mathcal{P}(Q^2{)}^N$ countable in $V[G]$, as asserted in F1. Use F3 to enumerate their dense members and replace each by its downward closure. Recursively assign $p_s\le p$ for $s\in 2^{<\omega }$. At stage $n$, extend every node into the first $n$ one-coordinate open dense sets and every ordered pair of distinct nodes into the first $n$ product open dense sets. There are only finitely many requirements at a level: process them successively, strengthening the affected coordinates each time. Downward closure preserves all requirements already met.

Below every $q\le p$ there are two extensions forcing incompatible initial segments of $\dot{\tau }$. Otherwise, for some $q$, any two decided strings would be compatible. For each length $k$, density of deciding conditions then gives one unique string $u_k\in 2^k$ that can be forced below $q$; least-string selection makes the sequence $(u_k)$ definable in $N$ from $q$ and $\dot{\tau }$. Its union is a real $u\in N$, and density closure gives $q⊩\dot{\tau }=\check{u}$, contradicting the displayed hypothesis, since $q\le p$. Apply this splitting below each node to make siblings $p_{s0},p_{s1}$ decide incompatible strings of length at least $\mathrm{\mid }s\mathrm{\mid }+1$, preserving all earlier finite requirements.

For $z\in 2^{\omega }$, the filter generated by the branch is $g_z=\{q\in Q:(\mathrm{\exists }n)p_{z\upharpoonright n}\le q\}$, the upward closure in the convention that smaller conditions are stronger. It meets every enumerated dense set and so is $N$-generic. Distinct $z,w$ give an $N$-generic pair by the product requirements, and the incompatible decisions make ${\dot{\tau }}_{g_z}\mathrm{\ne }{\dot{\tau }}_{g_w}$. Agreement through level $n$ fixes an output prefix of length $n$, so $z\mapsto {\dot{\tau }}_{g_z}$ is continuous. Compactness makes its injective image perfect and nonempty.

Use F2 to choose $\xi <\kappa$ such that $N=V[G_{\xi }]$ contains F1's real parameter; keep the finite ordinal parameters explicit. Fix an ambient enumeration $e:\omega \twoheadrightarrow {\mathbb{R}}^N$. If $A\subseteq N$, choose one $a_0\in A$ (available because $A$ is uncountable) and define $e_A(n)=e(n)$ when $e(n)\in A$, and $e_A(n)=a_0$ otherwise. This is an ambient omega-surjection onto $A$ with values in $M$, so F3 puts it in $M$, contradicting internal uncountability. Hence some $x\in A\setminus N$ exists.

Use F2 again to choose $\eta$ with $\xi <\eta <\kappa$ and $x\in V[G_{\eta }]$. Let $Q$ be the finite-condition collapse on $[\xi ,\eta )\times \omega$ and $H=G_{\eta }\upharpoonright ([\xi ,\eta )\times \omega )$. The disjoint-coordinate projection in F2 gives $V[G_{\eta }]=N[H]$, with $Q\in N$ and $Q$ small. By the defining valuation formula for $N[H]$ in F2, choose a $Q$-name $\dot{\tau }\in N$ with ${\dot{\tau }}_H=x$.

In $N$ form the downward-open set $D=\{q\in Q:(\mathrm{\exists }y\in {\mathbb{R}}^N)q{⊩}_Q\dot{\tau }=\check{y}\}$. The actual generic $H$ misses $D$, since the truth lemma would otherwise put $x={\dot{\tau }}_H$ in $N$. The set $D\cup \{q:q\perp D\}$ is dense and belongs to $N$, so genericity gives $p_0\in H$ incompatible with every member of $D$. Hence no extension of $p_0$ forces $\dot{\tau }$ equal to a real of $N$. Separately, the truth lemma and tail homogeneity give $p_1\in H$ forcing the fixed real-membership formula defining $A$ (with its localized real and ordinal parameters). Directedness of $H$ gives $p\in H$ below $p_0,p_1$. This $p$ has the exact forcing-newness premise of F5 and forces every branch interpretation to satisfy the definition of $A$; no external class formula “$\dot{\tau }\mathrm{\notin }N$” has been used in the forcing language.

Apply F5 below $p$. Every branch interpretation satisfies the same definition, so its compact injective image $P$ lies in $A$. The construction has a real code; since $M$ has all reals, that code lies in $M$, and F6 says internally that $P$ is nonempty perfect.

Let $D\subseteq [0,1)$ consist of the reals whose canonical binary code has no eventually-$1$ subsequence in any residue class modulo $n$; its complement is the finite union of Borel null sets. Split the digits of a code in $D$ by residue modulo $n$. This is a Borel bijection $T:D\to [0,1{)}^n$ with Borel inverse given by interleaving the canonical coordinate codes. A length-$nk$ cylinder maps to the corresponding product of $n$ dyadic intervals, each of length $2^{-k}$; both sides have measure $2^{-nk}$. The monotone-class extension and F2–F3 make $T$ measure preserving on all Borel sets and send Borel null sets both ways. F3 assumes countable choice, supplied here exactly by internal DC through F4–F5; the digit map itself makes no selections.

For arbitrary $E\subseteq [0,1{)}^n$, F1 makes $T^{-1}(E)$ measurable. Completion gives Borel $B_0$ and Borel null $N_0$ with $T^{-1}(E)\mathrm{△}{B}_0\subseteq N_0$. Put $B=B_0\cap D$ and $N=N_0\cap D$, so both lie in the domain of $T$. Bimeasurability and step 1.1 give $E\mathrm{△}T(B)\subseteq T(N)$, with Borel measurable $T(B)$ and null $T(N)$; hence $E$ is measurable.

Cover ${\mathbb{R}}^n$ by the explicitly indexed disjoint half-open cubes $k+[0,1{)}^n$, $k\in {\mathbb{Z}}^n$. For each $k$, the set $E_k=(E\cap (k+[0,1{)}^n))-k$ belongs to $M$ and is measurable by step 2.1; F6 makes its translate $E_k+k$ measurable. The defining closure of the Lebesgue sigma-algebra under the displayed countable union now gives $E={\bigcup }_{k\in {\mathbb{Z}}^n}(E_k+k)$ measurable, with no selection of representatives. When $n=1$, there is one residue class, $D=[0,1)$ for canonical non-eventually-$1$ codes, and $T$ is the identity under that code, so step 2.1 is exactly F1. The case $n=0$ is outside the stated positive range.

Suppose $V$ were a Vitali selector. F1 makes it measurable. If $\lambda (V)=0$, the countably many rational translates covering $[0,1]$ have null union, contradicting $\lambda ([0,1])=1$. If $\lambda (V)>0$, finitely many pairwise disjoint translates inside $[-1,2]$ have arbitrarily large total measure, contradicting $\lambda ([-1,2])=3$. The selector and translation facts are F2, while F3 supplies subadditivity, finite additivity and the interval values.

Suppose $B$ were Bernstein. Both $B$ and $\mathbb{R}\setminus B$ contain no nonempty perfect subset. They cannot both be countable: F5 would make their two-term union $\mathbb{R}$ countable, contrary to its uncountability. Therefore one is uncountable, and F4 gives it a nonempty perfect subset, a contradiction. This repairs the tempting but unsupported assertion that the definition alone makes $B$ uncountable.

The two contradictions exclude both supplied pathologies without using their ZFC existence constructions.

Suppose $H$ is a Hamel basis. It is nonempty because it spans $1$; choose one $b\in H$ (one existential choice, not AC). Define $c_b(x)$ as the unique rational coefficient of $b$ in the finite expansion of $x$. Then $c_b$ is additive, and F1 makes $W=\ker c_b$ a measurable proper subgroup. Moreover, $\mathbb{R}={\bigcup }_{q\in \mathbb{Q}}(qb+W)$. By F6, Countable Choice holds in $M$. If $\lambda (W)>0$, F3 gives $W=\mathbb{R}$; if $\lambda (W)=0$, translation invariance in F4 makes every $qb+W$ measurable and null, and countable subadditivity makes their explicitly rational-indexed union null. Monotonicity then gives $\lambda ([0,1])=0$, contradicting the value $1$ from F4.

Let $f$ be additive and put $E_n=\{x\in [-1,1]:\mathrm{\mid }f(x)\mathrm{\mid }\le n\}$. F1 makes these sets measurable, and they cover $[-1,1]$. By F6, Countable Choice holds in $M$. If each were null, F4 would make their explicitly indexed union null, contrary to $\lambda ([-1,1])=2$; hence some $E_n$ has positive measure. Steinhaus gives an interval about zero in $E_n-E_n$, where additivity bounds $\mathrm{\mid }f\mathrm{\mid }$ by $2n$. F5 then yields continuity and $f(x)=xf(1)$ for every real $x$. The zero map and $n=0$ cause no exception.

Step 1.1 excludes a basis, and step 1.2 excludes every discontinuous additive solution, without invoking an AC basis-existence theorem.

By F4, Countable Choice holds in $M$. If the radius is $r>0$, the ball contains a cube of side $2r\mathrm{/}\sqrt{3}$ and lies in a cube of side $2r$; hence F3 gives $0<V={\lambda }_3(K)<\mathrm{\infty }$. Finite additivity gives $V={\sum }_{i<m}\lambda (A_i)$, and F2 gives ${\sum }_{i<m}\lambda (g_i[A_i])=V$. But the displayed one-use reassembly and the disjoint congruent copies give ${\sum }_{i<m}\lambda (g_i[A_i])=\lambda (K_0\bigsqcup K_1)=2V$. Thus $V=2V$, contradicting $0<V<\mathrm{\infty }$.

If $r=0$, $K$ is a singleton. Its finite partition has exactly one nonempty piece. Because the statement permits exactly one image of each original piece, the displayed union of the $g_i[A_i]$ has one point, whereas $K_0\bigsqcup K_1$ has two. Thus the zero-volume endpoint is excluded without the volume calculation.

The positive- and zero-radius cases exhaust closed balls, proving the claim.

Assume for contradiction that $M\models AC$. Since $M$ is a transitive ZF model with its own full real line, the proof in F2 relativizes to $M$ and constructs there a Bernstein set.

This contradicts F1. Therefore $M\models ̸AC$. Its already proved DC is compatible with this failure because DC is strictly the serial omega-chain assertion, not a well-ordering principle.

Induction makes every $L_{\alpha }(\mathbb{R})$ transitive and makes the hierarchy continuous at limits. Empty set, pairing, union, infinity and every required finite construction occur at a bounded later definability stage; Extensionality and Foundation are absolute to the transitive union. For a fixed formula and parameters, the usual finite-formula reflection construction closes an ordinal stage under witnesses for that formula and its subformulas. Separation over a set is consequently definable at the next stage. For Replacement, ambient Replacement first collects the uniquely specified witnesses and their least hierarchy ranks; their supremum is an ordinal, and reflection above that bound makes the image definable over one set stage. For Power Set, ambient Separation forms the set of $L(\mathbb{R})$-members of $\mathcal{P}(a)$; ambient Replacement bounds their least hierarchy ranks, so at a later stage this entire internal power set is the definable set $\{x\in L_{\theta }(\mathbb{R}):x\subseteq a\}$. These arguments also give Collection. Thus $L(\mathbb{R})\models ZF$, and F1 gives equality of its reals and ordinals with the ambient model.

Recursively unfold a successor-stage definition into its finitely branching tree of earlier parameter definitions. This tree is finite: if it had nodes at every finite depth, repeatedly taking the least extendible child would give a strictly descending omega-sequence of hierarchy ranks. Encode its finite shape and formula numbers by natural numbers. Bound its finitely many ordinal labels by one ordinal; F2 orders the resulting fixed-arity bounded tuple, and finite ordinal pairing absorbs that tuple, the shape, and the formula numbers into one ordinal. Interleave the finitely many real leaves into one real. Decoding all such pairs defines a surjection $F:\mathrm{O}\mathrm{r}\mathrm{d}\times \mathbb{R}\twoheadrightarrow L(\mathbb{R})$; invalid codes return $\mathrm{\varnothing }$. The same recursion is set-sized below every fixed ordinal stage. At no point are the real leaves or all of a hierarchy stage well-ordered.

Let $A,R,a_0\in L(\mathbb{R})$, where $A\mathrm{\ne }\mathrm{\varnothing }$, $a_0\in A$, and $R$ is serial on $A$. Ambient AC first supplies one choice function on the set of all nonempty subsets of $\mathbb{R}$. Let ${\alpha }_0$ be the least ordinal for which some real codes $a_0$ via $F$, and use that choice function to select such an $x_0$. Recursively let ${\alpha }_{n+1}$ be the least ordinal for which some real $x$ codes via $F$ an $R$-successor in $A$ of $F({\alpha }_n,x_n)$, and apply the same choice function to this nonempty set of real witnesses to obtain $x_{n+1}$. Membership of the current point in $A$ and seriality on $A$ make every successor-witness set nonempty. Thus ordinal minimization is canonical, while F4 is used exactly for the real witnesses.